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.