Proof of the combined main theorem

anomalous_dissipation_full is the combined main theorem (AVenhance.anomalous_dissipation_full) without the IsContinuousIntoHolder conjunct, which the public statement derives from it at a larger exponent. It is proved by anomalous_dissipation_full_of_noSelection from noSelection_of_separated, separatedChains_of_inputs and the input contracts.

theorem AVenhance.Proofs.anomalous_dissipation_full (α : ℝ) (hα₀ : 0 < α) (hα₁ : α < 1 / 3) : ∃ (b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2), IsHolderClass α b ∧ IsDivFree b ∧ ∃ (ϱ : ℝ → ℝ), (∀ (r : ℝ), 0 < ϱ r ∧ ϱ r ≤ 1) ∧ ∃ (κseq : ℕ → ℝ), (∀ (j : ℕ), 0 < κseq j) ∧ (∀ (j : ℕ), 4 * κseq (j + 1) < κseq j) ∧ Filter.Tendsto κseq Filter.atTop (nhds 0) ∧ ∃ (μ : ℝ) (ν : ℝ) (C : ℝ), 0 < μ ∧ 0 < ν ∧ ∃ (𝒟 : Set (Homogenization.Vec 2 → ℝ)), (∀ (θ₀ : 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 θ₀) ∧ (∀ (θ₀ : Homogenization.Vec 2 → ℝ) (Dθ₀ : Homogenization.Vec 2 → Homogenization.Vec 2), IsPeriodicH1With θ₀ Dθ₀ → Homogenization.MeanZeroOn unitCube θ₀ → ∀ κ ∈ ⋃ (j : ℕ), Set.Icc (κseq j / 2) (2 * κseq j), ∀ (θ : ℝ → Homogenization.Vec 2 → ℝ), IsWeakSolution b κ θ₀ θ → HolderTimeL2Le μ (C * √(l2NormSq θ₀ + gradNormSq Dθ₀)) θ) ∧ (∀ θ₀ ∈ 𝒟, ContDiff ℝ (↑⊤) θ₀ ∧ IsZ2Periodic θ₀ ∧ Homogenization.MeanZeroOn unitCube θ₀ ∧ 0 < l2NormSq θ₀) ∧ (∀ θ₀ ∈ 𝒟, ∀ (c : ℝ), c ≠ 0 → (fun (x : Homogenization.Vec 2) => c * θ₀ x) ∈ 𝒟) ∧ (∀ (N : ℕ), ∃ (n : ℕ), N ≤ n ∧ (fun (x : Homogenization.Vec 2) => Real.cos (2 * Real.pi * ↑n * x 0)) ∈ 𝒟) ∧ ∀ θ₀ ∈ 𝒟, ∀ (θ : ℝ → ℝ → Homogenization.Vec 2 → ℝ), (∀ (κ : ℝ), 0 < κ → IsWeakSolution b κ θ₀ (θ κ)) → ∃ (θ₁ : ℝ → Homogenization.Vec 2 → ℝ) (θ₂ : ℝ → Homogenization.Vec 2 → ℝ), IsTransportWeakSolution b θ₀ θ₁ ∧ IsTransportWeakSolution b θ₀ θ₂ ∧ (∀ (η : ℝ), 0 < η → ∀ᶠ (j : ℕ) in Filter.atTop, HolderTimeL2Le ν η fun (t : ℝ) (x : Homogenization.Vec 2) => θ (κseq (2 * j) / 2) t x - θ₁ t x) ∧ (∀ (η : ℝ), 0 < η → ∀ᶠ (j : ℕ) in Filter.atTop, HolderTimeL2Le ν η fun (t : ℝ) (x : Homogenization.Vec 2) => θ (2 * κseq (2 * j)) t x - θ₂ t x) ∧ ∃ t ∈ Set.Icc 0 1, l2NormSq (θ₁ t) ≠ l2NormSq (θ₂ t)

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