Lax Lean Archive

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

Finite relative entropy and support costs

Lax342547.RelativeEntropy · concepts/Lax342547/RelativeEntropy.lean · lax-342547

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

    Lemma

    Finite probability weights have nonnegative relative entropy on their common support. Continuous entropy has compact minimizers, pointwise density caps give an upper budget, and support restriction costs the negative logarithm of its mass.

    Concept map
    5 concepts
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on ADescendants are omitted for concepts with more than 10 descendants.
    Evidence

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

    1 compact_entropy_minimizer proven

    2 continuous_entropy proven

    3 entropy_decomposition proven

    4 entropy_density_bound proven

    5 entropy_nonneg proven

    6 entropy_support_cost proven

    7 probability_compact proven

    8 probability_convex proven

    Lean source view on GitHub

    1import Mathlib.InformationTheory.KullbackLeibler.KLFun
    2import Mathlib.Topology.Instances.Real.Lemmas
    3import Mathlib.Analysis.Convex.StdSimplex
    4import Lax342547.RetainedImages
    5
    6/-!
    7---
    8title: Finite relative entropy and support costs
    9type: lemma
    10---
    11Finite probability weights have nonnegative relative entropy on their common support. Continuous entropy has compact minimizers, pointwise density caps give an upper budget, and support restriction costs the negative logarithm of its mass.
    12-/
    13
    14namespace Lax342547.RelativeEntropy
    15
    16open scoped BigOperators
    17
    18noncomputable def entropy {Ω : Type} [Fintype Ω] (ρ q : Ω → ℝ) : ℝ :=
    19 ∑ x, (ρ x * Real.log (ρ x) - ρ x * Real.log (q x))
    20
    21def Probability {Ω : Type} [Fintype Ω] (ρ : Ω → ℝ) : Prop :=
    22 (∀ x, 0 ≤ ρ x) ∧ ∑ x, ρ x = 1
    23
    24axiom entropy_nonneg {Ω : Type} [Fintype Ω] (ρ q : Ω → ℝ)
    25 (hρ : Probability ρ) (hq : Probability q) (hsupport : ∀ x, 0 < ρ x → 0 < q x) :
    26 0 ≤ entropy ρ q
    27
    28axiom entropy_density_bound {Ω : Type} [Fintype Ω] (ρ q : Ω → ℝ) (cap : ℝ)
    29 (hρ : Probability ρ) (hq : ∀ x, 0 < q x) (_hcap : 0 < cap)
    30 (hbound : ∀ x, ρ x ≤ cap*q x) : entropy ρ q ≤ Real.log cap
    31
    32axiom continuous_entropy {Ω : Type} [Fintype Ω] (q : Ω → ℝ) : Continuous (fun ρ : Ω → ℝ => entropy ρ q)
    33
    34axiom compact_entropy_minimizer {Ω : Type} [Fintype Ω]
    35 (P : Set (Ω → ℝ)) (q : Ω → ℝ) (hP : IsCompact P) (hne : P.Nonempty) :
    36 ∃ ρ ∈ P, ∀ ρ' ∈ P, entropy ρ q ≤ entropy ρ' q
    37
    38axiom entropy_decomposition {Ω : Type} [Fintype Ω] (ρ ρ' q : Ω → ℝ)
    39 (_hsupport : ∀ x, 0 < ρ' x → 0 < ρ x)
    40 (_hρ : ∀ x, 0 ≤ ρ x) (_hρ' : ∀ x, 0 ≤ ρ' x) :
    41 entropy ρ' q - entropy ρ q = entropy ρ' ρ +
    42 ∑ x, (ρ' x-ρ x)*(Real.log (ρ x)-Real.log (q x))
    43
    44axiom probability_compact {Ω : Type} [Fintype Ω] : IsCompact {ρ : Ω → ℝ | Probability ρ}
    45
    46axiom probability_convex {Ω : Type} [Fintype Ω] : Convex ℝ {ρ : Ω → ℝ | Probability ρ}
    47
    48axiom entropy_support_cost {Ω : Type} [Fintype Ω] (ρ q : Ω → ℝ) (S : Ω → Prop)
    49 (hρ : Probability ρ) (hq : Probability q)
    50 (hsupport : ∀ x, 0 < ρ x → 0 < q x) (hS : ∀ x, ¬ S x → ρ x = 0)
    51 (hmass : 0 < Lax342547.RetainedImages.cellMass q S) :
    52 -Real.log (Lax342547.RetainedImages.cellMass q S) ≤ entropy ρ q
    53
    54end Lax342547.RelativeEntropy
    55
    Show ProofShow ProofShow ProofShow ProofShow ProofShow ProofShow ProofShow Proof
    Builds on
    Used by
    From Mathlib

    Discussion

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

    Loading discussion…