Classical chains, telescoping in sup-L², and the tail of the ε-series

theorem AVenhance.Infra.FullTheorem.chain_exists {β C₀ c₁ Λ₁ : ℝ} (hW : WindowWith β C₀ c₁ Λ₁) (hc₁ : 0 < c₁) {I : Ingredients β} (hz : I.Czeta ≤ C₀) (hx : I.Cxi ≤ C₀) (hh : I.Chat ≤ C₀) (hΛ₁ : Λ₁ ≤ ↑I.Λ) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) {κ : ℝ} (hκ : κ ∈ permissibleSet β I.Λ) {M : ℕ} (hM : 1 ≤ M) (hκM : κ ∈ permittedInterval β I.Λ M) {R : ℝ} (hR : 0 < R) (hMm : mTheta0 β I.Λ R ≤ M) {θ₀ : Homogenization.Vec 2 → ℝ} (hθ₀ : ContDiff ℝ (↑⊤) θ₀) (hper : IsZ2Periodic θ₀) : ∃ (θs : ℕ → ℝ → Homogenization.Vec 2 → ℝ), ∀ (j : ℕ), mTheta0 β I.Λ R - 1 ≤ j → j ≤ M → 0 < I.kappaSeq κ M j ∧ IsClassicalSol (streamVel (Φ j)) (I.kappaSeq κ M j) (fun (x : ℝ) (x_1 : Homogenization.Vec 2) => 0) θ₀ (θs j)

The classical chain θ_{m₀-1}, …, θ_M exists and its diffusivities are positive.

theorem AVenhance.Infra.FullTheorem.chain_sup {f : ℕ → ℝ → Homogenization.Vec 2 → ℝ} {c : ℕ → ℝ} {ℓ : ℕ} {t : ℝ} (M : ℕ) : ℓ ≤ M → (∀ (n : ℕ), ℓ ≤ n → n ≤ M → Continuous (f n t)) → (∀ (n : ℕ), ℓ < n → n ≤ M → √(l2NormSq fun (x : Homogenization.Vec 2) => f n t x - f (n - 1) t x) ≤ c n) → √(l2NormSq fun (x : Homogenization.Vec 2) => f M t x - f ℓ t x) ≤ ∑ n ∈ Finset.Ioc ℓ M, c n

Telescoping in sup-L² at a fixed time.

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

Tail of the series ∑_{n ∈ (ℓ, M]} ε_{n-1}^s ≤ ε_ℓ^s/(1-Λ^{-s}).