TUpgrade Consumers Trace

Support for the Armstrong–Vicol anomalous-diffusion formalization.

theorem AVenhance.Infra.Section4.iterate_T_upgrade_of_initial_trace (β Ccut : ℝ) : ∃ (C₀ : ℝ), 1 ≤ C₀ ∧ ∀ (I : Ingredients β), I.Czeta ≤ Ccut → I.Cxi ≤ Ccut → I.Chat ≤ Ccut → ∀ {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (κ : ℝ) (M : ℕ) {m : ℕ} {θ₀ : Homogenization.Vec 2 → ℝ} {θprev : ℝ → Homogenization.Vec 2 → ℝ} {T : ℕ → ℝ → Homogenization.Vec 2 → ℝ}, I.IsTIterates hΦ m (I.kappaAt κ m (M - m)) (I.kappaAt κ (m - 1) (M - (m - 1))) θ₀ θprev T → IsClassicalSol (streamVel (Φ (m - 1))) (I.kappaAt κ (m - 1) (M - (m - 1))) (fun (x : ℝ) (x_1 : Homogenization.Vec 2) => 0) θ₀ θprev → 2 ≤ m → m ≤ M → κ ∈ permittedInterval β I.Λ M → ∀ (Rθ N : ℝ), 0 ≤ N → 0 < Rθ → epsilon β I.Λ (m - 1) ^ (1 + gamma β / 2) ≤ Rθ → epsilon β I.Λ (m - 1) ^ (2 * delta β) ≤ (4 * C₀ ^ 3)⁻¹ → (I.kappaSeq κ M (m - 1) * spaceTimeGradNormSq fun (t : ℝ) => spaceGrad (θprev t)) ≤ N ^ 2 → (∀ (w : List (Fin 2)), 1 ≤ w.length → √(∫ (x : Homogenization.Vec 2) in unitCube, classicalWordDerivative w θ₀ x ^ 2) ≤ N * (↑w.length.factorial / Rθ ^ w.length)) → √(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