Fast factors of the nondivergence parts of twistie4, twistie5

sdFast4 = ∂_aΧ_{m,k,j} and sdFast5 = ζ̂ζ ψ_{m,k} σ_{aj} + κ_m ∂_aΧ_{m,k,j}: continuous, 1/ε_m-periodic (fast periodic at frequency ergodicFrequency β Λ m = ε_m⁻¹), mean zero, and bounded by a_m ε_m² / κ_m resp. 2 a_m ε_m².

sdFast4

theorem AVenhance.Infra.Section5.Contracts.sdFast4_isFastPeriodic {β : ℝ} (I : Ingredients β) {m : ℕ} (hm : 1 ≤ m) (κm : ℝ) (k : ℤ) (t : ℝ) (p q : Fin 2) : Ergodic.IsFastPeriodic (ergodicFrequency β I.Λ m) (sdFast4 I κm m k t p q)

theorem AVenhance.Infra.Section5.Contracts.sdFast4_continuous {β : ℝ} (I : Ingredients β) (m : ℕ) (κm : ℝ) (k : ℤ) (t : ℝ) (p q : Fin 2) : Continuous (sdFast4 I κm m k t p q)

theorem AVenhance.Infra.Section5.Contracts.sdFast4_cellAverage {β : ℝ} (I : Ingredients β) {m : ℕ} (hm : 1 ≤ m) (κm : ℝ) (k : ℤ) (t : ℝ) (p q : Fin 2) : Ergodic.cellAverage (sdFast4 I κm m k t p q) = 0

theorem AVenhance.Infra.Section5.Contracts.sdFast4_abs_le {β : ℝ} (I : Ingredients β) {m : ℕ} (hm : 1 ≤ m) {κm : ℝ} (hκm : 0 < κm) (k : ℤ) (t : ℝ) (p q : Fin 2) (y : Homogenization.Vec 2) : |sdFast4 I κm m k t p q y| ≤ a β I.Λ m * epsilon β I.Λ m ^ 2 / κm

ψ_{m,k}

theorem AVenhance.Infra.Section5.Contracts.psi_fast_shift {β : ℝ} (I : Ingredients β) {m : ℕ} (k : ℤ) (y : Homogenization.Vec 2) (n : Fin 2 → ℤ) : psi β I.Λ m k (y + fun (i : Fin 2) => ↑(n i) / ↑(ergodicFrequency β I.Λ m)) = psi β I.Λ m k y

theorem AVenhance.Infra.Section5.Contracts.psi_spaceAvg {β : ℝ} (I : Ingredients β) {m : ℕ} (hm : 1 ≤ m) (k : ℤ) : spaceAvg (psi β I.Λ m k) = 0

sdFast5

theorem AVenhance.Infra.Section5.Contracts.sdFast5_continuous {β : ℝ} (I : Ingredients β) (m : ℕ) (κm : ℝ) (k : ℤ) (t : ℝ) (p q : Fin 2) : Continuous (sdFast5 I κm m k t p q)

theorem AVenhance.Infra.Section5.Contracts.sdFast5_isFastPeriodic {β : ℝ} (I : Ingredients β) {m : ℕ} (hm : 1 ≤ m) (κm : ℝ) (k : ℤ) (t : ℝ) (p q : Fin 2) : Ergodic.IsFastPeriodic (ergodicFrequency β I.Λ m) (sdFast5 I κm m k t p q)

theorem AVenhance.Infra.Section5.Contracts.sdFast5_cellAverage {β : ℝ} (I : Ingredients β) {m : ℕ} (hm : 1 ≤ m) (κm : ℝ) (k : ℤ) (t : ℝ) (p q : Fin 2) : Ergodic.cellAverage (sdFast5 I κm m k t p q) = 0

theorem AVenhance.Infra.Section5.Contracts.sdFast5_abs_le {β : ℝ} (I : Ingredients β) {m : ℕ} (hm : 1 ≤ m) {κm : ℝ} (hκm : 0 < κm) (k : ℤ) (t : ℝ) (p q : Fin 2) (y : Homogenization.Vec 2) : |sdFast5 I κm m k t p q y| ≤ 2 * (a β I.Λ m * epsilon β I.Λ m ^ 2)