TUpgrade Consumers Contracts

Support for the Armstrong–Vicol anomalous-diffusion formalization.

theorem AVenhance.Infra.Section4.iterate_T_analytic_consumer_bounds (β Ccut : ℝ) : ∃ (C₀ : ℝ) (A : ℝ), 1 ≤ C₀ ∧ 1 ≤ A ∧ ∀ (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θ : ℝ), 0 < Rθ → epsilon β I.Λ (m - 1) ^ (1 + gamma β / 2) ≤ Rθ → epsilon β I.Λ (m - 1) ^ (2 * delta β) ≤ (4 * C₀ ^ 3)⁻¹ → IsThetaAnalytic Rθ θ₀ → √(I.kappaSeq κ M (m - 1)) * √(spaceTimeGradNormSq fun (t : ℝ) => spaceGrad (T (Nstar β) t)) ≤ A * √(l2NormSq θ₀) ∧ Section5.AnalyticBridge.TmRegUpgradeLinfL2 A (epsilon β I.Λ (m - 1) ^ (1 + gamma β / 2)) θ₀ (T (Nstar β)) ∧ ∀ (i : Fin 2), ∀ s ∈ Set.Icc 0 1, √(l2NormSq fun (x : Homogenization.Vec 2) => spaceGrad (T (Nstar β) s) x i) ≤ A ^ 2 * √(l2NormSq θ₀) * epsilon β I.Λ (m - 1) ^ (-(1 + gamma β / 2))