The separate carré-du-champ identification needed for Fisher energy

AutoSamplingTheory.TechnicalLemmas.InformationTheory.CanonicalDirichletFisher.HasCanonicalFisherGamma · def · Teaching coverage

Statement

For arbitrary μ and π on finite-dimensional Euclidean space and a real-linear operator L on functions, HasCanonicalFisherGamma is the assertion that, π-almost everywhere, the algebraic carré du champ of the selected density ρ and log-ratio r equals ρ times the squared totalized gradient of r. This equality is a separate input to the bridge, not a chain rule derived by the definition.

All objects and hypotheses

• ι is a finite index type (Fintype ι), and E = EuclideanSpace ℝ ι has its standard real inner product, norm, topology and Borel measurable structure. Empty ι is allowed; no Nonempty ι assumption is made.
• μ and π are arbitrary measures on E. No probability, finite-total-mass, or normalization hypothesis is present.
• Use the exact selected functions ρ(x) = (μ.rnDeriv π x).toReal and r(x) = RNLogRatio.logRatio μ π x = MeasureTheory.llr μ π x = Real.log(ρ(x)); put q(x) = ‖gradient r x‖². These are fixed by the original ordered pair (μ,π), not arbitrary versions.
• L is a real-linear map from all functions E → ℝ to all functions E → ℝ. Its linearity alone does not say that it generates a Markov semigroup, preserves a measure, or is a diffusion.
• This proposition is defined without assuming any domain witness, absolute continuity, integrability, σ-finiteness, or differentiability. To use it as a hypothesis, a caller must actually prove its π-a.e. equality.

Construction and meaning

def HasCanonicalFisherGamma
    (mu pi : Measure (State (ι := ι)))
    (generator :
      (State (ι := ι) → ℝ) →ₗ[ℝ] (State (ι := ι) → ℝ)) : Prop

def HasCanonicalFisherGamma
    (mu pi : Measure (State (ι := ι)))
    (generator :
      (State (ι := ι) → ℝ) →ₗ[ℝ] (State (ι := ι) → ℝ)) : Prop :=
  ∀ᵐ x ∂pi,
    StochasticProcesses.CarreDuChamp.carreDuChamp generator
      (RNLogRatio.density mu pi) (RNLogRatio.logRatio mu pi) x =
      RNLogRatio.density mu pi x *
        CanonicalRelativeFisher.scoreSq mu pi x

/-- Chewi Theorem 1.2.14 plus the concrete Gamma/score identification gives
exactly the canonical relative Fisher information:

`E_pi(dmu/dpi, log(dmu/dpi)) = FI(mu || pi)`.

This is the reusable Dirichlet--Fisher edge consumed by KL dissipation and by
the generator form of log-Sobolev inequalities. -/

Scope and omitted-condition boundaries

• This is the selected RN/log-ratio and its totalized classical gradient, not a representative-free Sobolev score. Equality of log-ratios merely a.e. does not by itself identify their gradients. Mathlib sets gradient to zero at nondifferentiable points; the score-domain witness excludes those points only μ-a.e.
• These are only local pair conditions. No global stationarity, reversibility, generator-domain closure, concrete Langevin generator, or diffusion chain rule is derived.
• No existence of the smooth score domain is proved. No weak derivative, Sobolev-domain membership, lower-semicontinuous or extended-valued Fisher extension, or square-root-density identity 4∫‖∇√ρ‖² dπ is established.
• A μ-a.e. identity alone would not be the same stated hypothesis; the integral comparison later uses this π-a.e. identity.
• This does not follow from absolute continuity alone and does not construct a valid canonical-density chain rule.