Samplinglib mathematical lesson

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

AutoSamplingTheory.lsiKlFiSqrtDensityFisherChainIntegralFiniteSum · theorem · Teaching coverage

Read this first

Mathematical 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).\]

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.

Download module (.lean)

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

Proof roadmap

1Combine 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.
2Apply the finite-sum theorem at that x
Treat r(x) and the coordinate values as scalar data for the previous theorem.
3Use integral congruence
A.e. equality suffices for equality of the real integrals under Mathlib's totalized convention.

Full assumptions and notation

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 verification

The exact proof begins folded immediately after the mathematical argument; the statement is folded beside the claim above.

Lean proof · lsiKlFiSqrtDensityFisherChainIntegralFiniteSum

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

Download module (.lean)

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

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.

Sources, dependencies, and reuse

Source and reuse

Samplinglib 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.

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