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.

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