Iterates Theta Gradient Base

Support for the Armstrong–Vicol anomalous-diffusion formalization.

theorem AVenhance.Infra.Section4.iterate_theta_gradient_base_profile {κ : ℝ} {u : ℝ → Homogenization.Vec 2 → ℝ} {B l L : ℝ} (hu : ContDiffOn ℝ (↑⊤) (fun (z : AmnrSpace) => u z.1 z.2) (Set.Ici 0 ×ˢ Set.univ)) (hκ : 0 < κ) (hB : 0 ≤ B) (hl : 0 ≤ l) (hL : 4 * l ≤ L) (hzero : (κ * spaceTimeGradNormSq fun (t : ℝ) => spaceGrad (u t)) ≤ B ^ 2) (hsource : ∀ (v w : List (Fin 2)), 1 ≤ v.length → w.length = v.length + 1 → ∀ (s : ℝ), 0 ≤ s → s ≤ 1 → √(l2NormSq (iterateSpatialWord v (u s))) + √κ * √(∫ (z : ℝ × Homogenization.Vec 2) in timeCube, iterateSpatialWord w (u z.1) z.2 ^ 2) ≤ 2 * B * ↑v.length.factorial * l ^ v.length) : iterateCoordinateEnergyProfile u κ B L 0

An abstract-amplitude theta base for both normalizations. The zeroth-order input is exclusively its integrated gradient, never its scalar supremum.