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.