Case M ≤ m₀ − 1 of the analytic case of r.LeBron.2 #
Lemma U directly for θ, with κ ≥ ½ ε_M^{β-γ} ≥ ½ ε_{m₀-1}^{β-γ}.
theorem
AVenhance.Infra.FullTheorem.case_small
{β CU Bφ : ℝ}
(hU : LemmaUWith CU)
(hCU : 0 < CU)
(hBφ : 0 ≤ Bφ)
{I : Ingredients β}
(hΛs : 2 ^ (1 / (β - gamma β)) ≤ ↑I.Λ)
{φ : ℝ → Homogenization.Vec 2 → ℝ}
(hb_meas :
MeasureTheory.AEStronglyMeasurable (fun (p : ℝ × Homogenization.Vec 2) => streamVel φ p.1 p.2)
(MeasureTheory.volume.restrict (Set.Icc 0 1 ×ˢ Set.univ)))
(hb_per : ∀ t ∈ Set.Icc 0 1, IsZ2Periodic (streamVel φ t))
(hdiv : IsDivFree (streamVel φ))
(hb_bdd : ∀ t ∈ Set.Icc 0 1, ∀ (x : Homogenization.Vec 2), ‖streamVel φ t x‖ ≤ Bφ)
{κ : ℝ}
{M : ℕ}
(hM : 1 ≤ M)
(hκM : κ ∈ permittedInterval β I.Λ M)
{R : ℝ}
{θ₀ : Homogenization.Vec 2 → ℝ}
(hθ₀ : ContDiff ℝ (↑⊤) θ₀)
(hper : IsZ2Periodic θ₀)
{θ : ℝ → Homogenization.Vec 2 → ℝ}
(hθ : IsWeakSolution (streamVel φ) κ θ₀ θ)
(hMm : M ≤ mTheta0 β I.Λ R - 1)
: