Cutoff localization of the shear coefficient on a selected mode.

theorem AVenhance.Infra.Section5.psiTilde_eq_selected_mode {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (hm : 1 ≤ m) (k : ℤ) (t : ℝ) (x : Homogenization.Vec 2) (hk : Odd k) (hxi : I.xiMK m k t ≠ 0) : psiTilde I hΦ m t x = I.zetaProd m k t * psi β I.Λ m k (I.xFlowInv hΦ m (lIdx β I.Λ m k) t x)

On the support of an odd fine cutoff, the odd-mode sum defining the pulled shear coefficient reduces to that selected mode.

theorem AVenhance.Infra.Section5.diffusionMatrix_mul_one_plus_gradChi_eq_correctorFlux {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (hm : 1 ≤ m) (κ : ℝ) (k : ℤ) (t : ℝ) (hk : Odd k) (hxi : I.xiMK m k t ≠ 0) : (fun (y : Homogenization.Vec 2) => diffusionMatrix I hΦ m κ t y * (1 + gradChiTilde I hΦ m κ k t y)) = correctorFlux I hΦ m κ k t

The full twisted diffusion matrix agrees with the selected corrector matrix wherever its odd cutoff is nonzero.