Case M ≥ m₀ of the analytic case of r.LeBron.2 #
θ = θ_M + (θ − θ_M): the chain bound for θ_M (ThetaM) plus the tail piece (TailHolder).
theorem
AVenhance.Infra.FullTheorem.case_big
{β C₀ CU μB CB c₁ Λ₁ Ct Bφ : ℝ}
(hU : LemmaUWith CU)
(hCU : 0 < CU)
(hμB : 0 < μB)
(hB : LebronWith β C₀ μB CB)
(hc₁ : 0 < c₁)
(hW : WindowWith β C₀ c₁ Λ₁)
(hCt : 0 ≤ Ct)
(hBφ : 0 ≤ Bφ)
{I : Ingredients β}
(hz : I.Czeta ≤ C₀)
(hx : I.Cxi ≤ C₀)
(hh : I.Chat ≤ C₀)
(hCB : CB ≤ ↑I.Λ)
(hΛ₁ : Λ₁ ≤ ↑I.Λ)
(hΛs : 2 ^ (1 / (β - gamma β)) ≤ ↑I.Λ)
{Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ}
(hΦ : IsStreamSeq I Φ)
{φ : ℝ → Homogenization.Vec 2 → ℝ}
(htail : ∀ (M : ℕ) (t : ℝ) (x : Homogenization.Vec 2), |φ t x - Φ M t x| ≤ Ct * epsilon β I.Λ (M + 1) ^ β)
(hφ_meas :
MeasureTheory.AEStronglyMeasurable (fun (p : ℝ × Homogenization.Vec 2) => φ p.1 p.2)
(MeasureTheory.volume.restrict (Set.Icc 0 1 ×ˢ Set.univ)))
(hφ_per : ∀ t ∈ Set.Icc 0 1, IsZ2Periodic (φ t))
(hφ_diff : ∀ t ∈ Set.Icc 0 1, Differentiable ℝ (φ t))
(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φ)
{κ : ℝ}
(hκ : κ ∈ permissibleSet β I.Λ)
{M : ℕ}
(hM : 1 ≤ M)
(hκM : κ ∈ permittedInterval β I.Λ M)
{R : ℝ}
(hR : 0 < R)
{θ₀ : Homogenization.Vec 2 → ℝ}
(hθ₀ : ContDiff ℝ (↑⊤) θ₀)
(hper : IsZ2Periodic θ₀)
(hmean : Homogenization.MeanZeroOn unitCube θ₀)
(han : IsThetaAnalytic R θ₀)
{θ : ℝ → Homogenization.Vec 2 → ℝ}
(hθ : IsWeakSolution (streamVel φ) κ θ₀ θ)
(hMm : mTheta0 β I.Λ R ≤ M)
: