Samplinglib mathematical lesson

Integrating a backward exponential derivative bound

AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.endpoint_le_of_deriv_le_exponential_kernel · theorem · Teaching coverage

Read this first

Mathematical statement

A scalar interpolation starting at zero inherits the exact endpoint bound obtained by integrating its backward exponential derivative majorant.

\[H'(s)\le q e^{-r(t-s)}E,\ H(0)=0\Longrightarrow H(t)\le\frac{q}{r}(1-e^{-rt})E\]

Lean statement · endpoint_le_of_deriv_le_exponential_kernel

All scalar quantities, interval scopes, and endpoint hypotheses 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 endpoint_le_of_deriv_le_exponential_kernel
    {H H' : ℝ → ℝ} {rate source t energy : ℝ}
    (hrate : 0 < rate) (ht : 0 ≤ t)
    (hH : ∀ s ∈ Icc (0 : ℝ) t, HasDerivAt H (H' s) s)
    (hzero : H 0 = 0)
    (hderiv : ∀ s ∈ Ioo (0 : ℝ) t,
      H' s ≤ source * Real.exp (-rate * (t - s)) * energy) :
    H t ≤ (source / rate) * (1 - Real.exp (-rate * t)) * energy

Exact module and namespace context

Proof roadmap

1Build the exact comparison primitive
Define B(s) from the integrated exponential kernel so that B(0)=0 and B'(s)=q e^{-r(t-s)}E.
2Compare derivatives
The assumed bound gives (B-H)'≥0, hence B-H is monotone on [0,t].
3Evaluate both endpoints
At zero both functions vanish; evaluating B at t gives the exact convolution factor.

Full assumptions and notation

All objects and hypotheses

r>0 and t≥0.
H has derivative H' at every point of [0,t].
The displayed upper derivative bound holds for 0<s<t.
q and E are arbitrary real scalars; their required order information is already encoded in the derivative inequality.

Mathematical proof

1. Build the exact comparison primitive

Define B(s) from the integrated exponential kernel so that B(0)=0 and B'(s)=q e^{-r(t-s)}E.

\[B(s)=\frac qr(e^{-r(t-s)}-e^{-rt})E\]

Corresponding Lean step

Differentiate Real.exp and cancel r using r>0.

2. Compare derivatives

The assumed bound gives (B-H)'≥0, hence B-H is monotone on [0,t].

\[B'(s)-H'(s)\ge0\]

Corresponding Lean step

Apply monotoneOn_of_deriv_nonneg on Icc 0 t.

3. Evaluate both endpoints

At zero both functions vanish; evaluating B at t gives the exact convolution factor.

\[B(t)=\frac qr(1-e^{-rt})E\]

Corresponding Lean step

Use Real.exp_zero and normalize the endpoint algebra.

Lean verification

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

Lean proof · endpoint_le_of_deriv_le_exponential_kernel

The proof differentiates the exact comparison primitive and applies Mathlib's derivative monotonicity theorem.

Download module (.lean)

theorem endpoint_le_of_deriv_le_exponential_kernel
    {H H' : ℝ → ℝ} {rate source t energy : ℝ}
    (hrate : 0 < rate) (ht : 0 ≤ t)
    (hH : ∀ s ∈ Icc (0 : ℝ) t, HasDerivAt H (H' s) s)
    (hzero : H 0 = 0)
    (hderiv : ∀ s ∈ Ioo (0 : ℝ) t,
      H' s ≤ source * Real.exp (-rate * (t - s)) * energy) :
    H t ≤ (source / rate) * (1 - Real.exp (-rate * t)) * energy := by
  let B : ℝ → ℝ := fun s =>
    (source / rate) *
      (Real.exp (-rate * (t - s)) - Real.exp (-rate * t)) * energy
  have hB : ∀ s : ℝ,
      HasDerivAt B
        (source * Real.exp (-rate * (t - s)) * energy) s := by
    intro s
    have hinner : HasDerivAt (fun u : ℝ => -rate * (t - u)) rate s := by
      have hcoeff : -(-rate) = rate := by ring
      simpa only [Pi.sub_apply, id_eq, zero_sub, mul_neg, mul_one, hcoeff] using
        (((hasDerivAt_const s t).sub (hasDerivAt_id s)).const_mul (-rate))
    have hexp := (Real.hasDerivAt_exp (-rate * (t - s))).comp s hinner
    have hsub := hexp.sub_const (Real.exp (-rate * t))
    have hmul := (hsub.const_mul (source / rate)).mul_const energy
    convert hmul using 1 <;> try rfl
    field_simp [ne_of_gt hrate]
  have hmono : MonotoneOn (fun s => B s - H s) (Icc (0 : ℝ) t) := by
    apply monotoneOn_of_deriv_nonneg (convex_Icc (0 : ℝ) t)
    · exact continuousOn_of_forall_continuousAt fun s hs =>
        ((hB s).sub (hH s hs)).continuousAt
    · intro s hs
      exact ((hB s).sub (hH s (interior_subset hs))).differentiableAt.differentiableWithinAt
    · intro s hs
      change 0 ≤ deriv (B - H) s
      rw [((hB s).sub (hH s (interior_subset hs))).deriv]
      exact sub_nonneg.mpr (hderiv s (by simpa only [interior_Icc] using hs))
  have hend := hmono ⟨le_rfl, ht⟩ ⟨ht, le_rfl⟩ ht
  dsimp [B] at hend
  have hBzero :
      (source / rate) *
        (Real.exp (-rate * (t - 0)) - Real.exp (-rate * t)) * energy = 0 := by
    ring_nf
  rw [hBzero, hzero] at hend
  have hBt :
      (source / rate) *
        (Real.exp (-rate * (t - t)) - Real.exp (-rate * t)) * energy =
      (source / rate) * (1 - Real.exp (-rate * t)) * energy := by
    rw [sub_self, mul_zero, Real.exp_zero]
  rw [hBt] at hend
  exact sub_nonneg.mp (by simpa only [sub_self] using hend)

end

end AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities

Exact module and namespace context

Scope and omitted-condition boundaries

This is the real-analysis leaf after a semigroup has supplied its entropy-production and gradient-contraction estimates.

Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

monotoneOn_of_deriv_nonneg
Real.hasDerivAt_exp

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.