Iterates Actual Coordinate Induction

Support for the Armstrong–Vicol anomalous-diffusion formalization.

theorem AVenhance.Infra.Section4.iterate_actual_coordinate_induction_of_scales {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) {m : ℕ} {κm κprev : ℝ} {θ₀ : Homogenization.Vec 2 → ℝ} {θprev : ℝ → Homogenization.Vec 2 → ℝ} {T : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hT : I.IsTIterates hΦ m κm κprev θ₀ θprev T) (hθ : IsClassicalSol (streamVel (Φ (m - 1))) κprev (fun (x : ℝ) (x_1 : Homogenization.Vec 2) => 0) θ₀ θprev) (hm : 2 ≤ m) (hκm : 0 < κm) (hκ : 0 < κprev) (hflow : ∀ (l : ℤ), ContDiff ℝ ↑⊤ fun (z : AmnrSpace) => I.flowGrad hΦ m l z.1 z.2) (hflowp : ∀ (t : ℝ), 0 < t → ∀ (l : ℤ), IsZ2Periodic (I.flowGrad hΦ m l t)) (hA3 : ∀ (j : ℕ), 1 ≤ j → ∀ (t : ℝ) (n : ℕ), 2 ≤ n → barNorm n (2 ^ 8 * (epsilon β I.Λ j)⁻¹) (Φ j t) ≤ ENNReal.ofReal (2 ^ 5 * AVenhance.a β I.Λ j * epsilon β I.Λ j ^ 2 * ((↑n + 2) ^ 2 / (↑n + 1) ^ 3))) {Ccoef Cs C C₀ N B r L D Bflow ρ F : ℝ} (hL : 0 < L) (hg : 2 * (r / L) ^ 2 ≤ 1 / 2) (hvel : 2 * (256 * (epsilon β I.Λ (m - 1))⁻¹ / L) ^ 2 ≤ 1 / 4) (hD : 0 ≤ D) (hCs : 0 ≤ Cs) (hC : 0 ≤ C) (hN : 0 ≤ N) (hB : 0 ≤ B) (hr : 0 ≤ r) (hρ : 0 < ρ) (hρq : ρ ≤ ρ * F ^ 2) (hC₀ : 1 ≤ C₀) (hF : C₀ ≤ F) (hlarge : 32 * C ≤ C₀) (hsmall : C₀ * (ρ * F ^ 2) ≤ 1) (hQ : ∀ (t : ℝ) (j k : Fin 2), |iterateKmatPrimitive I κm m t j k| ≤ D) (hscale : D * L ^ 2 ≤ Cs * (ρ * F ^ 2)) (hvelocity : 8192 * a β I.Λ (m - 1) * epsilon β I.Λ (m - 1) * (256 * (epsilon β I.Λ (m - 1))⁻¹) ≤ Cs * κprev * L ^ 2) (hBr : B * r = 8192 * a β I.Λ (m - 1) * epsilon β I.Λ (m - 1) * (256 * (epsilon β I.Λ (m - 1))⁻¹)) (hjet : ∀ (t : ℝ) (x : Homogenization.Vec 2) (p : List (Fin 2)), 1 ≤ p.length → ∀ (j : Fin 2), |iterateSpatialWord p (fun (y : Homogenization.Vec 2) => streamVel (Φ (m - 1)) t y j) x| ≤ B * ↑p.length.factorial * r ^ p.length) (hFlowBound : ∀ (t : ℝ) (x : Homogenization.Vec 2) (j k : Fin 2), |gradMatrix (streamVel (Φ (m - 1)) t) x j k| ≤ Bflow) (hFlowScale : D * Bflow ≤ Cs * κprev * ρ) (hcoef : ∀ (t : ℝ) (x : Homogenization.Vec 2) (p : List (Fin 2)) (j k : Fin 2), |iterateMatrixWord (fun (y : Homogenization.Vec 2) => I.Kmat κm m t - κprev • 1 + I.sMat hΦ m κm t y) p x j k| ≤ κprev * Ccoef * ↑p.length.factorial * r ^ p.length) (hrem : ∀ (t : ℝ) (x : Homogenization.Vec 2) (p : List (Fin 2)) (j k : Fin 2), |iterateMatrixWord (fun (y : Homogenization.Vec 2) => timeAvgMat (I.Kmat κm m) - κprev • 1 + I.sMat hΦ m κm t y) p x j k| ≤ κprev * Ccoef * ρ * ↑p.length.factorial * r ^ p.length) (hbase : iterateCoordinateEnergyProfile θprev κprev N L 0) (hmat : 24 * amnrMaterialMajorantConstant Ccoef Cs Cs Cs ≤ C) (hfirst : 24 * (iterateFirstMaterialCoefficient Cs Ccoef + 384 * Cs ^ 2 + 32 * Ccoef ^ 2) ≤ C) (hu : 24 * (2 * (2 ^ 19 * a β I.Λ (m - 1)) / L ^ 2) / κprev ≤ C / F ^ 2) (hv : 24 * (16 / κprev * (32 * a β I.Λ (m - 1) * epsilon β I.Λ (m - 1) ^ 2) ^ 2 * (2 * (256 * (epsilon β I.Λ (m - 1))⁻¹ / L) ^ 2) ^ 2) / κprev ≤ C / F ^ 4) (hc : 24 * (8 * D * (8192 * a β I.Λ (m - 1) * epsilon β I.Λ (m - 1)) * (256 * (epsilon β I.Λ (m - 1))⁻¹)) / κprev ≤ C * ρ) (i : ℕ) : i ≤ Nstar β → iterateCoordinateEnergyProfile (iterateIncrement T i) κprev (N * iterateAmplitude (C₀ * (ρ * F ^ 2)) i) L i

Actual all-order increment induction from coefficient jets, scalar scale inequalities, and the analytic homogeneous base. No material, forcing, flux, energy recurrence, or preceding increment estimate is assumed.