Dissipation with forcing converges to a floor
AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.SemigroupDecay.forced_exponential_decay_of_scaled_dissipation_from · theorem · Teaching coverage
Mathematical statement
Let an energy curve have the exact right derivative E'(u)=-qD(u). If r>0 and rE(u)≤qD(u)+b at every time, then between any s≤t the energy is bounded by the exponential interpolation between E(s) and the forcing floor b/r.
Lean statement · forced_exponential_decay_of_scaled_dissipation_from
Lean keeps the dissipation scale q, decay rate r, forcing b, curve, and both endpoint times 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 forced_exponential_decay_of_scaled_dissipation_from
{scale rate forcing : ℝ} (hrate : 0 < rate)
(curve : DissipationCurve scale)
(hcoercive : ∀ u : ℝ,
rate * curve.energy u ≤ scale * curve.dissipation u + forcing)
{s t : ℝ} (hst : s ≤ t) :
curve.energy t ≤
curve.energy s * Real.exp (-rate * (t - s)) +
(forcing / rate) * (1 - Real.exp (-rate * (t - s)))Proof roadmap
- 1Convert coercivity into a differential inequality
Negating the forced coercivity inequality and using the derivative identity gives E'(u)≤-rE(u)+b.
- 2Apply one-sided Grönwall
Mathlib's right-slope Grönwall theorem applies directly because the curve is continuous and the exact right derivative controls every right slope.
- 3Expose the forcing floor
Since r is nonzero, unfold the closed Grönwall expression and rewrite b/(-r)(e^{-rΔ}-1) as (b/r)(1-e^{-rΔ}).
Full assumptions and notation
All objects and hypotheses
- The energy curve is continuous on the real line.
- At each time u, its right derivative within [u,∞) is exactly -qD(u).
- The decay rate r is strictly positive.
- The forced coercivity inequality rE(u)≤qD(u)+b holds for every real u.
- The terminal time satisfies s≤t.
Mathematical proof
1. Convert coercivity into a differential inequality
Negating the forced coercivity inequality and using the derivative identity gives E'(u)≤-rE(u)+b.
Corresponding Lean step
The proof combines neg_le_neg (hcoercive u) with linear arithmetic.
2. Apply one-sided Grönwall
Mathlib's right-slope Grönwall theorem applies directly because the curve is continuous and the exact right derivative controls every right slope.
Corresponding Lean step
Use le_gronwallBound_of_liminf_deriv_right_le with K=-r and ε=b.
3. Expose the forcing floor
Since r is nonzero, unfold the closed Grönwall expression and rewrite b/(-r)(e^{-rΔ}-1) as (b/r)(1-e^{-rΔ}).
Corresponding Lean step
Unfold gronwallBound; field_simp and ring verify the scalar identity.
Lean verification
The exact proof begins folded immediately after the mathematical argument; the statement is folded beside the claim above.
Lean proof · forced_exponential_decay_of_scaled_dissipation_from
The proof is a direct specialization of Mathlib's one-sided Grönwall theorem, followed by exact field algebra.
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 forced_exponential_decay_of_scaled_dissipation_from
{scale rate forcing : ℝ} (hrate : 0 < rate)
(curve : DissipationCurve scale)
(hcoercive : ∀ u : ℝ,
rate * curve.energy u ≤ scale * curve.dissipation u + forcing)
{s t : ℝ} (hst : s ≤ t) :
curve.energy t ≤
curve.energy s * Real.exp (-rate * (t - s)) +
(forcing / rate) * (1 - Real.exp (-rate * (t - s))) := by
have hbound : ∀ x ∈ Ico s t,
-scale * curve.dissipation x ≤
(-rate) * curve.energy x + forcing := by
intro x _hx
have hneg := neg_le_neg (hcoercive x)
linarith
have hgronwall :=
le_gronwallBound_of_liminf_deriv_right_le
(f := curve.energy)
(f' := fun x => -scale * curve.dissipation x)
(δ := curve.energy s)
(K := -rate)
(ε := forcing)
(a := s)
(b := t)
curve.energy_continuous.continuousOn
(fun x _hx r hr => by
simpa [slope] using
(curve.energy_hasDerivWithinAt x).liminf_right_slope_le hr)
le_rfl
hbound
t
⟨hst, le_rfl⟩
rw [gronwallBound] at hgronwall
simp only [if_neg (neg_ne_zero.mpr hrate.ne')] at hgronwall
calc
curve.energy t ≤
curve.energy s * Real.exp (-rate * (t - s)) +
forcing / -rate *
(Real.exp (-rate * (t - s)) - 1) := hgronwall
_ = curve.energy s * Real.exp (-rate * (t - s)) +
(forcing / rate) *
(1 - Real.exp (-rate * (t - s))) := by
field_simp [hrate.ne']
ring
end
end SemigroupDecay
end FunctionalInequalities
end TechnicalLemmas
end AutoSamplingTheoryScope and omitted-condition boundaries
- The theorem does not construct a semigroup or prove a Bakry–Émery gradient identity. It consumes an exact right-derivative dissipation law and a forced coercivity inequality.
Sources, dependencies, and reuse
Source and reuse
Samplinglib parents called
Mathlib API called (external library)
- le_gronwallBound_of_liminf_deriv_right_le
- HasDerivWithinAt.liminf_right_slope_le
- gronwallBound
Mathematical sources
- Mathlib one-sided Grönwall theorem — The right-slope comparison theorem and the closed `gronwallBound` formula.
- Samplinglib compiled specialization — Exact forced dissipation 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.