Discrete Grönwall estimates for implicit time stepping

A discrete Grönwall argument shows that a quantity growing at most by the factor 1 + aτ per time step of length τ grows at most like exp (a t) up to time t. This file records the growth factor estimate (1 + aτ) ^ ⌈t / τ⌉₊ ≤ exp (a (t + τ)), valid uniformly in the time step (TauCeti.one_add_mul_pow_ceil_div_le_exp), and a discrete Grönwall bound for sequences that move in steps paid for by an energy which is bounded below in terms of the distance travelled (TauCeti.sq_le_mul_one_add_div_pow_of_sq_le_mul_sub).

Conversely, a nonincreasing quantity which drops at least by a factor q < 1 over every time interval of length T decays exponentially, at the rate -log q / T (TauCeti.le_div_mul_exp_of_antitoneOn). This is how a differential inequality E ≤ K (-E') is integrated without differentiating E: when E (s) - E (s + T) = ∫ₛ^{s + T} g with E ≤ K g, monotonicity gives T E (s + T) ≤ K (E s - E (s + T)), a drop by the factor K / (K + T).

The second estimate is the shape of the a priori bound for implicit Euler schemes of gradient flows whose energy is not bounded below. A sequence D n ≥ 0 with D 0 = 0 grows by steps D (n + 1) ≤ D n + d n whose squared lengths are bounded by the energy dissipated, d n ² ≤ 2τ (e n - e (n + 1)), and the energy obeys the coercivity bound 2τ' (A - e n) ≤ D n ². Then D n ² ≤ 2τ' (e 0 - A) (1 + 8τ / τ')ⁿ whenever 4τ ≤ τ'.

Main declarations

• TauCeti.one_add_mul_pow_ceil_div_le_exp: (1 + aτ) ^ ⌈t / τ⌉₊ ≤ exp (a (t + τ)).
• TauCeti.sq_le_mul_one_add_div_pow_of_sq_le_mul_sub: the discrete Grönwall bound D n ² ≤ 2τ' (e 0 - A) (1 + 8τ / τ')ⁿ under coercivity.
• TauCeti.le_div_mul_exp_of_antitoneOn: exponential decay of a nonincreasing function which drops by a fixed factor over every interval of a fixed length.

References

• L. Ambrosio, N. Gigli, G. Savaré, Gradient Flows in Metric Spaces and in the Space of Probability Measures, 2nd ed., Birkhäuser 2008, Chapter 3, Section 3.2.

theorem TauCeti.one_add_mul_pow_ceil_div_le_exp {a τ t : ℝ} (ha : 0 ≤ a) (htτ : 0 ≤ t + τ) : (1 + a * τ) ^ ⌈t / τ⌉₊ ≤ Real.exp (a * (t + τ))

After ⌈t / τ⌉₊ time steps of length τ, a growth factor 1 + aτ per step accumulates to at most exp (a (t + τ)), since less than t + τ time has passed. The bound is uniform in the time step τ. Only 0 ≤ t + τ is needed: when t ≤ 0 or τ ≤ 0 no step is taken and the bound reads 1 ≤ exp (a (t + τ)).

theorem TauCeti.sq_le_mul_one_add_div_pow_of_sq_le_mul_sub {D d e : ℕ → ℝ} {τ τ' A : ℝ} (hτ : 0 ≤ τ) (hττ' : 4 * τ ≤ τ') (hD0 : D 0 = 0) (hD : ∀ (n : ℕ), 0 ≤ D n) (htri : ∀ (n : ℕ), D (n + 1) ≤ D n + d n) (hstep : ∀ (n : ℕ), d n ^ 2 ≤ 2 * τ * (e n - e (n + 1))) (hcoer : ∀ (n : ℕ), 2 * τ' * (A - e n) ≤ D n ^ 2) (n : ℕ) : D n ^ 2 ≤ 2 * τ' * (e 0 - A) * (1 + 8 * τ / τ') ^ n

Discrete Grönwall bound under coercivity. Let D n ≥ 0 with D 0 = 0 grow by steps D (n + 1) ≤ D n + d n whose squared lengths are paid for by an energy e, d n ² ≤ 2τ (e n - e (n + 1)), and let the energy satisfy the coercivity bound 2τ' (A - e n) ≤ D n ², where 0 ≤ τ and 4τ ≤ τ'. Then D n ² ≤ 2τ' (e 0 - A) (1 + 8τ / τ')ⁿ.

theorem TauCeti.le_div_mul_exp_of_antitoneOn {E : ℝ → ℝ} {s₀ T q : ℝ} (hq : 0 < q) (hq1 : q ≤ 1) (hE : AntitoneOn E (Set.Ici s₀)) (h0 : 0 ≤ E s₀) (hstep : ∀ (s : ℝ), s₀ ≤ s → E (s + T) ≤ q * E s) {s : ℝ} (hs : s₀ ≤ s) : E s ≤ E s₀ / q * Real.exp (Real.log q / T * (s - s₀))

Exponential decay from a fixed-step contraction. Let E be nonincreasing on [s₀, ∞), with E s₀ ≥ 0, and suppose that E (s + T) ≤ q E s for every s ≥ s₀, where 0 < q ≤ 1. Then E s ≤ (E s₀ / q) exp ((log q / T) (s - s₀)) for every s ≥ s₀.