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.