Smoothness and periodicity of the defect matrices at a fixed time

For fixed (m, k, t) the entries of the defect matrices D_k, E_k are C^∞ and ℤ²-periodic in the position; the Y = X⁻¹_{m-1,l_k}(t,·) gradient is periodic because Y is lattice equivariant, and ∇Χ_{m,k} is periodic because the shear field is.

theorem AVenhance.Infra.Section5.Contracts.sd_xFlowInv_slice {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (l : ℤ) (t : ℝ) : ContDiff ℝ (↑⊤) (I.xFlowInv hΦ m l t)

theorem AVenhance.Infra.Section5.Contracts.sd_chiMK_component_contDiff {β : ℝ} (I : Ingredients β) (κm : ℝ) (m : ℕ) (k : ℤ) (t : ℝ) (j : Fin 2) : ContDiff ℝ ↑⊤ fun (z : Homogenization.Vec 2) => I.chiMK κm m k t z j

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

theorem AVenhance.Infra.Section5.Contracts.sd_gradChi_contDiff {β : ℝ} (I : Ingredients β) (κm : ℝ) (m : ℕ) (k : ℤ) (t : ℝ) (a j : Fin 2) : ContDiff ℝ ↑⊤ fun (y : Homogenization.Vec 2) => gradMatrix (fun (z : Homogenization.Vec 2) => I.chiMK κm m k t z) y a j

Entries of ∇Χ_{m,k} are C^∞.

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

Entries of ∇Χ_{m,k} are ℤ²-periodic.

theorem AVenhance.Infra.Section5.Contracts.sd_gradY_contDiff {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (l : ℤ) (t : ℝ) (i a : Fin 2) : ContDiff ℝ ↑⊤ fun (x : Homogenization.Vec 2) => gradMatrix (fun (z : Homogenization.Vec 2) => I.xFlowInv hΦ m l t z) x i a

theorem AVenhance.Infra.Section5.Contracts.sd_gradY_periodic {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (l : ℤ) (t : ℝ) (i a : Fin 2) : IsZ2Periodic fun (x : Homogenization.Vec 2) => gradMatrix (fun (z : Homogenization.Vec 2) => I.xFlowInv hΦ m l t z) x i a

theorem AVenhance.Infra.Section5.Contracts.sd_gradChi_comp_contDiff {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (κm : ℝ) (m : ℕ) (k : ℤ) (t : ℝ) (a j : Fin 2) : ContDiff ℝ ↑⊤ fun (x : Homogenization.Vec 2) => gradMatrix (fun (z : Homogenization.Vec 2) => I.chiMK κm m k t z) (I.xFlowInv hΦ m (lIdx β I.Λ m k) t x) a j

Entries of ∇Χ_{m,k} ∘ Y are C^∞.

theorem AVenhance.Infra.Section5.Contracts.sd_gradChi_comp_periodic {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (κm : ℝ) (m : ℕ) (k : ℤ) (t : ℝ) (a j : Fin 2) : IsZ2Periodic fun (x : Homogenization.Vec 2) => gradMatrix (fun (z : Homogenization.Vec 2) => I.chiMK κm m k t z) (I.xFlowInv hΦ m (lIdx β I.Λ m k) t x) a j

D_k

theorem AVenhance.Infra.Section5.Contracts.sd_defect4_contDiff {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κm : ℝ) (k : ℤ) (t : ℝ) (i j : Fin 2) : ContDiff ℝ ↑⊤ fun (x : Homogenization.Vec 2) => sdDefect4 I hΦ m κm k t x i j

theorem AVenhance.Infra.Section5.Contracts.sd_defect4_periodic {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κm : ℝ) (k : ℤ) (t : ℝ) : IsZ2Periodic (sdDefect4 I hΦ m κm k t)

E_k

theorem AVenhance.Infra.Section5.Contracts.sd_psiCoeff_contDiff {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (k : ℤ) (t : ℝ) : ContDiff ℝ ↑⊤ fun (x : Homogenization.Vec 2) => I.hatZetaML m (lIdx β I.Λ m k) t * I.zetaMK m k t * psi β I.Λ m k (I.xFlowInv hΦ m (lIdx β I.Λ m k) t x)

theorem AVenhance.Infra.Section5.Contracts.sd_flowGradK_contDiff {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (k : ℤ) (t : ℝ) (i j : Fin 2) : ContDiff ℝ ↑⊤ fun (x : Homogenization.Vec 2) => flowGradK I hΦ m k t x i j

theorem AVenhance.Infra.Section5.Contracts.sd_defect5_contDiff {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κm : ℝ) (k : ℤ) (t : ℝ) (i j : Fin 2) : ContDiff ℝ ↑⊤ fun (x : Homogenization.Vec 2) => sdDefect5 I hΦ m κm k t x i j

theorem AVenhance.Infra.Section5.Contracts.sd_defect5_periodic {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κm : ℝ) (k : ℤ) (t : ℝ) : IsZ2Periodic (sdDefect5 I hΦ m κm k t)