recursive construction of the T iterates

assumes only that classical solutions exist for the finite drifts with jointly smooth periodic forcing (ClassicalSolvable; AVenhance.classical_wellposed is its precise form). Then the actual T iterates T^{(0)} = θ_{m-1}, T^{(i)} the classical solution of e.Tm-1.i are constructed recursively: each T^{(i)} is classical, hence jointly smooth and periodic, so the next forcing (TForcing_contDiffOn, TForcing_periodic) is admissible.

def AVenhance.Infra.Section5.RelativeError.ClassicalSolvable (b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2) : Prop

Classical solvability of the finite-level transport–diffusion problem with smooth data and smooth periodic forcing (the existence hypothesis of the relative step; AVenhance.classical_wellposed is its general form).

Equations

• One or more equations did not get rendered due to their size.

theorem AVenhance.Infra.Section5.RelativeError.exists_TIterates {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) {m : ℕ} (hm : 1 ≤ m) {κm κprev : ℝ} (hκm : 0 < κm) (hκprev : 0 < κprev) (hsolv : ClassicalSolvable (streamVel (Φ (m - 1)))) {θ₀ : Homogenization.Vec 2 → ℝ} (hθ₀ : ContDiff ℝ (↑⊤) θ₀) (hθ₀p : IsZ2Periodic θ₀) {θprev : ℝ → Homogenization.Vec 2 → ℝ} (hθprev : IsClassicalSol (streamVel (Φ (m - 1))) κprev (fun (x : ℝ) (x_1 : Homogenization.Vec 2) => 0) θ₀ θprev) : ∃ (T : ℕ → ℝ → Homogenization.Vec 2 → ℝ), I.IsTIterates hΦ m κm κprev θ₀ θprev T

Existence of the T iterates from classical solvability of the finite drifts.