The corrector χ_{m,k} as the fast factor of the twistie1 ergodic estimate

For each component j, g = χ_{m,k}(t,·)_j = -τ_k(t) (u_{m,k})_j is ε_m-periodic (fast periodic at the integer frequency ε_m⁻¹), has zero cell mean (it is a constant times a coordinate cosine of integer frequency), and is bounded by ε_m · (a_m ε_m²/κ_m) (e.corrm).

theorem AVenhance.Infra.Section5.Contracts.se_intervalAverage_cos_nat {N : ℕ} (hN : 0 < N) : ∫ (t : ℝ) in 0..1, Real.cos (2 * Real.pi * ↑N * t) = 0

∫₀¹ cos(2π N t) dt = 0 for N ≥ 1.

theorem AVenhance.Infra.Section5.Contracts.se_uShear_form {β : ℝ} (I : Ingredients β) (m : ℕ) (k : ℤ) (j : Fin 2) : ∃ (c : ℝ) (r : Fin 2), ∀ (y : Homogenization.Vec 2), uShear β I.Λ m k y j = c * Real.cos (2 * Real.pi * ↑(ergodicFrequency β I.Λ m) * y r)

Every component of u_{m,k} is a constant times a coordinate cosine of frequency N = ε_m⁻¹.

theorem AVenhance.Infra.Section5.Contracts.se_chi_form {β : ℝ} (I : Ingredients β) (m : ℕ) (κ : ℝ) (k : ℤ) (t : ℝ) (j : Fin 2) : ∃ (c : ℝ) (r : Fin 2), ∀ (y : Homogenization.Vec 2), I.chiMK κ m k t y j = c * Real.cos (2 * Real.pi * ↑(ergodicFrequency β I.Λ m) * y r)

Generic form of a corrector component.

theorem AVenhance.Infra.Section5.Contracts.se_chi_continuous {β : ℝ} (I : Ingredients β) (m : ℕ) (κ : ℝ) (k : ℤ) (t : ℝ) (j : Fin 2) : Continuous fun (y : Homogenization.Vec 2) => I.chiMK κ m k t y j

theorem AVenhance.Infra.Section5.Contracts.se_chi_fastPeriodic {β : ℝ} (I : Ingredients β) (m : ℕ) (κ : ℝ) (k : ℤ) (t : ℝ) (j : Fin 2) : Ergodic.IsFastPeriodic (ergodicFrequency β I.Λ m) fun (y : Homogenization.Vec 2) => I.chiMK κ m k t y j

theorem AVenhance.Infra.Section5.Contracts.se_chi_cellAverage {β : ℝ} (I : Ingredients β) (m : ℕ) (κ : ℝ) (k : ℤ) (t : ℝ) (j : Fin 2) : (Ergodic.cellAverage fun (y : Homogenization.Vec 2) => I.chiMK κ m k t y j) = 0

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

e.corrm: |χ_{m,k,j}| ≤ ε_m · (a_m ε_m²/κ).