Public statement.

theorem AVenhance.bigbound (β C₀ : ℝ) : ∃ (C : ℝ), ∀ (I : Ingredients β), I.Czeta ≤ C₀ → I.Cxi ≤ C₀ → I.Chat ≤ C₀ → C ≤ ↑I.Λ → ∀ (Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ) (hΦ : IsStreamSeq I Φ), ∀ κ ∈ permissibleSet β I.Λ, ∀ (M : ℕ), 1 ≤ M → κ ∈ permittedInterval β I.Λ M → ∀ (R : ℝ), 0 < R → ∀ (θ₀ : Homogenization.Vec 2 → ℝ), ContDiff ℝ (↑⊤) θ₀ → IsZ2Periodic θ₀ → Homogenization.MeanZeroOn unitCube θ₀ → IsThetaAnalytic R θ₀ → ∀ (m : ℕ), mTheta0 β I.Λ R ≤ m → m ≤ M → ∀ (θprev : ℝ → Homogenization.Vec 2 → ℝ) (T : ℕ → ℝ → Homogenization.Vec 2 → ℝ), IsClassicalSol (streamVel (Φ (m - 1))) (I.kappaSeq κ M (m - 1)) (fun (x : ℝ) (x_1 : Homogenization.Vec 2) => 0) θ₀ θprev → I.IsTIterates hΦ m (I.kappaSeq κ M m) (I.kappaSeq κ M (m - 1)) θ₀ θprev T → ENNReal.ofReal (I.kappaSeq κ M m ^ (-(1 / 2))) * (∫⁻ (t : ℝ) in Set.Ioo 0 1, (hMinusOneNorm fun (x : Homogenization.Vec 2) => advDiffOp (streamVel (Φ m)) (I.kappaSeq κ M m) (I.ansatz hΦ m (I.kappaSeq κ M m) (T (Nstar β))) t x) ^ 2) ^ (1 / 2) ≤ ENNReal.ofReal (C * epsilon β I.Λ (m - 1) ^ delta β * √(l2NormSq θ₀))

Big-bound estimate: e.bigbound (7013-7021), for m ∈ {m_{θ₀},…,M} (e.m.restriction, 7008-7012). C = C(β) (with the three cutoff-constant bounds C₀, as in l_recurse) is placed before I, Λ = I.Λ, Φ, κ, M, R, θ₀, m; the premise "Λ ≥ C" is e.Lambda.restriction. θ_{m-1} and T_{m-1} = T (Nstar β) are quantified as solutions (IsClassicalSol, IsTIterates), θ_m does not occur. The L²((0,1);HDot⁻¹) norm is (∫⁻ ‖·‖²)^{1/2} in ℝ≥0∞.