Iterates Terminal Coercivity

Support for the Armstrong–Vicol anomalous-diffusion formalization.

theorem AVenhance.Infra.Section4.iterate_terminal_full_energy_bound {e₁ e g gpart κ a R : ℝ} (he₁ : 0 ≤ e₁) (hg : 0 ≤ g) (hgp : 0 ≤ gpart) (hκ : 0 ≤ κ) (ha : a ≤ 1 / 2) (hfull : e₁ / 2 + κ * g ≤ a * κ * g + R) (hpartial : e / 2 + κ * gpart ≤ a * κ * g + R) : e + κ * g ≤ 6 * R

Full dissipation is first controlled at terminal time one, then used in each partial-time inequality. No partial dissipation is replaced by full dissipation on the left-hand side.