Iterates Coordinate Induction

Support for the Armstrong–Vicol anomalous-diffusion formalization.

theorem AVenhance.Infra.Section4.iterate_coordinate_two_index_induction {u : ℕ → ℝ → Homogenization.Vec 2 → ℝ} {κ N L η : ℝ} {K : ℕ} (hκ : 0 < κ) (hbase : iterateCoordinateEnergyProfile (u 0) κ N L 0) (hstep : ∀ (i : ℕ), 1 ≤ i → i ≤ K → (∀ j < i, iterateCoordinateEnergyProfile (u j) κ (N * iterateAmplitude η j) L j) → ∀ (w : List (Fin 2)), (∀ (p : List (Fin 2)), p.length < w.length → (spaceTimeGradNormSq fun (t : ℝ) => spaceGrad (iterateSpatialWord p (u i t))) ≤ (N * iterateAmplitude η i / √κ) ^ 2 * iterateAnalyticWeight p.length i L ^ 2) → ∀ (s : ℝ), 0 ≤ s → s ≤ 1 → (√(l2NormSq (iterateSpatialWord w (u i s))) + √κ * √(spaceTimeGradNormSq fun (t : ℝ) => spaceGrad (iterateSpatialWord w (u i t)))) ^ 2 ≤ N ^ 2 * iterateAmplitude η i ^ 2 * iterateAnalyticWeight w.length i L ^ 2 / 4) (i : ℕ) : i ≤ K → iterateCoordinateEnergyProfile (u i) κ (N * iterateAmplitude η i) L i

Structural induction over the finite increment index and every coordinate order. The step is applied only to previously established scalar energies; this helper does not claim a PDE estimate for the family.