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.