Statement file: anomalous_dissipation (Roots). This file contains exactly one declaration of the formalization's public statement surface.

theorem AVenhance.anomalous_dissipation (α : ℝ) (hα₀ : 0 < α) (hα₁ : α < 1 / 3) : ∃ (b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2), IsHolderClass α b ∧ IsContinuousIntoHolder α b ∧ IsDivFree b ∧ ∃ (ϱ : ℝ → ℝ), (∀ (r : ℝ), 0 < ϱ r ∧ ϱ r ≤ 1) ∧ ∀ (θ₀ : Homogenization.Vec 2 → ℝ) (Dθ₀ : Homogenization.Vec 2 → Homogenization.Vec 2), IsPeriodicH1With θ₀ Dθ₀ → Homogenization.MeanZeroOn unitCube θ₀ → ∀ (θ : ℝ → ℝ → Homogenization.Vec 2 → ℝ) (Dθ : ℝ → ℝ → Homogenization.Vec 2 → Homogenization.Vec 2), (∀ (κ : ℝ), 0 < κ → IsWeakSolutionGrad b κ θ₀ (θ κ) (Dθ κ)) → Filter.limsup (fun (κ : ℝ) => κ * spaceTimeGradNormSq (Dθ κ)) (nhdsWithin 0 (Set.Ioi 0)) ≥ ϱ (√(l2NormSq θ₀) / √(gradNormSq Dθ₀)) ^ 2 * l2NormSq θ₀

Theorem 1.1 of Armstrong–Vicol (anomalous dissipation), in dimension 2. For every α ∈ (0, 1/3) there is a divergence-free, ℤ²-periodic drift b in C⁰_t C^{0,α}_x ∩ C^{0,α}_t C⁰_x on [0,1] × 𝕋² and a rate ϱ with values in (0,1] such that every mean-zero H¹ datum satisfies limsup_{κ→0⁺} κ ‖∇θ^κ‖²_{L²((0,1)×𝕋²)} ≥ ϱ(‖θ₀‖_{L²}/‖∇θ₀‖_{L²})² ‖θ₀‖²_{L²}.