Lax Lean Archive

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

Edge mass bounds the average entropy decrease

Lax263307.EntropyGap · concepts/Lax263307/EntropyGap.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 π\pi be a probability vector and let qq be a symmetric nonnegative joint distribution with marginals π\pi. Suppose quv=0q_{uv}=0 on edges of GG. For πv>0\pi_v>0, set πuv=quv/πv\pi^v_u=q_{uv}/\pi_v. Then

    H(π)−∑vπvH(πv)≥∑u,v: uv∈E(G)πuπv.H(\pi)-\sum_v\pi_v H(\pi^v) \ge\sum_{u,v:\,uv\in E(G)}\pi_u\pi_v.

    Terms with πv=0\pi_v=0 have weight zero.

    Concept map
    2 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.Entropy
    2
    3/-!
    4---
    5title: Edge mass bounds the average entropy decrease
    6type: theorem
    7---
    8Let π\pi be a probability vector and let qq be a symmetric nonnegative
    9joint distribution with marginals π\pi. Suppose quv=0q_{uv}=0 on edges of GG.
    10For πv>0\pi_v>0, set πuv=quv/πv\pi^v_u=q_{uv}/\pi_v. Then
    11H(π)−∑vπvH(πv)≥∑u,v: uv∈E(G)πuπv.H(\pi)-\sum_v\pi_v H(\pi^v) \ge\sum_{u,v:\,uv\in E(G)}\pi_u\pi_v.
    12
    13Terms with πv=0\pi_v=0 have weight zero.
    14
    15# Attribution
    16
    17Bonnet–Chang, proof of Lemma 12, equations (17) and (18).
    18
    19# Formalization notes
    20
    21The lower bound uses xln⁡x≥x−1x\ln x\ge x-1 on the support of qq.
    22All edge pairs lie outside that support. Converting natural-log entropy
    23to bits only increases this nonnegative bound, since 0<ln⁡2≤10<\ln2\le1.
    24-/
    25
    26namespace Lax263307.EntropyGap
    27
    28open Entropy
    29
    30/-- The expected loss in entropy dominates the ordered adjacency mass. -/
    31axiom average_entropy_gap {n : ℕ} (G : SimpleGraph (Fin n)) [DecidableRel G.Adj]
    32 (π : Fin n → ℝ) (q : Fin n → Fin n → ℝ)
    33 (probability : IsProbability π) (nonnegative : ∀ u v, 0 ≤ q u v)
    34 (symmetric : ∀ u v, q u v = q v u)
    35 (marginals : ∀ v, (∑ u, q u v) = π v)
    36 (edge_zero : ∀ u v, G.Adj u v → q u v = 0) :
    37 adjacencyMass G π ≤ entropy π - ∑ v, π v * entropy (fun u => q u v / π v)
    38
    39end Lax263307.EntropyGap
    40
    Show Proof

    Attribution

    Bonnet–Chang, proof of Lemma 12, equations (17) and (18).

    Formalization notes

    The lower bound uses xln⁡x≥x−1x\ln x\ge x-1 on the support of qq. All edge pairs lie outside that support. Converting natural-log entropy to bits only increases this nonnegative bound, since 0<ln⁡2≤10<\ln2\le1.

    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…