ASTIS mathematical exposition

Integrate the a.e. finite-coordinate Fisher-chain identity

AutoSamplingTheory.lsiKlFiSqrtDensityFisherChainIntegralFiniteSum · theorem · Teaching coverage

Statement

Under the finite-coordinate hypotheses below, suppose positivity of r and both families of derivative-coefficient identities hold μ-a.e. Then the real integral of ∑dSqrt_i² equals the real integral of (1/4)r∑dLog_i². This is a congruence identity for totalized integrals, with no integrability premise.

\[\int\sum_i d_{\sqrt{\ },i}(x)^2\,d\mu(x)=\int\frac14\left(r(x)\sum_i d_{\log,i}(x)^2\right)\,d\mu(x).\]

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.

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

1. Combine the three a.e. hypotheses

Intersect the full-measure sets for positivity and the two uniform coordinate identities. At every remaining x all scalar hypotheses hold together.

\[r(x)>0,\ d_{\sqrt{\ },i}(x)=dr_i(x)/(2\sqrt{r(x)}),\ d_{\log,i}(x)=dr_i(x)/r(x)\quad\forall i.\]

Corresponding Lean step

filter_upwards [hr,hdSqrt,hdLog]

2. Apply the finite-sum theorem at that x

Treat r(x) and the coordinate values as scalar data for the previous theorem.

\[\sum_i d_{\sqrt{\ },i}(x)^2=\tfrac14r(x)\sum_i d_{\log,i}(x)^2\quad\mu\text{-a.e.}\]

Corresponding Lean step

lsiKlFiSqrtDensityFisherChainFiniteSumScalar hx hSqrt hLog

3. Use integral congruence

A.e. equality suffices for equality of the real integrals under Mathlib's totalized convention.

\[\int A\,d\mu=\int B\,d\mu\quad\text{if }A=B\ \mu\text{-a.e.}\]

Corresponding Lean step

integral_congr_ae

Lean statement · lsiKlFiSqrtDensityFisherChainIntegralFiniteSum

The a.e. assumptions quantify over x first and every coordinate second. They are not a theorem proving those derivative identities.

Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.

theorem lsiKlFiSqrtDensityFisherChainIntegralFiniteSum
    {α ι : Type*} [MeasurableSpace α] [Fintype ι] (mu : Measure α)
    {r : α → Real} {dr dSqrt dLog : ι → α → Real}
    (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) :
    ∫ x, (∑ i, dSqrt i x ^ 2) ∂mu =
      ∫ x, (1 / 4) * (r x * ∑ i, dLog i x ^ 2) ∂mu

Exact module and namespace context

Lean proof · lsiKlFiSqrtDensityFisherChainIntegralFiniteSum

The proof intersects the a.e. events, invokes the scalar finite-sum identity pointwise, then integrates that equality.

theorem lsiKlFiSqrtDensityFisherChainIntegralFiniteSum
    {α ι : Type*} [MeasurableSpace α] [Fintype ι] (mu : Measure α)
    {r : α → Real} {dr dSqrt dLog : ι → α → Real}
    (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) :
    ∫ x, (∑ i, dSqrt i x ^ 2) ∂mu =
      ∫ x, (1 / 4) * (r x * ∑ i, dLog i x ^ 2) ∂mu := by
  refine integral_congr_ae ?_
  filter_upwards [hr, hdSqrt, hdLog] with x hx hSqrt hLog
  exact lsiKlFiSqrtDensityFisherChainFiniteSumScalar hx hSqrt hLog

/-- Scalar Dirichlet/Fisher handoff after the integral finite-sum identity.

This packages the exact `dirichlet=(1/4)*FI` input consumed by the existing
LSI/KL/FI scalar bridges when the analytic backend represents the Dirichlet
and Fisher quantities by finite-coordinate integrals.  It does not identify
those finite-coordinate integrals with the paper's vector-gradient quantities.
-/

Exact module and namespace context

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.
Does not assert finite Dirichlet/Fisher integrals or justify exchanging coordinate sums and integrals. No such interchange is used.

Source and reuse

ASTIS parents called

AutoSamplingTheory.lsiKlFiSqrtDensityFisherChainFiniteSumScalar

Mathlib API called (external library)

MeasureTheory.integral_congr_ae

Mathematical sources

Exact existing ASTIS declaration and body — Directly read local source; not a new proof or source-fidelity verdict.
MeasureTheory.integral_congr_ae — Directly inspected pinned Mathlib theorem/API. Reuse is distinguished from a new ASTIS proof.
AutoSamplingTheory.lsiKlFiSqrtDensityFisherChainFiniteSumScalar — Existing root ASTIS dependency; use its own adjacent teaching unit.

ASTIS prose is not a quotation or a source-equivalence certificate. Definitions and aliases are explained as constructions, not counted as new mathematical proofs.