Lax Lean Archive

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

Entropy along feasible mixture lines, including new support

Lax342547.EntropyLines · concepts/Lax342547/EntropyLines.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

    Old occupied coordinates have a finite directional derivative. Newly occupied coordinates give an exact t log t term whose positive coefficient forces the entropy difference quotient to negative infinity.

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

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

    1 entropy_mix_identity proven

    2 entropy_new_support_slope proven

    3 mix_derivative proven

    4 old_entropy_derivative proven

    5 old_entropy_zero proven

    Lean source view on GitHub

    1import Lax342547.RelativeEntropy
    2import Mathlib.Analysis.Calculus.Deriv.Slope
    3
    4/-!
    5---
    6title: Entropy along feasible mixture lines, including new support
    7type: lemma
    8---
    9Old occupied coordinates have a finite directional derivative. Newly occupied coordinates give an exact t log t term whose positive coefficient forces the entropy difference quotient to negative infinity.
    10-/
    11
    12namespace Lax342547.EntropyLines
    13
    14open Lax342547.RelativeEntropy
    15open scoped Topology BigOperators
    16open Filter
    17
    18noncomputable def mix {Ω : Type} (ρ ρ' : Ω → ℝ) (t : ℝ) : Ω → ℝ :=
    19 fun x => (1-t)*ρ x+t*ρ' x
    20
    21noncomputable def coordinate (p q : ℝ) : ℝ := p*Real.log p-p*Real.log q
    22
    23noncomputable def oldEntropy {Ω : Type} [Fintype Ω] (ρ ρ' q : Ω → ℝ) (t : ℝ) : ℝ := by
    24 classical
    25 exact ∑ x, if ρ x = 0 then 0 else coordinate (mix ρ ρ' t x) (q x)
    26
    27noncomputable def oldDerivative {Ω : Type} [Fintype Ω] (ρ ρ' q : Ω → ℝ) : ℝ := by
    28 classical
    29 exact ∑ x, if ρ x = 0 then 0 else (ρ' x-ρ x)*(Real.log (ρ x)+1-Real.log (q x))
    30
    31noncomputable def newMass {Ω : Type} [Fintype Ω] (ρ ρ' : Ω → ℝ) : ℝ := by
    32 classical
    33 exact ∑ x, if ρ x = 0 then ρ' x else 0
    34
    35noncomputable def newEntropy {Ω : Type} [Fintype Ω] (ρ ρ' q : Ω → ℝ) : ℝ := by
    36 classical
    37 exact ∑ x, if ρ x = 0 then coordinate (ρ' x) (q x) else 0
    38
    39axiom mix_derivative {Ω : Type} (ρ ρ' : Ω → ℝ) (x : Ω) :
    40 HasDerivAt (fun t => mix ρ ρ' t x) (ρ' x-ρ x) 0
    41
    42axiom old_entropy_derivative {Ω : Type} [Fintype Ω] (ρ ρ' q : Ω → ℝ) :
    43 HasDerivAt (oldEntropy ρ ρ' q) (oldDerivative ρ ρ' q) 0
    44
    45axiom entropy_mix_identity {Ω : Type} [Fintype Ω] (ρ ρ' q : Ω → ℝ)
    46 (hρ' : ∀ x, 0 ≤ ρ' x) (t : ℝ) (ht : 0 < t) :
    47 entropy (mix ρ ρ' t) q = oldEntropy ρ ρ' q t + t*newMass ρ ρ'*Real.log t + t*newEntropy ρ ρ' q
    48
    49axiom old_entropy_zero {Ω : Type} [Fintype Ω] (ρ ρ' q : Ω → ℝ) :
    50 oldEntropy ρ ρ' q 0 = entropy ρ q
    51
    52axiom entropy_new_support_slope {Ω : Type} [Fintype Ω] (ρ ρ' q : Ω → ℝ)
    53 (hρ' : ∀ x, 0 ≤ ρ' x) (hnew : 0 < newMass ρ ρ') :
    54 Tendsto (fun t => (entropy (mix ρ ρ' t) q-entropy ρ q)/t) (𝓝[>] 0) atBot
    55
    56end Lax342547.EntropyLines
    57
    Show 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…