The classical chain θ_{m₀-1}, …, θ_M and the Hölder bound of θ_M

• Lemma U for the classical iterates (uniform drift bound velBound β);
• existence of the classical chain (classical well-posedness);
• the series ∑ ε_{n-1}^s is bounded by 1/(1-128^{-s});
• θ_M is μ₁-Hölder in L² with constant S₁ ε_{m₀-1}^{-P/2} ‖θ₀‖_{H¹} (Lemma U at the base level and Lemma r.LeBron for the increments).

theorem AVenhance.Infra.FullTheorem.classical_quarter {CU : ℝ} (hU : LemmaUWith CU) {β : ℝ} {I : Ingredients β} {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (j : ℕ) {κj : ℝ} (h0 : 0 < κj) (h1 : κj ≤ 1) {θ₀ : Homogenization.Vec 2 → ℝ} (hθ₀ : ContDiff ℝ (↑⊤) θ₀) (hper : IsZ2Periodic θ₀) {θ : ℝ → Homogenization.Vec 2 → ℝ} (hθ : IsClassicalSol (streamVel (Φ j)) κj (fun (x : ℝ) (x_1 : Homogenization.Vec 2) => 0) θ₀ θ) (s : ℝ) : s ∈ Set.Icc 0 1 → ∀ t ∈ Set.Icc 0 1, √(l2NormSq fun (x : Homogenization.Vec 2) => θ t x - θ s x) ≤ CU * (1 + velBound β) / √κj * |t - s| ^ (1 / 4) * √(l2NormSq θ₀ + gradNormSq (spaceGrad θ₀))

Lemma U for a classical iterate.

theorem AVenhance.Infra.FullTheorem.eps_sum_Ioc_le {β s : ℝ} (I : Ingredients β) (hs : 0 < s) (n₀ M : ℕ) (hn₀ : 2 ≤ n₀) : ∑ n ∈ Finset.Ioc (n₀ - 1) M, epsilon β I.Λ (n - 1) ^ s ≤ 1 / (1 - 128 ^ (-s))

The series bound ∑_{n ∈ (n₀-1, M]} ε_{n-1}^s ≤ 1/(1-128^{-s}) for n₀ ≥ 2.

theorem AVenhance.Infra.FullTheorem.exists_classical_chain {β : ℝ} {I : Ingredients β} {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) {κ : ℝ} {M n₀ : ℕ} (hpos : ∀ (j : ℕ), n₀ ≤ j → j ≤ M → 0 < I.kappaSeq κ M j) {θ₀ : Homogenization.Vec 2 → ℝ} (hθ₀ : ContDiff ℝ (↑⊤) θ₀) (hper : IsZ2Periodic θ₀) : ∃ (θs : ℕ → ℝ → Homogenization.Vec 2 → ℝ), ∀ (j : ℕ), n₀ ≤ j → j ≤ M → IsClassicalSol (streamVel (Φ j)) (I.kappaSeq κ M j) (fun (x : ℝ) (x_1 : Homogenization.Vec 2) => 0) θ₀ (θs j)

The classical chain exists (classical well-posedness), at every level with positive diffusivity.