AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.SemigroupDecay

- Chewi's differential Gronwall lemma on `[0, T]`. The source assumes a differentiable scalar function satisfying `g' t ≤ c * g t`. Mathlib's one-sided Gronwall theorem accepts the weaker right-slope formulation; ordinary differentiability supplies that hypothesis.

theorem chewi_lemma_1_2_20
    {T c : ℝ} (_hT : 0 < T) (g : ℝ → ℝ)
    (hg : Differentiable ℝ g)
    (hbound : ∀ t ∈ Icc (0 : ℝ) T, deriv g t ≤ c * g t)
    {t : ℝ} (ht : t ∈ Icc (0 : ℝ) T) :
    g t ≤ g 0 * Real.exp (c * t) := by
  have hgronwall :=
    le_gronwallBound_of_liminf_deriv_right_le
      (f := g)
      (f' := deriv g)
      (δ := g 0)
      (K := c)
      (ε := 0)
      (a := 0)
      (b := T)
      hg.continuous.continuousOn
      (fun x _ r hr =>
        (hg x).hasDerivAt.hasDerivWithinAt.liminf_right_slope_le hr)
      le_rfl
      (fun x hx => by
        simpa using hbound x ⟨hx.1, le_of_lt hx.2⟩)
      t
      ht
  rw [gronwallBound_ε0, sub_zero] at hgronwall
  exact hgronwall

/-- A scalar energy/dissipation curve with an exact right-derivative identity.

`scale` records the coefficient in
`d/dt energy(t) = -scale * dissipation(t)`. The derivative is taken within
`[t, ∞)`, matching semigroups defined by nonnegative time increments. -/

AutoSamplingTheory/TechnicalLemmas/FunctionalInequalities/SemigroupDecay.lean:38published source at 77184245109aOpen detailed card

- A scalar energy/dissipation curve with an exact right-derivative identity. `scale` records the coefficient in `d/dt energy(t) = -scale * dissipation(t)`. The derivative is taken within `[t, ∞)`, matching semigroups defined by nonnegative time increments.

structure DissipationCurve (scale : ℝ) where
  energy : ℝ → ℝ
  dissipation : ℝ → ℝ
  energy_continuous : Continuous energy
  energy_hasDerivWithinAt :
    ∀ t : ℝ,
      HasDerivWithinAt energy (-scale * dissipation t) (Ici t) t

/-- Coercivity plus exact dissipation gives exponential decay between any two
times `s ≤ t`. -/

AutoSamplingTheory/TechnicalLemmas/FunctionalInequalities/SemigroupDecay.lean:69published source at 77184245109a

- Coercivity plus exact dissipation gives exponential decay between any two times `s ≤ t`.

theorem exponential_decay_of_scaled_dissipation_from
    {scale rate : ℝ} (curve : DissipationCurve scale)
    (hcoercive : ∀ u : ℝ,
      rate * curve.energy u ≤ scale * curve.dissipation u)
    {s t : ℝ} (hst : s ≤ t) :
    curve.energy t ≤
      curve.energy s * Real.exp (-rate * (t - s)) := by
  have hbound : ∀ x ∈ Ico s t,
      -scale * curve.dissipation x ≤
        (-rate) * curve.energy x + 0 := by
    intro x hx
    have hneg := neg_le_neg (hcoercive x)
    simpa [neg_mul] using hneg
  have hgronwall :=
    le_gronwallBound_of_liminf_deriv_right_le
      (f := curve.energy)
      (f' := fun x => -scale * curve.dissipation x)
      (δ := curve.energy s)
      (K := -rate)
      (ε := 0)
      (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_ε0] at hgronwall
  exact hgronwall

/-- A coercive inequality along a dissipation curve implies exponential decay
from time zero. -/

AutoSamplingTheory/TechnicalLemmas/FunctionalInequalities/SemigroupDecay.lean:79published source at 77184245109aOpen detailed card

- A coercive inequality along a dissipation curve implies exponential decay from time zero.

theorem exponential_decay_of_scaled_dissipation
    {scale rate : ℝ} (curve : DissipationCurve scale)
    (hcoercive : ∀ s : ℝ,
      rate * curve.energy s ≤ scale * curve.dissipation s)
    {t : ℝ} (ht : 0 ≤ t) :
    curve.energy t ≤ curve.energy 0 * Real.exp (-rate * t) := by
  simpa [sub_zero] using
    exponential_decay_of_scaled_dissipation_from
      curve hcoercive ht

/-- Exponential decay from every starting time forces the instantaneous
coercivity inequality.

The proof compares the energy with its exponential envelope on `[s, ∞)`. Their
difference has a local maximum at `s`; the one-sided Fermat inequality then
compares the two right derivatives. -/

AutoSamplingTheory/TechnicalLemmas/FunctionalInequalities/SemigroupDecay.lean:114published source at 77184245109aOpen detailed card

- Exponential decay from every starting time forces the instantaneous coercivity inequality. The proof compares the energy with its exponential envelope on `[s, ∞)`. Their difference has a local maximum at `s`; the one-sided Fermat inequality then compares the two right derivatives.

theorem scaled_dissipation_of_exponential_decay
    {scale rate : ℝ} (curve : DissipationCurve scale)
    (hdecay : ∀ s t : ℝ, 0 ≤ t →
      curve.energy (s + t) ≤
        curve.energy s * Real.exp (-rate * t)) :
    ∀ s : ℝ,
      rate * curve.energy s ≤ scale * curve.dissipation s := by
  intro s
  let comparison : ℝ → ℝ := fun x =>
    curve.energy x -
      curve.energy s * Real.exp (-rate * (x - s))
  have hmax : IsLocalMaxOn comparison (Ici s) s := by
    filter_upwards [self_mem_nhdsWithin] with x hx
    have hdecay_x :
        curve.energy x ≤
          curve.energy s * Real.exp (-rate * (x - s)) := by
      have h := hdecay s (x - s) (sub_nonneg.mpr hx)
      calc
        curve.energy x = curve.energy (s + (x - s)) := by
          congr 1
          ring
        _ ≤ curve.energy s * Real.exp (-rate * (x - s)) := h
    dsimp [comparison]
    calc
      curve.energy x -
          curve.energy s * Real.exp (-rate * (x - s)) ≤ 0 :=
        sub_nonpos.mpr hdecay_x
      _ = curve.energy s -
          curve.energy s * Real.exp (-rate * (s - s)) := by simp
  have hinner :
      HasDerivAt (fun x : ℝ => -rate * (x - s)) (-rate) s := by
    change HasDerivAt (fun y : ℝ => -rate * (id y - s)) (-rate) s
    have hraw := ((hasDerivAt_id s).sub_const s).const_mul (-rate)
    exact hraw.congr_deriv (by ring)
  have hexponential :
      HasDerivAt
        (fun x : ℝ =>
          curve.energy s * Real.exp (-rate * (x - s)))
        (-rate * curve.energy s) s := by
    have hraw := hinner.exp.const_mul (curve.energy s)
    apply hraw.congr_deriv
    rw [sub_self, mul_zero, Real.exp_zero]
    ring
  have hderiv :
-- Source excerpt truncated; follow the exact source link.

AutoSamplingTheory/TechnicalLemmas/FunctionalInequalities/SemigroupDecay.lean:130published source at 77184245109aOpen detailed card

Excerpt truncated; the exact source link is authoritative.

- Forward direction of Chewi, Theorem 1.2.21, between arbitrary times.

theorem chewi_theorem_1_2_21_forward_from
    {C : ℝ} (hC : 0 < C) (curve : DissipationCurve 2)
    (hPI : ∀ s : ℝ,
      curve.energy s ≤ C * curve.dissipation s)
    {s t : ℝ} (hst : s ≤ t) :
    curve.energy t ≤
      curve.energy s * Real.exp (-(2 / C) * (t - s)) := by
  apply exponential_decay_of_scaled_dissipation_from
    (curve := curve) (rate := 2 / C) ?_ hst
  intro u
  have hfactor : 0 ≤ (2 : ℝ) / C := by positivity
  calc
    (2 / C) * curve.energy u ≤
        (2 / C) * (C * curve.dissipation u) :=
      mul_le_mul_of_nonneg_left (hPI u) hfactor
    _ = 2 * curve.dissipation u := by
      field_simp [hC.ne']

/-- Forward direction of Chewi, Theorem 1.2.21, from time zero. -/

AutoSamplingTheory/TechnicalLemmas/FunctionalInequalities/SemigroupDecay.lean:202published source at 77184245109a

- Forward direction of Chewi, Theorem 1.2.21, from time zero.

theorem chewi_theorem_1_2_21_forward
    {C : ℝ} (hC : 0 < C) (curve : DissipationCurve 2)
    (hPI : ∀ s : ℝ,
      curve.energy s ≤ C * curve.dissipation s)
    {t : ℝ} (ht : 0 ≤ t) :
    curve.energy t ≤
      curve.energy 0 * Real.exp (-(2 / C) * t) := by
  simpa [sub_zero] using
    chewi_theorem_1_2_21_forward_from hC curve hPI ht

/-- Backward scalar direction of Chewi, Theorem 1.2.21. -/

AutoSamplingTheory/TechnicalLemmas/FunctionalInequalities/SemigroupDecay.lean:221published source at 77184245109aOpen detailed card

- Backward scalar direction of Chewi, Theorem 1.2.21.

theorem chewi_theorem_1_2_21_backward
    {C : ℝ} (hC : 0 < C) (curve : DissipationCurve 2)
    (hdecay : ∀ s t : ℝ, 0 ≤ t →
      curve.energy (s + t) ≤
        curve.energy s * Real.exp (-(2 / C) * t)) :
    ∀ s : ℝ,
      curve.energy s ≤ C * curve.dissipation s := by
  have hscaled :=
    scaled_dissipation_of_exponential_decay
      (curve := curve) (rate := 2 / C) hdecay
  intro s
  have hfactor : 0 ≤ C / 2 := by positivity
  calc
    curve.energy s =
        (C / 2) * ((2 / C) * curve.energy s) := by
      field_simp [hC.ne']
    _ ≤ (C / 2) * (2 * curve.dissipation s) :=
      mul_le_mul_of_nonneg_left (hscaled s) hfactor
    _ = C * curve.dissipation s := by ring

/-- Scalar equivalence behind Chewi, Theorem 1.2.21. -/

AutoSamplingTheory/TechnicalLemmas/FunctionalInequalities/SemigroupDecay.lean:232published source at 77184245109a

- Scalar equivalence behind Chewi, Theorem 1.2.21.

theorem chewi_theorem_1_2_21_scalar_equivalence
    {C : ℝ} (hC : 0 < C) (curve : DissipationCurve 2) :
    (∀ s : ℝ,
      curve.energy s ≤ C * curve.dissipation s) ↔
    (∀ s t : ℝ, 0 ≤ t →
      curve.energy (s + t) ≤
        curve.energy s * Real.exp (-(2 / C) * t)) := by
  constructor
  · intro hPI s t ht
    have h := chewi_theorem_1_2_21_forward_from
      hC curve hPI (show s ≤ s + t by linarith)
    simpa using h
  · exact chewi_theorem_1_2_21_backward hC curve

/-- Forward direction of Chewi, Theorem 1.2.22, between arbitrary times. -/

AutoSamplingTheory/TechnicalLemmas/FunctionalInequalities/SemigroupDecay.lean:253published source at 77184245109aOpen detailed card

- Forward direction of Chewi, Theorem 1.2.22, between arbitrary times.

theorem chewi_theorem_1_2_22_forward_from
    {C : ℝ} (hC : 0 < C) (curve : DissipationCurve 2)
    (hPI : ∀ s : ℝ,
      curve.energy s ≤ C * curve.dissipation s)
    {s t : ℝ} (hst : s ≤ t) :
    curve.energy t ≤
      curve.energy s * Real.exp (-(2 / C) * (t - s)) :=
  chewi_theorem_1_2_21_forward_from hC curve hPI hst

/-- Forward direction of Chewi, Theorem 1.2.22, from time zero. -/

AutoSamplingTheory/TechnicalLemmas/FunctionalInequalities/SemigroupDecay.lean:268published source at 77184245109a

- Forward direction of Chewi, Theorem 1.2.22, from time zero.

theorem chewi_theorem_1_2_22_forward
    {C : ℝ} (hC : 0 < C) (curve : DissipationCurve 2)
    (hPI : ∀ s : ℝ,
      curve.energy s ≤ C * curve.dissipation s)
    {t : ℝ} (ht : 0 ≤ t) :
    curve.energy t ≤
      curve.energy 0 * Real.exp (-(2 / C) * t) :=
  chewi_theorem_1_2_21_forward hC curve hPI ht

/-- Backward scalar direction of Chewi, Theorem 1.2.22. -/

AutoSamplingTheory/TechnicalLemmas/FunctionalInequalities/SemigroupDecay.lean:278published source at 77184245109aOpen detailed card

- Backward scalar direction of Chewi, Theorem 1.2.22.

theorem chewi_theorem_1_2_22_backward
    {C : ℝ} (hC : 0 < C) (curve : DissipationCurve 2)
    (hdecay : ∀ s t : ℝ, 0 ≤ t →
      curve.energy (s + t) ≤
        curve.energy s * Real.exp (-(2 / C) * t)) :
    ∀ s : ℝ,
      curve.energy s ≤ C * curve.dissipation s :=
  chewi_theorem_1_2_21_backward hC curve hdecay

/-- Scalar equivalence behind Chewi, Theorem 1.2.22. -/

AutoSamplingTheory/TechnicalLemmas/FunctionalInequalities/SemigroupDecay.lean:288published source at 77184245109a

- Scalar equivalence behind Chewi, Theorem 1.2.22.

theorem chewi_theorem_1_2_22_scalar_equivalence
    {C : ℝ} (hC : 0 < C) (curve : DissipationCurve 2) :
    (∀ s : ℝ,
      curve.energy s ≤ C * curve.dissipation s) ↔
    (∀ s t : ℝ, 0 ≤ t →
      curve.energy (s + t) ≤
        curve.energy s * Real.exp (-(2 / C) * t)) :=
  chewi_theorem_1_2_21_scalar_equivalence hC curve

/-- Forward direction of Chewi, Theorem 1.2.26, between arbitrary times. -/

AutoSamplingTheory/TechnicalLemmas/FunctionalInequalities/SemigroupDecay.lean:298published source at 77184245109aOpen detailed card

- Forward direction of Chewi, Theorem 1.2.26, between arbitrary times.

theorem chewi_theorem_1_2_26_forward_from
    {C : ℝ} (hC : 0 < C) (curve : DissipationCurve 1)
    (hLSI : ∀ s : ℝ,
      curve.energy s ≤ (C / 2) * curve.dissipation s)
    {s t : ℝ} (hst : s ≤ t) :
    curve.energy t ≤
      curve.energy s * Real.exp (-(2 / C) * (t - s)) := by
  apply exponential_decay_of_scaled_dissipation_from
    (curve := curve) (rate := 2 / C) ?_ hst
  intro u
  have hfactor : 0 ≤ (2 : ℝ) / C := by positivity
  calc
    (2 / C) * curve.energy u ≤
        (2 / C) * ((C / 2) * curve.dissipation u) :=
      mul_le_mul_of_nonneg_left (hLSI u) hfactor
    _ = 1 * curve.dissipation u := by
      field_simp [hC.ne']

/-- Forward direction of Chewi, Theorem 1.2.26, from time zero. -/

AutoSamplingTheory/TechnicalLemmas/FunctionalInequalities/SemigroupDecay.lean:308published source at 77184245109a

- Forward direction of Chewi, Theorem 1.2.26, from time zero.

theorem chewi_theorem_1_2_26_forward
    {C : ℝ} (hC : 0 < C) (curve : DissipationCurve 1)
    (hLSI : ∀ s : ℝ,
      curve.energy s ≤ (C / 2) * curve.dissipation s)
    {t : ℝ} (ht : 0 ≤ t) :
    curve.energy t ≤
      curve.energy 0 * Real.exp (-(2 / C) * t) := by
  simpa [sub_zero] using
    chewi_theorem_1_2_26_forward_from hC curve hLSI ht

/-- Backward scalar direction of Chewi, Theorem 1.2.26. -/

AutoSamplingTheory/TechnicalLemmas/FunctionalInequalities/SemigroupDecay.lean:327published source at 77184245109aOpen detailed card

- Backward scalar direction of Chewi, Theorem 1.2.26.

theorem chewi_theorem_1_2_26_backward
    {C : ℝ} (hC : 0 < C) (curve : DissipationCurve 1)
    (hdecay : ∀ s t : ℝ, 0 ≤ t →
      curve.energy (s + t) ≤
        curve.energy s * Real.exp (-(2 / C) * t)) :
    ∀ s : ℝ,
      curve.energy s ≤ (C / 2) * curve.dissipation s := by
  have hscaled :=
    scaled_dissipation_of_exponential_decay
      (curve := curve) (rate := 2 / C) hdecay
  intro s
  have hfactor : 0 ≤ C / 2 := by positivity
  calc
    curve.energy s =
        (C / 2) * ((2 / C) * curve.energy s) := by
      field_simp [hC.ne']
    _ ≤ (C / 2) * (1 * curve.dissipation s) :=
      mul_le_mul_of_nonneg_left (hscaled s) hfactor
    _ = (C / 2) * curve.dissipation s := by ring

/-- Scalar equivalence behind Chewi, Theorem 1.2.26. -/

AutoSamplingTheory/TechnicalLemmas/FunctionalInequalities/SemigroupDecay.lean:338published source at 77184245109a

- Scalar equivalence behind Chewi, Theorem 1.2.26.

theorem chewi_theorem_1_2_26_scalar_equivalence
    {C : ℝ} (hC : 0 < C) (curve : DissipationCurve 1) :
    (∀ s : ℝ,
      curve.energy s ≤ (C / 2) * curve.dissipation s) ↔
    (∀ s t : ℝ, 0 ≤ t →
      curve.energy (s + t) ≤
        curve.energy s * Real.exp (-(2 / C) * t)) := by
  constructor
  · intro hLSI s t ht
    have h := chewi_theorem_1_2_26_forward_from
      hC curve hLSI (show s ≤ s + t by linarith)
    simpa using h
  · exact chewi_theorem_1_2_26_backward hC curve

end

end SemigroupDecay
end FunctionalInequalities
end TechnicalLemmas
end AutoSamplingTheory

AutoSamplingTheory/TechnicalLemmas/FunctionalInequalities/SemigroupDecay.lean:359published source at 77184245109aOpen detailed card