Transfer a supplied weak derivative from samples to laws
AutoSamplingTheory.lawMapIntegralHasDerivAtOfSample · theorem · Teaching coverage
Mathematical 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.
Lean statement · lawMapIntegralHasDerivAtOfSample
The universal time hypotheses support equality of the entire two integral functions, while the derivative is asserted only at s₀.
Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.
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 s0Proof roadmap
- 1Identify both functions at every time
Apply the pushforward-integral identity separately at each s. Functional extensionality turns these pointwise equalities into equality of the two real functions.
- 2Transfer the existing derivative
Equal functions have the same derivative assertion at the same point. Replace G by F in the supplied derivative theorem.
Full assumptions and notation
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
1. Identify both functions at every time
Apply the pushforward-integral identity separately at each s. Functional extensionality turns these pointwise equalities into equality of the two real functions.
Corresponding Lean step
hfun; funext s; lawMapIntegral (hX s) (hφ s)
2. Transfer the existing derivative
Equal functions have the same derivative assertion at the same point. Replace G by F in the supplied derivative theorem.
Corresponding Lean step
simpa [hfun] using hderiv
Lean verification
The exact proof begins folded immediately after the mathematical argument; the statement is folded beside the claim above.
Lean proof · lawMapIntegralHasDerivAtOfSample
The proof first names the equality of functions, then rewrites the already supplied derivative. It supplies no pathwise derivative or domination estimate.
Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.
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 hderivScope 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.
Sources, dependencies, and reuse
Source and reuse
Samplinglib parents called
Mathlib API called (external library)
No direct Mathlib call recorded; see the Samplinglib parents.
Mathematical sources
- Exact existing ASTIS declaration and body — Directly read local source; not a new proof or source-fidelity verdict.
- AutoSamplingTheory.lawMapIntegral — Existing root ASTIS dependency; use its own adjacent teaching unit.
Samplinglib prose is not a quotation or a source-equivalence certificate. Definitions and aliases are explained as constructions, not counted as new mathematical proofs.