Main theorem from the three statements

anomalous_dissipation_of_keystones derives the main theorem (t.anomalous.diffusion) from the literal statements of the estimates step-down estimate, classical well-posedness and stream-function estimates. Everything else (choice of β, ingredients, stream sequence, Hölder / ∃ b packaging, later-start cascade, H¹ reduction) is proved. The statement files themselves are never imported.

theorem AVenhance.Infra.Section5.Integration.AnomalousDissipation.limit_periodic {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} {φ : ℝ → Homogenization.Vec 2 → ℝ} (hΦ : ∀ (M : ℕ), IsAdmissibleStream (Φ M)) (htend : ∀ (t : ℝ) (x : Homogenization.Vec 2), Filter.Tendsto (fun (M : ℕ) => Φ M t x) Filter.atTop (nhds (φ t x))) (t : ℝ) : IsZ2Periodic (φ t)

The pointwise limit of periodic streams is periodic.

theorem AVenhance.Infra.Section5.Integration.AnomalousDissipation.limit_aestronglyMeasurable {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} {φ : ℝ → Homogenization.Vec 2 → ℝ} (hΦ : ∀ (M : ℕ), IsAdmissibleStream (Φ M)) (htend : ∀ (t : ℝ) (x : Homogenization.Vec 2), Filter.Tendsto (fun (M : ℕ) => Φ M t x) Filter.atTop (nhds (φ t x))) (μ : MeasureTheory.Measure (ℝ × Homogenization.Vec 2)) : MeasureTheory.AEStronglyMeasurable (fun (p : ℝ × Homogenization.Vec 2) => φ p.1 p.2) μ

The pointwise limit of admissible streams is jointly measurable.

theorem AVenhance.Infra.Section5.Integration.AnomalousDissipation.exists_beta (α : ℝ) (hα₀ : 0 < α) (hα₁ : α < 1 / 3) : ∃ (β : ℝ), 6 / 5 ≤ β ∧ α < β - 1 ∧ β < 4 / 3 ∧ 1 < β

Numerical choice of the exponent β.

theorem AVenhance.Infra.Section5.Integration.anomalous_dissipation_of_keystones (hA8 : ∀ (β C₀ : ℝ), IndyStepDownStatement β C₀) (hA1c : ClassicalWellposedStatement) (hA3b : ∀ (β : ℝ), LimitFieldRegularStatement β) : AnomalousDissipationStatement

Main theorem from the three estimates. The main theorem follows from the literal statements of step-down estimate, classical well-posedness and Stream-function estimates; everything else is proved.