Lax Lean Archive

While this submission is a draft, it cannot be used by other submissions.

Protected balls for the rounded ellipsoid method

Lax263307.BufferedEllipsoid · concepts/Lax263307/BufferedEllipsoid.lean · lax-263307

proven

Loading review…

Community review

Flags

Each flag is tied to a public ORCID identity and explains why this concept may be incorrect.

No flags have been submitted.

    Community review

    Flag this concept

    State precisely what appears incorrect. This explanation will be public under your ORCID name.

    No source line selected.

    Natural Language Statement

    Theorem

    Scaling a moment vector in the unit cube by 4N puts it well inside the initial unit ball. A perturbation of Euclidean radius at most one quarter stays in that ball. Euclidean balls are contained in the corresponding coordinate cubes, so the central-cut buffers apply to them. Every nonzero integer normal has squared Euclidean norm at least one.

    Concept map
    1 concept; 10 descendants hidden
    100%
    Proven claimThis conceptRelated conceptA → B: B builds on A
    Evidence

    This concept declares 4 statements. Each proof establishes one of them relative to its assumptions.

    1 coordinate_ball_bound proven

    2 initial_ball proven

    3 integer_normal_norm proven

    4 scaled_cube_norm proven

    Lean source view on GitHub

    1import Mathlib.LinearAlgebra.Matrix.PosDef
    2
    3/-!
    4---
    5title: Protected balls for the rounded ellipsoid method
    6type: theorem
    7---
    8Scaling a moment vector in the unit cube by 4N puts it well inside the
    9initial unit ball. A perturbation of Euclidean radius at most one quarter
    10stays in that ball. Euclidean balls are contained in the corresponding
    11coordinate cubes, so the central-cut buffers apply to them. Every nonzero
    12integer normal has squared Euclidean norm at least one.
    13
    14# Formalization notes
    15
    16The squared norms use finite dot products, matching the registered LP
    17ellipsoid sequence. These geometric estimates do not assume that the
    18independent-set hull has interior. Coordinate scaling is defined over an
    19arbitrary field so its rational specialization is computable.
    20-/
    21
    22namespace Lax263307.BufferedEllipsoid
    23
    24open Matrix
    25
    26def scale {K : Type} [Field K] {n : ℕ} (z : Fin n → K) : Fin n → K := fun i => z i / (4 * (n : K))
    27
    28axiom coordinate_ball_bound {n : ℕ} (e : Fin n → ℝ) (ρ : ℝ) (nonnegative : 0 ≤ ρ)
    29 (ball : e ⬝ᵥ e ≤ ρ ^ 2) : ∀ i, |e i| ≤ ρ
    30
    31axiom scaled_cube_norm {n : ℕ} (positive : 0 < n) (z : Fin n → ℝ)
    32 (cube : ∀ i, 0 ≤ z i ∧ z i ≤ 1) : scale z ⬝ᵥ scale z ≤ (1 / 16 : ℝ)
    33
    34axiom initial_ball {n : ℕ} (positive : 0 < n) (z : Fin n → ℝ)
    35 (cube : ∀ i, 0 ≤ z i ∧ z i ≤ 1) (ρ : ℝ) (nonnegative : 0 ≤ ρ) (small : ρ ≤ 1 / 4)
    36 (e : Fin n → ℝ) (ball : e ⬝ᵥ e ≤ ρ ^ 2) :
    37 (scale z + e) ⬝ᵥ (scale z + e) ≤ 1
    38
    39axiom integer_normal_norm {n : ℕ} (a : Fin n → ℤ) (nonzero : ∃ i, a i ≠ 0) :
    40 1 ≤ (fun i => (a i : ℝ)) ⬝ᵥ (fun i => (a i : ℝ))
    41
    42end Lax263307.BufferedEllipsoid
    43
    Show ProofShow ProofShow ProofShow Proof
    Formalization notes

    The squared norms use finite dot products, matching the registered LP ellipsoid sequence. These geometric estimates do not assume that the independent-set hull has interior. Coordinate scaling is defined over an arbitrary field so its rational specialization is computable.

    Builds on

    none

    Used by
    From Mathlib

    Discussion

    Ask a question or add context. Endorsements and structured flags are kept in the review panel above.

    Loading discussion…