Iterates TA5Upgrade

Support for the Armstrong–Vicol anomalous-diffusion formalization.

theorem AVenhance.Infra.Section4.iterate_T_upgrade_conditional_A3_A5_flow_material {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (κ : ℝ) (M : ℕ) {m : ℕ} {θ₀ : Homogenization.Vec 2 → ℝ} {θprev : ℝ → Homogenization.Vec 2 → ℝ} {T : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hT : I.IsTIterates hΦ m (I.kappaAt κ m (M - m)) (I.kappaAt κ (m - 1) (M - (m - 1))) θ₀ θprev T) (hθ : IsClassicalSol (streamVel (Φ (m - 1))) (I.kappaAt κ (m - 1) (M - (m - 1))) (fun (x : ℝ) (x_1 : Homogenization.Vec 2) => 0) θ₀ θprev) (hm : 2 ≤ m) (hmM : m ≤ M) (hκtop : 0 < κ) (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))) {c Ck K Cflow Cmean Rflow Cθ Rθ C₀ N : ℝ} (hN : 0 < N) (hc : 0 < c) (hcC : c < Ck) (hA5 : ∀ (j : ℕ), 1 ≤ j → j < M → c * (AVenhance.a β I.Λ j * epsilon β I.Λ j ^ (2 + gamma β)) ≤ I.kappaAt κ j (M - j) ∧ I.kappaAt κ j (M - j) ≤ Ck * (AVenhance.a β I.Λ j * epsilon β I.Λ j ^ (2 + gamma β))) (hK : 0 ≤ K) (hCf : 0 ≤ Cflow) (hCm : 0 ≤ Cmean) (hRf : 256 ≤ Rflow) (hRθ : 0 < Rθ) (hC₀ : iterateSourceConstant (iterateBudgetUniversalConstant K Ck c (2 ^ (-25)) Cflow Cmean) Rflow Cθ ≤ C₀) (hradius : epsilon β I.Λ (m - 1) ^ (1 + gamma β / 2) ≤ Rθ) (hsmall : epsilon β I.Λ (m - 1) ^ (2 * delta β) ≤ (4 * C₀ ^ 3)⁻¹) (hKm : ∀ (t : ℝ) (j k : Fin 2), |I.Kmat (I.kappaAt κ m (M - m)) m t j k| ≤ K * I.kappaAt κ (m - 1) (M - (m - 1))) (hcondition : epsilon β I.Λ m ^ 2 ≤ I.kappaAt κ m (M - m) * tau β I.Λ m / 2) (hMeanScale : iterateMeanErrorBound I (I.kappaAt κ m (M - m)) m ≤ I.kappaAt κ (m - 1) (M - (m - 1)) * Cmean * epsilon β I.Λ (m - 1) ^ (2 * delta β)) (hzero : ∀ (t : ℝ) (x : Homogenization.Vec 2) (l : ℤ), I.hatXiML m l t ≠ 0 → ∀ (j k : Fin 2), |(I.flowGrad hΦ m l t x - 1) j k| ≤ Cflow * epsilon β I.Λ (m - 1) ^ (2 * delta β)) (hpositive : ∀ (t : ℝ) (x : Homogenization.Vec 2) (l : ℤ), I.hatXiML m l t ≠ 0 → ∀ (p : List (Fin 2)), 1 ≤ p.length → ∀ (j k : Fin 2), |iterateSpatialWord p (fun (y : Homogenization.Vec 2) => (I.flowGrad hΦ m l t y - 1) j k) x| ≤ Cflow * ↑p.length.factorial * (Rflow / epsilon β I.Λ (m - 1)) ^ p.length) (hbase : iterateCoordinateEnergyProfile θprev (I.kappaAt κ (m - 1) (M - (m - 1))) N (C₀ * epsilon β I.Λ (m - 1) ^ (-1 - gamma β / 2)) 0) : √(I.kappaAt κ (m - 1) (M - (m - 1))) * √(spaceTimeGradNormSq fun (t : ℝ) => spaceGrad (T (Nstar β) t)) ≤ N * (1 + C₀ ^ 3 * epsilon β I.Λ (m - 1) ^ (2 * delta β) * ↑(Nstar β) * ↑(2 * Nstar β).factorial) ∧ ∀ (v w : List (Fin 2)), v.length = w.length → 1 ≤ v.length → ∀ (s : ℝ), 0 ≤ s → s ≤ 1 → √(l2NormSq (iterateSpatialWord v (T (Nstar β) s))) + √(I.kappaAt κ (m - 1) (M - (m - 1))) * √(spaceTimeGradNormSq fun (t : ℝ) => spaceGrad (iterateSpatialWord w (T (Nstar β) t))) ≤ N * 4 ^ Nstar β * ↑(2 * Nstar β).factorial * ↑v.length.factorial * (4 * C₀ ^ 3 * epsilon β I.Λ (m - 1) ^ (-1 - gamma β / 2)) ^ v.length

The actual-chain conditional T upgrade with stream-regularity/diffusivity-recursion. Its amplitude is abstract and positive. The theta base excludes the scalar zeroth-order supremum, and the mean comparison retains both E21c errors.