Lax Lean Archive

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

Joint distributions for the entropy-decrease argument

Lax263307.ConditioningDistribution · concepts/Lax263307/ConditioningDistribution.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 y∈Rr(G,k)y\in R_r(G,k), k>0k>0, ∣A∣<r|A|<r, and yA>0y_A>0, set

    πv=yA∪{v}kyA,quv=yA∪{u,v}k2yA.\pi_v=\frac{y_{A\cup\{v\}}}{k y_A},\qquad q_{uv}=\frac{y_{A\cup\{u,v\}}}{k^2 y_A}.

    The vector π\pi is a probability distribution. The entries of qq are nonnegative and symmetric, with both marginals equal to π\pi, and quv=0q_{uv}=0 whenever uvuv is an edge. For πv>0\pi_v>0, the distribution after conditioning on vv is given by πuv=quv/πv\pi^v_u=q_{uv}/\pi_v.

    Concept map
    3 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.ConditionedCosts
    2
    3/-!
    4---
    5title: Joint distributions for the entropy-decrease argument
    6type: theorem
    7---
    8For y∈Rr(G,k)y\in R_r(G,k), k>0k>0, ∣A∣<r|A|<r, and yA>0y_A>0, set
    9πv=yA∪{v}kyA,quv=yA∪{u,v}k2yA.\pi_v=\frac{y_{A\cup\{v\}}}{k y_A},\qquad q_{uv}=\frac{y_{A\cup\{u,v\}}}{k^2 y_A}.
    10
    11The vector π\pi is a probability distribution. The entries of qq are
    12nonnegative and symmetric, with both marginals equal to π\pi, and quv=0q_{uv}=0
    13whenever uvuv is an edge. For πv>0\pi_v>0, the distribution after conditioning
    14on vv is given by πuv=quv/πv\pi^v_u=q_{uv}/\pi_v.
    15
    16# Attribution
    17
    18Bonnet–Chang, proof of Lemma 12, equations (15) and (16).
    19-/
    20
    21namespace Lax263307.ConditioningDistribution
    22
    23open LinearRelaxation
    24
    25/-- Normalize conditioned vertex costs to a probability vector. -/
    26noncomputable def marginal {n r : ℕ} (y : MomentVector n r)
    27 (A : Finset (Fin n)) (k : ℕ) (v : Fin n) : ℝ :=
    28 conditioned y A v / k
    29
    30/-- The joint distribution obtained from moments containing two extra vertices. -/
    31noncomputable def joint {n r : ℕ} (y : MomentVector n r)
    32 (A : Finset (Fin n)) (k : ℕ) (u v : Fin n) : ℝ :=
    33 value y (insert u (insert v A)) / ((k : ℝ) ^ 2 * value y A)
    34
    35/-- The probability and conditional-probability identities for the moment relaxation. -/
    36axiom distribution_identities {n : ℕ} (G : SimpleGraph (Fin n)) (k r : ℕ)
    37 (y : MomentVector n r) (feasible : IsFeasible G k r y)
    38 (A : Finset (Fin n)) (size : A.card < r) (positive : 0 < value y A)
    39 (target_positive : 0 < k) :
    40 (∀ v, 0 ≤ marginal y A k v) ∧
    41 (∑ v : Fin n, marginal y A k v) = 1 ∧
    42 (∀ u v, 0 ≤ joint y A k u v) ∧
    43 (∀ u v, joint y A k u v = joint y A k v u) ∧
    44 (∀ v, (∑ u : Fin n, joint y A k u v) = marginal y A k v) ∧
    45 (∀ u v, G.Adj u v → joint y A k u v = 0) ∧
    46 (∀ u v, 0 < marginal y A k v →
    47 marginal y (insert v A) k u = joint y A k u v / marginal y A k v)
    48
    49end Lax263307.ConditioningDistribution
    50
    Show Proof

    Attribution

    Bonnet–Chang, proof of Lemma 12, equations (15) and (16).

    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…