Iterates Energy Recurrence Norm #
Support for the Armstrong–Vicol anomalous-diffusion formalization.
theorem
AVenhance.Infra.Section4.iterate_energy_recurrence_norm_sq
{e gpart : ℝ → ℝ}
{g κ R : ℝ}
(he : ∀ (t : ℝ), 0 ≤ e t)
(hg : 0 ≤ g)
(hgp : ∀ (t : ℝ), 0 ≤ gpart t)
(hκ : 0 ≤ κ)
(hg1 : gpart 1 = g)
(henergy : ∀ (t : ℝ), 0 ≤ t → t ≤ 1 → e t / 2 + κ * gpart t ≤ e t / 4 + 3 * κ / 8 * g + R)
{s : ℝ}
(hs : 0 ≤ s)
(hs1 : s ≤ 1)
:
A uniform differentiated energy remainder controls each terminal norm. The partial dissipation remains on its original interval.