Public statement.

theorem AVenhance.stream_regularity (β : ℝ) : ∃ (C : ℝ), 1 ≤ C ∧ ∀ (I : Ingredients β) (Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ), IsStreamSeq I Φ → ∀ (m : ℕ), 1 ≤ m → ∀ (t : ℝ), (∀ (n : ℕ), barNorm n (2 ^ 7 * (epsilon β I.Λ m)⁻¹) (Φ m t - Φ (m - 1) t) ≤ ENNReal.ofReal (10 * epsilon β I.Λ m ^ β)) ∧ (∀ (n : ℕ), 2 ≤ n → barNorm n (2 ^ 8 * (epsilon β I.Λ m)⁻¹) (Φ m t) ≤ ENNReal.ofReal (2 ^ 5 * AVenhance.a β I.Λ m * epsilon β I.Λ m ^ 2 * ((↑n + 2) ^ 2 / (↑n + 1) ^ 3))) ∧ ∀ n ≤ 1, barNorm n (C * (epsilon β I.Λ m)⁻¹) (Φ m t) ≤ ENNReal.ofReal (C * epsilon β I.Λ m ^ n)

Stream-function estimates (i): p.SAMS.regularity first display e.phi.m.m-1.bounds (1538-1547; constants universal, as in the source), e.phimbounds.subbed (1746-1753, for n ≥ 2 as in the source; universal constants; consumed by c.flowreg), and c.phim e.C1beta.phi.m (1967-1982; C = C(β), placed before I, m). Uniform in m ≥ 1 and t ∈ ℝ, Λ = I.Λ.