TUpgrade Consumers Profile

Support for the Armstrong–Vicol anomalous-diffusion formalization.

theorem AVenhance.Infra.Section4.iterate_squared_amplitude_bound {a N K : ℝ} (hN : 0 ≤ N) (hK : 0 ≤ K) (h : ∀ (B : ℝ), N < B → a ≤ B ^ 2 * K) : a ≤ N ^ 2 * K

Closedness of squared energy bounds under strictly enlarged amplitudes.

theorem AVenhance.Infra.Section4.theta_iterate_profile_of_initial_trace_nonneg_A3_A5 {β : ℝ} {M m : ℕ} (I : Ingredients β) (Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ) (hΦ : IsStreamSeq I Φ) (hm : 2 ≤ m) (hmM : m ≤ M) {κ : ℝ} {θ₀ : Homogenization.Vec 2 → ℝ} {θ : ℝ → Homogenization.Vec 2 → ℝ} {c C B R C₀ : ℝ} (hc : 0 < c) (hC : c < C) (hB : 0 ≤ B) (hR : 0 < R) (hRadius : 8 * max (thetaAnalyticRadiusBase c) 2 ≤ C₀) (hscale : epsilon β I.Λ (m - 1) ^ (1 + gamma β / 2) ≤ R) (hzero : (I.kappaSeq κ M (m - 1) * spaceTimeGradNormSq fun (t : ℝ) => spaceGrad (θ t)) ≤ B ^ 2) (hTrace : ∀ (w : List (Fin 2)), 1 ≤ w.length → √(∫ (x : Homogenization.Vec 2) in unitCube, classicalWordDerivative w θ₀ x ^ 2) ≤ B * (↑w.length.factorial / R ^ w.length)) (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))) (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) ≤ C * (AVenhance.a β I.Λ j * epsilon β I.Λ j ^ (2 + gamma β))) (hsol : IsClassicalSol (streamVel (Φ (m - 1))) (I.kappaSeq κ M (m - 1)) (fun (x : ℝ) (x_1 : Homogenization.Vec 2) => 0) θ₀ θ) : iterateCoordinateEnergyProfile θ (I.kappaSeq κ M (m - 1)) B (C₀ * epsilon β I.Λ (m - 1) ^ (-1 - gamma β / 2)) 0

The generic initial-trace profile also permits zero dissipation amplitude.