Samplinglib mathematical lesson

Backward interpolation yields gradient contraction

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

Read this first

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.

\[\Phi'(u)=P_u(L\Gamma(q_u)-2\Gamma(q_u,Lq_u))\ge2\alpha\Phi(u)\Longrightarrow\Phi(s)\le\Phi(t)e^{-2\alpha(t-s)}\]

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.

Download module (.lean)

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

Exact module and namespace context

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.

\[L\Gamma(q_u)-2\Gamma(q_u,Lq_u)\ge2\alpha\Gamma(q_u)\]

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

\[\Phi'(u)\ge2\alpha\Phi(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.

\[\Phi(s)\le\Phi(t)e^{-2\alpha(t-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.

Download module (.lean)

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 AutoSamplingTheory

Exact module and namespace context

Scope 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

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.