Probability: mathematical reading route

Almost-everywhere equal variables have the same pushforward

AutoSamplingTheory.lawMapEqOfAEEq · theorem · Teaching coverage

Statement

On measurable spaces Ω and E, let P be any measure and X,Y:Ω→E any functions. If X=Y P-almost everywhere, their pushforward measures are equal. No measurability assumption is present in this totalized-map identity.

All objects and hypotheses

• Ω and E are arbitrary measurable spaces; P is any measure on Ω, with no finiteness or probability hypothesis.
• X,Y are arbitrary functions Ω→E; hXY asserts their P-almost-everywhere equality.

Notation and interpretation

Pushforward law

P is an arbitrary measure unless explicitly declared finite or a probability. The word law here abbreviates a pushforward measure; probability-language interpretations require normalization separately. Mathlib totalizes map to zero when X is not a.e. measurable; unqualified map-congruence and some law-space adapters intentionally retain that generality.

\[(X_\#\mu)(A)=\mu(X^{-1}A)\quad\text{when the measurable pushforward interpretation applies}\]

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.}\]

Mathematical proof

theorem lawMapEqOfAEEq {Ω E : Type*} [MeasurableSpace Ω] [MeasurableSpace E]
    {P : Measure Ω} {X Y : Ω → E}
    (hXY : X =ᵐ[P] Y) :
    Measure.map X P = Measure.map Y P

theorem lawMapEqOfAEEq {Ω E : Type*} [MeasurableSpace Ω] [MeasurableSpace E]
    {P : Measure Ω} {X Y : Ω → E}
    (hXY : X =ᵐ[P] Y) :
    Measure.map X P = Measure.map Y P := by
  exact Measure.map_congr hXY

/-- Integrating a test against a pushforward law is the same as integrating
the composed test on the original probability space.

This is the weak-test bookkeeping used before differentiating EM
interpolation laws.  It does not prove any time differentiability, generator
identity, conditional law, density, or Fokker--Planck equation.
-/

Scope and omitted-condition boundaries

• P is an arbitrary measure unless explicitly declared finite or a probability. The word law here abbreviates a pushforward measure; probability-language interpretations require normalization separately.
• Measure.map is totalized: without AEMeasurable assumptions, this is not a claim that the expression is the usual nondegenerate distribution of an arbitrary nonmeasurable random variable.
• No pointwise equality, process construction, conditional drift, or density theorem.

Integrate a test function through a pushforward measure

AutoSamplingTheory.lawMapIntegral · theorem · Teaching coverage

Statement

Let P be any measure on measurable Ω and let X:Ω→E be P-almost-everywhere measurable. If B is a real normed vector space and φ:E→B is almost-everywhere strongly measurable under X#P, then the integral of φ against X#P equals the integral of φ∘X against P. No integrability or completeness assumption is imposed by this equality.

All objects and hypotheses

• Ω and E are arbitrary measurable spaces; P is any measure on Ω, with no finiteness or probability hypothesis.
• B has NormedAddCommGroup and NormedSpace ℝ structures; completeness is not assumed.
• X:Ω→E is AEMeasurable under P; φ:E→B is AEStronglyMeasurable under X#P.

Notation and interpretation

Pushforward law

P is an arbitrary measure unless explicitly declared finite or a probability. The word law here abbreviates a pushforward measure; probability-language interpretations require normalization separately. Mathlib totalizes map to zero when X is not a.e. measurable; unqualified map-congruence and some law-space adapters intentionally retain that generality.

\[(X_\#\mu)(A)=\mu(X^{-1}A)\quad\text{when the measurable pushforward interpretation applies}\]

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 lawMapIntegral {Ω E B : Type*} [MeasurableSpace Ω]
    [MeasurableSpace E] [NormedAddCommGroup B] [NormedSpace ℝ B]
    {P : Measure Ω} {X : Ω → E} {φ : E → B}
    (hX : AEMeasurable X P)
    (hφ : AEStronglyMeasurable φ (Measure.map X P)) :
    (∫ x, φ x ∂Measure.map X P) = ∫ ω, φ (X ω) ∂P

theorem lawMapIntegral {Ω E B : Type*} [MeasurableSpace Ω]
    [MeasurableSpace E] [NormedAddCommGroup B] [NormedSpace ℝ B]
    {P : Measure Ω} {X : Ω → E} {φ : E → B}
    (hX : AEMeasurable X P)
    (hφ : AEStronglyMeasurable φ (Measure.map X P)) :
    (∫ x, φ x ∂Measure.map X P) = ∫ ω, φ (X ω) ∂P := by
  rw [integral_map hX hφ]

/-- Transport a supplied sample-space derivative to the corresponding
pushforward-law weak-test integral.

The analytic derivative is still an explicit hypothesis.  This lemma only
packages the `Measure.map` integral rewrite needed before applying a future
EM generator/Fokker--Planck theorem.
-/

Scope and omitted-condition boundaries

• P is an arbitrary measure unless explicitly declared finite or a probability. The word law here abbreviates a pushforward measure; probability-language interpretations require normalization separately.
• ∫ 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.
• This is a bookkeeping equality, not time differentiability, a generator identity or a Fokker–Planck equation.

Transfer a supplied weak derivative from samples to laws

AutoSamplingTheory.lawMapIntegralHasDerivAtOfSample · theorem · Teaching coverage

Statement

Under the time-indexed measurability hypotheses, suppose the real function s↦∫φ(X_s(ω))dP has derivative g at s₀. Then s↦∫φ(x)d((X_s)#P)(x) has the same derivative g at s₀. The analytic derivative is assumed, not derived.

All objects and hypotheses

• Ω and E are arbitrary measurable spaces; P is any measure on Ω, with no finiteness or probability hypothesis.
• X:ℝ→Ω→E is a time-indexed family, φ:E→ℝ is a fixed real test, and s₀,g are real numbers.
• For every real s, X_s is P-a.e. measurable and φ is a.e. strongly measurable under (X_s)#P.
• hderiv is HasDerivAt of the sample-space integral function, with derivative value g at s₀.

Notation and interpretation

Pushforward law

P is an arbitrary measure unless explicitly declared finite or a probability. The word law here abbreviates a pushforward measure; probability-language interpretations require normalization separately. Mathlib totalizes map to zero when X is not a.e. measurable; unqualified map-congruence and some law-space adapters intentionally retain that generality.

\[(X_\#\mu)(A)=\mu(X^{-1}A)\quad\text{when the measurable pushforward interpretation applies}\]

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\]

Derivatives

Derivative premises are never silently promoted to derived path regularity. The dominated differentiation units explicitly distinguish eventually-near-time assumptions from a.e.-sample, all-times-in-one-neighborhood assumptions.

\[\operatorname{HasDerivAt}(F,g,s_0)\ \Longrightarrow\ F\text{ is differentiable at }s_0\text{ and }F'(s_0)=g.\]

Mathematical proof

theorem lawMapIntegralHasDerivAtOfSample {Ω E : Type*}
    [MeasurableSpace Ω] [MeasurableSpace E]
    {P : Measure Ω} {X : ℝ → Ω → E} {φ : E → ℝ} {s0 g : ℝ}
    (hX : ∀ s, AEMeasurable (X s) P)
    (hφ : ∀ s, AEStronglyMeasurable φ (Measure.map (X s) P))
    (hderiv : HasDerivAt (fun s => ∫ ω, φ (X s ω) ∂P) g s0) :
    HasDerivAt (fun s => ∫ x, φ x ∂Measure.map (X s) P) g s0

theorem lawMapIntegralHasDerivAtOfSample {Ω E : Type*}
    [MeasurableSpace Ω] [MeasurableSpace E]
    {P : Measure Ω} {X : ℝ → Ω → E} {φ : E → ℝ} {s0 g : ℝ}
    (hX : ∀ s, AEMeasurable (X s) P)
    (hφ : ∀ s, AEStronglyMeasurable φ (Measure.map (X s) P))
    (hderiv : HasDerivAt (fun s => ∫ ω, φ (X s ω) ∂P) g s0) :
    HasDerivAt (fun s => ∫ x, φ x ∂Measure.map (X s) P) g s0 := by
  have hfun :
      (fun s => ∫ x, φ x ∂Measure.map (X s) P) =
        (fun s => ∫ ω, φ (X s ω) ∂P) := by
    funext s
    exact lawMapIntegral (hX s) (hφ s)
  simpa [hfun] using hderiv

/-- Transport a sample-space derivative to a named law path equal to a
`Measure.map` path.

This is the named-law variant used when a paper first writes
`hat rho_s = Law(hat X_s)` and the Lean target keeps `hatRhoS` as a separate
measure-valued path.  The only analytic derivative input remains the
sample-space derivative; this lemma just combines the named-law equality with
`lawMapIntegralHasDerivAtOfSample`.
-/

Scope and omitted-condition boundaries

• P is an arbitrary measure unless explicitly declared finite or a probability. The word law here abbreviates a pushforward measure; probability-language interpretations require normalization separately.
• ∫ 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.
• The derivative is an explicit premise; no generator, process, weak PDE or new differentiability result is inferred.

Transfer the derivative to a separately named law path

AutoSamplingTheory.lawIntegralHasDerivAtOfMeasureMapEqAndSample · theorem · Teaching coverage

Statement

Let ρ:ℝ→Measure E be a named path of measures with ρ_s=(X_s)#P for every s. Assume X_s is P-a.e. measurable, φ is ρ_s-a.e. strongly measurable at every time, and the sample integral has derivative g at s₀. Then the integral of φ under ρ_s also has derivative g at s₀.

All objects and hypotheses

• Ω and E are arbitrary measurable spaces; P is any measure on Ω, with no finiteness or probability hypothesis.
• X:ℝ→Ω→E, ρ:ℝ→Measure E, φ:E→ℝ, s₀,g∈ℝ.
• For every s, ρ_s=(X_s)#P, X_s is P-a.e. measurable, and φ is ρ_s-a.e. strongly measurable.
• The sample-space integral function has derivative g at s₀.

Notation and interpretation

Pushforward law

P is an arbitrary measure unless explicitly declared finite or a probability. The word law here abbreviates a pushforward measure; probability-language interpretations require normalization separately. Mathlib totalizes map to zero when X is not a.e. measurable; unqualified map-congruence and some law-space adapters intentionally retain that generality.

\[(X_\#\mu)(A)=\mu(X^{-1}A)\quad\text{when the measurable pushforward interpretation applies}\]

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\]

Derivatives

Derivative premises are never silently promoted to derived path regularity. The dominated differentiation units explicitly distinguish eventually-near-time assumptions from a.e.-sample, all-times-in-one-neighborhood assumptions.

\[\operatorname{HasDerivAt}(F,g,s_0)\ \Longrightarrow\ F\text{ is differentiable at }s_0\text{ and }F'(s_0)=g.\]

Mathematical proof

theorem lawIntegralHasDerivAtOfMeasureMapEqAndSample {Ω E : Type*}
    [MeasurableSpace Ω] [MeasurableSpace E]
    {P : Measure Ω} {X : ℝ → Ω → E} {ρ : ℝ → Measure E}
    {φ : E → ℝ} {s0 g : ℝ}
    (hρ : ∀ s, ρ s = Measure.map (X s) P)
    (hX : ∀ s, AEMeasurable (X s) P)
    (hφ : ∀ s, AEStronglyMeasurable φ (ρ s))
    (hderiv : HasDerivAt (fun s => ∫ ω, φ (X s ω) ∂P) g s0) :
    HasDerivAt (fun s => ∫ x, φ x ∂ρ s) g s0

theorem lawIntegralHasDerivAtOfMeasureMapEqAndSample {Ω E : Type*}
    [MeasurableSpace Ω] [MeasurableSpace E]
    {P : Measure Ω} {X : ℝ → Ω → E} {ρ : ℝ → Measure E}
    {φ : E → ℝ} {s0 g : ℝ}
    (hρ : ∀ s, ρ s = Measure.map (X s) P)
    (hX : ∀ s, AEMeasurable (X s) P)
    (hφ : ∀ s, AEStronglyMeasurable φ (ρ s))
    (hderiv : HasDerivAt (fun s => ∫ ω, φ (X s ω) ∂P) g s0) :
    HasDerivAt (fun s => ∫ x, φ x ∂ρ s) g s0 := by
  have hφMap :
      ∀ s, AEStronglyMeasurable φ (Measure.map (X s) P) := by
    intro s
    simpa [hρ s] using hφ s
  have hmap :
      HasDerivAt
        (fun s => ∫ x, φ x ∂Measure.map (X s) P) g s0 :=
    lawMapIntegralHasDerivAtOfSample
      (P := P) (X := X) (φ := φ) hX hφMap hderiv
  have hfun :
      (fun s => ∫ x, φ x ∂ρ s) =
        fun s => ∫ x, φ x ∂Measure.map (X s) P := by
    funext s
    rw [hρ s]
  simpa [hfun] using hmap

/-- Transport a dominated pointwise derivative to a pushforward-law weak-test
derivative.

This is the first parametric-integral step below the cycle-79 law-map handoff:
Mathlib's dominated derivative-under-integral theorem proves the sample-space
weak-test derivative, and `lawMapIntegralHasDerivAtOfSample` transports it to
the mapped law.  The EM path derivative, neighborhood, and domination data stay
explicit.
-/

Scope and omitted-condition boundaries

• P is an arbitrary measure unless explicitly declared finite or a probability. The word law here abbreviates a pushforward measure; probability-language interpretations require normalization separately.
• ∫ 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.
• Named-law reuse wrapper; all analytic derivative hypotheses remain external.

A dominated pathwise derivative yields a weak derivative of the law

AutoSamplingTheory.lawMapIntegralHasDerivAtOfDominated · theorem · Teaching coverage

Statement

On arbitrary measurable Ω and E with measure P, suppose the full neighborhood, measurability, integrability, pathwise differentiability and integrable domination conditions listed below hold. If the integral of the sample derivative at s₀ equals g, the test integral under the pushforward law s↦(X_s)#P has derivative g at s₀.

All objects and hypotheses

• Ω and E are arbitrary measurable spaces; P is any measure on Ω, with no finiteness or probability hypothesis.
• X:ℝ→Ω→E, φ:E→ℝ, s₀,g∈ℝ; D:ℝ→Ω→ℝ is the supplied sampleDeriv; U⊆ℝ is the supplied neighborhood; b:Ω→ℝ is the bound.
• For every s, X_s is P-a.e. measurable and φ is a.e. strongly measurable under its designated law.
• U belongs to the neighborhood filter of s₀. For all s sufficiently near s₀, ω↦φ(X_sω) is P-a.e. strongly measurable.
• ω↦φ(X_{s₀}ω) is P-integrable, and D(s₀,·) is P-a.e. strongly measurable.
• For P-almost every ω, simultaneously for every s∈U, |D(s,ω)|≤b(ω); b is P-integrable.
• For P-almost every ω, simultaneously for every s∈U, t↦φ(X_tω) has derivative D(s,ω) at s.
• The integral ∫D(s₀,ω)dP(ω) is supplied to equal g.

Notation and interpretation

Pushforward law

P is an arbitrary measure unless explicitly declared finite or a probability. The word law here abbreviates a pushforward measure; probability-language interpretations require normalization separately. Mathlib totalizes map to zero when X is not a.e. measurable; unqualified map-congruence and some law-space adapters intentionally retain that generality.

\[(X_\#\mu)(A)=\mu(X^{-1}A)\quad\text{when the measurable pushforward interpretation applies}\]

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\]

Derivatives

Derivative premises are never silently promoted to derived path regularity. The dominated differentiation units explicitly distinguish eventually-near-time assumptions from a.e.-sample, all-times-in-one-neighborhood assumptions.

\[\operatorname{HasDerivAt}(F,g,s_0)\ \Longrightarrow\ F\text{ is differentiable at }s_0\text{ and }F'(s_0)=g.\]

Mathematical proof

theorem lawMapIntegralHasDerivAtOfDominated {Ω E : Type*}
    [MeasurableSpace Ω] [MeasurableSpace E]
    {P : Measure Ω} {X : ℝ → Ω → E} {φ : E → ℝ} {s0 g : ℝ}
    {sampleDeriv : ℝ → Ω → ℝ} {neighborhood : Set ℝ}
    {bound : Ω → ℝ}
    (hX : ∀ s, AEMeasurable (X s) P)
    (hφ : ∀ s, AEStronglyMeasurable φ (Measure.map (X s) P))
    (hneighborhood : neighborhood ∈ 𝓝 s0)
    (hFMeas :
      ∀ᶠ s in 𝓝 s0, AEStronglyMeasurable (fun ω => φ (X s ω)) P)
    (hFInt : Integrable (fun ω => φ (X s0 ω)) P)
    (hDerivMeas : AEStronglyMeasurable (sampleDeriv s0) P)
    (hDerivBound :
      ∀ᵐ ω ∂P, ∀ s ∈ neighborhood, ‖sampleDeriv s ω‖ ≤ bound ω)
    (hBoundInt : Integrable bound P)
    (hPathDeriv :
      ∀ᵐ ω ∂P, ∀ s ∈ neighborhood,
        HasDerivAt (fun t => φ (X t ω)) (sampleDeriv s ω) s)
    (hDerivValue : (∫ ω, sampleDeriv s0 ω ∂P) = g) :
    HasDerivAt (fun s => ∫ x, φ x ∂Measure.map (X s) P) g s0

theorem lawMapIntegralHasDerivAtOfDominated {Ω E : Type*}
    [MeasurableSpace Ω] [MeasurableSpace E]
    {P : Measure Ω} {X : ℝ → Ω → E} {φ : E → ℝ} {s0 g : ℝ}
    {sampleDeriv : ℝ → Ω → ℝ} {neighborhood : Set ℝ}
    {bound : Ω → ℝ}
    (hX : ∀ s, AEMeasurable (X s) P)
    (hφ : ∀ s, AEStronglyMeasurable φ (Measure.map (X s) P))
    (hneighborhood : neighborhood ∈ 𝓝 s0)
    (hFMeas :
      ∀ᶠ s in 𝓝 s0, AEStronglyMeasurable (fun ω => φ (X s ω)) P)
    (hFInt : Integrable (fun ω => φ (X s0 ω)) P)
    (hDerivMeas : AEStronglyMeasurable (sampleDeriv s0) P)
    (hDerivBound :
      ∀ᵐ ω ∂P, ∀ s ∈ neighborhood, ‖sampleDeriv s ω‖ ≤ bound ω)
    (hBoundInt : Integrable bound P)
    (hPathDeriv :
      ∀ᵐ ω ∂P, ∀ s ∈ neighborhood,
        HasDerivAt (fun t => φ (X t ω)) (sampleDeriv s ω) s)
    (hDerivValue : (∫ ω, sampleDeriv s0 ω ∂P) = g) :
    HasDerivAt (fun s => ∫ x, φ x ∂Measure.map (X s) P) g s0 := by
  have hsample :
      HasDerivAt (fun s => ∫ ω, φ (X s ω) ∂P)
        (∫ ω, sampleDeriv s0 ω ∂P) s0 :=
    (hasDerivAt_integral_of_dominated_loc_of_deriv_le
      (F := fun s ω => φ (X s ω))
      (F' := sampleDeriv)
      (x₀ := s0)
      (s := neighborhood)
      (bound := bound)
      (μ := P)
      hneighborhood hFMeas hFInt hDerivMeas hDerivBound hBoundInt
      hPathDeriv).2
  rw [hDerivValue] at hsample
  exact lawMapIntegralHasDerivAtOfSample (P := P) (X := X) (φ := φ) hX hφ hsample

/-- Named-law version of `lawMapIntegralHasDerivAtOfDominated`.

If a paper keeps a named law path `ρ s` with `ρ s = Measure.map (X s) P`,
this combines the dominated sample-space derivative-under-integral step with
the named-law equality rewrite.
-/

Scope and omitted-condition boundaries

• P is an arbitrary measure unless explicitly declared finite or a probability. The word law here abbreviates a pushforward measure; probability-language interpretations require normalization separately.
• No finite measure is required, but the bound and base integrand must be integrable. No source-specific path derivative, drift formula, generator or PDE is proved here.

A dominated derivative for a named law path

AutoSamplingTheory.lawIntegralHasDerivAtOfMeasureMapEqAndDominated · theorem · Teaching coverage

Statement

Let ρ_s=(X_s)#P at every real s. With φ a.e. strongly measurable under ρ_s and all the dominated sample-derivative hypotheses below, including ∫D(s₀,ω)dP=g, the named weak integral s↦∫φdρ_s has derivative g at s₀.

All objects and hypotheses

• Ω and E are arbitrary measurable spaces; P is any measure on Ω, with no finiteness or probability hypothesis.
• ρ:ℝ→Measure E satisfies ρ_s=(X_s)#P for every s; the designated law for φ's measurability is ρ_s.
• X:ℝ→Ω→E, φ:E→ℝ, s₀,g∈ℝ; D:ℝ→Ω→ℝ is the supplied sampleDeriv; U⊆ℝ is the supplied neighborhood; b:Ω→ℝ is the bound.
• For every s, X_s is P-a.e. measurable and φ is a.e. strongly measurable under its designated law.
• U belongs to the neighborhood filter of s₀. For all s sufficiently near s₀, ω↦φ(X_sω) is P-a.e. strongly measurable.
• ω↦φ(X_{s₀}ω) is P-integrable, and D(s₀,·) is P-a.e. strongly measurable.
• For P-almost every ω, simultaneously for every s∈U, |D(s,ω)|≤b(ω); b is P-integrable.
• For P-almost every ω, simultaneously for every s∈U, t↦φ(X_tω) has derivative D(s,ω) at s.
• The integral ∫D(s₀,ω)dP(ω) is supplied to equal g.

Notation and interpretation

Pushforward law

P is an arbitrary measure unless explicitly declared finite or a probability. The word law here abbreviates a pushforward measure; probability-language interpretations require normalization separately. Mathlib totalizes map to zero when X is not a.e. measurable; unqualified map-congruence and some law-space adapters intentionally retain that generality.

\[(X_\#\mu)(A)=\mu(X^{-1}A)\quad\text{when the measurable pushforward interpretation applies}\]

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\]

Derivatives

Derivative premises are never silently promoted to derived path regularity. The dominated differentiation units explicitly distinguish eventually-near-time assumptions from a.e.-sample, all-times-in-one-neighborhood assumptions.

\[\operatorname{HasDerivAt}(F,g,s_0)\ \Longrightarrow\ F\text{ is differentiable at }s_0\text{ and }F'(s_0)=g.\]

Mathematical proof

theorem lawIntegralHasDerivAtOfMeasureMapEqAndDominated {Ω E : Type*}
    [MeasurableSpace Ω] [MeasurableSpace E]
    {P : Measure Ω} {X : ℝ → Ω → E} {ρ : ℝ → Measure E}
    {φ : E → ℝ} {s0 g : ℝ}
    {sampleDeriv : ℝ → Ω → ℝ} {neighborhood : Set ℝ}
    {bound : Ω → ℝ}
    (hρ : ∀ s, ρ s = Measure.map (X s) P)
    (hX : ∀ s, AEMeasurable (X s) P)
    (hφ : ∀ s, AEStronglyMeasurable φ (ρ s))
    (hneighborhood : neighborhood ∈ 𝓝 s0)
    (hFMeas :
      ∀ᶠ s in 𝓝 s0, AEStronglyMeasurable (fun ω => φ (X s ω)) P)
    (hFInt : Integrable (fun ω => φ (X s0 ω)) P)
    (hDerivMeas : AEStronglyMeasurable (sampleDeriv s0) P)
    (hDerivBound :
      ∀ᵐ ω ∂P, ∀ s ∈ neighborhood, ‖sampleDeriv s ω‖ ≤ bound ω)
    (hBoundInt : Integrable bound P)
    (hPathDeriv :
      ∀ᵐ ω ∂P, ∀ s ∈ neighborhood,
        HasDerivAt (fun t => φ (X t ω)) (sampleDeriv s ω) s)
    (hDerivValue : (∫ ω, sampleDeriv s0 ω ∂P) = g) :
    HasDerivAt (fun s => ∫ x, φ x ∂ρ s) g s0

theorem lawIntegralHasDerivAtOfMeasureMapEqAndDominated {Ω E : Type*}
    [MeasurableSpace Ω] [MeasurableSpace E]
    {P : Measure Ω} {X : ℝ → Ω → E} {ρ : ℝ → Measure E}
    {φ : E → ℝ} {s0 g : ℝ}
    {sampleDeriv : ℝ → Ω → ℝ} {neighborhood : Set ℝ}
    {bound : Ω → ℝ}
    (hρ : ∀ s, ρ s = Measure.map (X s) P)
    (hX : ∀ s, AEMeasurable (X s) P)
    (hφ : ∀ s, AEStronglyMeasurable φ (ρ s))
    (hneighborhood : neighborhood ∈ 𝓝 s0)
    (hFMeas :
      ∀ᶠ s in 𝓝 s0, AEStronglyMeasurable (fun ω => φ (X s ω)) P)
    (hFInt : Integrable (fun ω => φ (X s0 ω)) P)
    (hDerivMeas : AEStronglyMeasurable (sampleDeriv s0) P)
    (hDerivBound :
      ∀ᵐ ω ∂P, ∀ s ∈ neighborhood, ‖sampleDeriv s ω‖ ≤ bound ω)
    (hBoundInt : Integrable bound P)
    (hPathDeriv :
      ∀ᵐ ω ∂P, ∀ s ∈ neighborhood,
        HasDerivAt (fun t => φ (X t ω)) (sampleDeriv s ω) s)
    (hDerivValue : (∫ ω, sampleDeriv s0 ω ∂P) = g) :
    HasDerivAt (fun s => ∫ x, φ x ∂ρ s) g s0 := by
  have hφMap :
      ∀ s, AEStronglyMeasurable φ (Measure.map (X s) P) := by
    intro s
    simpa [hρ s] using hφ s
  have hmap :
      HasDerivAt
        (fun s => ∫ x, φ x ∂Measure.map (X s) P) g s0 :=
    lawMapIntegralHasDerivAtOfDominated
      (P := P) (X := X) (φ := φ) (sampleDeriv := sampleDeriv)
      (neighborhood := neighborhood) (bound := bound)
      hX hφMap hneighborhood hFMeas hFInt hDerivMeas hDerivBound
      hBoundInt hPathDeriv hDerivValue
  have hfun :
      (fun s => ∫ x, φ x ∂ρ s) =
        fun s => ∫ x, φ x ∂Measure.map (X s) P := by
    funext s
    rw [hρ s]
  simpa [hfun] using hmap

/-- Pushforward-law equality for paired random variables from componentwise
almost-everywhere equality.

This is a narrow endpoint-law helper for stitched EM paths: once two endpoint
representatives agree almost everywhere component by component, their joint
pushforward law agrees.  It does not construct conditional laws, densities, or
Fokker--Planck backends.
-/

Scope and omitted-condition boundaries

• P is an arbitrary measure unless explicitly declared finite or a probability. The word law here abbreviates a pushforward measure; probability-language interpretations require normalization separately.
• The uniform a.e.-sample/for-all-time hypotheses and integrable domination are not derived. No new weak PDE is asserted.

Componentwise a.e. equality preserves the joint image law

AutoSamplingTheory.lawMapProdEqOfAEEq · theorem · Teaching coverage

Statement

Let Ω,E,F be measurable spaces, P any measure, X,X′:Ω→E and Y,Y′:Ω→F any functions. If X=X′ P-a.e. and Y=Y′ P-a.e., then the image measures of the paired variables (X,Y) and (X′,Y′) are equal. No separate measurability is assumed.

All objects and hypotheses

• Ω,E,F are measurable spaces; P is any measure on Ω.
• X,X′:Ω→E and Y,Y′:Ω→F; the two component equalities hold P-almost everywhere.

Notation and interpretation

Pushforward law

P is an arbitrary measure unless explicitly declared finite or a probability. The word law here abbreviates a pushforward measure; probability-language interpretations require normalization separately. Mathlib totalizes map to zero when X is not a.e. measurable; unqualified map-congruence and some law-space adapters intentionally retain that generality.

\[(X_\#\mu)(A)=\mu(X^{-1}A)\quad\text{when the measurable pushforward interpretation applies}\]

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.}\]

Mathematical proof

theorem lawMapProdEqOfAEEq {Ω E F : Type*} [MeasurableSpace Ω]
    [MeasurableSpace E] [MeasurableSpace F]
    {P : Measure Ω} {X X' : Ω → E} {Y Y' : Ω → F}
    (hX : X =ᵐ[P] X') (hY : Y =ᵐ[P] Y') :
    Measure.map (fun ω => (X ω, Y ω)) P =
      Measure.map (fun ω => (X' ω, Y' ω)) P

theorem lawMapProdEqOfAEEq {Ω E F : Type*} [MeasurableSpace Ω]
    [MeasurableSpace E] [MeasurableSpace F]
    {P : Measure Ω} {X X' : Ω → E} {Y Y' : Ω → F}
    (hX : X =ᵐ[P] X') (hY : Y =ᵐ[P] Y') :
    Measure.map (fun ω => (X ω, Y ω)) P =
      Measure.map (fun ω => (X' ω, Y' ω)) P := by
  exact Measure.map_congr <| by
    filter_upwards [hX, hY] with ω hx hy
    simp [hx, hy]

/-- First marginal of a paired pushforward law.

This is endpoint-law bookkeeping for common-space EM arguments: after a joint
endpoint law has been represented as a paired pushforward, projecting the first
coordinate recovers the first endpoint law.  Measurability is explicit; the
lemma does not construct any process, density, or conditional law.
-/

Scope and omitted-condition boundaries

• P is an arbitrary measure unless explicitly declared finite or a probability. The word law here abbreviates a pushforward measure; probability-language interpretations require normalization separately.
• As in map_congr, totalized map semantics apply without measurability. No conditional law or coupling construction is supplied.

Extract the first marginal of a joint image law

AutoSamplingTheory.lawMapProdFst · theorem · Teaching coverage

Statement

Let Ω,E,F be measurable spaces and P any measure on Ω. For measurable X:Ω→E and Y:Ω→F, pushing the joint law (X,Y)#P through its first projection gives X#P.

All objects and hypotheses

• Ω,E,F are arbitrary measurable spaces and P is any measure on Ω.
• X:Ω→E and Y:Ω→F are both measurable, not merely assumed equal in law.

Notation and interpretation

Pushforward law

P is an arbitrary measure unless explicitly declared finite or a probability. The word law here abbreviates a pushforward measure; probability-language interpretations require normalization separately. Mathlib totalizes map to zero when X is not a.e. measurable; unqualified map-congruence and some law-space adapters intentionally retain that generality.

\[(X_\#\mu)(A)=\mu(X^{-1}A)\quad\text{when the measurable pushforward interpretation applies}\]

Mathematical proof

theorem lawMapProdFst {Ω E F : Type*} [MeasurableSpace Ω]
    [MeasurableSpace E] [MeasurableSpace F]
    {P : Measure Ω} {X : Ω → E} {Y : Ω → F}
    (hX : Measurable X) (hY : Measurable Y) :
    Measure.map Prod.fst (Measure.map (fun ω => (X ω, Y ω)) P) =
      Measure.map X P

theorem lawMapProdFst {Ω E F : Type*} [MeasurableSpace Ω]
    [MeasurableSpace E] [MeasurableSpace F]
    {P : Measure Ω} {X : Ω → E} {Y : Ω → F}
    (hX : Measurable X) (hY : Measurable Y) :
    Measure.map Prod.fst (Measure.map (fun ω => (X ω, Y ω)) P) =
      Measure.map X P := by
  rw [Measure.map_map measurable_fst (hX.prod hY)]
  rfl

/-- Second marginal of a paired pushforward law.

This is the right-endpoint analogue of `lawMapProdFst`; it keeps marginal-law
extraction separate from the conditional-drift and Fokker--Planck obligations.
-/

Scope and omitted-condition boundaries

• P is an arbitrary measure unless explicitly declared finite or a probability. The word law here abbreviates a pushforward measure; probability-language interpretations require normalization separately.
• Only orientation/marginal bookkeeping; no independence, conditional kernel, process or density construction.

Extract the second marginal of a joint image law

AutoSamplingTheory.lawMapProdSnd · theorem · Teaching coverage

Statement

Let Ω,E,F be measurable spaces and P any measure on Ω. For measurable X:Ω→E and Y:Ω→F, pushing the joint law (X,Y)#P through its second projection gives Y#P.

All objects and hypotheses

• Ω,E,F are arbitrary measurable spaces and P is any measure on Ω.
• X:Ω→E and Y:Ω→F are both measurable, not merely assumed equal in law.

Notation and interpretation

Pushforward law

P is an arbitrary measure unless explicitly declared finite or a probability. The word law here abbreviates a pushforward measure; probability-language interpretations require normalization separately. Mathlib totalizes map to zero when X is not a.e. measurable; unqualified map-congruence and some law-space adapters intentionally retain that generality.

\[(X_\#\mu)(A)=\mu(X^{-1}A)\quad\text{when the measurable pushforward interpretation applies}\]

Mathematical proof

theorem lawMapProdSnd {Ω E F : Type*} [MeasurableSpace Ω]
    [MeasurableSpace E] [MeasurableSpace F]
    {P : Measure Ω} {X : Ω → E} {Y : Ω → F}
    (hX : Measurable X) (hY : Measurable Y) :
    Measure.map Prod.snd (Measure.map (fun ω => (X ω, Y ω)) P) =
      Measure.map Y P

theorem lawMapProdSnd {Ω E F : Type*} [MeasurableSpace Ω]
    [MeasurableSpace E] [MeasurableSpace F]
    {P : Measure Ω} {X : Ω → E} {Y : Ω → F}
    (hX : Measurable X) (hY : Measurable Y) :
    Measure.map Prod.snd (Measure.map (fun ω => (X ω, Y ω)) P) =
      Measure.map Y P := by
  rw [Measure.map_map measurable_snd (hX.prod hY)]
  rfl

/-- Swap the coordinate order of a paired pushforward law.

Mathlib conditional-distribution APIs usually represent the joint law for
`Y | X` in the order `(X,Y)`.  Some paper proofs first name the joint law in the
opposite order.  This helper records only the `Measure.map` orientation
bookkeeping; it does not construct a conditional law.
-/

Scope and omitted-condition boundaries

• P is an arbitrary measure unless explicitly declared finite or a probability. The word law here abbreviates a pushforward measure; probability-language interpretations require normalization separately.
• Only orientation/marginal bookkeeping; no independence, conditional kernel, process or density construction.

Swap the coordinate order of a joint image law

AutoSamplingTheory.lawMapProdSwap · theorem · Teaching coverage

Statement

Let Ω,E,F be measurable spaces and P any measure on Ω. For measurable X:Ω→E and Y:Ω→F, pushing the joint law (X,Y)#P through coordinate swap gives the joint law (Y,X)#P.

All objects and hypotheses

• Ω,E,F are arbitrary measurable spaces and P is any measure on Ω.
• X:Ω→E and Y:Ω→F are both measurable, not merely assumed equal in law.

Notation and interpretation

Pushforward law

P is an arbitrary measure unless explicitly declared finite or a probability. The word law here abbreviates a pushforward measure; probability-language interpretations require normalization separately. Mathlib totalizes map to zero when X is not a.e. measurable; unqualified map-congruence and some law-space adapters intentionally retain that generality.

\[(X_\#\mu)(A)=\mu(X^{-1}A)\quad\text{when the measurable pushforward interpretation applies}\]

Mathematical proof

theorem lawMapProdSwap {Ω E F : Type*} [MeasurableSpace Ω]
    [MeasurableSpace E] [MeasurableSpace F]
    {P : Measure Ω} {X : Ω → E} {Y : Ω → F}
    (hX : Measurable X) (hY : Measurable Y) :
    Measure.map Prod.swap (Measure.map (fun ω => (X ω, Y ω)) P) =
      Measure.map (fun ω => (Y ω, X ω)) P

theorem lawMapProdSwap {Ω E F : Type*} [MeasurableSpace Ω]
    [MeasurableSpace E] [MeasurableSpace F]
    {P : Measure Ω} {X : Ω → E} {Y : Ω → F}
    (hX : Measurable X) (hY : Measurable Y) :
    Measure.map Prod.swap (Measure.map (fun ω => (X ω, Y ω)) P) =
      Measure.map (fun ω => (Y ω, X ω)) P := by
  rw [Measure.map_map measurable_swap (hX.prod hY)]
  rfl

/-- Mathlib orientation bridge between `condDistrib` and `condExpKernel`.

For the SALD conditional drift, instantiate `Y` with `X_k^eta` and `X` with
`hat X_s`: the conditional distribution of `X_k^eta` given `hat X_s` agrees
almost everywhere with the conditional-expectation kernel mapped by `X_k^eta`.
This is a local theorem from Mathlib's conditional-kernel backend, not a weak
Fokker--Planck or KL differentiability result.
-/

Scope and omitted-condition boundaries

• P is an arbitrary measure unless explicitly declared finite or a probability. The word law here abbreviates a pushforward measure; probability-language interpretations require normalization separately.
• Only orientation/marginal bookkeeping; no independence, conditional kernel, process or density construction.

Match the conditional distribution and mapped conditional-expectation kernel

AutoSamplingTheory.condDistribAeEqCondExpKernelMap · theorem · Teaching coverage

Statement

Let Ω and γ be Standard Borel measurable spaces, with γ nonempty; let β be any measurable space and μ any finite measure on Ω. For measurable X:Ω→β and Y:Ω→γ and a fixed measurable set S⊆γ, the selected conditional probability of Y∈S given X, evaluated at X(ω), agrees μ-almost everywhere with the conditional-expectation kernel for σ(X), pushed forward by Y and evaluated on S.

All objects and hypotheses

• Ω, β, γ have measurable-space structures; Ω and γ are Standard Borel, and γ is nonempty. No Standard Borel assumption on β or Nonempty Ω is required.
• μ is finite; X:Ω→β and Y:Ω→γ are measurable; S⊆γ is measurable.

Notation and interpretation

Pushforward law

P is an arbitrary measure unless explicitly declared finite or a probability. The word law here abbreviates a pushforward measure; probability-language interpretations require normalization separately. Mathlib totalizes map to zero when X is not a.e. measurable; unqualified map-congruence and some law-space adapters intentionally retain that generality.

\[(X_\#\mu)(A)=\mu(X^{-1}A)\quad\text{when the measurable pushforward interpretation applies}\]

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.}\]

Conditional integral notation

The selected conditional distribution is a probability kernel, characterized as a conditional law only almost everywhere under the conditioning marginal. No pointwise choice, simultaneous equality on all events from a single-event a.e. theorem, or null-fiber support is asserted. Finite non-probability measures are reconstructed with their original total mass; any version changes on marginal-null inputs must retain a measurable kernel.

\[\lambda=(X,Y)_\#\mu,\quad m=X_\#\mu,\quad q(x)=\operatorname{condDistrib}(Y\mid X;\mu)(x),\quad C(x)=\int f(x,y)\,dq(x)(y)\]

Mathematical proof

theorem condDistribAeEqCondExpKernelMap {Ω β γ : Type*}
    [MeasurableSpace Ω] [MeasurableSpace β] [MeasurableSpace γ]
    [StandardBorelSpace Ω] [StandardBorelSpace γ] [Nonempty γ]
    {μ : Measure Ω} [IsFiniteMeasure μ] {X : Ω → β} {Y : Ω → γ}
    (hX : Measurable X) (hY : Measurable Y) {s : Set γ}
    (hs : MeasurableSet s) :
    (fun a => ProbabilityTheory.condDistrib Y X μ (X a) s) =ᵐ[μ]
      fun a =>
        (ProbabilityTheory.condExpKernel μ
            ((inferInstance : MeasurableSpace β).comap X)).map Y a s

theorem condDistribAeEqCondExpKernelMap {Ω β γ : Type*}
    [MeasurableSpace Ω] [MeasurableSpace β] [MeasurableSpace γ]
    [StandardBorelSpace Ω] [StandardBorelSpace γ] [Nonempty γ]
    {μ : Measure Ω} [IsFiniteMeasure μ] {X : Ω → β} {Y : Ω → γ}
    (hX : Measurable X) (hY : Measurable Y) {s : Set γ}
    (hs : MeasurableSet s) :
    (fun a => ProbabilityTheory.condDistrib Y X μ (X a) s) =ᵐ[μ]
      fun a =>
        (ProbabilityTheory.condExpKernel μ
            ((inferInstance : MeasurableSpace β).comap X)).map Y a s := by
  exact ProbabilityTheory.condDistrib_apply_ae_eq_condExpKernel_map
    (μ := μ) (X := Y) (Y := X) hY hX hs

/-- Sample-space component-version bridge from `condExpKernel.map` to
`condDistrib`.

For the SALD `condC` field, this isolates the remaining Mathlib-facing
boundary after `condDistrib` and `condExpKernel.map` have been aligned as
measure-valued kernels almost everywhere.  It turns a selected
`condExpKernel.map` version of the component field into the displayed
`condDistrib` integral equality after composing with `hat X_s`.  The theorem
does not prove the measure-valued kernel equality or choose the component
version; those remain the smaller conditional-kernel obligations.
-/

Scope and omitted-condition boundaries

• The selected conditional distribution is a probability kernel, characterized as a conditional law only almost everywhere under the conditioning marginal. No pointwise choice, simultaneous equality on all events from a single-event a.e. theorem, or null-fiber support is asserted.
• The exceptional set may depend on the fixed event S; do not upgrade this declaration alone to measure-valued a.e. kernel equality.
• No weak Fokker–Planck equation or KL differentiability result.

Transfer a chosen conditional integral version between equal kernels

AutoSamplingTheory.condDistribIntegralSampleAeEqOfCondExpKernelMap · theorem · Teaching coverage

Statement

Use the finite-measure conditional-kernel setting with Ω additionally Standard Borel. Suppose q(Xω) and the Y-image of the conditional-expectation kernel for σ(X) are equal as measures μ-a.e. Suppose integrating y↦f(Xω,y) against the latter measure gives a chosen field v(Xω) μ-a.e. Then integrating against q(Xω) also gives v(Xω) μ-a.e. The two a.e. identities are assumptions.

All objects and hypotheses

• Ω, β and γ are measurable spaces; γ is Standard Borel and nonempty.
• μ is a finite measure on Ω, not necessarily a probability; X:Ω→β and Y:Ω→γ are functions.
• F is a real normed vector space (NormedAddCommGroup and NormedSpace ℝ); no CompleteSpace assumption is added. The integrand f:β×γ→F is as specified below.
• Notation: λ=(ω↦(Xω,Yω))#μ, m=X#μ, q(x)=condDistrib(Y|X;μ)(x), and C(x)=∫f(x,y)dq(x)(y).
• Ω is also Standard Borel; v:β→F is a chosen field; R(ω)=(condExpKernel μ σ(X)).map Y (ω).
• hkernel gives equality q(Xω)=R(ω) as measures μ-a.e.; this is stronger than a separate eventwise statement with event-dependent null sets.
• hfield gives the stated integral equality to v(Xω) μ-a.e. No X/Y measurability or f integrability is separately assumed by this substitution theorem.

Notation and interpretation

Pushforward law

P is an arbitrary measure unless explicitly declared finite or a probability. The word law here abbreviates a pushforward measure; probability-language interpretations require normalization separately. Mathlib totalizes map to zero when X is not a.e. measurable; unqualified map-congruence and some law-space adapters intentionally retain that generality.

\[(X_\#\mu)(A)=\mu(X^{-1}A)\quad\text{when the measurable pushforward interpretation applies}\]

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\]

Conditional integral notation

The selected conditional distribution is a probability kernel, characterized as a conditional law only almost everywhere under the conditioning marginal. No pointwise choice, simultaneous equality on all events from a single-event a.e. theorem, or null-fiber support is asserted. Finite non-probability measures are reconstructed with their original total mass; any version changes on marginal-null inputs must retain a measurable kernel.

\[\lambda=(X,Y)_\#\mu,\quad m=X_\#\mu,\quad q(x)=\operatorname{condDistrib}(Y\mid X;\mu)(x),\quad C(x)=\int f(x,y)\,dq(x)(y)\]

Mathematical proof

theorem condDistribIntegralSampleAeEqOfCondExpKernelMap {Ω β γ F : Type*}
    [MeasurableSpace Ω] [MeasurableSpace β] [MeasurableSpace γ]
    [NormedAddCommGroup F] [NormedSpace ℝ F]
    [StandardBorelSpace Ω] [StandardBorelSpace γ] [Nonempty γ]
    {μ : Measure Ω} [IsFiniteMeasure μ] {X : Ω → β} {Y : Ω → γ}
    {f : β × γ → F} {field : β → F}
    (hkernel :
      (fun a => ProbabilityTheory.condDistrib Y X μ (X a)) =ᵐ[μ]
        fun a =>
          (ProbabilityTheory.condExpKernel μ
            ((inferInstance : MeasurableSpace β).comap X)).map Y a)
    (hfield :
      (fun a => ∫ y, f (X a, y)
          ∂(ProbabilityTheory.condExpKernel μ
            ((inferInstance : MeasurableSpace β).comap X)).map Y a) =ᵐ[μ]
        fun a => field (X a)) :
    (fun a => ∫ y, f (X a, y)
        ∂ProbabilityTheory.condDistrib Y X μ (X a)) =ᵐ[μ]
      fun a => field (X a)

theorem condDistribIntegralSampleAeEqOfCondExpKernelMap {Ω β γ F : Type*}
    [MeasurableSpace Ω] [MeasurableSpace β] [MeasurableSpace γ]
    [NormedAddCommGroup F] [NormedSpace ℝ F]
    [StandardBorelSpace Ω] [StandardBorelSpace γ] [Nonempty γ]
    {μ : Measure Ω} [IsFiniteMeasure μ] {X : Ω → β} {Y : Ω → γ}
    {f : β × γ → F} {field : β → F}
    (hkernel :
      (fun a => ProbabilityTheory.condDistrib Y X μ (X a)) =ᵐ[μ]
        fun a =>
          (ProbabilityTheory.condExpKernel μ
            ((inferInstance : MeasurableSpace β).comap X)).map Y a)
    (hfield :
      (fun a => ∫ y, f (X a, y)
          ∂(ProbabilityTheory.condExpKernel μ
            ((inferInstance : MeasurableSpace β).comap X)).map Y a) =ᵐ[μ]
        fun a => field (X a)) :
    (fun a => ∫ y, f (X a, y)
        ∂ProbabilityTheory.condDistrib Y X μ (X a)) =ᵐ[μ]
      fun a => field (X a) := by
  filter_upwards [hkernel, hfield] with a hka hfa
  rw [hka, hfa]

/-- Strong measurability of a vector-valued conditional integral against
`condDistrib`.

This packages the Mathlib theorem in the orientation used by the SALD
component fields: conditioning variable `X`, sampled variable `Y`, and an
integrand on `(X,Y)`.  It does not prove the EM interpolation law or any weak
Fokker--Planck identity.
-/

Scope and omitted-condition boundaries

• The selected conditional distribution is a probability kernel, characterized as a conditional law only almost everywhere under the conditioning marginal. No pointwise choice, simultaneous equality on all events from a single-event a.e. theorem, or null-fiber support is asserted.
• ∫ 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.
• No regularity of the chosen field follows from this substitution alone.

The conditional integral is almost-everywhere strongly measurable on the sample space

AutoSamplingTheory.condDistribIntegralAEStronglyMeasurable · theorem · Teaching coverage

Statement

In the finite-measure conditional-distribution setting and notation below, assume Y is μ-a.e. measurable and X is μ-a.e. measurable. If f is almost-everywhere strongly measurable under the joint image measure λ, then C∘X is almost-everywhere strongly measurable under μ.

All objects and hypotheses

• Ω, β and γ are measurable spaces; γ is Standard Borel and nonempty.
• μ is a finite measure on Ω, not necessarily a probability; X:Ω→β and Y:Ω→γ are functions.
• F is a real normed vector space (NormedAddCommGroup and NormedSpace ℝ); no CompleteSpace assumption is added. The integrand f:β×γ→F is as specified below.
• Notation: λ=(ω↦(Xω,Yω))#μ, m=X#μ, q(x)=condDistrib(Y|X;μ)(x), and C(x)=∫f(x,y)dq(x)(y).
• Y is μ-a.e. measurable.
• X is μ-a.e. measurable.
• f is almost-everywhere strongly measurable under λ.

Notation and interpretation

Pushforward law

P is an arbitrary measure unless explicitly declared finite or a probability. The word law here abbreviates a pushforward measure; probability-language interpretations require normalization separately. Mathlib totalizes map to zero when X is not a.e. measurable; unqualified map-congruence and some law-space adapters intentionally retain that generality.

\[(X_\#\mu)(A)=\mu(X^{-1}A)\quad\text{when the measurable pushforward interpretation applies}\]

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\]

Conditional integral notation

The selected conditional distribution is a probability kernel, characterized as a conditional law only almost everywhere under the conditioning marginal. No pointwise choice, simultaneous equality on all events from a single-event a.e. theorem, or null-fiber support is asserted. Finite non-probability measures are reconstructed with their original total mass; any version changes on marginal-null inputs must retain a measurable kernel.

\[\lambda=(X,Y)_\#\mu,\quad m=X_\#\mu,\quad q(x)=\operatorname{condDistrib}(Y\mid X;\mu)(x),\quad C(x)=\int f(x,y)\,dq(x)(y)\]

Mathematical proof

theorem condDistribIntegralAEStronglyMeasurable {Ω β γ F : Type*}
    [MeasurableSpace Ω] [MeasurableSpace β] [MeasurableSpace γ]
    [NormedAddCommGroup F] [NormedSpace ℝ F]
    [StandardBorelSpace γ] [Nonempty γ]
    {μ : Measure Ω} [IsFiniteMeasure μ] {X : Ω → β} {Y : Ω → γ}
    {f : β × γ → F}
    (hX : AEMeasurable X μ) (hY : AEMeasurable Y μ)
    (hf : AEStronglyMeasurable f (μ.map fun a => (X a, Y a))) :
    AEStronglyMeasurable
      (fun a => ∫ y, f (X a, y) ∂ProbabilityTheory.condDistrib Y X μ (X a))
      μ

theorem condDistribIntegralAEStronglyMeasurable {Ω β γ F : Type*}
    [MeasurableSpace Ω] [MeasurableSpace β] [MeasurableSpace γ]
    [NormedAddCommGroup F] [NormedSpace ℝ F]
    [StandardBorelSpace γ] [Nonempty γ]
    {μ : Measure Ω} [IsFiniteMeasure μ] {X : Ω → β} {Y : Ω → γ}
    {f : β × γ → F}
    (hX : AEMeasurable X μ) (hY : AEMeasurable Y μ)
    (hf : AEStronglyMeasurable f (μ.map fun a => (X a, Y a))) :
    AEStronglyMeasurable
      (fun a => ∫ y, f (X a, y) ∂ProbabilityTheory.condDistrib Y X μ (X a))
      μ := by
  exact hf.integral_condDistrib hX hY

/-- Integrability of a vector-valued conditional integral against
`condDistrib`.

For SALD this is the Mathlib-local handoff needed to turn integrable frozen
drift summands into integrable component conditional fields before the
existing `bar b_{k,s}` regularity wrappers are used.
-/

Scope and omitted-condition boundaries

• The selected conditional distribution is a probability kernel, characterized as a conditional law only almost everywhere under the conditioning marginal. No pointwise choice, simultaneous equality on all events from a single-event a.e. theorem, or null-fiber support is asserted.
• ∫ 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.
• No specified SALD component version, path law, or weak PDE is constructed.

The conditional integral is integrable on the sample space

AutoSamplingTheory.condDistribIntegralIntegrable · theorem · Teaching coverage

Statement

In the finite-measure conditional-distribution setting and notation below, assume Y is μ-a.e. measurable and X is μ-a.e. measurable. If f is integrable under the joint image measure λ, then C∘X is integrable under μ.

All objects and hypotheses

• Ω, β and γ are measurable spaces; γ is Standard Borel and nonempty.
• μ is a finite measure on Ω, not necessarily a probability; X:Ω→β and Y:Ω→γ are functions.
• F is a real normed vector space (NormedAddCommGroup and NormedSpace ℝ); no CompleteSpace assumption is added. The integrand f:β×γ→F is as specified below.
• Notation: λ=(ω↦(Xω,Yω))#μ, m=X#μ, q(x)=condDistrib(Y|X;μ)(x), and C(x)=∫f(x,y)dq(x)(y).
• Y is μ-a.e. measurable.
• X is μ-a.e. measurable.
• f is integrable under λ.

Notation and interpretation

Pushforward law

P is an arbitrary measure unless explicitly declared finite or a probability. The word law here abbreviates a pushforward measure; probability-language interpretations require normalization separately. Mathlib totalizes map to zero when X is not a.e. measurable; unqualified map-congruence and some law-space adapters intentionally retain that generality.

\[(X_\#\mu)(A)=\mu(X^{-1}A)\quad\text{when the measurable pushforward interpretation applies}\]

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\]

Conditional integral notation

The selected conditional distribution is a probability kernel, characterized as a conditional law only almost everywhere under the conditioning marginal. No pointwise choice, simultaneous equality on all events from a single-event a.e. theorem, or null-fiber support is asserted. Finite non-probability measures are reconstructed with their original total mass; any version changes on marginal-null inputs must retain a measurable kernel.

\[\lambda=(X,Y)_\#\mu,\quad m=X_\#\mu,\quad q(x)=\operatorname{condDistrib}(Y\mid X;\mu)(x),\quad C(x)=\int f(x,y)\,dq(x)(y)\]

Mathematical proof

theorem condDistribIntegralIntegrable {Ω β γ F : Type*}
    [MeasurableSpace Ω] [MeasurableSpace β] [MeasurableSpace γ]
    [NormedAddCommGroup F] [NormedSpace ℝ F]
    [StandardBorelSpace γ] [Nonempty γ]
    {μ : Measure Ω} [IsFiniteMeasure μ] {X : Ω → β} {Y : Ω → γ}
    {f : β × γ → F}
    (hX : AEMeasurable X μ) (hY : AEMeasurable Y μ)
    (hf : Integrable f (μ.map fun a => (X a, Y a))) :
    Integrable
      (fun a => ∫ y, f (X a, y) ∂ProbabilityTheory.condDistrib Y X μ (X a))
      μ

theorem condDistribIntegralIntegrable {Ω β γ F : Type*}
    [MeasurableSpace Ω] [MeasurableSpace β] [MeasurableSpace γ]
    [NormedAddCommGroup F] [NormedSpace ℝ F]
    [StandardBorelSpace γ] [Nonempty γ]
    {μ : Measure Ω} [IsFiniteMeasure μ] {X : Ω → β} {Y : Ω → γ}
    {f : β × γ → F}
    (hX : AEMeasurable X μ) (hY : AEMeasurable Y μ)
    (hf : Integrable f (μ.map fun a => (X a, Y a))) :
    Integrable
      (fun a => ∫ y, f (X a, y) ∂ProbabilityTheory.condDistrib Y X μ (X a))
      μ := by
  exact hf.integral_condDistrib hX hY

/-- Strong measurability of the state-space conditional integral under the
conditioning law `μ.map X`.

This is the law-space version needed for the SALD named `hat rho_s` field:
Mathlib's `condDistrib` backend already gives measurability of
`x ↦ ∫ y, f (x,y) ∂condDistrib Y X μ x` under the marginal law of the
conditioning variable.  It does not choose a SALD-specific version of the
conditional component field.
-/

Scope and omitted-condition boundaries

• The selected conditional distribution is a probability kernel, characterized as a conditional law only almost everywhere under the conditioning marginal. No pointwise choice, simultaneous equality on all events from a single-event a.e. theorem, or null-fiber support is asserted.
• ∫ 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.
• No specified SALD component version, path law, or weak PDE is constructed.

The conditional integral is almost-everywhere strongly measurable under the conditioning law

AutoSamplingTheory.condDistribIntegralMapAEStronglyMeasurable · theorem · Teaching coverage

Statement

In the finite-measure conditional-distribution setting and notation below, assume Y is μ-a.e. measurable. If f is almost-everywhere strongly measurable under the joint image measure λ, then C is almost-everywhere strongly measurable under m. No a.e. measurability assumption on X is required by this law-space adapter.

All objects and hypotheses

• Ω, β and γ are measurable spaces; γ is Standard Borel and nonempty.
• μ is a finite measure on Ω, not necessarily a probability; X:Ω→β and Y:Ω→γ are functions.
• F is a real normed vector space (NormedAddCommGroup and NormedSpace ℝ); no CompleteSpace assumption is added. The integrand f:β×γ→F is as specified below.
• Notation: λ=(ω↦(Xω,Yω))#μ, m=X#μ, q(x)=condDistrib(Y|X;μ)(x), and C(x)=∫f(x,y)dq(x)(y).
• Y is μ-a.e. measurable.
• f is almost-everywhere strongly measurable under λ.

Notation and interpretation

Pushforward law

P is an arbitrary measure unless explicitly declared finite or a probability. The word law here abbreviates a pushforward measure; probability-language interpretations require normalization separately. Mathlib totalizes map to zero when X is not a.e. measurable; unqualified map-congruence and some law-space adapters intentionally retain that generality.

\[(X_\#\mu)(A)=\mu(X^{-1}A)\quad\text{when the measurable pushforward interpretation applies}\]

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\]

Conditional integral notation

The selected conditional distribution is a probability kernel, characterized as a conditional law only almost everywhere under the conditioning marginal. No pointwise choice, simultaneous equality on all events from a single-event a.e. theorem, or null-fiber support is asserted. Finite non-probability measures are reconstructed with their original total mass; any version changes on marginal-null inputs must retain a measurable kernel.

\[\lambda=(X,Y)_\#\mu,\quad m=X_\#\mu,\quad q(x)=\operatorname{condDistrib}(Y\mid X;\mu)(x),\quad C(x)=\int f(x,y)\,dq(x)(y)\]

Mathematical proof

theorem condDistribIntegralMapAEStronglyMeasurable {Ω β γ F : Type*}
    [MeasurableSpace Ω] [MeasurableSpace β] [MeasurableSpace γ]
    [NormedAddCommGroup F] [NormedSpace ℝ F]
    [StandardBorelSpace γ] [Nonempty γ]
    {μ : Measure Ω} [IsFiniteMeasure μ] {X : Ω → β} {Y : Ω → γ}
    {f : β × γ → F}
    (hY : AEMeasurable Y μ)
    (hf : AEStronglyMeasurable f (μ.map fun a => (X a, Y a))) :
    AEStronglyMeasurable
      (fun x => ∫ y, f (x, y) ∂ProbabilityTheory.condDistrib Y X μ x)
      (μ.map X)

theorem condDistribIntegralMapAEStronglyMeasurable {Ω β γ F : Type*}
    [MeasurableSpace Ω] [MeasurableSpace β] [MeasurableSpace γ]
    [NormedAddCommGroup F] [NormedSpace ℝ F]
    [StandardBorelSpace γ] [Nonempty γ]
    {μ : Measure Ω} [IsFiniteMeasure μ] {X : Ω → β} {Y : Ω → γ}
    {f : β × γ → F}
    (hY : AEMeasurable Y μ)
    (hf : AEStronglyMeasurable f (μ.map fun a => (X a, Y a))) :
    AEStronglyMeasurable
      (fun x => ∫ y, f (x, y) ∂ProbabilityTheory.condDistrib Y X μ x)
      (μ.map X) := by
  exact hf.integral_condDistrib_map hY

/-- Integrability of the state-space conditional integral under the
conditioning law `μ.map X`.

For SALD this is the Mathlib-local input that turns an integrable frozen
drift or score summand on the joint law of `(hat X_s, X_k^eta)` into an
integrable canonical conditional field under `hat rho_s = Law(hat X_s)`.
-/

Scope and omitted-condition boundaries

• The selected conditional distribution is a probability kernel, characterized as a conditional law only almost everywhere under the conditioning marginal. No pointwise choice, simultaneous equality on all events from a single-event a.e. theorem, or null-fiber support is asserted.
• ∫ 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.
• X need not be a.e. measurable in this exact signature; without it, the displayed image measures retain Mathlib's totalized-map semantics.
• No specified SALD component version, path law, or weak PDE is constructed.

The conditional integral is integrable under the conditioning law

AutoSamplingTheory.condDistribIntegralMapIntegrable · theorem · Teaching coverage

Statement

In the finite-measure conditional-distribution setting and notation below, assume Y is μ-a.e. measurable. If f is integrable under the joint image measure λ, then C is integrable under m. No a.e. measurability assumption on X is required by this law-space adapter.

All objects and hypotheses

• Ω, β and γ are measurable spaces; γ is Standard Borel and nonempty.
• μ is a finite measure on Ω, not necessarily a probability; X:Ω→β and Y:Ω→γ are functions.
• F is a real normed vector space (NormedAddCommGroup and NormedSpace ℝ); no CompleteSpace assumption is added. The integrand f:β×γ→F is as specified below.
• Notation: λ=(ω↦(Xω,Yω))#μ, m=X#μ, q(x)=condDistrib(Y|X;μ)(x), and C(x)=∫f(x,y)dq(x)(y).
• Y is μ-a.e. measurable.
• f is integrable under λ.

Notation and interpretation

Pushforward law

P is an arbitrary measure unless explicitly declared finite or a probability. The word law here abbreviates a pushforward measure; probability-language interpretations require normalization separately. Mathlib totalizes map to zero when X is not a.e. measurable; unqualified map-congruence and some law-space adapters intentionally retain that generality.

\[(X_\#\mu)(A)=\mu(X^{-1}A)\quad\text{when the measurable pushforward interpretation applies}\]

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\]

Conditional integral notation

The selected conditional distribution is a probability kernel, characterized as a conditional law only almost everywhere under the conditioning marginal. No pointwise choice, simultaneous equality on all events from a single-event a.e. theorem, or null-fiber support is asserted. Finite non-probability measures are reconstructed with their original total mass; any version changes on marginal-null inputs must retain a measurable kernel.

\[\lambda=(X,Y)_\#\mu,\quad m=X_\#\mu,\quad q(x)=\operatorname{condDistrib}(Y\mid X;\mu)(x),\quad C(x)=\int f(x,y)\,dq(x)(y)\]

Mathematical proof

theorem condDistribIntegralMapIntegrable {Ω β γ F : Type*}
    [MeasurableSpace Ω] [MeasurableSpace β] [MeasurableSpace γ]
    [NormedAddCommGroup F] [NormedSpace ℝ F]
    [StandardBorelSpace γ] [Nonempty γ]
    {μ : Measure Ω} [IsFiniteMeasure μ] {X : Ω → β} {Y : Ω → γ}
    {f : β × γ → F}
    (hY : AEMeasurable Y μ)
    (hf : Integrable f (μ.map fun a => (X a, Y a))) :
    Integrable
      (fun x => ∫ y, f (x, y) ∂ProbabilityTheory.condDistrib Y X μ x)
      (μ.map X)

theorem condDistribIntegralMapIntegrable {Ω β γ F : Type*}
    [MeasurableSpace Ω] [MeasurableSpace β] [MeasurableSpace γ]
    [NormedAddCommGroup F] [NormedSpace ℝ F]
    [StandardBorelSpace γ] [Nonempty γ]
    {μ : Measure Ω} [IsFiniteMeasure μ] {X : Ω → β} {Y : Ω → γ}
    {f : β × γ → F}
    (hY : AEMeasurable Y μ)
    (hf : Integrable f (μ.map fun a => (X a, Y a))) :
    Integrable
      (fun x => ∫ y, f (x, y) ∂ProbabilityTheory.condDistrib Y X μ x)
      (μ.map X) := by
  exact hf.integral_condDistrib_map hY

/-- Disintegrate an integral through the `condDistrib` kernel.

For the SALD conditional drift in `appendix.tex:1368-1377`, instantiate `X`
with `hat X_s`, `Y` with `X_k^eta`, and `f` with the weak test-gradient
pairing against one frozen component.  This proves the map-law
conditional-integral identity behind the canonical `condDistrib` component
generator action; it does not prove the weak Fokker--Planck equation,
boundary integration by parts, or log-ratio admissibility.
-/

Scope and omitted-condition boundaries

• The selected conditional distribution is a probability kernel, characterized as a conditional law only almost everywhere under the conditioning marginal. No pointwise choice, simultaneous equality on all events from a single-event a.e. theorem, or null-fiber support is asserted.
• ∫ 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.
• X need not be a.e. measurable in this exact signature; without it, the displayed image measures retain Mathlib's totalized-map semantics.
• No specified SALD component version, path law, or weak PDE is constructed.

Integrating the conditional average recovers the joint integral

AutoSamplingTheory.condDistribIntegralMapIntegral · theorem · Teaching coverage

Statement

In the finite-measure conditional setting below, assume X and Y are μ-a.e. measurable and f is integrable under their joint image measure λ. Then integrating the conditional integral C(x) against the conditioning law m=X#μ equals integrating f(Xω,Yω) against μ. This is finite-measure disintegration, without probability normalization.

All objects and hypotheses

• Ω, β and γ are measurable spaces; γ is Standard Borel and nonempty.
• μ is a finite measure on Ω, not necessarily a probability; X:Ω→β and Y:Ω→γ are functions.
• F is a real normed vector space (NormedAddCommGroup and NormedSpace ℝ); no CompleteSpace assumption is added. The integrand f:β×γ→F is as specified below.
• Notation: λ=(ω↦(Xω,Yω))#μ, m=X#μ, q(x)=condDistrib(Y|X;μ)(x), and C(x)=∫f(x,y)dq(x)(y).
• X and Y are μ-a.e. measurable, and f is λ-integrable.

Notation and interpretation

Pushforward law

P is an arbitrary measure unless explicitly declared finite or a probability. The word law here abbreviates a pushforward measure; probability-language interpretations require normalization separately. Mathlib totalizes map to zero when X is not a.e. measurable; unqualified map-congruence and some law-space adapters intentionally retain that generality.

\[(X_\#\mu)(A)=\mu(X^{-1}A)\quad\text{when the measurable pushforward interpretation applies}\]

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\]

Conditional integral notation

The selected conditional distribution is a probability kernel, characterized as a conditional law only almost everywhere under the conditioning marginal. No pointwise choice, simultaneous equality on all events from a single-event a.e. theorem, or null-fiber support is asserted. Finite non-probability measures are reconstructed with their original total mass; any version changes on marginal-null inputs must retain a measurable kernel.

\[\lambda=(X,Y)_\#\mu,\quad m=X_\#\mu,\quad q(x)=\operatorname{condDistrib}(Y\mid X;\mu)(x),\quad C(x)=\int f(x,y)\,dq(x)(y)\]

Mathematical proof

theorem condDistribIntegralMapIntegral {Ω β γ F : Type*}
    [MeasurableSpace Ω] [MeasurableSpace β] [MeasurableSpace γ]
    [NormedAddCommGroup F] [NormedSpace ℝ F]
    [StandardBorelSpace γ] [Nonempty γ]
    {μ : Measure Ω} [IsFiniteMeasure μ] {X : Ω → β} {Y : Ω → γ}
    {f : β × γ → F}
    (hX : AEMeasurable X μ) (hY : AEMeasurable Y μ)
    (hf : Integrable f (μ.map fun a => (X a, Y a))) :
    (∫ x, ∫ y, f (x, y) ∂ProbabilityTheory.condDistrib Y X μ x
        ∂μ.map X) =
      ∫ a, f (X a, Y a) ∂μ

theorem condDistribIntegralMapIntegral {Ω β γ F : Type*}
    [MeasurableSpace Ω] [MeasurableSpace β] [MeasurableSpace γ]
    [NormedAddCommGroup F] [NormedSpace ℝ F]
    [StandardBorelSpace γ] [Nonempty γ]
    {μ : Measure Ω} [IsFiniteMeasure μ] {X : Ω → β} {Y : Ω → γ}
    {f : β × γ → F}
    (hX : AEMeasurable X μ) (hY : AEMeasurable Y μ)
    (hf : Integrable f (μ.map fun a => (X a, Y a))) :
    (∫ x, ∫ y, f (x, y) ∂ProbabilityTheory.condDistrib Y X μ x
        ∂μ.map X) =
      ∫ a, f (X a, Y a) ∂μ := by
  have hcomp := ProbabilityTheory.compProd_map_condDistrib
    (μ := μ) (X := X) (Y := Y) (mβ := inferInstance) hY
  have hfComp :
      Integrable f ((μ.map X) ⊗ₘ ProbabilityTheory.condDistrib Y X μ) := by
    rw [hcomp]
    exact hf
  calc
    (∫ x, ∫ y, f (x, y) ∂ProbabilityTheory.condDistrib Y X μ x
        ∂μ.map X)
        = ∫ z, f z ∂((μ.map X) ⊗ₘ
            ProbabilityTheory.condDistrib Y X μ) := by
          exact (Measure.integral_compProd
            (μ := μ.map X) (κ := ProbabilityTheory.condDistrib Y X μ)
            hfComp).symm
    _ = ∫ a, f (X a, Y a) ∂μ := by
          rw [hcomp]
          rw [integral_map (hX.prodMk hY) hf.1]

/-- Named-law variant of `condDistribIntegralMapIntegral`.

This is the paper-oriented form for `\hat\rho_s = Law(\hat X_s)`.
-/

Scope and omitted-condition boundaries

• The selected conditional distribution is a probability kernel, characterized as a conditional law only almost everywhere under the conditioning marginal. No pointwise choice, simultaneous equality on all events from a single-event a.e. theorem, or null-fiber support is asserted.
• ∫ 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.
• For probability μ this is a two-stage expectation identity. For general finite μ, q(x) has mass one but the outer measure m has total mass μ(Ω); the reconstruction preserves that mass.
• No integration by parts, admissible log-ratio test or Fokker–Planck theorem.

Disintegration written with a named conditioning law

AutoSamplingTheory.condDistribIntegralNamedLawIntegral · theorem · Teaching coverage

Statement

In the finite-measure conditional setting below, let ρ̂ be a measure on β with ρ̂=X#μ. Assume Y is μ-a.e. measurable and X is μ-a.e. measurable, and f is integrable under λ. Then the averaged conditional integral equals the joint sample integral. This only replaces the mapped measure by an equal named measure.

All objects and hypotheses

• Ω, β and γ are measurable spaces; γ is Standard Borel and nonempty.
• μ is a finite measure on Ω, not necessarily a probability; X:Ω→β and Y:Ω→γ are functions.
• F is a real normed vector space (NormedAddCommGroup and NormedSpace ℝ); no CompleteSpace assumption is added. The integrand f:β×γ→F is as specified below.
• Notation: λ=(ω↦(Xω,Yω))#μ, m=X#μ, q(x)=condDistrib(Y|X;μ)(x), and C(x)=∫f(x,y)dq(x)(y).
• ρ̂ is a measure on β and hhatRho gives ρ̂=X#μ.
• Y is μ-a.e. measurable.
• X is μ-a.e. measurable.
• f is integrable under λ.

Notation and interpretation

Pushforward law

P is an arbitrary measure unless explicitly declared finite or a probability. The word law here abbreviates a pushforward measure; probability-language interpretations require normalization separately. Mathlib totalizes map to zero when X is not a.e. measurable; unqualified map-congruence and some law-space adapters intentionally retain that generality.

\[(X_\#\mu)(A)=\mu(X^{-1}A)\quad\text{when the measurable pushforward interpretation applies}\]

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\]

Conditional integral notation

The selected conditional distribution is a probability kernel, characterized as a conditional law only almost everywhere under the conditioning marginal. No pointwise choice, simultaneous equality on all events from a single-event a.e. theorem, or null-fiber support is asserted. Finite non-probability measures are reconstructed with their original total mass; any version changes on marginal-null inputs must retain a measurable kernel.

\[\lambda=(X,Y)_\#\mu,\quad m=X_\#\mu,\quad q(x)=\operatorname{condDistrib}(Y\mid X;\mu)(x),\quad C(x)=\int f(x,y)\,dq(x)(y)\]

Mathematical proof

theorem condDistribIntegralNamedLawIntegral {Ω β γ F : Type*}
    [MeasurableSpace Ω] [MeasurableSpace β] [MeasurableSpace γ]
    [NormedAddCommGroup F] [NormedSpace ℝ F]
    [StandardBorelSpace γ] [Nonempty γ]
    {μ : Measure Ω} [IsFiniteMeasure μ] {hatRho : Measure β}
    {X : Ω → β} {Y : Ω → γ} {f : β × γ → F}
    (hhatRho : hatRho = μ.map X)
    (hX : AEMeasurable X μ) (hY : AEMeasurable Y μ)
    (hf : Integrable f (μ.map fun a => (X a, Y a))) :
    (∫ x, ∫ y, f (x, y) ∂ProbabilityTheory.condDistrib Y X μ x
        ∂hatRho) =
      ∫ a, f (X a, Y a) ∂μ

theorem condDistribIntegralNamedLawIntegral {Ω β γ F : Type*}
    [MeasurableSpace Ω] [MeasurableSpace β] [MeasurableSpace γ]
    [NormedAddCommGroup F] [NormedSpace ℝ F]
    [StandardBorelSpace γ] [Nonempty γ]
    {μ : Measure Ω} [IsFiniteMeasure μ] {hatRho : Measure β}
    {X : Ω → β} {Y : Ω → γ} {f : β × γ → F}
    (hhatRho : hatRho = μ.map X)
    (hX : AEMeasurable X μ) (hY : AEMeasurable Y μ)
    (hf : Integrable f (μ.map fun a => (X a, Y a))) :
    (∫ x, ∫ y, f (x, y) ∂ProbabilityTheory.condDistrib Y X μ x
        ∂hatRho) =
      ∫ a, f (X a, Y a) ∂μ := by
  rw [hhatRho]
  exact condDistribIntegralMapIntegral hX hY hf

/-- Named-law variant of `condDistribIntegralMapAEStronglyMeasurable`.

Instantiate `hatRho` with `Law(hat X_s)`, `X` with `hat X_s`, and `Y` with
`X_k^eta`.  The hypothesis `hatRho = μ.map X` is the paper's
`\hat\rho_s = Law(\hat X_s)` line.
-/

Scope and omitted-condition boundaries

• The selected conditional distribution is a probability kernel, characterized as a conditional law only almost everywhere under the conditioning marginal. No pointwise choice, simultaneous equality on all events from a single-event a.e. theorem, or null-fiber support is asserted.
• ∫ 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.
• Reuse wrapper, not a separate proof of disintegration.

A.e. strong measurability under a named conditioning law

AutoSamplingTheory.condDistribIntegralNamedLawAEStronglyMeasurable · theorem · Teaching coverage

Statement

In the finite-measure conditional setting below, let ρ̂ be a measure on β with ρ̂=X#μ. Assume Y is μ-a.e. measurable, and f is a.e. strongly measurable under λ. Then C is ρ̂-a.e. strongly measurable. This only replaces the mapped measure by an equal named measure.

All objects and hypotheses

• Ω, β and γ are measurable spaces; γ is Standard Borel and nonempty.
• μ is a finite measure on Ω, not necessarily a probability; X:Ω→β and Y:Ω→γ are functions.
• F is a real normed vector space (NormedAddCommGroup and NormedSpace ℝ); no CompleteSpace assumption is added. The integrand f:β×γ→F is as specified below.
• Notation: λ=(ω↦(Xω,Yω))#μ, m=X#μ, q(x)=condDistrib(Y|X;μ)(x), and C(x)=∫f(x,y)dq(x)(y).
• ρ̂ is a measure on β and hhatRho gives ρ̂=X#μ.
• Y is μ-a.e. measurable.
• f is a.e. strongly measurable under λ.

Notation and interpretation

Pushforward law

P is an arbitrary measure unless explicitly declared finite or a probability. The word law here abbreviates a pushforward measure; probability-language interpretations require normalization separately. Mathlib totalizes map to zero when X is not a.e. measurable; unqualified map-congruence and some law-space adapters intentionally retain that generality.

\[(X_\#\mu)(A)=\mu(X^{-1}A)\quad\text{when the measurable pushforward interpretation applies}\]

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\]

Conditional integral notation

The selected conditional distribution is a probability kernel, characterized as a conditional law only almost everywhere under the conditioning marginal. No pointwise choice, simultaneous equality on all events from a single-event a.e. theorem, or null-fiber support is asserted. Finite non-probability measures are reconstructed with their original total mass; any version changes on marginal-null inputs must retain a measurable kernel.

\[\lambda=(X,Y)_\#\mu,\quad m=X_\#\mu,\quad q(x)=\operatorname{condDistrib}(Y\mid X;\mu)(x),\quad C(x)=\int f(x,y)\,dq(x)(y)\]

Mathematical proof

theorem condDistribIntegralNamedLawAEStronglyMeasurable {Ω β γ F : Type*}
    [MeasurableSpace Ω] [MeasurableSpace β] [MeasurableSpace γ]
    [NormedAddCommGroup F] [NormedSpace ℝ F]
    [StandardBorelSpace γ] [Nonempty γ]
    {μ : Measure Ω} [IsFiniteMeasure μ] {hatRho : Measure β}
    {X : Ω → β} {Y : Ω → γ} {f : β × γ → F}
    (hhatRho : hatRho = μ.map X)
    (hY : AEMeasurable Y μ)
    (hf : AEStronglyMeasurable f (μ.map fun a => (X a, Y a))) :
    AEStronglyMeasurable
      (fun x => ∫ y, f (x, y) ∂ProbabilityTheory.condDistrib Y X μ x)
      hatRho

theorem condDistribIntegralNamedLawAEStronglyMeasurable {Ω β γ F : Type*}
    [MeasurableSpace Ω] [MeasurableSpace β] [MeasurableSpace γ]
    [NormedAddCommGroup F] [NormedSpace ℝ F]
    [StandardBorelSpace γ] [Nonempty γ]
    {μ : Measure Ω} [IsFiniteMeasure μ] {hatRho : Measure β}
    {X : Ω → β} {Y : Ω → γ} {f : β × γ → F}
    (hhatRho : hatRho = μ.map X)
    (hY : AEMeasurable Y μ)
    (hf : AEStronglyMeasurable f (μ.map fun a => (X a, Y a))) :
    AEStronglyMeasurable
      (fun x => ∫ y, f (x, y) ∂ProbabilityTheory.condDistrib Y X μ x)
      hatRho := by
  rw [hhatRho]
  exact condDistribIntegralMapAEStronglyMeasurable hY hf

/-- Named-law variant of `condDistribIntegralMapIntegrable`. -/

Scope and omitted-condition boundaries

• The selected conditional distribution is a probability kernel, characterized as a conditional law only almost everywhere under the conditioning marginal. No pointwise choice, simultaneous equality on all events from a single-event a.e. theorem, or null-fiber support is asserted.
• ∫ 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.
• No AEMeasurable X assumption appears in this named regularity theorem; retain the totalized-map boundary.
• Reuse wrapper, not a separate proof of disintegration.

Integrability under a named conditioning law

AutoSamplingTheory.condDistribIntegralNamedLawIntegrable · theorem · Teaching coverage

Statement

In the finite-measure conditional setting below, let ρ̂ be a measure on β with ρ̂=X#μ. Assume Y is μ-a.e. measurable, and f is integrable under λ. Then C is integrable under the named law ρ̂. This only replaces the mapped measure by an equal named measure.

All objects and hypotheses

• Ω, β and γ are measurable spaces; γ is Standard Borel and nonempty.
• μ is a finite measure on Ω, not necessarily a probability; X:Ω→β and Y:Ω→γ are functions.
• F is a real normed vector space (NormedAddCommGroup and NormedSpace ℝ); no CompleteSpace assumption is added. The integrand f:β×γ→F is as specified below.
• Notation: λ=(ω↦(Xω,Yω))#μ, m=X#μ, q(x)=condDistrib(Y|X;μ)(x), and C(x)=∫f(x,y)dq(x)(y).
• ρ̂ is a measure on β and hhatRho gives ρ̂=X#μ.
• Y is μ-a.e. measurable.
• f is integrable under λ.

Notation and interpretation

Pushforward law

P is an arbitrary measure unless explicitly declared finite or a probability. The word law here abbreviates a pushforward measure; probability-language interpretations require normalization separately. Mathlib totalizes map to zero when X is not a.e. measurable; unqualified map-congruence and some law-space adapters intentionally retain that generality.

\[(X_\#\mu)(A)=\mu(X^{-1}A)\quad\text{when the measurable pushforward interpretation applies}\]

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\]

Conditional integral notation

The selected conditional distribution is a probability kernel, characterized as a conditional law only almost everywhere under the conditioning marginal. No pointwise choice, simultaneous equality on all events from a single-event a.e. theorem, or null-fiber support is asserted. Finite non-probability measures are reconstructed with their original total mass; any version changes on marginal-null inputs must retain a measurable kernel.

\[\lambda=(X,Y)_\#\mu,\quad m=X_\#\mu,\quad q(x)=\operatorname{condDistrib}(Y\mid X;\mu)(x),\quad C(x)=\int f(x,y)\,dq(x)(y)\]

Mathematical proof

theorem condDistribIntegralNamedLawIntegrable {Ω β γ F : Type*}
    [MeasurableSpace Ω] [MeasurableSpace β] [MeasurableSpace γ]
    [NormedAddCommGroup F] [NormedSpace ℝ F]
    [StandardBorelSpace γ] [Nonempty γ]
    {μ : Measure Ω} [IsFiniteMeasure μ] {hatRho : Measure β}
    {X : Ω → β} {Y : Ω → γ} {f : β × γ → F}
    (hhatRho : hatRho = μ.map X)
    (hY : AEMeasurable Y μ)
    (hf : Integrable f (μ.map fun a => (X a, Y a))) :
    Integrable
      (fun x => ∫ y, f (x, y) ∂ProbabilityTheory.condDistrib Y X μ x)
      hatRho

theorem condDistribIntegralNamedLawIntegrable {Ω β γ F : Type*}
    [MeasurableSpace Ω] [MeasurableSpace β] [MeasurableSpace γ]
    [NormedAddCommGroup F] [NormedSpace ℝ F]
    [StandardBorelSpace γ] [Nonempty γ]
    {μ : Measure Ω} [IsFiniteMeasure μ] {hatRho : Measure β}
    {X : Ω → β} {Y : Ω → γ} {f : β × γ → F}
    (hhatRho : hatRho = μ.map X)
    (hY : AEMeasurable Y μ)
    (hf : Integrable f (μ.map fun a => (X a, Y a))) :
    Integrable
      (fun x => ∫ y, f (x, y) ∂ProbabilityTheory.condDistrib Y X μ x)
      hatRho := by
  rw [hhatRho]
  exact condDistribIntegralMapIntegrable hY hf

/-- Versioning theorem for a named conditional-integral component field.

If a SALD component field such as `condC_{k,s}` or `condScore_{k,s}` is chosen
as a `hatRho`-a.e. version of the canonical `condDistrib` integral, then the
Mathlib law-space conditional-integral lemmas give the component's
measurability and integrability under the named law.  This is still a
conditional-kernel component theorem, not a weak Fokker--Planck theorem.
-/

Scope and omitted-condition boundaries

• The selected conditional distribution is a probability kernel, characterized as a conditional law only almost everywhere under the conditioning marginal. No pointwise choice, simultaneous equality on all events from a single-event a.e. theorem, or null-fiber support is asserted.
• ∫ 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.
• No AEMeasurable X assumption appears in this named regularity theorem; retain the totalized-map boundary.
• Reuse wrapper, not a separate proof of disintegration.

A chosen a.e. version inherits conditional-integral regularity

AutoSamplingTheory.condDistribIntegralNamedFieldRegularity · theorem · Teaching coverage

Statement

In the conditional setting below, let ρ̂=X#μ and v:β→F be a chosen field equal to C ρ̂-almost everywhere. If Y is μ-a.e. measurable and f is both a.e. strongly measurable and integrable under λ, then v is a.e. strongly measurable and integrable under ρ̂.

All objects and hypotheses

• Ω, β and γ are measurable spaces; γ is Standard Borel and nonempty.
• μ is a finite measure on Ω, not necessarily a probability; X:Ω→β and Y:Ω→γ are functions.
• F is a real normed vector space (NormedAddCommGroup and NormedSpace ℝ); no CompleteSpace assumption is added. The integrand f:β×γ→F is as specified below.
• Notation: λ=(ω↦(Xω,Yω))#μ, m=X#μ, q(x)=condDistrib(Y|X;μ)(x), and C(x)=∫f(x,y)dq(x)(y).
• ρ̂ is a measure on β equal to X#μ, and v:β→F is a chosen field.
• Y is μ-a.e. measurable; hfMeas explicitly supplies AEStronglyMeasurable f λ and hfInt explicitly supplies Integrable f λ (both premises are retained).
• hfield supplies C=v ρ̂-a.e.; X a.e. measurability is not separately required.

Notation and interpretation

Pushforward law

P is an arbitrary measure unless explicitly declared finite or a probability. The word law here abbreviates a pushforward measure; probability-language interpretations require normalization separately. Mathlib totalizes map to zero when X is not a.e. measurable; unqualified map-congruence and some law-space adapters intentionally retain that generality.

\[(X_\#\mu)(A)=\mu(X^{-1}A)\quad\text{when the measurable pushforward interpretation applies}\]

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\]

Conditional integral notation

The selected conditional distribution is a probability kernel, characterized as a conditional law only almost everywhere under the conditioning marginal. No pointwise choice, simultaneous equality on all events from a single-event a.e. theorem, or null-fiber support is asserted. Finite non-probability measures are reconstructed with their original total mass; any version changes on marginal-null inputs must retain a measurable kernel.

\[\lambda=(X,Y)_\#\mu,\quad m=X_\#\mu,\quad q(x)=\operatorname{condDistrib}(Y\mid X;\mu)(x),\quad C(x)=\int f(x,y)\,dq(x)(y)\]

Mathematical proof

theorem condDistribIntegralNamedFieldRegularity {Ω β γ F : Type*}
    [MeasurableSpace Ω] [MeasurableSpace β] [MeasurableSpace γ]
    [NormedAddCommGroup F] [NormedSpace ℝ F]
    [StandardBorelSpace γ] [Nonempty γ]
    {μ : Measure Ω} [IsFiniteMeasure μ] {hatRho : Measure β}
    {X : Ω → β} {Y : Ω → γ} {f : β × γ → F} {field : β → F}
    (hhatRho : hatRho = μ.map X)
    (hY : AEMeasurable Y μ)
    (hfMeas : AEStronglyMeasurable f (μ.map fun a => (X a, Y a)))
    (hfInt : Integrable f (μ.map fun a => (X a, Y a)))
    (hfield :
      (fun x => ∫ y, f (x, y) ∂ProbabilityTheory.condDistrib Y X μ x)
        =ᵐ[hatRho] field) :
    AEStronglyMeasurable field hatRho ∧ Integrable field hatRho

theorem condDistribIntegralNamedFieldRegularity {Ω β γ F : Type*}
    [MeasurableSpace Ω] [MeasurableSpace β] [MeasurableSpace γ]
    [NormedAddCommGroup F] [NormedSpace ℝ F]
    [StandardBorelSpace γ] [Nonempty γ]
    {μ : Measure Ω} [IsFiniteMeasure μ] {hatRho : Measure β}
    {X : Ω → β} {Y : Ω → γ} {f : β × γ → F} {field : β → F}
    (hhatRho : hatRho = μ.map X)
    (hY : AEMeasurable Y μ)
    (hfMeas : AEStronglyMeasurable f (μ.map fun a => (X a, Y a)))
    (hfInt : Integrable f (μ.map fun a => (X a, Y a)))
    (hfield :
      (fun x => ∫ y, f (x, y) ∂ProbabilityTheory.condDistrib Y X μ x)
        =ᵐ[hatRho] field) :
    AEStronglyMeasurable field hatRho ∧ Integrable field hatRho := by
  have hmeas :
      AEStronglyMeasurable
        (fun x => ∫ y, f (x, y) ∂ProbabilityTheory.condDistrib Y X μ x)
        hatRho :=
    condDistribIntegralNamedLawAEStronglyMeasurable hhatRho hY hfMeas
  have hint :
      Integrable
        (fun x => ∫ y, f (x, y) ∂ProbabilityTheory.condDistrib Y X μ x)
        hatRho :=
    condDistribIntegralNamedLawIntegrable hhatRho hY hfInt
  exact ⟨hmeas.congr hfield, hint.congr hfield⟩

/-- A named probability measure or time-indexed law in a paper proof. -/

Scope and omitted-condition boundaries

• The selected conditional distribution is a probability kernel, characterized as a conditional law only almost everywhere under the conditioning marginal. No pointwise choice, simultaneous equality on all events from a single-event a.e. theorem, or null-fiber support is asserted.
• ∫ 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.
• Does not choose v or prove its version equality. Both explicit regularity premises remain in the source signature. No whole-PDE regularity follows.

Record the name and provenance of a measure

AutoSamplingTheory.MeasureContract · structure · Teaching coverage

Statement

This record stores descriptions of a named measure, its state space, optional density and smoothness labels, and its source. It contains no actual Measure value and no evidence that a density or regularity property exists.

All objects and hypotheses

• name has type String: required label of the measure or law.
• stateSpace has type String: required description of its state space.
• densityName has type String: optional density label, default empty string.
• smoothness has type String: optional regularity description, default empty string.
• source has type SourceAnchor: required provenance record.
• No ambient measurable space, measure, analytic hypothesis or proof witness is a parameter of this metadata structure. Default fields may be overridden when constructing a record.

Notation and interpretation

Analytic values versus metadata

Contracts and obligation/interface constructors store strings and status labels. They are not propositions asserting the written mathematics and supply no Lean proof of it.

\[\texttt{ProofObligation}\ne\text{proof of its statement string}\]

Construction and meaning

structure MeasureContract where
  name : String
  stateSpace : String
  densityName : String := ""
  smoothness : String := ""
  source : SourceAnchor
deriving Repr, DecidableEq

/-- Forward KL divergence contract `KL(rho || pi)`. -/

structure MeasureContract where
  name : String
  stateSpace : String
  densityName : String := ""
  smoothness : String := ""
  source : SourceAnchor
deriving Repr, DecidableEq

/-- Forward KL divergence contract `KL(rho || pi)`. -/

Scope and omitted-condition boundaries

• Contracts and obligation/interface constructors store strings and status labels. They are not propositions asserting the written mathematics and supply no Lean proof of it.
• Measure and regularity labels remain text; a record can describe an unproved object.

Record a forward-KL expression and its status

AutoSamplingTheory.KLContract · structure · Teaching coverage

Statement

This record stores labels for rho and pi, a written forward-KL expression, source provenance and a status defaulting to contractOnly. It does not define KL as an analytic functional or prove the expression correct.

All objects and hypotheses

• rho has type String: first measure label.
• pi has type String: reference-measure label.
• expression has type String: written KL expression.
• source has type SourceAnchor: provenance.
• status has type ProofStatus: default contractOnly.
• No ambient measurable space, measure, analytic hypothesis or proof witness is a parameter of this metadata structure. Default fields may be overridden when constructing a record.

Notation and interpretation

Analytic values versus metadata

Contracts and obligation/interface constructors store strings and status labels. They are not propositions asserting the written mathematics and supply no Lean proof of it.

\[\texttt{ProofObligation}\ne\text{proof of its statement string}\]

Construction and meaning

structure KLContract where
  rho : String
  pi : String
  expression : String
  source : SourceAnchor
  status : ProofStatus := ProofStatus.contractOnly
deriving Repr, DecidableEq

/-- Fisher information contract `FI(rho || pi)`. -/

structure KLContract where
  rho : String
  pi : String
  expression : String
  source : SourceAnchor
  status : ProofStatus := ProofStatus.contractOnly
deriving Repr, DecidableEq

/-- Fisher information contract `FI(rho || pi)`. -/

Scope and omitted-condition boundaries

• Contracts and obligation/interface constructors store strings and status labels. They are not propositions asserting the written mathematics and supply no Lean proof of it.
• The order rho, pi records forward KL notation but supplies no absolute continuity, finite entropy or nonnegativity proof.

Record a Fisher-information expression and its status

AutoSamplingTheory.FIContract · structure · Teaching coverage

Statement

This record stores labels for the two measures, a Fisher-information expression, source provenance and a status defaulting to contractOnly. It contains no gradient, density or integrability witness.

All objects and hypotheses

• rho has type String: first measure label.
• pi has type String: reference-measure label.
• expression has type String: written Fisher-information expression.
• source has type SourceAnchor: provenance.
• status has type ProofStatus: default contractOnly.
• No ambient measurable space, measure, analytic hypothesis or proof witness is a parameter of this metadata structure. Default fields may be overridden when constructing a record.

Notation and interpretation

Analytic values versus metadata

Contracts and obligation/interface constructors store strings and status labels. They are not propositions asserting the written mathematics and supply no Lean proof of it.

\[\texttt{ProofObligation}\ne\text{proof of its statement string}\]

Construction and meaning

structure FIContract where
  rho : String
  pi : String
  expression : String
  source : SourceAnchor
  status : ProofStatus := ProofStatus.contractOnly
deriving Repr, DecidableEq

/-- Log-Sobolev inequality contract. -/

structure FIContract where
  rho : String
  pi : String
  expression : String
  source : SourceAnchor
  status : ProofStatus := ProofStatus.contractOnly
deriving Repr, DecidableEq

/-- Log-Sobolev inequality contract. -/

Scope and omitted-condition boundaries

• Contracts and obligation/interface constructors store strings and status labels. They are not propositions asserting the written mathematics and supply no Lean proof of it.
• Writing a Fisher-information expression does not establish differentiability, Sobolev regularity or finiteness.

Record a log-Sobolev inequality as an obligation

AutoSamplingTheory.LSIContract · structure · Teaching coverage

Statement

This record stores a measure label, a constant label, an inequality written as text, its source, and a status defaulting to obligation. No log-Sobolev inequality is asserted as a proposition by this structure.

All objects and hypotheses

• measureName has type String: measure label.
• constantName has type String: inequality-constant label.
• statement has type String: written inequality.
• source has type SourceAnchor: provenance.
• status has type ProofStatus: default obligation.
• No ambient measurable space, measure, analytic hypothesis or proof witness is a parameter of this metadata structure. Default fields may be overridden when constructing a record.

Notation and interpretation

Analytic values versus metadata

Contracts and obligation/interface constructors store strings and status labels. They are not propositions asserting the written mathematics and supply no Lean proof of it.

\[\texttt{ProofObligation}\ne\text{proof of its statement string}\]

Construction and meaning

structure LSIContract where
  measureName : String
  constantName : String
  statement : String
  source : SourceAnchor
  status : ProofStatus := ProofStatus.obligation
deriving Repr, DecidableEq

/-- Poincare inequality contract. -/

structure LSIContract where
  measureName : String
  constantName : String
  statement : String
  source : SourceAnchor
  status : ProofStatus := ProofStatus.obligation
deriving Repr, DecidableEq

/-- Poincare inequality contract. -/

Scope and omitted-condition boundaries

• Contracts and obligation/interface constructors store strings and status labels. They are not propositions asserting the written mathematics and supply no Lean proof of it.
• No constant convention, positivity, admissible test class or validity of LSI is enforced by string fields.

Record a Poincaré inequality as an obligation

AutoSamplingTheory.PIContract · structure · Teaching coverage

Statement

This record stores labels and text for a Poincaré inequality with provenance and a default obligation status. It is metadata rather than a proof of the inequality.

All objects and hypotheses

• measureName has type String: measure label.
• constantName has type String: inequality-constant label.
• statement has type String: written inequality.
• source has type SourceAnchor: provenance.
• status has type ProofStatus: default obligation.
• No ambient measurable space, measure, analytic hypothesis or proof witness is a parameter of this metadata structure. Default fields may be overridden when constructing a record.

Notation and interpretation

Analytic values versus metadata

Contracts and obligation/interface constructors store strings and status labels. They are not propositions asserting the written mathematics and supply no Lean proof of it.

\[\texttt{ProofObligation}\ne\text{proof of its statement string}\]

Construction and meaning

structure PIContract where
  measureName : String
  constantName : String
  statement : String
  source : SourceAnchor
  status : ProofStatus := ProofStatus.obligation
deriving Repr, DecidableEq

/-- Transport velocity field satisfying a continuity equation. -/

structure PIContract where
  measureName : String
  constantName : String
  statement : String
  source : SourceAnchor
  status : ProofStatus := ProofStatus.obligation
deriving Repr, DecidableEq

/-- Transport velocity field satisfying a continuity equation. -/

Scope and omitted-condition boundaries

• Contracts and obligation/interface constructors store strings and status labels. They are not propositions asserting the written mathematics and supply no Lean proof of it.
• The structure does not assert a spectral gap, compare Poincaré and LSI constants, or impose a function domain.

Record a proposed continuity-equation velocity

AutoSamplingTheory.TransportVelocityContract · structure · Teaching coverage

Statement

This record stores a named measure path, a named velocity field, a continuity equation written as text, provenance and a default contractOnly status. It contains no analytic path or velocity value.

All objects and hypotheses

• pathName has type String: measure-path label.
• velocityName has type String: velocity-field label.
• continuityEquation has type String: written continuity equation.
• source has type SourceAnchor: provenance.
• status has type ProofStatus: default contractOnly.
• No ambient measurable space, measure, analytic hypothesis or proof witness is a parameter of this metadata structure. Default fields may be overridden when constructing a record.

Notation and interpretation

Analytic values versus metadata

Contracts and obligation/interface constructors store strings and status labels. They are not propositions asserting the written mathematics and supply no Lean proof of it.

\[\texttt{ProofObligation}\ne\text{proof of its statement string}\]

Construction and meaning

structure TransportVelocityContract where
  pathName : String
  velocityName : String
  continuityEquation : String
  source : SourceAnchor
  status : ProofStatus := ProofStatus.contractOnly
deriving Repr, DecidableEq

/-- Guide tilt `pi_t proportional to p_t exp(-F_t)`. -/

structure TransportVelocityContract where
  pathName : String
  velocityName : String
  continuityEquation : String
  source : SourceAnchor
  status : ProofStatus := ProofStatus.contractOnly
deriving Repr, DecidableEq

/-- Guide tilt `pi_t proportional to p_t exp(-F_t)`. -/

Scope and omitted-condition boundaries

• Contracts and obligation/interface constructors store strings and status labels. They are not propositions asserting the written mathematics and supply no Lean proof of it.
• A stored continuity equation does not prove weak differentiability, divergence regularity, boundary behavior or a transport identity.

Record the intended labels of a guided tilt

AutoSamplingTheory.GuidedTiltContract · structure · Teaching coverage

Statement

This record stores names for a base path, guide, guided path and terminal target together with a source and default contractOnly status. The intended exponentially tilted relationship is descriptive, not an enforced measure equality.

All objects and hypotheses

• basePath has type String: base-path label.
• guideName has type String: guide label.
• guidedPath has type String: tilted-path label.
• terminalTarget has type String: terminal target label.
• source has type SourceAnchor: provenance.
• status has type ProofStatus: default contractOnly.
• No ambient measurable space, measure, analytic hypothesis or proof witness is a parameter of this metadata structure. Default fields may be overridden when constructing a record.

Notation and interpretation

Analytic values versus metadata

Contracts and obligation/interface constructors store strings and status labels. They are not propositions asserting the written mathematics and supply no Lean proof of it.

\[\texttt{ProofObligation}\ne\text{proof of its statement string}\]

Construction and meaning

structure GuidedTiltContract where
  basePath : String
  guideName : String
  guidedPath : String
  terminalTarget : String
  source : SourceAnchor
  status : ProofStatus := ProofStatus.contractOnly
deriving Repr, DecidableEq

/-- Source-cited interface for the Donsker--Varadhan entropy duality formula.

This is data, not a proof.  It records the exact analytic shape needed by the
SALD paper before theorem-specific finite-log-mgf witnesses instantiate it.
-/

structure GuidedTiltContract where
  basePath : String
  guideName : String
  guidedPath : String
  terminalTarget : String
  source : SourceAnchor
  status : ProofStatus := ProofStatus.contractOnly
deriving Repr, DecidableEq

/-- Source-cited interface for the Donsker--Varadhan entropy duality formula.

This is data, not a proof.  It records the exact analytic shape needed by the
SALD paper before theorem-specific finite-log-mgf witnesses instantiate it.
-/

Scope and omitted-condition boundaries

• Contracts and obligation/interface constructors store strings and status labels. They are not propositions asserting the written mathematics and supply no Lean proof of it.
• It proves neither finite normalizer nor target correctness and does not construct the tilted law.

Record the cited entropy-duality interface

AutoSamplingTheory.DvVariationalFormulaInterface · structure · Teaching coverage

Statement

This record packages text describing the Donsker–Varadhan variational formula, its intended hypotheses, selected tests, scalar bridges and citation. Status defaults to sourceCited. Every analytic slot is text, not a Lean hypothesis or proved equality.

All objects and hypotheses

• source has type SourceAnchor: provenance.
• probabilityMeasures has type String: described measure assumptions.
• klFunctional has type String: KL expression.
• testFunctionClass has type String: described test class.
• finiteLogMgfPredicate has type String: described admissibility predicate.
• logMgfFunctional has type String: log moment-generating-functional description.
• variationalFunctional has type String: variational-test value description.
• supremumStatement has type String: written supremum identity.
• oneSidedConsequence has type String: written test-wise consequence.
• oneSidedScalarBridge has type String: description of available bridge declarations.
• citation has type String: citation text.
• status has type ProofStatus: default sourceCited.
• No ambient measurable space, measure, analytic hypothesis or proof witness is a parameter of this metadata structure. Default fields may be overridden when constructing a record.

Notation and interpretation

Analytic values versus metadata

Contracts and obligation/interface constructors store strings and status labels. They are not propositions asserting the written mathematics and supply no Lean proof of it.

\[\texttt{ProofObligation}\ne\text{proof of its statement string}\]

Construction and meaning

structure DvVariationalFormulaInterface where
  source : SourceAnchor
  probabilityMeasures : String
  klFunctional : String
  testFunctionClass : String
  finiteLogMgfPredicate : String
  logMgfFunctional : String
  variationalFunctional : String
  supremumStatement : String
  oneSidedConsequence : String
  oneSidedScalarBridge : String
  citation : String
  status : ProofStatus := ProofStatus.sourceCited
deriving Repr, DecidableEq

/-- Donsker--Varadhan variational formula as a cited-result contract. -/

structure DvVariationalFormulaInterface where
  source : SourceAnchor
  probabilityMeasures : String
  klFunctional : String
  testFunctionClass : String
  finiteLogMgfPredicate : String
  logMgfFunctional : String
  variationalFunctional : String
  supremumStatement : String
  oneSidedConsequence : String
  oneSidedScalarBridge : String
  citation : String
  status : ProofStatus := ProofStatus.sourceCited
deriving Repr, DecidableEq

/-- Donsker--Varadhan variational formula as a cited-result contract. -/

Scope and omitted-condition boundaries

• Contracts and obligation/interface constructors store strings and status labels. They are not propositions asserting the written mathematics and supply no Lean proof of it.
• No admissibility predicate, supremum functional or theorem is enforced by this data schema; even sourceCited is a metadata label, not certification.

Construct a source-cited DV proof-obligation record

AutoSamplingTheory.dvVariationalObligation · def · Teaching coverage

Statement

Given any source anchor, construct a ProofObligation with id probability.dv_variational_formula, the written KL variational-supremum statement, that source, sourceCited status, and a note that the result must be ported or kept as a cited analytic dependency. This creates metadata, not a proof of entropy duality.

All objects and hypotheses

• source is any Core SourceAnchor; it is the sole function parameter.
• The stored text describes KL(ν‖μ)=sup_Z{EνZ−log Eμexp Z} under the paper's integrability assumptions; those assumptions are text, not formal parameters.
• ProofObligation's omitted dependsOn list is empty by default; the supplied note is descriptive.

Notation and interpretation

Analytic values versus metadata

Contracts and obligation/interface constructors store strings and status labels. They are not propositions asserting the written mathematics and supply no Lean proof of it.

\[\texttt{ProofObligation}\ne\text{proof of its statement string}\]

Construction and meaning

def dvVariationalObligation (source : SourceAnchor) : ProofObligation

def dvVariationalObligation (source : SourceAnchor) : ProofObligation where
  id := "probability.dv_variational_formula"
  statement := "KL(nu || mu) = sup_Z { E_nu[Z] - log E_mu[exp Z] } under the paper's integrability assumptions."
  source := source
  status := ProofStatus.sourceCited
  note := "Port from Mathlib/SLT or keep as cited analytic dependency until formalized."

/-- Precise source-cited DV interface matching `appendix.tex:73-79`.

Downstream proof obligations may depend on this interface only as a cited
analytic result until an actual Lean proof or imported theorem replaces it.
-/

Scope and omitted-condition boundaries

• Contracts and obligation/interface constructors store strings and status labels. They are not propositions asserting the written mathematics and supply no Lean proof of it.
• No Boucheron supremum equality has been proved by this constructor. The passed anchor is not validated here.

Populate the paper-facing DV interface without claiming its proof

AutoSamplingTheory.dvVariationalFormulaInterface · def · Teaching coverage

Statement

Given a source anchor, populate the DvVariationalFormulaInterface with the existing paper-facing textual description: common probability measures, KL with source-specific side conditions, measurable real tests with finite log-mgf, the variational supremum expression, its one-sided consequence, descriptions of available scalar/tilting bridges, the Boucheron–Lugosi–Massart Corollary 4.15 citation, and sourceCited status. These are stored descriptions only.

All objects and hypotheses

• source:SourceAnchor is the only parameter; no measures, test functions, absolute-continuity proofs or admissibility witnesses are passed.
• All twelve data fields of DvVariationalFormulaInterface are populated. The reference to SALD appendix.tex:73–79 is an existing source comment, not a new independent reading or source-fidelity verdict.

Notation and interpretation

Analytic values versus metadata

Contracts and obligation/interface constructors store strings and status labels. They are not propositions asserting the written mathematics and supply no Lean proof of it.

\[\texttt{ProofObligation}\ne\text{proof of its statement string}\]

Construction and meaning

def dvVariationalFormulaInterface (source : SourceAnchor) :
    DvVariationalFormulaInterface

def dvVariationalFormulaInterface (source : SourceAnchor) :
    DvVariationalFormulaInterface where
  source := source
  probabilityMeasures := "mu and nu are probability distributions on the same measurable space."
  klFunctional := "KL(nu || mu), with the paper's absolute-continuity and finite-entropy side conditions supplied by each theorem block."
  testFunctionClass := "real-valued measurable random variables Z on the common space."
  finiteLogMgfPredicate := "log E_mu[exp(Z)] < +infty."
  logMgfFunctional := "Z |-> log E_mu[exp(Z)]."
  variationalFunctional := "Z |-> E_nu[Z] - log E_mu[exp(Z)]."
  supremumStatement := "KL(nu || mu) = sup_Z { E_nu[Z] - log E_mu[exp(Z)] }, where the supremum is over finite-log-mgf tests."
  oneSidedConsequence := "For every admissible Z, E_nu[Z] <= KL(nu || mu) + log E_mu[exp(Z)]."
  oneSidedScalarBridge := "AutoSamplingTheory.dvVariationalOneSidedConsequenceScalar proves the real-order rearrangement from E_nu[Z] - logMgf <= KL to E_nu[Z] <= KL + logMgf; AutoSamplingTheory.dvVariationalOneSidedFromSupremumScalar additionally proves the scalar step from admissible-test membership plus the source supremum identity to that one-sided bound; AutoSamplingTheory.dvVariationalTiltedRightOneSidedConsequence combines the Mathlib tilted backend with the scalar rearrangement under explicit selected-test hypotheses."
  citation := "Boucheron, Lugosi, and Massart, Concentration Inequalities, Corollary 4.15, cited by SALD appendix.tex:73."
  status := ProofStatus.sourceCited

/-- Pointwise square identity for the LSI density test `phi = sqrt(r)`.

In the SALD source step `main_body.tex:208-215`, this is the local scalar
part of replacing `phi^2` by the Radon-Nikodym density ratio `r = rho/pi`.
The measure-theoretic density and integral transport remain separate
obligations.
-/

Scope and omitted-condition boundaries

• Contracts and obligation/interface constructors store strings and status labels. They are not propositions asserting the written mathematics and supply no Lean proof of it.
• Names embedded in oneSidedScalarBridge are not formal theorem dependencies.
• Do not present the stored test class or finite-log-mgf clause as a proved sufficient hypothesis for the full supremum equality.

The square-root density squares back to the density

AutoSamplingTheory.lsiKlFiSqrtDensitySquareScalar · theorem · Teaching coverage

Statement

For every nonnegative real number r, the square of its nonnegative real square root equals r.

All objects and hypotheses

• r is a real number and hr supplies 0≤r; no measure or density construction is assumed.

Mathematical proof

theorem lsiKlFiSqrtDensitySquareScalar {r : Real} (hr : 0 ≤ r) :
    (Real.sqrt r) ^ 2 = r

theorem lsiKlFiSqrtDensitySquareScalar {r : Real} (hr : 0 ≤ r) :
    (Real.sqrt r) ^ 2 = r := by
  exact Real.sq_sqrt hr

/-- Pointwise entropy-integrand rewrite for `phi = sqrt(r)`.

This proves only the scalar rewrite
`phi^2 log(phi^2) = r log r` after nonnegativity of the density ratio is
available.  Integrability, zero-density conventions, and the KL integral
identity are still analytic obligations.
-/

Scope and omitted-condition boundaries

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

Rewrite the square-root test's entropy integrand

AutoSamplingTheory.lsiKlFiSqrtDensityEntropyIntegrandScalar · theorem · Teaching coverage

Statement

For every real r≥0, the expression (√r)² log((√r)²) equals r log r, using Mathlib's real logarithm convention, including its value at zero.

All objects and hypotheses

• r∈ℝ and 0≤r. The real logarithm is totalized; Real.log 0=0, so the displayed identity includes r=0.

Mathematical proof

theorem lsiKlFiSqrtDensityEntropyIntegrandScalar {r : Real} (hr : 0 ≤ r) :
    (Real.sqrt r) ^ 2 * Real.log ((Real.sqrt r) ^ 2) = r * Real.log r

theorem lsiKlFiSqrtDensityEntropyIntegrandScalar {r : Real} (hr : 0 ≤ r) :
    (Real.sqrt r) ^ 2 * Real.log ((Real.sqrt r) ^ 2) = r * Real.log r := by
  rw [lsiKlFiSqrtDensitySquareScalar hr]

/-- Scalar normalization handoff for the LSI test `phi = sqrt(r)`.

After an integral backend has shown that the mass of `phi^2` equals the mass of
the density ratio `r`, probability normalization of `r` gives the LSI test
normalization.  This does not prove the integral equality itself.
-/

Scope and omitted-condition boundaries

• 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 finite-entropy or analytic zero-density admissibility theorem is asserted.

Transfer a supplied unit-mass identity

AutoSamplingTheory.lsiKlFiSqrtDensityNormalizationScalar · theorem · Teaching coverage

Statement

Let densityMass and testMass be real numbers. If testMass=densityMass and densityMass=1, then testMass=1. Their names carry no measure-theoretic meaning unless an application supplies it.

All objects and hypotheses

• densityMass,testMass∈ℝ; the two displayed equalities are supplied.

Mathematical proof

theorem lsiKlFiSqrtDensityNormalizationScalar {densityMass testMass : Real}
    (htest : testMass = densityMass)
    (hdensity : densityMass = 1) :
    testMass = 1

theorem lsiKlFiSqrtDensityNormalizationScalar {densityMass testMass : Real}
    (htest : testMass = densityMass)
    (hdensity : densityMass = 1) :
    testMass = 1 := by
  rw [htest, hdensity]

/-- Radon-Nikodym mass normalization for the LSI density ratio.

For probability measures `rho << pi`, the density ratio `d rho / d pi` has
unit `pi`-mass.  This is the measure-level backend behind the source line
`int phi^2 d pi = int (rho/pi) d pi = 1` before converting to real integrals.
-/

Scope and omitted-condition boundaries

• 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.
• This is an equality handoff, not a normalization theorem for any measure.

The Radon–Nikodym density has unit nonnegative integral

AutoSamplingTheory.lsiKlFiRnDerivLIntegralMassOne · theorem · Teaching coverage

Statement

For probability measures ρ and π on a measurable space with ρ≪π, the nonnegative extended integral of dρ/dπ against π equals one.

All objects and hypotheses

• α is an arbitrary measurable space; ρ and π are measures on it, both with IsProbabilityMeasure instances.
• hrho_pi supplies absolute continuity ρ≪π. Probability assumptions supply the finite/sigma-finite and Lebesgue-decomposition requirements of the imported Radon–Nikodym APIs.
• Write R=dρ/dπ for Mathlib's ℝ≥0∞-valued rnDeriv representative and r=R.toReal for its real-valued conversion; r≥0 everywhere.

Notation and interpretation

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 lsiKlFiRnDerivLIntegralMassOne {α : Type*} [MeasurableSpace α]
    (rho pi : Measure α) [IsProbabilityMeasure rho] [IsProbabilityMeasure pi]
    (hrho_pi : rho ≪ pi) :
    ∫⁻ x, rho.rnDeriv pi x ∂pi = 1

theorem lsiKlFiRnDerivLIntegralMassOne {α : Type*} [MeasurableSpace α]
    (rho pi : Measure α) [IsProbabilityMeasure rho] [IsProbabilityMeasure pi]
    (hrho_pi : rho ≪ pi) :
    ∫⁻ x, rho.rnDeriv pi x ∂pi = 1 := by
  rw [Measure.lintegral_rnDeriv hrho_pi]
  simp

/-- Real-integral normalization of the Radon-Nikodym density ratio.

This supplies the real mass input used by the scalar normalization bridge for
the LSI test `phi=sqrt(d rho/d pi)`.
-/

Scope and omitted-condition boundaries

• 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 differentiability or admissible square-root test follows from unit mass.

The real Radon–Nikodym density also has unit integral

AutoSamplingTheory.lsiKlFiRnDerivDensityMassOne · theorem · Teaching coverage

Statement

For absolutely continuous probability measures ρ≪π, the real-valued function r=(dρ/dπ).toReal has real integral one against π.

All objects and hypotheses

• α is an arbitrary measurable space; ρ and π are measures on it, both with IsProbabilityMeasure instances.
• hrho_pi supplies absolute continuity ρ≪π. Probability assumptions supply the finite/sigma-finite and Lebesgue-decomposition requirements of the imported Radon–Nikodym APIs.
• Write R=dρ/dπ for Mathlib's ℝ≥0∞-valued rnDeriv representative and r=R.toReal for its real-valued conversion; r≥0 everywhere.

Notation and interpretation

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 lsiKlFiRnDerivDensityMassOne {α : Type*} [MeasurableSpace α]
    (rho pi : Measure α) [IsProbabilityMeasure rho] [IsProbabilityMeasure pi]
    (hrho_pi : rho ≪ pi) :
    ∫ x, (rho.rnDeriv pi x).toReal ∂pi = 1

theorem lsiKlFiRnDerivDensityMassOne {α : Type*} [MeasurableSpace α]
    (rho pi : Measure α) [IsProbabilityMeasure rho] [IsProbabilityMeasure pi]
    (hrho_pi : rho ≪ pi) :
    ∫ x, (rho.rnDeriv pi x).toReal ∂pi = 1 := by
  rw [Measure.integral_toReal_rnDeriv hrho_pi]
  simp

/-- Normalization of the source LSI test `phi=sqrt(d rho/d pi)`.

This combines the pointwise square identity for the square-root density test
with the Radon-Nikodym mass theorem.  Smooth/admissible-test and approximation
requirements remain separate analytic obligations.
-/

Scope and omitted-condition boundaries

• 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.
• The chosen real density r is (rnDeriv ρ π).toReal, with ENNReal.toReal(∞)=0. Do not replace this with an arbitrary pointwise density version; absolute continuity and probability measures justify the a.e. density interpretation.

The squared square-root Radon–Nikodym test has unit mass

AutoSamplingTheory.lsiKlFiSqrtRnDerivTestMassOne · theorem · Teaching coverage

Statement

For probability measures ρ≪π and r=(dρ/dπ).toReal, the real integral of (√r)² against π is one.

All objects and hypotheses

• α is an arbitrary measurable space; ρ and π are measures on it, both with IsProbabilityMeasure instances.
• hrho_pi supplies absolute continuity ρ≪π. Probability assumptions supply the finite/sigma-finite and Lebesgue-decomposition requirements of the imported Radon–Nikodym APIs.
• Write R=dρ/dπ for Mathlib's ℝ≥0∞-valued rnDeriv representative and r=R.toReal for its real-valued conversion; r≥0 everywhere.

Notation and interpretation

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 lsiKlFiSqrtRnDerivTestMassOne {α : Type*} [MeasurableSpace α]
    (rho pi : Measure α) [IsProbabilityMeasure rho] [IsProbabilityMeasure pi]
    (hrho_pi : rho ≪ pi) :
    ∫ x, (Real.sqrt ((rho.rnDeriv pi x).toReal)) ^ 2 ∂pi = 1

theorem lsiKlFiSqrtRnDerivTestMassOne {α : Type*} [MeasurableSpace α]
    (rho pi : Measure α) [IsProbabilityMeasure rho] [IsProbabilityMeasure pi]
    (hrho_pi : rho ≪ pi) :
    ∫ x, (Real.sqrt ((rho.rnDeriv pi x).toReal)) ^ 2 ∂pi = 1 := by
  rw [← lsiKlFiRnDerivDensityMassOne rho pi hrho_pi]
  refine integral_congr_ae ?_
  filter_upwards with x
  exact Real.sq_sqrt ENNReal.toReal_nonneg

/-- Entropy transport from the density-ratio integral to the KL log-likelihood integral.

For `rho << pi`, Mathlib's log-likelihood-ratio backend identifies
`int (d rho/d pi) log(d rho/d pi) d pi` with the paper's KL integrand
`int log(d rho/d pi) d rho`.  Finite-KL assumptions for theorem use remain
explicit downstream.
-/

Scope and omitted-condition boundaries

• 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.
• The chosen real density r is (rnDeriv ρ π).toReal, with ENNReal.toReal(∞)=0. Do not replace this with an arbitrary pointwise density version; absolute continuity and probability measures justify the a.e. density interpretation.

Transport the density entropy integral to the log-likelihood measure

AutoSamplingTheory.lsiKlFiRnDerivEntropyIntegral · theorem · Teaching coverage

Statement

For probability measures ρ≪π, with r=(dρ/dπ).toReal and ℓρ,π=log r, the real integral ∫r log r dπ equals ∫ℓρ,π dρ. This is equality of Mathlib's totalized real integrals; it does not assert their integrability or finiteness as entropy quantities.

All objects and hypotheses

• α is an arbitrary measurable space; ρ and π are measures on it, both with IsProbabilityMeasure instances.
• hrho_pi supplies absolute continuity ρ≪π. Probability assumptions supply the finite/sigma-finite and Lebesgue-decomposition requirements of the imported Radon–Nikodym APIs.
• Write R=dρ/dπ for Mathlib's ℝ≥0∞-valued rnDeriv representative and r=R.toReal for its real-valued conversion; r≥0 everywhere.

Notation and interpretation

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 lsiKlFiRnDerivEntropyIntegral {α : Type*} [MeasurableSpace α]
    (rho pi : Measure α) [IsProbabilityMeasure rho] [IsProbabilityMeasure pi]
    (hrho_pi : rho ≪ pi) :
    ∫ x, (rho.rnDeriv pi x).toReal * Real.log (rho.rnDeriv pi x).toReal ∂pi =
      ∫ x, llr rho pi x ∂rho

theorem lsiKlFiRnDerivEntropyIntegral {α : Type*} [MeasurableSpace α]
    (rho pi : Measure α) [IsProbabilityMeasure rho] [IsProbabilityMeasure pi]
    (hrho_pi : rho ≪ pi) :
    ∫ x, (rho.rnDeriv pi x).toReal * Real.log (rho.rnDeriv pi x).toReal ∂pi =
      ∫ x, llr rho pi x ∂rho := by
  exact integral_rnDeriv_mul_log hrho_pi

/-- Entropy transport for the square-root density test used by LSI.

This rewrites the LSI entropy integrand for
`phi=sqrt(d rho/d pi)` and then uses the Radon-Nikodym entropy transport
identity.  It still does not prove admissibility of `phi` or the Fisher
chain-rule side of `eq:LSI-KL-FI`.
-/

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.
• The chosen real density r is (rnDeriv ρ π).toReal, with ENNReal.toReal(∞)=0. Do not replace this with an arbitrary pointwise density version; absolute continuity and probability measures justify the a.e. density interpretation.
• 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.
• Do not identify this equality alone with a finite KL formula; downstream hypotheses must control the log-likelihood integral.

Rewrite the square-root test entropy as a log-likelihood integral

AutoSamplingTheory.lsiKlFiSqrtRnDerivEntropyIntegral · theorem · Teaching coverage

Statement

For probability measures ρ≪π and r=(dρ/dπ).toReal, the real integral of (√r)² log((√r)²) under π equals the integral of llr(ρ,π) under ρ. No finite-entropy or test-admissibility claim is made.

All objects and hypotheses

• α is an arbitrary measurable space; ρ and π are measures on it, both with IsProbabilityMeasure instances.
• hrho_pi supplies absolute continuity ρ≪π. Probability assumptions supply the finite/sigma-finite and Lebesgue-decomposition requirements of the imported Radon–Nikodym APIs.
• Write R=dρ/dπ for Mathlib's ℝ≥0∞-valued rnDeriv representative and r=R.toReal for its real-valued conversion; r≥0 everywhere.

Notation and interpretation

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 lsiKlFiSqrtRnDerivEntropyIntegral {α : Type*} [MeasurableSpace α]
    (rho pi : Measure α) [IsProbabilityMeasure rho] [IsProbabilityMeasure pi]
    (hrho_pi : rho ≪ pi) :
    ∫ x, (Real.sqrt ((rho.rnDeriv pi x).toReal)) ^ 2 *
        Real.log ((Real.sqrt ((rho.rnDeriv pi x).toReal)) ^ 2) ∂pi =
      ∫ x, llr rho pi x ∂rho

theorem lsiKlFiSqrtRnDerivEntropyIntegral {α : Type*} [MeasurableSpace α]
    (rho pi : Measure α) [IsProbabilityMeasure rho] [IsProbabilityMeasure pi]
    (hrho_pi : rho ≪ pi) :
    ∫ x, (Real.sqrt ((rho.rnDeriv pi x).toReal)) ^ 2 *
        Real.log ((Real.sqrt ((rho.rnDeriv pi x).toReal)) ^ 2) ∂pi =
      ∫ x, llr rho pi x ∂rho := by
  rw [← lsiKlFiRnDerivEntropyIntegral rho pi hrho_pi]
  refine integral_congr_ae ?_
  filter_upwards with x
  exact lsiKlFiSqrtDensityEntropyIntegrandScalar ENNReal.toReal_nonneg

/-- One-dimensional pointwise Fisher-chain coefficient for the LSI test.

For a positive density ratio `r`, the source substitution
`phi=sqrt(r)` has differential coefficient
`d phi = (2*sqrt(r))^{-1} d r`, while
`d log r = r^{-1} d r`.  This scalar lemma proves the resulting
`1/4` factor in the Fisher integrand.  The vector-gradient and integral
versions remain separate analytic obligations.
-/

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.
• The chosen real density r is (rnDeriv ρ π).toReal, with ENNReal.toReal(∞)=0. Do not replace this with an arbitrary pointwise density version; absolute continuity and probability measures justify the a.e. density interpretation.
• 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.

The scalar square-root/logarithm coefficients give a factor of one quarter

AutoSamplingTheory.lsiKlFiSqrtDensityFisherChainScalar · theorem · Teaching coverage

Statement

For any positive real r and any real dr, the squared expression dr/(2√r) equals one quarter of r times (dr/r)². The symbols are numbers, not derivatives whose existence is established here.

All objects and hypotheses

• r,dr∈ℝ; hr asserts r>0. Strict positivity, not mere nonnegativity, permits clearing both denominators.

Mathematical proof

theorem lsiKlFiSqrtDensityFisherChainScalar {r dr : Real} (hr : 0 < r) :
    ((1 / (2 * Real.sqrt r)) * dr) ^ 2 =
      (1 / 4) * (r * (dr / r) ^ 2)

theorem lsiKlFiSqrtDensityFisherChainScalar {r dr : Real} (hr : 0 < r) :
    ((1 / (2 * Real.sqrt r)) * dr) ^ 2 =
      (1 / 4) * (r * (dr / r) ^ 2) := by
  have hsqrt_sq : (Real.sqrt r) ^ 2 = r := Real.sq_sqrt (le_of_lt hr)
  have hsqrt_ne : Real.sqrt r ≠ 0 := ne_of_gt (Real.sqrt_pos.2 hr)
  have hr_ne : r ≠ 0 := ne_of_gt hr
  field_simp [hsqrt_ne, hr_ne]
  nlinarith [hsqrt_sq]

/-- Pointwise Fisher-chain handoff with named derivative identities.

This packages the scalar part of
`nabla sqrt(r) = (2*sqrt(r))^{-1} nabla r` and
`nabla log r = r^{-1} nabla r`.  It does not prove differentiability,
gradient existence, or the vector norm/integral transport backend.
-/

Scope and omitted-condition boundaries

• 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.
• The r=0 case is excluded; no zero-density extension or vector-norm identity is proved.

Apply the scalar coefficient identity to supplied derivative values

AutoSamplingTheory.lsiKlFiSqrtDensityFisherChainOfDerivativesScalar · theorem · Teaching coverage

Statement

Let r>0 and dr,dSqrt,dLog be real numbers. If dSqrt=dr/(2√r) and dLog=dr/r, then dSqrt²=(1/4)r dLog². The named derivative identities are explicit assumptions.

All objects and hypotheses

• r,dr,dSqrt,dLog∈ℝ with r>0.
• The two coefficient identities for dSqrt and dLog are supplied; no functions or differentiability hypotheses are inferred from their names.

Mathematical proof

theorem lsiKlFiSqrtDensityFisherChainOfDerivativesScalar
    {r dr dSqrt dLog : Real}
    (hr : 0 < r)
    (hdSqrt : dSqrt = (1 / (2 * Real.sqrt r)) * dr)
    (hdLog : dLog = dr / r) :
    dSqrt ^ 2 = (1 / 4) * (r * dLog ^ 2)

theorem lsiKlFiSqrtDensityFisherChainOfDerivativesScalar
    {r dr dSqrt dLog : Real}
    (hr : 0 < r)
    (hdSqrt : dSqrt = (1 / (2 * Real.sqrt r)) * dr)
    (hdLog : dLog = dr / r) :
    dSqrt ^ 2 = (1 / 4) * (r * dLog ^ 2) := by
  rw [hdSqrt, hdLog]
  exact lsiKlFiSqrtDensityFisherChainScalar hr

/-- Finite-coordinate Fisher-chain handoff for the LSI density test.

This lifts the pointwise scalar identity for `phi=sqrt(r)` to a finite sum of
coordinate-square terms.  It is still not the vector Sobolev chain rule or the
integral identity for Fisher information; those analytic backends must supply
the coordinate derivative identities and the later integral transport.
-/

Scope and omitted-condition boundaries

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

Sum the scalar Fisher-chain factor over finitely many coordinates

AutoSamplingTheory.lsiKlFiSqrtDensityFisherChainFiniteSumScalar · theorem · Teaching coverage

Statement

Let I be a finite index type, r>0 a real number, and dr,dSqrt,dLog:I→ℝ. If at every i the values satisfy dSqrt_i=dr_i/(2√r) and dLog_i=dr_i/r, then the sum of dSqrt_i² is (1/4)r times the sum of dLog_i². The empty finite index type is allowed.

All objects and hypotheses

• I is a type with Fintype; r∈ℝ is strictly positive.
• dr,dSqrt,dLog:I→ℝ and the two derivative-coefficient equalities hold for every i.

Mathematical proof

theorem lsiKlFiSqrtDensityFisherChainFiniteSumScalar
    {ι : Type*} [Fintype ι] {r : Real} {dr dSqrt dLog : ι → Real}
    (hr : 0 < r)
    (hdSqrt : ∀ i, dSqrt i = (1 / (2 * Real.sqrt r)) * dr i)
    (hdLog : ∀ i, dLog i = dr i / r) :
    (∑ i, dSqrt i ^ 2) = (1 / 4) * (r * ∑ i, dLog i ^ 2)

theorem lsiKlFiSqrtDensityFisherChainFiniteSumScalar
    {ι : Type*} [Fintype ι] {r : Real} {dr dSqrt dLog : ι → Real}
    (hr : 0 < r)
    (hdSqrt : ∀ i, dSqrt i = (1 / (2 * Real.sqrt r)) * dr i)
    (hdLog : ∀ i, dLog i = dr i / r) :
    (∑ i, dSqrt i ^ 2) = (1 / 4) * (r * ∑ i, dLog i ^ 2) := by
  calc
    (∑ i, dSqrt i ^ 2) = ∑ i, (1 / 4) * (r * dLog i ^ 2) := by
      refine Finset.sum_congr rfl ?_
      intro i _hi
      rw [hdSqrt i, hdLog i]
      exact lsiKlFiSqrtDensityFisherChainScalar hr
    _ = ∑ i, ((1 / 4) * r) * dLog i ^ 2 := by
      refine Finset.sum_congr rfl ?_
      intro i _hi
      ring
    _ = ((1 / 4) * r) * ∑ i, dLog i ^ 2 := by
      rw [Finset.mul_sum]
    _ = (1 / 4) * (r * ∑ i, dLog i ^ 2) := by
      ring

/-- Finite-coordinate handoff to the Dirichlet/Fisher identity.

Once a density backend identifies the Dirichlet term with the finite coordinate
sum of `d sqrt(r)` squares and the Fisher term with
`r * sum_i (d log r_i)^2`, this lemma supplies the exact
`dirichlet = (1/4)*FI` input consumed by the existing LSI/KL/FI scalar bridge.
It does not construct the Radon--Nikodym density, prove differentiability, or
integrate the identity.
-/

Scope and omitted-condition boundaries

• 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.
• A coordinate-square sum is not automatically the squared norm of a gradient; an application must justify that identification.

Name the finite-coordinate Dirichlet and Fisher expressions

AutoSamplingTheory.lsiKlFiSqrtDensityFisherChainFiniteSumHandoffScalar · theorem · Teaching coverage

Statement

Let I be finite, r>0, and dr,dSqrt,dLog:I→ℝ satisfy the coefficient identities at every coordinate. If real numbers D and J are supplied to equal ∑dSqrt_i² and r∑dLog_i² respectively, then D=J/4.

All objects and hypotheses

• I has Fintype; r,D,J∈ℝ with r>0; dr,dSqrt,dLog:I→ℝ.
• D and J have the displayed finite-sum representations, and dSqrt_i=dr_i/(2√r), dLog_i=dr_i/r for every i.

Mathematical proof

theorem lsiKlFiSqrtDensityFisherChainFiniteSumHandoffScalar
    {ι : Type*} [Fintype ι] {r dirichlet fisher : Real}
    {dr dSqrt dLog : ι → Real}
    (hr : 0 < r)
    (hdirichlet : dirichlet = ∑ i, dSqrt i ^ 2)
    (hfisher : fisher = r * ∑ i, dLog i ^ 2)
    (hdSqrt : ∀ i, dSqrt i = (1 / (2 * Real.sqrt r)) * dr i)
    (hdLog : ∀ i, dLog i = dr i / r) :
    dirichlet = (1 / 4) * fisher

theorem lsiKlFiSqrtDensityFisherChainFiniteSumHandoffScalar
    {ι : Type*} [Fintype ι] {r dirichlet fisher : Real}
    {dr dSqrt dLog : ι → Real}
    (hr : 0 < r)
    (hdirichlet : dirichlet = ∑ i, dSqrt i ^ 2)
    (hfisher : fisher = r * ∑ i, dLog i ^ 2)
    (hdSqrt : ∀ i, dSqrt i = (1 / (2 * Real.sqrt r)) * dr i)
    (hdLog : ∀ i, dLog i = dr i / r) :
    dirichlet = (1 / 4) * fisher := by
  rw [hdirichlet, hfisher]
  exact lsiKlFiSqrtDensityFisherChainFiniteSumScalar hr hdSqrt hdLog

/-- Integral handoff for the finite-coordinate Fisher chain rule.

After a Sobolev backend supplies coordinate derivative identities almost
everywhere for `sqrt(r)` and `log r`, this pushes the cycle-38 finite-sum
coefficient through the `pi`-integral.  It is still below the full
vector-gradient/Fisher-information theorem: integrability, coordinate-to-vector
gradient equivalence, zero-density handling, and admissibility of `sqrt(r)`
remain separate obligations.
-/

Scope and omitted-condition boundaries

• 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.
• Named scalar handoff, not integration or geometric identification.

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.

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

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

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

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.

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.

Rearrange a supplied variational upper bound

AutoSamplingTheory.dvVariationalOneSidedConsequenceScalar · theorem · Teaching coverage

Statement

For arbitrary real numbers k,e,L, if e−L≤k, then e≤k+L. The names KL, expectation and log-mgf used in the Lean declaration are labels for these real inputs, not analytic definitions.

All objects and hypotheses

• kl, expectation and logMgf are arbitrary real numbers; hvar supplies expectation−logMgf≤kl.

Mathematical proof

theorem dvVariationalOneSidedConsequenceScalar {kl expectation logMgf : Real}
    (hvar : expectation - logMgf ≤ kl) :
    expectation ≤ kl + logMgf

theorem dvVariationalOneSidedConsequenceScalar {kl expectation logMgf : Real}
    (hvar : expectation - logMgf ≤ kl) :
    expectation ≤ kl + logMgf := by
  exact sub_le_iff_le_add.mp hvar

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

This does not prove Donsker--Varadhan.  It starts after a cited or eventually
formalized theorem has identified `kl` with the supremum of the admissible
variational values, and after the selected test has been shown admissible.
-/

Scope and omitted-condition boundaries

• Only a one-sided bound for a selected admissible test is established. The full Donsker–Varadhan/Boucheron variational supremum equality remains separate; no source-fidelity verdict is made.
• Pure scalar rearrangement; analytic meanings must be supplied downstream.

Extract one admissible scalar value from a known supremum

AutoSamplingTheory.dvVariationalOneSidedFromSupremumScalar · theorem · Teaching coverage

Statement

Let A⊆ℝ be bounded above, let v∈A, and suppose sup A=k and v=e−L for real k,e,L,v. Then e≤k+L. Membership supplies nonemptiness; the supremum identity and the selected test's representation are assumptions.

All objects and hypotheses

• admissibleValues=A is a set of real numbers; hbounded says A is bounded above.
• testValue=v belongs to A; kl=k, expectation=e and logMgf=L are real.
• hsup gives sSup A=k and htest gives v=e−L.

Mathematical proof

theorem dvVariationalOneSidedFromSupremumScalar {admissibleValues : Set Real}
    {kl expectation logMgf testValue : Real}
    (hbounded : BddAbove admissibleValues)
    (hmem : testValue ∈ admissibleValues)
    (hsup : sSup admissibleValues = kl)
    (htest : testValue = expectation - logMgf) :
    expectation ≤ kl + logMgf

theorem dvVariationalOneSidedFromSupremumScalar {admissibleValues : Set Real}
    {kl expectation logMgf testValue : Real}
    (hbounded : BddAbove admissibleValues)
    (hmem : testValue ∈ admissibleValues)
    (hsup : sSup admissibleValues = kl)
    (htest : testValue = expectation - logMgf) :
    expectation ≤ kl + logMgf := by
  have htest_le_sup : testValue ≤ sSup admissibleValues := le_csSup hbounded hmem
  have hvar : expectation - logMgf ≤ kl := by
    rw [← htest, ← hsup]
    exact htest_le_sup
  exact dvVariationalOneSidedConsequenceScalar hvar

/-- Finite-log-mgf monotonicity for the scaled tests used before DV.

If the exponential moment for `alpha0 * q` is integrable under a finite
measure, then the exponential moment for `alpha * q` is integrable for
`0 <= alpha <= alpha0`.  In SALD this is the local Mathlib-backed part of
turning an `alpha0`-complexity assumption into the finite-log-mgf hypothesis
for a selected DV test; it is not a proof of the DV formula itself.
-/

Scope and omitted-condition boundaries

• Only a one-sided bound for a selected admissible test is established. The full Donsker–Varadhan/Boucheron variational supremum equality remains separate; no source-fidelity verdict is made.
• The entropy supremum equality and admissible-test membership are not established here.

An integrable exponential moment remains integrable at a smaller nonnegative scale

AutoSamplingTheory.dvFiniteLogMgfOfLeAlpha · theorem · Teaching coverage

Statement

Let μ be a finite measure on measurable Ω and q:Ω→ℝ any function. If exp(α₀q) is μ-integrable and 0≤α≤α₀, then exp(αq) is μ-integrable. No nonnegativity of q, probability normalization, or separate measurability premise for q is assumed.

All objects and hypotheses

• Ω is measurable and μ is finite, possibly zero or unnormalized.
• q:Ω→ℝ and α,α₀∈ℝ; the exponential at α₀ is integrable, and 0≤α≤α₀.

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 dvFiniteLogMgfOfLeAlpha {Ω : Type*} [MeasurableSpace Ω]
    {mu : Measure Ω} [IsFiniteMeasure mu]
    {q : Ω → Real} {alpha alpha0 : Real}
    (hAlpha0 : Integrable (fun x ↦ Real.exp (alpha0 * q x)) mu)
    (hAlpha_nonneg : 0 ≤ alpha) (hAlpha_le : alpha ≤ alpha0) :
    Integrable (fun x ↦ Real.exp (alpha * q x)) mu

theorem dvFiniteLogMgfOfLeAlpha {Ω : Type*} [MeasurableSpace Ω]
    {mu : Measure Ω} [IsFiniteMeasure mu]
    {q : Ω → Real} {alpha alpha0 : Real}
    (hAlpha0 : Integrable (fun x ↦ Real.exp (alpha0 * q x)) mu)
    (hAlpha_nonneg : 0 ≤ alpha) (hAlpha_le : alpha ≤ alpha0) :
    Integrable (fun x ↦ Real.exp (alpha * q x)) mu := by
  exact ProbabilityTheory.integrable_exp_mul_of_nonneg_of_le (X := q) (u := alpha0)
    (t := alpha) hAlpha0 hAlpha_nonneg hAlpha_le

/-- Mathlib-backed one-sided Donsker--Varadhan inequality via exponential tilting.

This proves only the admissible-test upper bound
`E_nu[Z] - log E_mu[exp Z] <= KL(nu || mu)` under explicit Mathlib
measure-theoretic hypotheses.  It is not the Boucheron supremum equality from
`appendix.tex:73-79`.
-/

Scope and omitted-condition boundaries

• This result establishes exponential integrability at an intermediate nonnegative scale, not a Donsker–Varadhan inequality or a variational supremum formula. Its later use in a selected-test bound is a separate consumer; no source-fidelity verdict is made.
• For a probability target this supports a finite, positive exponential normalizer. For the allowed zero measure, the normalizer is zero, so do not read the title as an unqualified ordinary log-mgf statement.

Prove the selected-test entropy bound by exponential tilting

AutoSamplingTheory.dvVariationalOneSidedOfTiltedRight · theorem · Teaching coverage

Statement

For probability measures ν≪μ on a common measurable space, retain the explicit sigma-finiteness hypotheses and assume Z∈L¹(ν), exp Z∈L¹(μ), and llr(ν,μ)∈L¹(ν). Then ∫Z dν−log∫exp Z dμ≤(klDiv ν μ).toReal. These assumptions keep the selected normalizer positive and finite and put KL in its finite branch.

All objects and hypotheses

• α (or Ω) is an arbitrary measurable space; ν and μ are probability measures on that same space.
• Both SigmaFinite μ and SigmaFinite ν are explicitly present in the Lean signature; probability already supplies them, but they are not omitted here.
• ν≪μ; the chosen real test Z is ν-integrable; exp Z is μ-integrable; llr(ν,μ) is ν-integrable.
• Notation: ℓ=llr(ν,μ)=log((dν/dμ).toReal), M_Z=∫exp Z dμ, and K=(InformationTheory.klDiv ν μ).toReal.
• Z is an arbitrary real-valued function on the common space; no pointwise boundedness or smoothness is assumed.

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 dvVariationalOneSidedOfTiltedRight {α : Type*} [MeasurableSpace α]
    (nu mu : Measure α) [IsProbabilityMeasure nu] [IsProbabilityMeasure mu]
    [SigmaFinite mu] [SigmaFinite nu]
    (Z : α → Real)
    (hnu_mu : nu ≪ mu)
    (hZ_nu : Integrable Z nu)
    (hexp_mu : Integrable (fun x ↦ Real.exp (Z x)) mu)
    (hllr : Integrable (llr nu mu) nu) :
    (∫ x, Z x ∂nu) - Real.log (∫ x, Real.exp (Z x) ∂mu) ≤
      (klDiv nu mu).toReal

theorem dvVariationalOneSidedOfTiltedRight {α : Type*} [MeasurableSpace α]
    (nu mu : Measure α) [IsProbabilityMeasure nu] [IsProbabilityMeasure mu]
    [SigmaFinite mu] [SigmaFinite nu]
    (Z : α → Real)
    (hnu_mu : nu ≪ mu)
    (hZ_nu : Integrable Z nu)
    (hexp_mu : Integrable (fun x ↦ Real.exp (Z x)) mu)
    (hllr : Integrable (llr nu mu) nu) :
    (∫ x, Z x ∂nu) - Real.log (∫ x, Real.exp (Z x) ∂mu) ≤
      (klDiv nu mu).toReal := by
  let : IsProbabilityMeasure (mu.tilted Z) := isProbabilityMeasure_tilted hexp_mu
  have hmu_tilted : mu ≪ mu.tilted Z := absolutelyContinuous_tilted hexp_mu
  have hnu_tilted : nu ≪ mu.tilted Z := hnu_mu.trans hmu_tilted
  have hllr_tilted : Integrable (llr nu (mu.tilted Z)) nu :=
    integrable_llr_tilted_right (μ := nu) (ν := mu) (f := Z) hnu_mu hZ_nu hllr
      hexp_mu
  have hnonneg := integral_llr_add_sub_measure_univ_nonneg (μ := nu) (ν := mu.tilted Z)
    hnu_tilted hllr_tilted
  have hnonneg_llr : 0 ≤ ∫ x, llr nu (mu.tilted Z) x ∂nu := by
    simpa using hnonneg
  have htilted :=
    integral_llr_tilted_right (μ := nu) (ν := mu) (f := Z) hnu_mu hZ_nu hexp_mu
      hllr
  have hnonneg_rewrite :
      0 ≤ (∫ x, llr nu mu x ∂nu) - (∫ x, Z x ∂nu) +
        Real.log (∫ x, Real.exp (Z x) ∂mu) := by
    simpa [htilted] using hnonneg_llr
  have hineq :
      (∫ x, Z x ∂nu) - Real.log (∫ x, Real.exp (Z x) ∂mu) ≤
        ∫ x, llr nu mu x ∂nu := by
    linarith
  have hkl : (klDiv nu mu).toReal = ∫ x, llr nu mu x ∂nu := by
    simpa using toReal_klDiv_of_measure_eq (μ := nu) (ν := mu) hnu_mu (by simp)
  simpa [hkl] using hineq

/-- One-sided DV inequality for a SALD-style scaled selected test.

This packages the theorem-instance side conditions for tests of the form
`Z = alpha * q`.  The `alpha0` exponential-moment assumption supplies the
finite-log-mgf hypothesis by `dvFiniteLogMgfOfLeAlpha`, and the remaining
absolute-continuity, selected-test integrability, and log-likelihood
integrability hypotheses are kept explicit.  The Boucheron supremum equality
from `appendix.tex:73-79` remains source-cited.
-/

Scope and omitted-condition boundaries

• Only a one-sided bound for a selected admissible test is established. The full Donsker–Varadhan/Boucheron variational supremum equality remains separate; no source-fidelity verdict is made.
• No supremum equality, optimizer characterization or equality case is proved. The assumptions are not replaceable by merely finite-looking totalized integrals.

Use an upper-scale exponential moment for the selected scaled test

AutoSamplingTheory.dvVariationalOneSidedOfScaledTest · theorem · Teaching coverage

Statement

For the probability measures and hypotheses below, including integrability of the selected test αq under ν and an exponential moment at α₀ with 0≤α≤α₀, the selected-test DV bound holds at scale α. No positivity of q or strict positivity of α is needed.

All objects and hypotheses

• Ω is measurable; ν and μ are probability measures with explicit SigmaFinite μ and SigmaFinite ν instances.
• q:Ω→ℝ and α,α₀∈ℝ satisfy 0≤α≤α₀; ν≪μ.
• The selected test αq is ν-integrable, exp(α₀q) is μ-integrable, and llr(ν,μ) is ν-integrable.
• Write K=(klDiv ν μ).toReal and L_α=log∫exp(αq)dμ.

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 dvVariationalOneSidedOfScaledTest {Ω : Type*} [MeasurableSpace Ω]
    (nu mu : Measure Ω) [IsProbabilityMeasure nu] [IsProbabilityMeasure mu]
    [SigmaFinite mu] [SigmaFinite nu]
    (q : Ω → Real) {alpha alpha0 : Real}
    (hAlpha_nonneg : 0 ≤ alpha) (hAlpha_le : alpha ≤ alpha0)
    (hnu_mu : nu ≪ mu)
    (hZ_nu : Integrable (fun x ↦ alpha * q x) nu)
    (hexp_alpha0_mu : Integrable (fun x ↦ Real.exp (alpha0 * q x)) mu)
    (hllr : Integrable (llr nu mu) nu) :
    (∫ x, alpha * q x ∂nu) - Real.log (∫ x, Real.exp (alpha * q x) ∂mu) ≤
      (klDiv nu mu).toReal

theorem dvVariationalOneSidedOfScaledTest {Ω : Type*} [MeasurableSpace Ω]
    (nu mu : Measure Ω) [IsProbabilityMeasure nu] [IsProbabilityMeasure mu]
    [SigmaFinite mu] [SigmaFinite nu]
    (q : Ω → Real) {alpha alpha0 : Real}
    (hAlpha_nonneg : 0 ≤ alpha) (hAlpha_le : alpha ≤ alpha0)
    (hnu_mu : nu ≪ mu)
    (hZ_nu : Integrable (fun x ↦ alpha * q x) nu)
    (hexp_alpha0_mu : Integrable (fun x ↦ Real.exp (alpha0 * q x)) mu)
    (hllr : Integrable (llr nu mu) nu) :
    (∫ x, alpha * q x ∂nu) - Real.log (∫ x, Real.exp (alpha * q x) ∂mu) ≤
      (klDiv nu mu).toReal := by
  have hexp_mu : Integrable (fun x ↦ Real.exp (alpha * q x)) mu :=
    dvFiniteLogMgfOfLeAlpha (mu := mu) (q := q) hexp_alpha0_mu hAlpha_nonneg
      hAlpha_le
  exact dvVariationalOneSidedOfTiltedRight (nu := nu) (mu := mu)
    (Z := fun x ↦ alpha * q x) hnu_mu hZ_nu hexp_mu hllr

/-- Energy form of the one-sided DV bound for a scaled selected test.

For SALD use sites, `q` is a squared velocity or residual norm.  This theorem
starts after the selected-test hypotheses have been supplied, applies the
compiled one-sided backend for `Z=alpha*q`, divides by `alpha > 0`, and
rewrites the log-mgf quotient as the supplied alpha-complexity density
`eAlpha`.  The Boucheron supremum equality from `appendix.tex:73-79` remains
source-cited.
-/

Scope and omitted-condition boundaries

• Only a one-sided bound for a selected admissible test is established. The full Donsker–Varadhan/Boucheron variational supremum equality remains separate; no source-fidelity verdict is made.
• No q≥0 or α>0 hypothesis is added. No arbitrary-test supremum is taken.

Divide the scaled entropy bound by its positive scale

AutoSamplingTheory.dvVariationalScaledTestEnergyBound · theorem · Teaching coverage

Statement

Under the probability, absolute-continuity and integrability assumptions below, let 0<α≤α₀ and let e_α=α⁻¹log∫exp(αq)dμ. Then ∫q dν≤α⁻¹(klDiv ν μ).toReal+e_α. Although q may represent an energy in an application, this theorem does not require q≥0.

All objects and hypotheses

• Ω is measurable; ν and μ are probability measures with explicit SigmaFinite μ and SigmaFinite ν instances.
• q:Ω→ℝ is ν-integrable; α,α₀,e_α∈ℝ with 0<α≤α₀; ν≪μ.
• exp(α₀q) is μ-integrable and llr(ν,μ) is ν-integrable.
• The supplied named value e_α equals α⁻¹ log∫exp(αq)dμ. Write K=(klDiv ν μ).toReal.

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 dvVariationalScaledTestEnergyBound {Ω : Type*} [MeasurableSpace Ω]
    (nu mu : Measure Ω) [IsProbabilityMeasure nu] [IsProbabilityMeasure mu]
    [SigmaFinite mu] [SigmaFinite nu]
    (q : Ω → Real) {alpha alpha0 eAlpha : Real}
    (hAlpha_pos : 0 < alpha) (hAlpha_le : alpha ≤ alpha0)
    (hnu_mu : nu ≪ mu)
    (hq_nu : Integrable q nu)
    (hexp_alpha0_mu : Integrable (fun x ↦ Real.exp (alpha0 * q x)) mu)
    (hllr : Integrable (llr nu mu) nu)
    (heAlpha : eAlpha =
      alpha⁻¹ * Real.log (∫ x, Real.exp (alpha * q x) ∂mu)) :
    (∫ x, q x ∂nu) ≤ alpha⁻¹ * (klDiv nu mu).toReal + eAlpha

theorem dvVariationalScaledTestEnergyBound {Ω : Type*} [MeasurableSpace Ω]
    (nu mu : Measure Ω) [IsProbabilityMeasure nu] [IsProbabilityMeasure mu]
    [SigmaFinite mu] [SigmaFinite nu]
    (q : Ω → Real) {alpha alpha0 eAlpha : Real}
    (hAlpha_pos : 0 < alpha) (hAlpha_le : alpha ≤ alpha0)
    (hnu_mu : nu ≪ mu)
    (hq_nu : Integrable q nu)
    (hexp_alpha0_mu : Integrable (fun x ↦ Real.exp (alpha0 * q x)) mu)
    (hllr : Integrable (llr nu mu) nu)
    (heAlpha : eAlpha =
      alpha⁻¹ * Real.log (∫ x, Real.exp (alpha * q x) ∂mu)) :
    (∫ x, q x ∂nu) ≤ alpha⁻¹ * (klDiv nu mu).toReal + eAlpha := by
  have hZ_nu : Integrable (fun x ↦ alpha * q x) nu := by
    simpa [smul_eq_mul] using hq_nu.const_mul alpha
  have hdv := dvVariationalOneSidedOfScaledTest (nu := nu) (mu := mu)
    (q := q) hAlpha_pos.le hAlpha_le hnu_mu hZ_nu hexp_alpha0_mu hllr
  have hscaledIntegral :
      (∫ x, alpha * q x ∂nu) = alpha * ∫ x, q x ∂nu := by
    rw [integral_const_mul]
  have hscaled :
      alpha * (∫ x, q x ∂nu) ≤
        (klDiv nu mu).toReal + Real.log (∫ x, Real.exp (alpha * q x) ∂mu) := by
    have hvar :
        alpha * (∫ x, q x ∂nu) -
            Real.log (∫ x, Real.exp (alpha * q x) ∂mu) ≤
          (klDiv nu mu).toReal := by
      simpa [hscaledIntegral] using hdv
    exact sub_le_iff_le_add.mp hvar
  have hdiv :
      alpha⁻¹ * (alpha * (∫ x, q x ∂nu)) ≤
        alpha⁻¹ * ((klDiv nu mu).toReal +
          Real.log (∫ x, Real.exp (alpha * q x) ∂mu)) := by
    exact mul_le_mul_of_nonneg_left hscaled (inv_nonneg.mpr hAlpha_pos.le)
  calc
    (∫ x, q x ∂nu) = alpha⁻¹ * (alpha * (∫ x, q x ∂nu)) := by
      field_simp [ne_of_gt hAlpha_pos]
    _ ≤ alpha⁻¹ * ((klDiv nu mu).toReal +
          Real.log (∫ x, Real.exp (alpha * q x) ∂mu)) := hdiv
    _ = alpha⁻¹ * (klDiv nu mu).toReal + eAlpha := by
      rw [heAlpha]
      ring

/-- Coefficient-preserving energy form of the selected scaled-test DV bound.

This is the local algebraic shape used before Gronwall in SALD proofs after a
nonnegative prefactor, such as `(1/2)*dot{s}(t)^(-1)`, multiplies the
post-DV energy estimate.
-/

Scope and omitted-condition boundaries

• Only a one-sided bound for a selected admissible test is established. The full Donsker–Varadhan/Boucheron variational supremum equality remains separate; no source-fidelity verdict is made.
• No nonnegativity of q is required. It does not construct a complexity bound or prove a later Grönwall estimate.

Preserve an external nonnegative coefficient in the energy bound

AutoSamplingTheory.dvVariationalScaledTestEnergyBoundWithCoeff · theorem · Teaching coverage

Statement

Under the complete scaled-energy assumptions below, let c≥0 be any real coefficient. Then c∫q dν≤(cα⁻¹)(klDiv ν μ).toReal+c e_α. The coefficient may be zero and is independent of the integration variable.

All objects and hypotheses

• Ω is measurable; ν and μ are probability measures with explicit SigmaFinite μ and SigmaFinite ν instances.
• q:Ω→ℝ is ν-integrable; α,α₀,e_α∈ℝ with 0<α≤α₀; ν≪μ.
• exp(α₀q) is μ-integrable and llr(ν,μ) is ν-integrable.
• The supplied named value e_α equals α⁻¹ log∫exp(αq)dμ. Write K=(klDiv ν μ).toReal.
• c=coeff is a real scalar with hcoeff:0≤c.

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 dvVariationalScaledTestEnergyBoundWithCoeff {Ω : Type*} [MeasurableSpace Ω]
    (nu mu : Measure Ω) [IsProbabilityMeasure nu] [IsProbabilityMeasure mu]
    [SigmaFinite mu] [SigmaFinite nu]
    (q : Ω → Real) {alpha alpha0 eAlpha coeff : Real}
    (hAlpha_pos : 0 < alpha) (hAlpha_le : alpha ≤ alpha0)
    (hcoeff : 0 ≤ coeff)
    (hnu_mu : nu ≪ mu)
    (hq_nu : Integrable q nu)
    (hexp_alpha0_mu : Integrable (fun x ↦ Real.exp (alpha0 * q x)) mu)
    (hllr : Integrable (llr nu mu) nu)
    (heAlpha : eAlpha =
      alpha⁻¹ * Real.log (∫ x, Real.exp (alpha * q x) ∂mu)) :
    coeff * (∫ x, q x ∂nu) ≤
      (coeff * alpha⁻¹) * (klDiv nu mu).toReal + coeff * eAlpha

theorem dvVariationalScaledTestEnergyBoundWithCoeff {Ω : Type*} [MeasurableSpace Ω]
    (nu mu : Measure Ω) [IsProbabilityMeasure nu] [IsProbabilityMeasure mu]
    [SigmaFinite mu] [SigmaFinite nu]
    (q : Ω → Real) {alpha alpha0 eAlpha coeff : Real}
    (hAlpha_pos : 0 < alpha) (hAlpha_le : alpha ≤ alpha0)
    (hcoeff : 0 ≤ coeff)
    (hnu_mu : nu ≪ mu)
    (hq_nu : Integrable q nu)
    (hexp_alpha0_mu : Integrable (fun x ↦ Real.exp (alpha0 * q x)) mu)
    (hllr : Integrable (llr nu mu) nu)
    (heAlpha : eAlpha =
      alpha⁻¹ * Real.log (∫ x, Real.exp (alpha * q x) ∂mu)) :
    coeff * (∫ x, q x ∂nu) ≤
      (coeff * alpha⁻¹) * (klDiv nu mu).toReal + coeff * eAlpha := by
  have hbase := dvVariationalScaledTestEnergyBound (nu := nu) (mu := mu)
    (q := q) hAlpha_pos hAlpha_le hnu_mu hq_nu hexp_alpha0_mu hllr heAlpha
  have hmul :
      coeff * (∫ x, q x ∂nu) ≤
        coeff * (alpha⁻¹ * (klDiv nu mu).toReal + eAlpha) := by
    exact mul_le_mul_of_nonneg_left hbase hcoeff
  calc
    coeff * (∫ x, q x ∂nu) ≤
        coeff * (alpha⁻¹ * (klDiv nu mu).toReal + eAlpha) := hmul
    _ = (coeff * alpha⁻¹) * (klDiv nu mu).toReal + coeff * eAlpha := by
      ring

/-- One-sided Donsker--Varadhan consequence from the tilted backend.

This is the form consumed by SALD after a selected test has supplied the
explicit Mathlib hypotheses.  It remains a one-sided theorem only; the
Boucheron supremum equality in `appendix.tex:73-79` stays source-cited.
-/

Scope and omitted-condition boundaries

• Only a one-sided bound for a selected admissible test is established. The full Donsker–Varadhan/Boucheron variational supremum equality remains separate; no source-fidelity verdict is made.
• A scalar coefficient such as a time-change factor must have its sign established by the caller. No Grönwall, convergence or time-change theorem is proved here.

Write the tilted-backend test bound in additive form

AutoSamplingTheory.dvVariationalTiltedRightOneSidedConsequence · theorem · Teaching coverage

Statement

For probability measures ν≪μ with the explicit sigma-finiteness hypotheses, if Z is ν-integrable, exp Z is μ-integrable and llr(ν,μ) is ν-integrable, then ∫Z dν≤(klDiv ν μ).toReal+log∫exp Z dμ. This is the additive form of the already proved selected-test inequality.

All objects and hypotheses

• α (or Ω) is an arbitrary measurable space; ν and μ are probability measures on that same space.
• Both SigmaFinite μ and SigmaFinite ν are explicitly present in the Lean signature; probability already supplies them, but they are not omitted here.
• ν≪μ; the chosen real test Z is ν-integrable; exp Z is μ-integrable; llr(ν,μ) is ν-integrable.
• Notation: ℓ=llr(ν,μ)=log((dν/dμ).toReal), M_Z=∫exp Z dμ, and K=(InformationTheory.klDiv ν μ).toReal.

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 dvVariationalTiltedRightOneSidedConsequence {α : Type*} [MeasurableSpace α]
    (nu mu : Measure α) [IsProbabilityMeasure nu] [IsProbabilityMeasure mu]
    [SigmaFinite mu] [SigmaFinite nu]
    (Z : α → Real)
    (hnu_mu : nu ≪ mu)
    (hZ_nu : Integrable Z nu)
    (hexp_mu : Integrable (fun x ↦ Real.exp (Z x)) mu)
    (hllr : Integrable (llr nu mu) nu) :
    (∫ x, Z x ∂nu) ≤
      (klDiv nu mu).toReal + Real.log (∫ x, Real.exp (Z x) ∂mu)

theorem dvVariationalTiltedRightOneSidedConsequence {α : Type*} [MeasurableSpace α]
    (nu mu : Measure α) [IsProbabilityMeasure nu] [IsProbabilityMeasure mu]
    [SigmaFinite mu] [SigmaFinite nu]
    (Z : α → Real)
    (hnu_mu : nu ≪ mu)
    (hZ_nu : Integrable Z nu)
    (hexp_mu : Integrable (fun x ↦ Real.exp (Z x)) mu)
    (hllr : Integrable (llr nu mu) nu) :
    (∫ x, Z x ∂nu) ≤
      (klDiv nu mu).toReal + Real.log (∫ x, Real.exp (Z x) ∂mu) := by
  exact dvVariationalOneSidedConsequenceScalar
    (dvVariationalOneSidedOfTiltedRight (nu := nu) (mu := mu) (Z := Z)
      hnu_mu hZ_nu hexp_mu hllr)

/-- Log-Sobolev implies KL-FI comparison as a reusable proof target. -/

Scope and omitted-condition boundaries

• Only a one-sided bound for a selected admissible test is established. The full Donsker–Varadhan/Boucheron variational supremum equality remains separate; no source-fidelity verdict is made.
• Additive-form reuse wrapper, not a new variational principle.

Record the remaining LSI-to-KL/Fisher proof target

AutoSamplingTheory.lsiToKlFiObligation · def · Teaching coverage

Statement

Given any source anchor, construct the proof-obligation record named probability.lsi_to_kl_fi with the text that an LSI constant c_LSI should imply KL(ρ‖π)≤FI(ρ‖π)/(2c_LSI). The record has obligation status. It does not prove the inequality or supply its missing analytic hypotheses.

All objects and hypotheses

• source:SourceAnchor is the sole input. No positive constant, measures, LSI witness, density regularity or admissible-test proof is passed.
• The returned ProofObligation uses its default empty dependency list and empty note.

Notation and interpretation

Analytic values versus metadata

Contracts and obligation/interface constructors store strings and status labels. They are not propositions asserting the written mathematics and supply no Lean proof of it.

\[\texttt{ProofObligation}\ne\text{proof of its statement string}\]

Construction and meaning

def lsiToKlFiObligation (source : SourceAnchor) : ProofObligation

def lsiToKlFiObligation (source : SourceAnchor) : ProofObligation where
  id := "probability.lsi_to_kl_fi"
  statement := "If pi satisfies LSI with constant c_LSI, then KL(rho || pi) <= FI(rho || pi)/(2*c_LSI)."
  source := source
  status := ProofStatus.obligation

end AutoSamplingTheory

Scope and omitted-condition boundaries

• Contracts and obligation/interface constructors store strings and status labels. They are not propositions asserting the written mathematics and supply no Lean proof of it.
• No LSI-to-KL/FI conclusion may be inferred from compiling or displaying this record.