Backward interpolation yields gradient contraction
AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.backwardInterpolation_contraction_of_expandedBakryEmery · theorem · Teaching coverage
Mathematical statement
Let P_u be positive real-linear evolution operators and q_u a family of observables. If α>0, the expanded CD(α,∞) inequality holds, Φ(u)=P_uΓ(q_u) is continuous, and its exact right derivative is P_u(LΓ(q_u)−2Γ(q_u,Lq_u)), then Φ(s)≤Φ(t)e^{-2α(t-s)} for s≤t.
Lean statement · backwardInterpolation_contraction_of_expandedBakryEmery
Every curvature, positivity, continuity, derivative, and endpoint premise is explicit. The evolution and orbit are arbitrary functions of real time; no semigroup law is inferred.
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 backwardInterpolation_contraction_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))
(evolution : ℝ → (X → ℝ) →ₗ[ℝ] (X → ℝ))
(orbit : ℝ → X → ℝ) (x : X)
(hpositive : ∀ u : ℝ, ∀ {f g : X → ℝ},
(∀ y, f y ≤ g y) → ∀ z, evolution u f z ≤ evolution u g z)
(hcontinuous : Continuous (fun u =>
evolution u (carreDuChamp generator (orbit u) (orbit u)) x))
(hderiv : ∀ u : ℝ,
HasDerivWithinAt
(fun v => evolution v
(carreDuChamp generator (orbit v) (orbit v)) x)
(evolution u
(generator (carreDuChamp generator (orbit u) (orbit u)) -
(2 : ℝ) • carreDuChamp generator (orbit u) (generator (orbit u))) x)
(Ici u) u)
{s t : ℝ} (hst : s ≤ t) :
evolution s (carreDuChamp generator (orbit s) (orbit s)) x ≤
evolution t (carreDuChamp generator (orbit t) (orbit t)) x *
Real.exp (-(2 * alpha) * (t - s))Proof roadmap
- 1Turn curvature into a pointwise generator bound
The expanded CD inequality gives LΓ(q_u)−2Γ(q_u,Lq_u)≥2αΓ(q_u) at every state.
- 2Push the inequality through the positive linear evolution
Order preservation maps the pointwise bound through P_u; linearity pulls out 2α. The supplied derivative identity then gives Φ'(u)≥2αΦ(u).
- 3Read the backward interpolation endpoints
The scalar comparison theorem converts the derivative lower bound into exponential contraction from t back to s.
Full assumptions and notation
All objects and hypotheses
- X is arbitrary and L is real-linear on real-valued observables.
- The curvature parameter α is strictly positive and the fully expanded diagonal CD inequality holds for every observable and point.
- Each P_u is real-linear and preserves pointwise order.
- The scalar interpolation Φ(u)=P_uΓ(q_u)(x) is continuous.
- At every u, its exact right derivative within [u,∞) is P_u(LΓ(q_u)−2Γ(q_u,Lq_u))(x).
- The endpoints satisfy s≤t.
Mathematical proof
1. Turn curvature into a pointwise generator bound
The expanded CD inequality gives LΓ(q_u)−2Γ(q_u,Lq_u)≥2αΓ(q_u) at every state.
Corresponding Lean step
Apply interpolationDerivative_lower_bound_of_expandedBakryEmery to q_u.
2. Push the inequality through the positive linear evolution
Order preservation maps the pointwise bound through P_u; linearity pulls out 2α. The supplied derivative identity then gives Φ'(u)≥2αΦ(u).
Corresponding Lean step
Use hpositive, then simplify with the linear-map laws.
3. Read the backward interpolation endpoints
The scalar comparison theorem converts the derivative lower bound into exponential contraction from t back to s.
Corresponding Lean step
Apply backward_interpolation_contraction_of_growth with rate 2α.
Lean verification
The exact proof begins folded immediately after the mathematical argument; the statement is folded beside the claim above.
Lean proof · backwardInterpolation_contraction_of_expandedBakryEmery
The proof derives the pointwise curvature bound, transfers it through each positive linear operator, and invokes the independently verified scalar backward interpolation theorem.
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 backwardInterpolation_contraction_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))
(evolution : ℝ → (X → ℝ) →ₗ[ℝ] (X → ℝ))
(orbit : ℝ → X → ℝ) (x : X)
(hpositive : ∀ u : ℝ, ∀ {f g : X → ℝ},
(∀ y, f y ≤ g y) → ∀ z, evolution u f z ≤ evolution u g z)
(hcontinuous : Continuous (fun u =>
evolution u (carreDuChamp generator (orbit u) (orbit u)) x))
(hderiv : ∀ u : ℝ,
HasDerivWithinAt
(fun v => evolution v
(carreDuChamp generator (orbit v) (orbit v)) x)
(evolution u
(generator (carreDuChamp generator (orbit u) (orbit u)) -
(2 : ℝ) • carreDuChamp generator (orbit u) (generator (orbit u))) x)
(Ici u) u)
{s t : ℝ} (hst : s ≤ t) :
evolution s (carreDuChamp generator (orbit s) (orbit s)) x ≤
evolution t (carreDuChamp generator (orbit t) (orbit t)) x *
Real.exp (-(2 * alpha) * (t - s)) := by
apply backward_interpolation_contraction_of_growth hcontinuous hderiv ?_ hst
intro u
let gamma : X → ℝ := carreDuChamp generator (orbit u) (orbit u)
let mixed : X → ℝ :=
carreDuChamp generator (orbit u) (generator (orbit u))
have hpointwise : ∀ y,
((2 * alpha) • gamma) y ≤
(generator gamma - (2 : ℝ) • mixed) y := by
intro y
simpa [gamma, mixed] using
interpolationDerivative_lower_bound_of_expandedBakryEmery
generator halpha hcurvature (orbit u) y
have hmapped := hpositive u hpointwise x
simpa [gamma, mixed] using hmapped
end
end StochasticProcesses
end TechnicalLemmas
end AutoSamplingTheoryScope and omitted-condition boundaries
- The theorem assumes rather than proves the exact derivative identity, positivity, continuity, and domain closure for a concrete semigroup. It does not construct a diffusion or identify a concrete generator.
Sources, dependencies, and reuse
Source and reuse
Samplinglib parents called
AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.interpolationDerivative_lower_bound_of_expandedBakryEmeryAutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.SemigroupDecay.backward_interpolation_contraction_of_growth
Mathlib API called (external library)
- LinearMap.map_smul
- HasDerivWithinAt
- Continuous
- Real.exp
Mathematical sources
- Chewi, Definitions 1.2.28–1.2.29 — Γ₂ and CD(α,∞) background for the curvature step.
- Samplinglib compiled abstract adapter — Exact positivity, derivative, and endpoint composition.
Samplinglib prose is not a quotation or a source-equivalence certificate. Definitions and aliases are explained as constructions, not counted as new mathematical proofs.