Abstract short-time chain for the gradient energy

Pure real analysis. From the three integral inequalities (upper and lower for G, upper for H) produced by the differential inequalities of the PDE side, deduce (9/10) G₀ ≤ G r ≤ (11/10) G₀ on [0,t], using Lu t ≤ 1/10000, κ t λ ≤ 1/10000.

theorem AVenhance.Infra.FullTheorem.Separation.integral_le_mul {B : ℝ → ℝ} {C r t : ℝ} (hr0 : 0 ≤ r) (hrt : r ≤ t) (hB : ContinuousOn B (Set.Icc 0 t)) (hle : ∀ s ∈ Set.Icc 0 t, B s ≤ C) : ∫ (s : ℝ) in 0..r, B s ≤ r * C

theorem AVenhance.Infra.FullTheorem.Separation.mul_le_of_le {r t c A : ℝ} (hrt : r ≤ t) (hA : 0 ≤ A) (hc : 0 ≤ c) {ε : ℝ} (hct : c * t ≤ ε) : r * (c * A) ≤ ε * A

theorem AVenhance.Infra.FullTheorem.Separation.G_two_sided {G H : ℝ → ℝ} {κ Lu lam t : ℝ} (hκ : 0 < κ) (hLu : 0 ≤ Lu) (ht : 0 < t) (hLt : Lu * t ≤ 1 / 10000) (hkl : κ * t * lam ≤ 1 / 10000) (hGc : ContinuousOn G (Set.Icc 0 t)) (hHc : ContinuousOn H (Set.Icc 0 t)) (hG0 : ∀ r ∈ Set.Icc 0 t, 0 ≤ G r) (hH0 : ∀ r ∈ Set.Icc 0 t, 0 ≤ H r) (hHinit : H 0 ≤ lam * G 0) (hGu : ∀ r ∈ Set.Icc 0 t, G r ≤ G 0 + ∫ (s : ℝ) in 0..r, 4 * Lu * G s) (hGl : ∀ r ∈ Set.Icc 0 t, G 0 - ∫ (s : ℝ) in 0..r, 2 * κ * H s + 4 * Lu * G s ≤ G r) (hHu : ∀ r ∈ Set.Icc 0 t, H r ≤ H 0 + ∫ (s : ℝ) in 0..r, 12 * Lu * H s + 8 * (Lu ^ 2 / κ) * G s) (r : ℝ) : r ∈ Set.Icc 0 t → 9 / 10 * G 0 ≤ G r ∧ G r ≤ 11 / 10 * G 0