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.