Lax Lean Archive

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

A small conditioning set gives low edge cost

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

    Let p,k,rp,k,r be positive integers with r≥2plog⁡2nr\ge2p\log_2 n, and let y∈Rr(G,k)y\in R_r(G,k). There exists a set AA of size at most rr with yA>0y_A>0 such that the conditioned costs lie in [0,1][0,1], have total mass kk, and satisfy

    ∑uv∈E(G)xuxv≤k2/p.\sum_{uv\in E(G)}x_u x_v\le k^2/p.
    Concept map
    8 concepts
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on ADescendants are omitted for concepts with more than 10 descendants.
    Evidence

    Each proof establishes this claim relative to its assumptions.

    Lean source view on GitHub

    1import Lax263307.EntropyDecrease
    2import Lax263307.EntropyBounds
    3
    4/-!
    5---
    6title: A small conditioning set gives low edge cost
    7type: theorem
    8---
    9Let p,k,rp,k,r be positive integers with r≥2plog⁡2nr\ge2p\log_2 n, and let
    10y∈Rr(G,k)y\in R_r(G,k). There exists a set AA of size at most rr with yA>0y_A>0
    11such that the conditioned costs lie in [0,1][0,1], have total mass kk, and satisfy
    12∑uv∈E(G)xuxv≤k2/p.\sum_{uv\in E(G)}x_u x_v\le k^2/p.
    13
    14# Attribution
    15
    16Bonnet–Chang, the existence assertion in Lemma 12.
    17
    18# Formalization notes
    19
    20This statement supplies the mathematical guarantee for finite enumeration.
    21The rational implementation and its running-time bound are separate proof
    22obligations. No entropy values need to be computed by the enumeration.
    23-/
    24
    25namespace Lax263307.ConditioningExistence
    26
    27open LinearRelaxation ConditioningDistribution Entropy
    28
    29/-- Existence of the conditioning set promised by Lemma 12. -/
    30axiom exists_low_edge_cost {n : ℕ} (G : SimpleGraph (Fin n)) [DecidableRel G.Adj]
    31 (k r p : ℕ) (y : MomentVector n r) (feasible : IsFeasible G k r y)
    32 (target_positive : 0 < k) (level_positive : 0 < r) (threshold_positive : 0 < p)
    33 (budget : 2 * (p : ℝ) * Real.logb 2 n ≤ r) :
    34 ∃ A : Finset (Fin n), A.card ≤ r ∧ 0 < value y A ∧
    35 (∀ v, 0 ≤ conditioned y A v ∧ conditioned y A v ≤ 1) ∧
    36 (∑ v, conditioned y A v) = k ∧
    37 edgeCost G (conditioned y A) ≤ (k : ℝ) ^ 2 / p
    38
    39end Lax263307.ConditioningExistence
    40
    Show Proof

    Attribution

    Bonnet–Chang, the existence assertion in Lemma 12.

    Formalization notes

    This statement supplies the mathematical guarantee for finite enumeration. The rational implementation and its running-time bound are separate proof obligations. No entropy values need to be computed by the enumeration.

    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…