Iterates Profile Norms

Support for the Armstrong–Vicol anomalous-diffusion formalization.

theorem AVenhance.Infra.Section4.iterate_profile_gradient_norm {u : ℝ → Homogenization.Vec 2 → ℝ} {κ N L : ℝ} {i : ℕ} (hκ : 0 < κ) (hN : 0 ≤ N) (hL : 0 ≤ L) (hp : iterateCoordinateEnergyProfile u κ N L i) (w : List (Fin 2)) : √κ * √(spaceTimeGradNormSq fun (t : ℝ) => spaceGrad (iterateSpatialWord w (u t))) ≤ N * iterateAnalyticWeight w.length i L

Every gradient word is controlled, including the gradient-only base at zero.

theorem AVenhance.Infra.Section4.iterate_profile_mixed_norm {u : ℝ → Homogenization.Vec 2 → ℝ} {κ N L : ℝ} {i : ℕ} (hκ : 0 < κ) (hN : 0 ≤ N) (hL : 0 ≤ L) (hp : iterateCoordinateEnergyProfile u κ N L i) (v w : List (Fin 2)) (hvw : v.length = w.length) (hv : 1 ≤ v.length ∨ 1 ≤ i) {s : ℝ} (hs : 0 ≤ s) (hs1 : s ≤ 1) : √(l2NormSq (iterateSpatialWord v (u s))) + √κ * √(spaceTimeGradNormSq fun (t : ℝ) => spaceGrad (iterateSpatialWord w (u t))) ≤ 2 * N * iterateAnalyticWeight v.length i L

Mixed profile norms are used only at positive scalar order in the base.