Public statement.

theorem AVenhance.limit_field_regular (β : ℝ) : ∃ (C : ℝ), 1 ≤ C ∧ ∀ (I : Ingredients β) (Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ), IsStreamSeq I Φ → ∃ (φ : ℝ → Homogenization.Vec 2 → ℝ), (∀ (t : ℝ) (x : Homogenization.Vec 2), Filter.Tendsto (fun (M : ℕ) => Φ M t x) Filter.atTop (nhds (φ t x))) ∧ (∀ (M : ℕ) (t : ℝ) (x : Homogenization.Vec 2), |φ t x - Φ M t x| ≤ C * epsilon β I.Λ (M + 1) ^ β) ∧ (∀ (t : ℝ), Differentiable ℝ (φ t)) ∧ TendstoUniformlyOn (fun (M : ℕ) (p : ℝ × Homogenization.Vec 2) => streamVel (Φ M) p.1 p.2) (fun (p : ℝ × Homogenization.Vec 2) => streamVel φ p.1 p.2) Filter.atTop (Set.Icc 0 1 ×ˢ Set.univ) ∧ ∀ (α : ℝ), 0 < α → α < β - 1 → IsHolderClass α (streamVel φ) ∧ IsDivFree (streamVel φ)

Stream-function estimates (ii): the limit stream φ = lim φ_m and b = ∇^⊥ φ (e.def.b, 1487-1500), c.phim last sentence (1983-1984), e.b.reg (335), e.phi.m.m-1.bounds consumed at 9306-9310 (‖φ - φ_M‖_∞ ≤ C ε_{M+1}^β), e.divfree. Hölder exponents are α < β - 1 only: the source proves C^{1,β'} for β' < β - 1 (endpoint not proved: sum of ε_m^0).