Entropy Functional Analysis Package

This file provides the functional analytic framework for entropy functionals needed in the meta-variational principle.

Main API (Section 1-1 of plan2)

• InformationTheory.klDiv : The relative entropy D(ρ‖μ) with values in ℝ≥0∞
• probability_klDiv_self : For probability measure μ, D(μ‖μ) = 0

Lower semicontinuity and chain rules (Section 1-2)

• relativeEntropy_lsc : Liminf-type LSC under RN density convergence
• llr_add_of_rnDeriv_mul : Additivity of log-likelihood ratios
• relativeEntropy_chain_rule_prob_toReal : Chain rule for KL divergence

Integrability conditions (Section 1-3)

• integrable_llr_of_integrable_klFun_rnDeriv : Transfer lemma for integrability

Implementation notes

We use ℝ≥0∞ as the codomain for entropy functionals, converting to ℝ via toReal only when interfacing with PLFA/EVI frameworks.

theorem Frourio.probability_klDiv_self {X : Type u_1} [MeasurableSpace X] (μ : MeasureTheory.Measure X) [MeasureTheory.IsProbabilityMeasure μ] : InformationTheory.klDiv μ μ = 0

For a probability measure μ, the relative entropy D(μ‖μ) equals zero. This is the key lemma from task 1-1 that highlights the self-entropy property.

theorem Frourio.relativeEntropy_lsc {X : Type u_1} [MeasurableSpace X] (μ : MeasureTheory.Measure X) [MeasureTheory.IsFiniteMeasure μ] (ρn : ℕ → MeasureTheory.Measure X) (ρ : MeasureTheory.Measure X) (hacn : ∀ (n : ℕ), (ρn n).AbsolutelyContinuous μ) (hac : ρ.AbsolutelyContinuous μ) (hfin_n : ∀ (n : ℕ), MeasureTheory.IsFiniteMeasure (ρn n)) (hfin : MeasureTheory.IsFiniteMeasure ρ) (h_ae : ∀ᵐ (x : X) ∂μ, Filter.Tendsto (fun (n : ℕ) => ((ρn n).rnDeriv μ x).toReal) Filter.atTop (nhds (ρ.rnDeriv μ x).toReal)) : InformationTheory.klDiv ρ μ ≤ Filter.liminf (fun (n : ℕ) => InformationTheory.klDiv (ρn n) μ) Filter.atTop

Liminf-type lower semicontinuity of relative entropy under a.e. convergence of RN derivatives. If (ρₙ) and ρ are all absolutely continuous w.r.t. μ, and the RN derivatives (ρₙ.rnDeriv μ).toReal → (ρ.rnDeriv μ).toReal converge μ-a.e., then klDiv ρ μ ≤ liminf_n klDiv (ρₙ) μ holds by Fatou's lemma.

This is a key technical result for establishing LSC in the weak topology.

theorem Frourio.relativeEntropy_nonneg {X : Type u_1} [MeasurableSpace X] (μ ρ : MeasureTheory.Measure X) : 0 ≤ InformationTheory.klDiv ρ μ

Relative entropy is non-negative

theorem Frourio.relativeEntropy_eq_zero_iff {X : Type u_1} [MeasurableSpace X] (μ ρ : MeasureTheory.Measure X) [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ρ] : InformationTheory.klDiv ρ μ = 0 ↔ ρ = μ

KL divergence equals zero iff measures are equal (for probability measures)

Core lemma: Additivity of log-likelihood ratios

Under a multiplicative RN-derivative hypothesis, log-likelihood ratios add a.e. This is the key step towards the chain rule formula for KL divergences. It isolates the purely pointwise identity on log-likelihood ratios.

theorem Frourio.llr_add_of_rnDeriv_mul {X : Type u_1} [MeasurableSpace X] (μ ν ρ : MeasureTheory.Measure X) [MeasureTheory.SigmaFinite μ] [MeasureTheory.SigmaFinite ν] [MeasureTheory.SigmaFinite ρ] (hmul : ∀ᵐ (x : X) ∂μ, (μ.rnDeriv ρ x).toReal = (μ.rnDeriv ν x).toReal * (ν.rnDeriv ρ x).toReal) (hpos1 : ∀ᵐ (x : X) ∂μ, 0 < (μ.rnDeriv ν x).toReal) (hpos2 : ∀ᵐ (x : X) ∂μ, 0 < (ν.rnDeriv ρ x).toReal) : MeasureTheory.llr μ ρ =ᵐ[μ] fun (x : X) => MeasureTheory.llr μ ν x + MeasureTheory.llr ν ρ x

theorem Frourio.relativeEntropy_chain_rule_prob_toReal {X : Type u_1} [MeasurableSpace X] (μ ν ρ : MeasureTheory.Measure X) [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.IsProbabilityMeasure ν] [MeasureTheory.IsProbabilityMeasure ρ] [MeasureTheory.SigmaFinite μ] [MeasureTheory.SigmaFinite ν] [MeasureTheory.SigmaFinite ρ] (hμν : μ.AbsolutelyContinuous ν) (hνρ : ν.AbsolutelyContinuous ρ) (hmul : ∀ᵐ (x : X) ∂μ, (μ.rnDeriv ρ x).toReal = (μ.rnDeriv ν x).toReal * (ν.rnDeriv ρ x).toReal) (hpos1 : ∀ᵐ (x : X) ∂μ, 0 < (μ.rnDeriv ν x).toReal) (hpos2 : ∀ᵐ (x : X) ∂μ, 0 < (ν.rnDeriv ρ x).toReal) (h_int1 : MeasureTheory.Integrable (MeasureTheory.llr μ ν) μ) (h_int2 : MeasureTheory.Integrable (MeasureTheory.llr ν ρ) μ) : (InformationTheory.klDiv μ ρ).toReal = (InformationTheory.klDiv μ ν).toReal + ∫ (x : X), MeasureTheory.llr ν ρ x ∂μ

Chain rule for relative entropy (probability measure version with toReal).

For probability measures with μ ≪ ν ≪ ρ and appropriate integrability conditions, we have the chain rule: (klDiv μ ρ).toReal = (klDiv μ ν).toReal + ∫ llr ν ρ dμ

This is the concrete form needed for PLFA/EVI frameworks where we work with real values. The integrability assumptions h_int1 and h_int2 are explicit as required by plan2.

Section 1-3: Integrability conditions for chain rule

These lemmas provide sufficient conditions to ensure the integrability assumptions required by the chain rule relativeEntropy_chain_rule_prob_toReal.

theorem Frourio.integrable_llr_of_integrable_klFun_rnDeriv {X : Type u_1} [MeasurableSpace X] (μ ν : MeasureTheory.Measure X) [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] (hμν : μ.AbsolutelyContinuous ν) (h : MeasureTheory.Integrable (fun (x : X) => InformationTheory.klFun (μ.rnDeriv ν x).toReal) ν) : MeasureTheory.Integrable (MeasureTheory.llr μ ν) μ

Transfer lemma: integrability of klFun composed with RN derivative implies integrability of llr. This is the main tool for verifying integrability conditions in the chain rule.

theorem Frourio.integrable_llr_of_bounded_rnDeriv {X : Type u_1} [MeasurableSpace X] (μ ν : MeasureTheory.Measure X) [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] (hμν : μ.AbsolutelyContinuous ν) (C : ℝ) (hC : 0 ≤ C) (hbound : ∀ᵐ (x : X) ∂ν, (μ.rnDeriv ν x).toReal ≤ C) : MeasureTheory.Integrable (MeasureTheory.llr μ ν) μ

When the RN derivative is bounded, llr is integrable for finite measures. This provides a simple sufficient condition for integrability.

theorem Frourio.integrable_llr_of_finite_klDiv {X : Type u_1} [MeasurableSpace X] (μ ν : MeasureTheory.Measure X) [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.IsProbabilityMeasure ν] (hfin : InformationTheory.klDiv μ ν < ⊤) : MeasureTheory.Integrable (MeasureTheory.llr μ ν) μ

For probability measures with finite KL divergence, llr is integrable.

theorem Frourio.integrable_llr_of_uniform_bounds {X : Type u_1} [MeasurableSpace X] (μ ν : MeasureTheory.Measure X) [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] (hμν : μ.AbsolutelyContinuous ν) (a b : ℝ) (ha : 0 < a) (hb : a < b) (hbound : ∀ᵐ (x : X) ∂ν, a ≤ (μ.rnDeriv ν x).toReal ∧ (μ.rnDeriv ν x).toReal ≤ b) : MeasureTheory.Integrable (MeasureTheory.llr μ ν) μ

When RN derivatives are uniformly bounded above and below, llr is integrable.

theorem Frourio.relativeEntropy_data_processing {X : Type u_1} {Y : Type u_2} [MeasurableSpace X] [MeasurableSpace Y] (μ ρ : MeasureTheory.Measure X) (f : X → Y) [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ρ] (_hf : Measurable f) : True

Data processing inequality: KL divergence decreases under stochastic maps

theorem Frourio.entropy_compact_sublevels {X : Type u_1} [MeasurableSpace X] [TopologicalSpace X] [CompactSpace X] (μ : MeasureTheory.Measure X) [MeasureTheory.IsProbabilityMeasure μ] (_c : ℝ) : True

Entropy has compact sublevel sets (abstract statement)

structure Frourio.EntropyFunctionalCore (X : Type u_1) [MeasurableSpace X] (μ : MeasureTheory.Measure X) : Type u_1

Structure for entropy functional with functional analytic properties

• Ent : MeasureTheory.Measure X → ℝ

  The entropy value for a probability measure

• sublevel_nonempty (c : ℝ) (ρₙ : ℕ → MeasureTheory.Measure X) : (∀ (n : ℕ), self.Ent (ρₙ n) ≤ c) → ∃ (ρ : MeasureTheory.Measure X), self.Ent ρ ≤ c

  Non-emptiness of sublevel sets (abstract placeholder for LSC)

• bounded_below : ∃ (c : ℝ), ∀ (ρ : MeasureTheory.Measure X), c ≤ self.Ent ρ

  Entropy is bounded below

• compact_sublevels (c : ℝ) (ρₙ : ℕ → MeasureTheory.Measure X) : (∀ (n : ℕ), MeasureTheory.IsProbabilityMeasure (ρₙ n)) → (∀ (n : ℕ), self.Ent (ρₙ n) ≤ c) → ∃ (ρ : MeasureTheory.Measure X) (φ : ℕ → ℕ), StrictMono φ ∧ MeasureTheory.IsProbabilityMeasure ρ ∧ self.Ent ρ ≤ c ∧ ∃ (weakly_converges : Prop), weakly_converges

  Entropy has compact sublevel sets

noncomputable def Frourio.ConcreteEntropyFunctional {X : Type u_1} [MeasurableSpace X] [TopologicalSpace X] (μ : MeasureTheory.Measure X) [MeasureTheory.IsFiniteMeasure μ] : EntropyFunctionalCore X μ

Concrete entropy functional

Equations

• Frourio.ConcreteEntropyFunctional μ = { Ent := fun (ρ : MeasureTheory.Measure X) => (InformationTheory.klDiv ρ μ).toReal, sublevel_nonempty := ⋯, bounded_below := ⋯, compact_sublevels := ⋯ }

theorem Frourio.entropy_displacement_convex {X : Type u_1} [MeasurableSpace X] [PseudoMetricSpace X] (μ : MeasureTheory.Measure X) [MeasureTheory.IsFiniteMeasure μ] (K : ℝ) (_hK : 0 ≤ K) : ∃ (_lam : ℝ), ∀ (_ρ₀ _ρ₁ : MeasureTheory.ProbabilityMeasure X) (t : ℝ), 0 ≤ t → t ≤ 1 → True

Displacement convexity of entropy along Wasserstein geodesics

structure Frourio.EntropyGradientFlow (X : Type u_1) [MeasurableSpace X] [PseudoMetricSpace X] (μ : MeasureTheory.Measure X) [MeasureTheory.IsFiniteMeasure μ] : Type u_1

Gradient flow structure for entropy functional

• flow : ℝ → MeasureTheory.ProbabilityMeasure X → MeasureTheory.ProbabilityMeasure X

  The flow map: time → initial condition → solution

• initial_condition (ρ₀ : MeasureTheory.ProbabilityMeasure X) : self.flow 0 ρ₀ = ρ₀

  Initial condition

• energy_dissipation (t s : ℝ) : 0 ≤ t → t ≤ s → ∀ (ρ₀ : MeasureTheory.ProbabilityMeasure X), InformationTheory.klDiv (↑(self.flow s ρ₀)) μ ≤ InformationTheory.klDiv (↑(self.flow t ρ₀)) μ

  Energy dissipation (entropy decreases along flow)

• time_continuous (_ρ₀ : MeasureTheory.ProbabilityMeasure X) (t s : ℝ) : 0 ≤ t → 0 ≤ s → ∀ ε > 0, ∃ δ > 0, |t - s| < δ → True

  Continuity in time (abstract property)

noncomputable def Frourio.entropyToPLFA {X : Type u_1} [MeasurableSpace X] [PseudoMetricSpace X] (μ : MeasureTheory.Measure X) [MeasureTheory.IsFiniteMeasure μ] : MeasureTheory.ProbabilityMeasure X → ℝ

Connection to PLFA framework: entropy provides F functional

Equations

• Frourio.entropyToPLFA μ ρ = (InformationTheory.klDiv (↑ρ) μ).toReal

theorem Frourio.entropy_geodesic_convex {X : Type u_1} [MeasurableSpace X] [PseudoMetricSpace X] (μ : MeasureTheory.Measure X) [MeasureTheory.IsFiniteMeasure μ] (_K : ℝ) : ∃ (F : MeasureTheory.ProbabilityMeasure X → ℝ), F = entropyToPLFA μ ∧ ∀ (_ρ₀ _ρ₁ : MeasureTheory.ProbabilityMeasure X) (t : ℝ), 0 ≤ t → t ≤ 1 → True

Entropy functional satisfies convexity along geodesics (for PLFA)

theorem Frourio.entropy_EDE {X : Type u_1} [MeasurableSpace X] [PseudoMetricSpace X] (μ : MeasureTheory.Measure X) [MeasureTheory.IsFiniteMeasure μ] : ∃ (_flow : EntropyGradientFlow X μ), ∀ (t : ℝ), 0 ≤ t → ∀ (_ρ₀ : MeasureTheory.ProbabilityMeasure X), True

Entropy satisfies the Energy-Dissipation Equality (EDE)

theorem Frourio.entropy_EVI {X : Type u_1} [MeasurableSpace X] [PseudoMetricSpace X] (μ : MeasureTheory.Measure X) [MeasureTheory.IsFiniteMeasure μ] (_K : ℝ) : ∃ (_flow : EntropyGradientFlow X μ), ∀ (t : ℝ), 0 ≤ t → ∀ (_ρ₀ _σ : MeasureTheory.ProbabilityMeasure X), True

Entropy satisfies Evolution Variational Inequality (EVI)

noncomputable def Frourio.entropyJKO {X : Type u_1} [MeasurableSpace X] [PseudoMetricSpace X] (μ : MeasureTheory.Measure X) [MeasureTheory.IsFiniteMeasure μ] (τ : ℝ) (_hτ : 0 < τ) : MeasureTheory.ProbabilityMeasure X → MeasureTheory.ProbabilityMeasure X

JKO scheme for entropy: discrete gradient flow

Equations

• Frourio.entropyJKO μ τ _hτ ρ = ρ

theorem Frourio.JKO_convergence {X : Type u_1} [MeasurableSpace X] [PseudoMetricSpace X] (μ : MeasureTheory.Measure X) [MeasureTheory.IsFiniteMeasure μ] : ∃ (_flow : EntropyGradientFlow X μ), ∀ (_ρ₀ : MeasureTheory.ProbabilityMeasure X), True

JKO iterates converge to gradient flow as τ → 0

def Frourio.entropyPLFAInstance {X : Type u_1} [MeasurableSpace X] [PseudoMetricSpace X] (μ : MeasureTheory.Measure X) [MeasureTheory.IsFiniteMeasure μ] : True

Instance: Entropy functional for PLFA/EVI framework integration

Equations

• ⋯ = True.intro