Actual iterates: periodicity, increment equations and telescoping. These are structural prerequisites, not the quantitative V estimates.

def AVenhance.Infra.Section4.iterateIncrement (T : ℕ → ℝ → Homogenization.Vec 2 → ℝ) (i : ℕ) : ℝ → Homogenization.Vec 2 → ℝ

The increments in e.T.minus.theta.m-1, including V⁰ = θprev.

Equations

• AVenhance.Infra.Section4.iterateIncrement T i = if i = 0 then T 0 else fun (t : ℝ) (x : Homogenization.Vec 2) => T i t x - T (i - 1) t x

@[simp]

theorem AVenhance.Infra.Section4.iterateIncrement_zero (T : ℕ → ℝ → Homogenization.Vec 2 → ℝ) : iterateIncrement T 0 = T 0

@[simp]

theorem AVenhance.Infra.Section4.iterateIncrement_succ (T : ℕ → ℝ → Homogenization.Vec 2 → ℝ) (i : ℕ) : iterateIncrement T (i + 1) = fun (t : ℝ) (x : Homogenization.Vec 2) => T (i + 1) t x - T i t x

theorem AVenhance.Infra.Section4.iterate_eq_sum_increments (T : ℕ → ℝ → Homogenization.Vec 2 → ℝ) (N : ℕ) (t : ℝ) (x : Homogenization.Vec 2) : T N t x = ∑ i ∈ Finset.range (N + 1), iterateIncrement T i t x

Telescoping identity for the actual increment definition.

theorem AVenhance.Infra.Section4.iterate_sub_theta_eq_sum {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) {m : ℕ} {κm κprev : ℝ} {θ₀ : Homogenization.Vec 2 → ℝ} {θprev : ℝ → Homogenization.Vec 2 → ℝ} {T : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hT : I.IsTIterates hΦ m κm κprev θ₀ θprev T) (N : ℕ) (t : ℝ) (x : Homogenization.Vec 2) : T N t x - θprev t x = ∑ i ∈ Finset.range N, iterateIncrement T (i + 1) t x

e.T.minus.theta.m-1 with the base iterate, without assuming estimates.

theorem AVenhance.Infra.Section4.iterates_periodic {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) {m : ℕ} {κm κprev : ℝ} {θ₀ : Homogenization.Vec 2 → ℝ} {θprev : ℝ → Homogenization.Vec 2 → ℝ} {T : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hT : I.IsTIterates hΦ m κm κprev θ₀ θprev T) (hθ : ∀ (t : ℝ), 0 ≤ t → IsZ2Periodic (θprev t)) {i : ℕ} (hi : i ≤ Nstar β) {t : ℝ} (ht : 0 ≤ t) : IsZ2Periodic (T i t)

e.Tm-1.i#periodic, including the theta base case.

theorem AVenhance.Infra.Section4.IteratesBasic.classical_space_smooth {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} {κ : ℝ} {F : ℝ → Homogenization.Vec 2 → ℝ} {θ₀ : Homogenization.Vec 2 → ℝ} {u : ℝ → Homogenization.Vec 2 → ℝ} (hu : IsClassicalSol b κ F θ₀ u) {t : ℝ} (ht : 0 ≤ t) : ContDiff ℝ (↑⊤) (u t)

theorem AVenhance.Infra.Section4.IteratesBasic.classical_time_differentiable {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} {κ : ℝ} {F : ℝ → Homogenization.Vec 2 → ℝ} {θ₀ : Homogenization.Vec 2 → ℝ} {u : ℝ → Homogenization.Vec 2 → ℝ} (hu : IsClassicalSol b κ F θ₀ u) {t : ℝ} (ht : 0 < t) (x : Homogenization.Vec 2) : DifferentiableAt ℝ (fun (s : ℝ) => u s x) t

theorem AVenhance.Infra.Section4.classicalSol_sub {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} {κ : ℝ} {F G : ℝ → Homogenization.Vec 2 → ℝ} {u₀ v₀ : Homogenization.Vec 2 → ℝ} {u v : ℝ → Homogenization.Vec 2 → ℝ} (hu : IsClassicalSol b κ F u₀ u) (hv : IsClassicalSol b κ G v₀ v) : IsClassicalSol b κ (fun (t : ℝ) (x : Homogenization.Vec 2) => F t x - G t x) (fun (x : Homogenization.Vec 2) => u₀ x - v₀ x) fun (t : ℝ) (x : Homogenization.Vec 2) => u t x - v t x

Subtracting two actual classical solutions gives the difference equation. No energy or increment estimate is assumed.

theorem AVenhance.Infra.Section4.first_increment_classical {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) {m : ℕ} {κm κprev : ℝ} {θ₀ : Homogenization.Vec 2 → ℝ} {θprev : ℝ → Homogenization.Vec 2 → ℝ} {T : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hT : I.IsTIterates hΦ m κm κprev θ₀ θprev T) (hθ : IsClassicalSol (streamVel (Φ (m - 1))) κprev (fun (x : ℝ) (x_1 : Homogenization.Vec 2) => 0) θ₀ θprev) (hN : 1 ≤ Nstar β) : IsClassicalSol (streamVel (Φ (m - 1))) κprev (I.TForcing hΦ m κm κprev θprev) (fun (x : Homogenization.Vec 2) => 0) (iterateIncrement T 1)

The first positive increment solves the forced equation with zero data.

theorem AVenhance.Infra.Section4.later_increment_classical {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) {m : ℕ} {κm κprev : ℝ} {θ₀ : Homogenization.Vec 2 → ℝ} {θprev : ℝ → Homogenization.Vec 2 → ℝ} {T : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hT : I.IsTIterates hΦ m κm κprev θ₀ θprev T) (i : ℕ) (hi : i + 2 ≤ Nstar β) : IsClassicalSol (streamVel (Φ (m - 1))) κprev (fun (t : ℝ) (x : Homogenization.Vec 2) => I.TForcing hΦ m κm κprev (T (i + 1)) t x - I.TForcing hΦ m κm κprev (T i) t x) (fun (x : Homogenization.Vec 2) => 0) (iterateIncrement T (i + 2))

Each later increment solves the actual difference of consecutive forcing terms, with zero initial data.

theorem AVenhance.Infra.Section4.Jcut_le_iteration_budget (β : ℝ) : Jcut β ≤ Nstar β

The corrected Jcut does not exceed the actual iteration budget.