Lax Lean Archive

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

Rounding loses at most one weight unit per vertex

Lax263307.RoundingBounds · concepts/Lax263307/RoundingBounds.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

    For nonnegative weights and τ>0\tau>0, the multiplicities tv=⌊wv/τ⌋t_v=\lfloor w_v/\tau\rfloor satisfy

    wv−τ≤τtv≤wv.w_v-\tau\le\tau t_v\le w_v.

    Consequently, for each vertex set JJ,

    τ∑v∈Jtv≥w(J)−∣J∣τ.\tau\sum_{v\in J}t_v\ge w(J)-|J|\tau.

    With τ=εW/(2n)\tau=\varepsilon W/(2n), the total number of copies is at most 2n2/ε2n^2/\varepsilon.

    Concept map
    5 concepts; 3 descendants hidden
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A
    Evidence

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

    1 pointwise_bounds proven

    2 set_rounding_loss proven

    3 total_copy_bound proven

    Lean source view on GitHub

    1import Lax263307.WeightRounding
    2
    3/-!
    4---
    5title: Rounding loses at most one weight unit per vertex
    6type: theorem
    7---
    8For nonnegative weights and τ>0\tau>0, the multiplicities
    9tv=⌊wv/τ⌋t_v=\lfloor w_v/\tau\rfloor satisfy
    10wv−τ≤τtv≤wv.w_v-\tau\le\tau t_v\le w_v.
    11Consequently, for each vertex set JJ,
    12τ∑v∈Jtv≥w(J)−∣J∣τ.\tau\sum_{v\in J}t_v\ge w(J)-|J|\tau.
    13With τ=εW/(2n)\tau=\varepsilon W/(2n), the total number of copies is at most
    142n2/ε2n^2/\varepsilon.
    15
    16# Attribution
    17
    18Bonnet–Chang, proof of Theorem 2 in Section 6.
    19-/
    20
    21namespace Lax263307.RoundingBounds
    22
    23open WeightedIndependentSet WeightRounding
    24
    25/-- The floor approximation loses at most one positive scaling unit. -/
    26axiom pointwise_bounds {n : ℕ} (w : Fin n → ℚ) (τ : ℚ)
    27 (nonnegative : ∀ v, 0 ≤ w v) (positive_scale : 0 < τ) :
    28 ∀ v, τ * (roundedCopies w τ v : ℚ) ≤ w v ∧
    29 w v - τ ≤ τ * (roundedCopies w τ v : ℚ)
    30
    31/-- The additive rounding loss is at most the set cardinality times the scaling unit. -/
    32axiom set_rounding_loss {n : ℕ} (w : Fin n → ℚ) (τ : ℚ)
    33 (nonnegative : ∀ v, 0 ≤ w v) (positive_scale : 0 < τ) (J : Finset (Fin n)) :
    34 weight w J - (J.card : ℚ) * τ ≤ τ * ((∑ v ∈ J, roundedCopies w τ v : ℕ) : ℚ)
    35
    36/-- The rounded blow-up order is polynomial in the order and inverse accuracy. -/
    37axiom total_copy_bound {n : ℕ} (w : Fin n → ℚ) (ε : ℚ)
    38 (nonnegative : ∀ v, 0 ≤ w v) (positive_order : 0 < n)
    39 (positive_accuracy : 0 < ε) (positive_maximum : 0 < maximumWeight w) :
    40 ((∑ v, copies w ε v : ℕ) : ℚ) ≤ 2 * (n : ℚ) ^ 2 / ε
    41
    42end Lax263307.RoundingBounds
    43
    Show ProofShow ProofShow Proof

    Attribution

    Bonnet–Chang, proof of Theorem 2 in Section 6.

    Builds on
    Used by
    From Mathlib

    none

    Discussion

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

    Loading discussion…