A dominated derivative for a named law path
AutoSamplingTheory.lawIntegralHasDerivAtOfMeasureMapEqAndDominated · theorem · Teaching coverage
Mathematical 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₀.
Lean statement · lawIntegralHasDerivAtOfMeasureMapEqAndDominated
The extra path ρ changes the name of the law, not the analytic assumptions. Every dominated-differentiation condition is still explicitly required.
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 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 s0Proof roadmap
- 1Rewrite the test's measurability measure
The equality of named and image laws makes the all-time test measurability hypothesis match the dominated mapped-law theorem.
- 2Reuse dominated law differentiation
Pass the complete neighborhood, base-integrability, derivative-measurability, uniform bound, path-derivative and derivative-value data to the established mapped-law theorem.
- 3Restore the named path
Equality at every time identifies the real integral functions, hence transfers the derivative.
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.
- ρ:ℝ→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
1. Rewrite the test's measurability measure
The equality of named and image laws makes the all-time test measurability hypothesis match the dominated mapped-law theorem.
Corresponding Lean step
hφMap
2. Reuse dominated law differentiation
Pass the complete neighborhood, base-integrability, derivative-measurability, uniform bound, path-derivative and derivative-value data to the established mapped-law theorem.
Corresponding Lean step
lawMapIntegralHasDerivAtOfDominated hX hφMap ...
3. Restore the named path
Equality at every time identifies the real integral functions, hence transfers the derivative.
Corresponding Lean step
hfun; simpa [hfun] using hmap
Lean verification
The exact proof begins folded immediately after the mathematical argument; the statement is folded beside the claim above.
Lean proof · lawIntegralHasDerivAtOfMeasureMapEqAndDominated
The proof is a named-law reuse wrapper around the dominated derivative theorem; it rewrites the measure in measurability and in the final integral function.
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 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 hmapScope 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.
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.lawMapIntegralHasDerivAtOfDominated — 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.