Integrating a backward exponential derivative bound
AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.endpoint_le_of_deriv_le_exponential_kernel · theorem · Teaching coverage
Mathematical statement
A scalar interpolation starting at zero inherits the exact endpoint bound obtained by integrating its backward exponential derivative majorant.
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.
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)) * energyProof 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.
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].
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.
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.
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.
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.FunctionalInequalitiesScope 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.