BakryEmeryInterpolation: mathematical reading route

Read the statements and derivations in source order. Every result has its own optional Lean statement and proof. Source assumptions, library reuse and unproved boundaries are kept explicit.

Backward interpolation turns growth into contraction
Interval Bakry–Émery growth gives backward contraction

Samplinglib mathematical lesson

Backward interpolation turns growth into contraction

AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.SemigroupDecay.backward_interpolation_contraction_of_growth · theorem · Teaching coverage

Read this first

Mathematical statement

Let Φ be a continuous scalar interpolation with an exact right derivative. If Φ'(u)≥rΦ(u) at every time, then reading the interpolation from s to t gives Φ(s)≤Φ(t)e^{-r(t-s)} for every s≤t.

\[\Phi'(u)\ge r\Phi(u)\Longrightarrow \Phi(s)\le \Phi(t)e^{-r(t-s)}\]

Lean statement · backward_interpolation_contraction_of_growth

Lean records the interpolation, its derivative function, the rate, and both endpoint times explicitly.

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 backward_interpolation_contraction_of_growth
    {interpolation interpolation' : ℝ → ℝ} {rate s t : ℝ}
    (hcontinuous : Continuous interpolation)
    (hderiv : ∀ u : ℝ,
      HasDerivWithinAt interpolation (interpolation' u) (Ici u) u)
    (hgrowth : ∀ u : ℝ,
      rate * interpolation u ≤ interpolation' u)
    (hst : s ≤ t) :
    interpolation s ≤
      interpolation t * Real.exp (-rate * (t - s))

Exact module and namespace context

Proof roadmap

1Reverse the inequality by negating the curve
For g=-Φ, the lower growth bound becomes the upper differential inequality g'≤rg required by one-sided Grönwall.
2Apply one-sided Grönwall between the two endpoints
The comparison theorem gives -Φ(t)≤-Φ(s)e^{r(t-s)}, equivalently Φ(s)e^{r(t-s)}≤Φ(t).
3Move the exponential to the terminal side
Multiply by the positive inverse exponential and use e^{rΔ}e^{-rΔ}=1.

Full assumptions and notation

All objects and hypotheses

Φ and its supplied derivative are real-valued on the whole real line.
Φ is continuous.
At every u, the right derivative within [u,∞) is exactly Φ'(u).
The lower differential inequality rΦ(u)≤Φ'(u) holds at every real u.
The endpoints satisfy s≤t.
No sign condition on Φ or r is required.

Mathematical proof

1. Reverse the inequality by negating the curve

For g=-Φ, the lower growth bound becomes the upper differential inequality g'≤rg required by one-sided Grönwall.

\[g=-\Phi,\qquad g'=-\Phi'\le-r\Phi=rg\]

Corresponding Lean step

Negate hgrowth; HasDerivWithinAt.neg supplies the exact right derivative of g.

2. Apply one-sided Grönwall between the two endpoints

The comparison theorem gives -Φ(t)≤-Φ(s)e^{r(t-s)}, equivalently Φ(s)e^{r(t-s)}≤Φ(t).

\[\Phi(s)e^{r(t-s)}\le\Phi(t)\]

Corresponding Lean step

Use le_gronwallBound_of_liminf_deriv_right_le, then gronwallBound_ε0.

3. Move the exponential to the terminal side

Multiply by the positive inverse exponential and use e^{rΔ}e^{-rΔ}=1.

\[\Phi(s)\le\Phi(t)e^{-r(t-s)}\]

Corresponding Lean step

Use Real.exp_nonneg, Real.exp_add, and exact ring normalization of the exponents.

Lean verification

The exact proof begins folded immediately after the mathematical argument; the statement is folded beside the claim above.

Lean proof · backward_interpolation_contraction_of_growth

The proof applies Mathlib's one-sided Grönwall theorem to the negated interpolation and then cancels the positive exponential exactly.

Download module (.lean)

theorem backward_interpolation_contraction_of_growth
    {interpolation interpolation' : ℝ → ℝ} {rate s t : ℝ}
    (hcontinuous : Continuous interpolation)
    (hderiv : ∀ u : ℝ,
      HasDerivWithinAt interpolation (interpolation' u) (Ici u) u)
    (hgrowth : ∀ u : ℝ,
      rate * interpolation u ≤ interpolation' u)
    (hst : s ≤ t) :
    interpolation s ≤
      interpolation t * Real.exp (-rate * (t - s)) := by
  have hbound : ∀ x ∈ Ico s t,
      -interpolation' x ≤ rate * (-interpolation x) + 0 := by
    intro x _hx
    have hneg := neg_le_neg (hgrowth x)
    simpa [neg_mul] using hneg
  have hgronwall :=
    le_gronwallBound_of_liminf_deriv_right_le
      (f := fun x => -interpolation x)
      (f' := fun x => -interpolation' x)
      (δ := -interpolation s)
      (K := rate)
      (ε := 0)
      (a := s)
      (b := t)
      hcontinuous.neg.continuousOn
      (fun x _hx r hr => by
        simpa [slope] using ((hderiv x).neg.liminf_right_slope_le hr))
      le_rfl
      hbound
      t
      ⟨hst, le_rfl⟩
  rw [gronwallBound_ε0] at hgronwall
  have hexponential_growth :
      interpolation s * Real.exp (rate * (t - s)) ≤ interpolation t := by
    linarith
  have hscaled := mul_le_mul_of_nonneg_right hexponential_growth
    (Real.exp_nonneg (-rate * (t - s)))
  have hinverse :
      Real.exp (rate * (t - s)) * Real.exp (-rate * (t - s)) = 1 := by
    rw [← Real.exp_add]
    have hzero : rate * (t - s) + -rate * (t - s) = 0 := by ring
    rw [hzero, Real.exp_zero]
  calc
    interpolation s =
        (interpolation s * Real.exp (rate * (t - s))) *
          Real.exp (-rate * (t - s)) := by
      rw [mul_assoc, hinverse, mul_one]
    _ ≤ interpolation t * Real.exp (-rate * (t - s)) := hscaled

Exact module and namespace context

Scope and omitted-condition boundaries

The theorem is only the scalar endpoint comparison. It does not build a Markov semigroup, identify Φ with P_s Γ(P_{t-s}f), prove its derivative formula, or derive Γ₂≥κΓ for a concrete generator.

Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

le_gronwallBound_of_liminf_deriv_right_le
HasDerivWithinAt.neg
HasDerivWithinAt.liminf_right_slope_le
gronwallBound_ε0
Real.exp_add

Mathematical sources

Mathlib one-sided Grönwall theorem — The scalar comparison used after negating the interpolation.
Samplinglib compiled interpolation leaf — Exact endpoint contraction statement 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.

Samplinglib mathematical lesson

Interval Bakry–Émery growth gives backward contraction

AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.SemigroupDecay.backward_endpoint_contraction_of_growth_on_Icc · theorem · Teaching coverage

Read this first

Mathematical statement

On an ordered interval [s,t], a differentiable scalar interpolation whose derivative dominates r times its value satisfies the exact backward endpoint contraction.

\[r\Phi(u)\le\Phi'(u)\ (s<u<t)\Longrightarrow\Phi(s)\le\Phi(t)e^{-r(t-s)}\]

Lean statement · backward_endpoint_contraction_of_growth_on_Icc

The closed and open interval scopes, exact derivative witnesses, endpoint order, and constants are explicit.

Download module (.lean)

theorem backward_endpoint_contraction_of_growth_on_Icc
    {interpolation interpolation' : ℝ → ℝ} {rate s t : ℝ}
    (hst : s ≤ t)
    (hinterpolation : ∀ u ∈ Icc s t,
      HasDerivAt interpolation (interpolation' u) u)
    (hgrowth : ∀ u ∈ Ioo s t,
      rate * interpolation u ≤ interpolation' u) :
    interpolation s ≤
      interpolation t * Real.exp (-rate * (t - s))

Exact module and namespace context

Proof roadmap

1Attach the inverse exponential weight
Multiply the interpolation by the factor that cancels growth at rate r.
2Show the weighted derivative is nonnegative
The derivative bound makes both factors in W' nonnegative.
3Compare the endpoints
Derivative monotonicity gives W(s)≤W(t); evaluating the exponential weight yields the desired contraction.

Full assumptions and notation

All objects and hypotheses

s≤t.
Φ has the supplied genuine two-sided derivative Φ' at every point of [s,t].
rΦ(u)≤Φ'(u) for every u in (s,t).
No sign condition on Φ or r is required; s=t is allowed.

Mathematical proof

1. Attach the inverse exponential weight

Multiply the interpolation by the factor that cancels growth at rate r.

\[W(u)=\Phi(u)e^{-r(u-s)}\]

Corresponding Lean step

Differentiate the product using Real.hasDerivAt_exp.

2. Show the weighted derivative is nonnegative

The derivative bound makes both factors in W' nonnegative.

\[W'(u)=(\Phi'(u)-r\Phi(u))e^{-r(u-s)}\ge0\]

Corresponding Lean step

Use sub_nonneg and positivity of Real.exp.

3. Compare the endpoints

Derivative monotonicity gives W(s)≤W(t); evaluating the exponential weight yields the desired contraction.

\[\Phi(s)\le\Phi(t)e^{-r(t-s)}\]

Corresponding Lean step

Apply monotoneOn_of_deriv_nonneg on Icc s t and simplify both endpoints.

Lean verification

The exact proof begins folded immediately after the mathematical argument; the statement is folded beside the claim above.

Lean proof · backward_endpoint_contraction_of_growth_on_Icc

The proof makes the exponentially weighted interpolation monotone and evaluates it at the two endpoints.

Download module (.lean)

theorem backward_endpoint_contraction_of_growth_on_Icc
    {interpolation interpolation' : ℝ → ℝ} {rate s t : ℝ}
    (hst : s ≤ t)
    (hinterpolation : ∀ u ∈ Icc s t,
      HasDerivAt interpolation (interpolation' u) u)
    (hgrowth : ∀ u ∈ Ioo s t,
      rate * interpolation u ≤ interpolation' u) :
    interpolation s ≤
      interpolation t * Real.exp (-rate * (t - s)) := by
  let weighted : ℝ → ℝ := fun u =>
    interpolation u * Real.exp (-rate * (u - s))
  have hweighted : ∀ u ∈ Icc s t,
      HasDerivAt weighted
        ((interpolation' u - rate * interpolation u) *
          Real.exp (-rate * (u - s))) u := by
    intro u hu
    have hinner :
        HasDerivAt (fun v : ℝ => -rate * (v - s)) (-rate) u := by
      simpa using ((hasDerivAt_id u).sub_const s).const_mul (-rate)
    have hexp := (Real.hasDerivAt_exp (-rate * (u - s))).comp u hinner
    have hmul := (hinterpolation u hu).mul hexp
    change HasDerivAt
      (fun v => interpolation v * Real.exp (-rate * (v - s)))
      ((interpolation' u - rate * interpolation u) *
        Real.exp (-rate * (u - s))) u
    exact hmul.congr_deriv (by
      simp only [Function.comp_apply]
      ring)
  have hmono : MonotoneOn weighted (Icc s t) := by
    apply monotoneOn_of_deriv_nonneg (convex_Icc s t)
    · exact continuousOn_of_forall_continuousAt fun u hu =>
        (hweighted u hu).continuousAt
    · intro u hu
      exact (hweighted u (interior_subset hu)).differentiableAt.differentiableWithinAt
    · intro u hu
      rw [(hweighted u (interior_subset hu)).deriv]
      exact mul_nonneg (sub_nonneg.mpr
        (hgrowth u (by simpa only [interior_Icc] using hu)))
        (Real.exp_nonneg _)
  have hend := hmono ⟨le_rfl, hst⟩ ⟨hst, le_rfl⟩ hst
  simpa only [weighted, sub_self, mul_zero, Real.exp_zero, mul_one] using hend

end

end SemigroupDecay
end FunctionalInequalities
end TechnicalLemmas
end AutoSamplingTheory

Exact module and namespace context

Scope and omitted-condition boundaries

This scalar theorem does not build a Markov semigroup or prove its carré-du-champ derivative, Γ₂ curvature bound, or terminal energy identity.

Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

monotoneOn_of_deriv_nonneg
Real.hasDerivAt_exp
interior_Icc

Mathematical sources

Samplinglib compiled source — Exact statement 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.