Iterates Terminal Boundary Coercivity

Support for the Armstrong–Vicol anomalous-diffusion formalization.

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

The terminal primitive may consume half the current scalar energy. Full dissipation is still controlled at time one before treating partial time.