TUpgrade Consumers V

Support for the Armstrong–Vicol anomalous-diffusion formalization.

theorem AVenhance.Infra.Section4.iterate_V_upgrade_of_theta (β Ccut : ℝ) : ∃ (c : ℝ) (Ck : ℝ), 0 < c ∧ c < Ck ∧ ∀ (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 → ∀ (Cθ Rθ C₀ N : ℝ), 0 ≤ N → 0 < Rθ → iterateReducedSourceConstant β Ccut c Ck 40 (2 ^ 10) Cθ ≤ C₀ → epsilon β I.Λ (m - 1) ^ (1 + gamma β / 2) ≤ Rθ → epsilon β I.Λ (m - 1) ^ (2 * delta β) ≤ (4 * C₀ ^ 3)⁻¹ → iterateCoordinateEnergyProfile θprev (I.kappaAt κ (m - 1) (M - (m - 1))) N (C₀ * epsilon β I.Λ (m - 1) ^ (-1 - gamma β / 2)) 0 → Section5.Integration.VIncrementContract I m (I.kappaSeq κ M (m - 1)) T C₀ Rθ N