TUpgrade Consumers Scalar Trace

Support for the Armstrong–Vicol anomalous-diffusion formalization.

theorem AVenhance.Infra.Section4.iterate_T_upgrade_of_theta_scalar_zero_nonneg (β 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 → (∀ (s : ℝ), 0 ≤ s → s ≤ 1 → √(l2NormSq (θprev s)) ≤ N) → ∀ (s : ℝ), 0 ≤ s → s ≤ 1 → √(l2NormSq (T (Nstar β) s)) + √(I.kappaAt κ (m - 1) (M - (m - 1))) * √(spaceTimeGradNormSq fun (t : ℝ) => spaceGrad (T (Nstar β) t)) ≤ 2 * N * (1 + C₀ ^ 3 * epsilon β I.Λ (m - 1) ^ (2 * delta β) * ↑(Nstar β) * ↑(2 * Nstar β).factorial)

theorem AVenhance.Infra.Section4.iterate_T_scalar_zero_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)) → (∀ (s : ℝ), 0 ≤ s → s ≤ 1 → √(l2NormSq (θprev s)) ≤ N) → ∀ (s : ℝ), 0 ≤ s → s ≤ 1 → √(l2NormSq (T (Nstar β) s)) + √(I.kappaAt κ (m - 1) (M - (m - 1))) * √(spaceTimeGradNormSq fun (t : ℝ) => spaceGrad (T (Nstar β) t)) ≤ 2 * N * (1 + C₀ ^ 3 * epsilon β I.Λ (m - 1) ^ (2 * delta β) * ↑(Nstar β) * ↑(2 * Nstar β).factorial)