Proof of the main theorem, and its conditional assembly from analytic dissipation

anomalous_dissipation is the proof of the main theorem (AVenhance.anomalous_dissipation): its statement is the public one without the IsContinuousIntoHolder conjunct, which the public statement derives from this theorem at a larger exponent. It is proved from the step-down estimate (AVenhance.indystepdown) and classical well-posedness (AVenhance.classical_wellposed) by Infra.Section5.Integration.anomalous_dissipation_of_A8_A1c (the stream-function estimates are used inside). The theorem takes only the range of α; the drift and all other inputs are constructed internally. The module also proves the measurability of Hölder drifts used in the H¹ reduction.

theorem AVenhance.Proofs.AnomalousDissipation.holder_drift_aestronglyMeasurable {α : ℝ} {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hb : IsHolderClass α b) : MeasureTheory.AEStronglyMeasurable (fun (p : ℝ × Homogenization.Vec 2) => b p.1 p.2) (MeasureTheory.volume.restrict (Set.Icc 0 1 ×ˢ Set.univ))

theorem AVenhance.Proofs.anomalous_dissipation (α : ℝ) (hα₀ : 0 < α) (hα₁ : α < 1 / 3) : ∃ (b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2), IsHolderClass α 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 θ₀

The main theorem with the drift class IsHolderClass; see AVenhance.anomalous_dissipation.