Curvature controls the interpolation derivative expression
AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.interpolationDerivative_lower_bound_of_expandedBakryEmery · theorem · Teaching coverage
Mathematical statement
Let L be a real-linear generator and suppose it satisfies CD(α,∞): αΓ(f)≤Γ₂(f). Expanding Γ₂ gives the pointwise lower bound LΓ(f)−2Γ(f,Lf)≥2αΓ(f).
Lean statement · interpolationDerivative_lower_bound_of_expandedBakryEmery
Lean exposes the arbitrary type X, linear generator, α>0, every curvature quantifier, the one-half normalization, the observable f, and the point x directly in the theorem signature.
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 interpolationDerivative_lower_bound_of_expandedBakryEmery
(generator : (X → ℝ) →ₗ[ℝ] (X → ℝ))
{alpha : ℝ} (_halpha : 0 < alpha)
(hcurvature : ∀ (g : X → ℝ) (y : X),
alpha * carreDuChamp generator g g y ≤
(2 : ℝ)⁻¹ *
(generator (carreDuChamp generator g g) y -
carreDuChamp generator g (generator g) y -
carreDuChamp generator g (generator g) y))
(f : X → ℝ) (x : X) :
2 * alpha * carreDuChamp generator f f x ≤
generator (carreDuChamp generator f f) x -
2 * carreDuChamp generator f (generator f) xProof roadmap
- 1Specialize the expanded curvature premise
At the chosen observable and point, the globally quantified hypothesis gives the exact one-half normalized inequality.
- 2Combine the repeated mixed terms
The two identical subtractions are exactly twice the mixed carré-du-champ term.
- 3Clear the factor one half
Multiply the specialized inequality by two and normalize the real arithmetic.
Full assumptions and notation
All objects and hypotheses
- The state space X is arbitrary.
- L is a real-linear map from real-valued observables on X to real-valued observables on X.
- The curvature parameter α is strictly positive.
- For every observable g and point y, the exact expanded inequality αΓ(g,g)(y)≤(1/2)(LΓ(g,g)(y)−Γ(g,Lg)(y)−Γ(g,Lg)(y)) holds.
- No semigroup or differentiability assumption is present.
Mathematical proof
1. Specialize the expanded curvature premise
At the chosen observable and point, the globally quantified hypothesis gives the exact one-half normalized inequality.
Corresponding Lean step
Specialize hcurvature to f and x.
2. Combine the repeated mixed terms
The two identical subtractions are exactly twice the mixed carré-du-champ term.
Corresponding Lean step
Real-ring normalization identifies the repeated terms.
3. Clear the factor one half
Multiply the specialized inequality by two and normalize the real arithmetic.
Corresponding Lean step
nlinarith closes the scalar real inequality.
Lean verification
The exact proof begins folded immediately after the mathematical argument; the statement is folded beside the claim above.
Lean proof · interpolationDerivative_lower_bound_of_expandedBakryEmery
The proof specializes the fully expanded curvature hypothesis and discharges the exact real-arithmetic consequence; no hidden definition is unfolded.
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 interpolationDerivative_lower_bound_of_expandedBakryEmery
(generator : (X → ℝ) →ₗ[ℝ] (X → ℝ))
{alpha : ℝ} (_halpha : 0 < alpha)
(hcurvature : ∀ (g : X → ℝ) (y : X),
alpha * carreDuChamp generator g g y ≤
(2 : ℝ)⁻¹ *
(generator (carreDuChamp generator g g) y -
carreDuChamp generator g (generator g) y -
carreDuChamp generator g (generator g) y))
(f : X → ℝ) (x : X) :
2 * alpha * carreDuChamp generator f f x ≤
generator (carreDuChamp generator f f) x -
2 * carreDuChamp generator f (generator f) x := by
have h := hcurvature f x
nlinarith
end StochasticProcesses
end TechnicalLemmas
end AutoSamplingTheoryScope and omitted-condition boundaries
- This is the algebraic curvature-to-derivative-expression step only. It does not construct a Markov semigroup, prove order preservation, establish the identity d/ds[P_s Γ(P_{t-s}f)]=2P_s Γ₂(P_{t-s}f), or justify generator-domain closure.
Sources, dependencies, and reuse
Source and reuse
Samplinglib parents called
Mathlib API called (external library)
- nlinarith
Mathematical sources
- Chewi, Definition 1.2.28 — Definition of the iterated carré du champ Γ₂.
- Chewi, Definition 1.2.29 — The CD(α,∞) inequality.
- Samplinglib compiled algebraic leaf — Exact pointwise consequence and proof.
Samplinglib prose is not a quotation or a source-equivalence certificate. Definitions and aliases are explained as constructions, not counted as new mathematical proofs.