Extract the one-quarter factor from supplied integral representations

AutoSamplingTheory.lsiKlFiSqrtDensityFisherChainIntegralHandoffScalar · theorem · Teaching coverage

Statement

In the same arbitrary-measure finite-coordinate setting, suppose D and J are real numbers represented by ∫∑dSqrt_i²dμ and ∫r∑dLog_i²dμ. With the a.e. positivity and coordinate derivative identities listed below, D=J/4. No integrability is added by this representation handoff.

All objects and hypotheses

• α is measurable, I has Fintype, and μ is any measure on α; no finiteness or probability hypothesis.
• r:α→ℝ and dr,dSqrt,dLog:I→α→ℝ are arbitrary functions.
• For μ-almost every x, r(x)>0.
• For μ-almost every x, simultaneously for every i, dSqrt_i(x)=dr_i(x)/(2√r(x)); separately, for μ-almost every x, simultaneously for every i, dLog_i(x)=dr_i(x)/r(x).
• No measurability or integrability of these functions is assumed by this congruence statement.
• D,J∈ℝ with the two displayed integral-representation equalities.

Notation and interpretation

A.e. and strong measurability

A.e. means outside a μ-null set. AEMeasurable means equality a.e. to a measurable map; AEStronglyMeasurable (abbreviated AESM) means equality a.e. to a strongly measurable function, which is approximable by simple functions.

\[f=g\quad\mu\text{-a.e.}\]

Integrability and Bochner integrals

L¹ in the teaching formulas means Integrable, not a newly defined quotient-space element. ∫ denotes Mathlib's totalized Bochner integral: it is zero for nonintegrable functions, and also for a codomain lacking completeness. Do not infer integrability or a genuine finite expectation from an unqualified integral equality. Real-valued integrals have a complete codomain; missing integrability still matters.

\[f\in L^1(\mu)\quad\Longleftrightarrow\quad f\text{ is a.e. strongly measurable and }\int^{\!-}\|f\|\,d\mu<\infty\]

Mathematical proof

theorem lsiKlFiSqrtDensityFisherChainIntegralHandoffScalar
    {α ι : Type*} [MeasurableSpace α] [Fintype ι] (mu : Measure α)
    {r : α → Real} {dirichlet fisher : Real} {dr dSqrt dLog : ι → α → Real}
    (hdirichlet : dirichlet = ∫ x, (∑ i, dSqrt i x ^ 2) ∂mu)
    (hfisher : fisher = ∫ x, (r x * ∑ i, dLog i x ^ 2) ∂mu)
    (hr : ∀ᵐ x ∂mu, 0 < r x)
    (hdSqrt : ∀ᵐ x ∂mu,
      ∀ i, dSqrt i x = (1 / (2 * Real.sqrt (r x))) * dr i x)
    (hdLog : ∀ᵐ x ∂mu, ∀ i, dLog i x = dr i x / r x) :
    dirichlet = (1 / 4) * fisher

theorem lsiKlFiSqrtDensityFisherChainIntegralHandoffScalar
    {α ι : Type*} [MeasurableSpace α] [Fintype ι] (mu : Measure α)
    {r : α → Real} {dirichlet fisher : Real} {dr dSqrt dLog : ι → α → Real}
    (hdirichlet : dirichlet = ∫ x, (∑ i, dSqrt i x ^ 2) ∂mu)
    (hfisher : fisher = ∫ x, (r x * ∑ i, dLog i x ^ 2) ∂mu)
    (hr : ∀ᵐ x ∂mu, 0 < r x)
    (hdSqrt : ∀ᵐ x ∂mu,
      ∀ i, dSqrt i x = (1 / (2 * Real.sqrt (r x))) * dr i x)
    (hdLog : ∀ᵐ x ∂mu, ∀ i, dLog i x = dr i x / r x) :
    dirichlet = (1 / 4) * fisher := by
  rw [hdirichlet, hfisher]
  rw [← integral_const_mul]
  exact lsiKlFiSqrtDensityFisherChainIntegralFiniteSum mu hr hdSqrt hdLog

/-- Scalar rearrangement behind the one-sided use of the cited DV formula.

This is not a proof of Donsker--Varadhan.  It starts after a cited or
eventually formalized entropy-duality theorem has supplied the variational
upper bound for an admissible test.
-/

Scope and omitted-condition boundaries

• ∫ denotes Mathlib's totalized Bochner integral: it is zero for nonintegrable functions, and also for a codomain lacking completeness. Do not infer integrability or a genuine finite expectation from an unqualified integral equality. Real-valued integrals have a complete codomain; missing integrability still matters.
• These are scalar, density-integral or supplied-derivative handoffs. They do not prove an LSI, the admissibility of its square-root-density test, the vector/Sobolev chain rule or the full KL–Fisher comparison.
• No integral finiteness, vector-gradient identification, or LSI test admissibility is concluded.