Samplinglib mathematical lesson

Curvature controls the interpolation derivative expression

AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.interpolationDerivative_lower_bound_of_expandedBakryEmery · theorem · Teaching coverage

Read this first

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).

\[\Gamma_2(f)\ge\alpha\Gamma(f)\Longrightarrow L\Gamma(f)-2\Gamma(f,Lf)\ge2\alpha\Gamma(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.

Download module (.lean)

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

Exact module and namespace context

Proof 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.

\[\alpha\Gamma(f)(x)\le\tfrac12(L\Gamma(f)(x)-\Gamma(f,Lf)(x)-\Gamma(f,Lf)(x))\]

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.

\[\Gamma(f,Lf)+\Gamma(f,Lf)=2\Gamma(f,Lf)\]

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.

\[2\alpha\Gamma(f)\le L\Gamma(f)-2\Gamma(f,Lf)\]

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.

Download module (.lean)

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 AutoSamplingTheory

Exact module and namespace context

Scope 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

AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.CarreDuChamp.carreDuChamp

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.