Smooth analytic limit dissipation

Combines the base energy at the later start (later_base_energy), the telescoping chain (chain_lower_bound, from conjunct (ii) of the step-down body), and the stream-difference estimate (weak_dissipation_ge_classical) along κ^{(M)} = ε_M^{2β/(q+1)} → 0⁺ to bound the limsup of the dissipation of an arbitrary weak family for the limit drift streamVel φ.

theorem AVenhance.Infra.Section5.RelativeError.smooth_analytic_limit_dissipation (β C₀ : ℝ) (hβ : 6 / 5 ≤ β) (hA8 : Integration.IndyStepDownStatement β C₀) : ∃ (Λ₀ : ℝ), ∀ (I : Ingredients β), I.Czeta ≤ C₀ → I.Cxi ≤ C₀ → I.Chat ≤ C₀ → Λ₀ ≤ ↑I.Λ → ∀ (Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ), IsStreamSeq I Φ → (∀ (j : ℕ), ClassicalSolvable (streamVel (Φ j))) → ∀ (Ctail : ℝ), 1 ≤ Ctail → ∀ (φ : ℝ → Homogenization.Vec 2 → ℝ), MeasureTheory.AEStronglyMeasurable (fun (p : ℝ × Homogenization.Vec 2) => φ p.1 p.2) (MeasureTheory.volume.restrict (Set.Icc 0 1 ×ˢ Set.univ)) → (∀ t ∈ Set.Icc 0 1, IsZ2Periodic (φ t)) → (∀ t ∈ Set.Icc 0 1, Differentiable ℝ (φ t)) → (∀ (M : ℕ), 1 ≤ M → ∀ t ∈ Set.Icc 0 1, ∀ (x : Homogenization.Vec 2), |φ t x - Φ M t x| ≤ Ctail * epsilon β I.Λ (M + 1) ^ β) → MeasureTheory.AEStronglyMeasurable (fun (p : ℝ × Homogenization.Vec 2) => streamVel φ p.1 p.2) (MeasureTheory.volume.restrict (Set.Icc 0 1 ×ˢ Set.univ)) → (∃ (B : ℝ), ∀ t ∈ Set.Icc 0 1, ∀ (x : Homogenization.Vec 2), ‖streamVel φ t x‖ ≤ B) → (∀ t ∈ Set.Icc 0 1, IsZ2Periodic (streamVel φ t)) → IsDivFree (streamVel φ) → ∃ (c : ℝ), 0 < c ∧ AnalyticDissipationInput (streamVel φ) c (pPlus β)

.