Lax Lean Archive

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

Removing nonpositive weights

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

    Replace each rational weight wvw_v by max⁡(wv,0)\max(w_v,0). An approximation for these nonnegative weights yields the same approximation for the original weights by removing the nonpositive-weight vertices of its returned set. If all weights are nonpositive, the empty set is optimal.

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

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

    1 nonpositive_case proven

    2 signed_weight_transfer proven

    Lean source view on GitHub

    1import Lax263307.WeightedIndependentSet
    2
    3/-!
    4---
    5title: Removing nonpositive weights
    6type: theorem
    7---
    8Replace each rational weight wvw_v by max⁡(wv,0)\max(w_v,0). An approximation for
    9these nonnegative weights yields the same approximation for the original
    10weights by removing the nonpositive-weight vertices of its returned set.
    11If all weights are nonpositive, the empty set is optimal.
    12
    13# Formalization notes
    14
    15Clipping changes only vertex weights, so the graph stays in its original
    16class. Removing selected vertices preserves independence. The approximation
    17transfer assumes an accuracy in [0,1][0,1].
    18-/
    19
    20namespace Lax263307.PositiveWeights
    21
    22open WeightedIndependentSet
    23
    24/-- Clip negative weights to zero. -/
    25def positiveWeights {n : ℕ} (w : Fin n → ℚ) : Fin n → ℚ := fun v => max (w v) 0
    26
    27/-- Retain only the strictly positive-weight vertices of a returned set. -/
    28def discardNonpositive {n : ℕ} (w : Fin n → ℚ) (I : Finset (Fin n)) : Finset (Fin n) :=
    29 I.filter fun v => 0 < w v
    30
    31/-- Approximation for clipped weights transfers to arbitrary signed weights. -/
    32axiom signed_weight_transfer {n : ℕ} (G : SimpleGraph (Fin n)) (w : Fin n → ℚ)
    33 (ε : ℚ) (accuracy_nonnegative : 0 ≤ ε) (accuracy_le_one : ε ≤ 1)
    34 (I : Finset (Fin n)) (approximation : IsApproximation G (positiveWeights w) ε I) :
    35 IsApproximation G w ε (discardNonpositive w I)
    36
    37/-- The empty set solves instances whose weights are all nonpositive. -/
    38axiom nonpositive_case {n : ℕ} (G : SimpleGraph (Fin n)) (w : Fin n → ℚ)
    39 (nonpositive : ∀ v, w v ≤ 0) (ε : ℚ) (accuracy_nonnegative : 0 ≤ ε)
    40 (accuracy_le_one : ε ≤ 1) : IsApproximation G w ε ∅
    41
    42end Lax263307.PositiveWeights
    43
    Show ProofShow Proof
    Formalization notes

    Clipping changes only vertex weights, so the graph stays in its original class. Removing selected vertices preserves independence. The approximation transfer assumes an accuracy in [0,1][0,1].

    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…