Hölder bound of the top iterate θ_M (analytic case of r.LeBron.2) #
θ_M = θ_{m₀-1} + ∑_{m=m₀}^{M} (θ_m − θ_{m-1}): Lemma U for the base level m₀ - 1
(κ_{m₀-1} ≥ c₁ ε_{m₀-1}^P), Lemma r.LeBron for the increments, and the telescoping chain lemma.
theorem
AVenhance.Infra.FullTheorem.thetaM_holder
{β C₀ CU μB CB c₁ Λ₁ : ℝ}
(hU : LemmaUWith CU)
(hCU : 0 < CU)
(hμB : 0 < μB)
(hB : LebronWith β C₀ μB CB)
(hc₁ : 0 < c₁)
(hW : WindowWith β C₀ c₁ Λ₁)
{I : Ingredients β}
(hz : I.Czeta ≤ C₀)
(hx : I.Cxi ≤ C₀)
(hh : I.Chat ≤ C₀)
(hCB : CB ≤ ↑I.Λ)
(hΛ₁ : Λ₁ ≤ ↑I.Λ)
{Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ}
(hΦ : IsStreamSeq I Φ)
{κ : ℝ}
(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 θ₀)
(hm₀M : mTheta0 β I.Λ R ≤ M)
{θs : ℕ → ℝ → Homogenization.Vec 2 → ℝ}
(hθs :
∀ (j : ℕ),
mTheta0 β I.Λ R - 1 ≤ j →
j ≤ M →
IsClassicalSol (streamVel (Φ j)) (I.kappaSeq κ M j) (fun (x : ℝ) (x_1 : Homogenization.Vec 2) => 0) θ₀ (θs j))
: