Iterates Norm Components

Support for the Armstrong–Vicol anomalous-diffusion formalization.

theorem AVenhance.Infra.Section4.iterate_norm_sq_components {e g κ H : ℝ} (he : 0 ≤ e) (hg : 0 ≤ g) (hκ : 0 ≤ κ) (hbound : (√e + √κ * √g) ^ 2 ≤ H) : e ≤ H ∧ κ * g ≤ H

A squared sum norm bounds each energy separately.

theorem AVenhance.Infra.Section4.iterate_norm_sq_gradient_bound {e g κ N A W : ℝ} (he : 0 ≤ e) (hg : 0 ≤ g) (hκ : 0 < κ) (hbound : (√e + √κ * √g) ^ 2 ≤ N ^ 2 * A ^ 2 * W ^ 2) : g ≤ (N * A / √κ) ^ 2 * W ^ 2

The gradient component has the reciprocal diffusive amplitude, also when the initial-data norm vanishes.