Smoothness and ℤ²-periodicity of the slow factors

The slow factors section5SlowChoice2, section5SlowChoice3 are ξ_{m,k}(t) (a constant in x) times finite sums of products of entries of ∇X⁻¹ - I (respectively I - (∇X∘X⁻¹)ᵀ) and of ∇G_l, each smooth and ℤ²-periodic.

theorem AVenhance.Infra.Section5.Contracts.sds_isZPeriodic_of_isZ2Periodic {α : Type u_1} {f : Homogenization.Vec 2 → α} (h : IsZ2Periodic f) : Ergodic.IsZPeriodic f

theorem AVenhance.Infra.Section5.Contracts.sds_isZ2Periodic_mul {f g : Homogenization.Vec 2 → ℝ} (hf : IsZ2Periodic f) (hg : IsZ2Periodic g) : IsZ2Periodic fun (x : Homogenization.Vec 2) => f x * g x

theorem AVenhance.Infra.Section5.Contracts.sds_isZ2Periodic_sum {ι : Type u_1} (s : Finset ι) {f : ι → Homogenization.Vec 2 → ℝ} (hf : ∀ i ∈ s, IsZ2Periodic (f i)) : IsZ2Periodic fun (x : Homogenization.Vec 2) => ∑ i ∈ s, f i x

theorem AVenhance.Infra.Section5.Contracts.sds_isZ2Periodic_const_mul (c : ℝ) {f : Homogenization.Vec 2 → ℝ} (hf : IsZ2Periodic f) : IsZ2Periodic fun (x : Homogenization.Vec 2) => c * f x

theorem AVenhance.Infra.Section5.Contracts.sds_gradMatrix_entry_periodic {F : Homogenization.Vec 2 → Homogenization.Vec 2} (hF : Differentiable ℝ F) (he : ∀ (k : Fin 2 → ℤ) (x : Homogenization.Vec 2), F (x + latticeShift k) = F x + latticeShift k) (i j : Fin 2) : IsZ2Periodic fun (x : Homogenization.Vec 2) => gradMatrix F x i j

Entries of ∇F are periodic for a differentiable lattice-equivariant F.

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

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

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

theorem AVenhance.Infra.Section5.Contracts.sds_Y_entry_periodic {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (l : ℤ) (t : ℝ) (i a : Fin 2) : IsZ2Periodic fun (x : Homogenization.Vec 2) => (1 - (I.flowGrad hΦ m l t x).transpose) i a

theorem AVenhance.Infra.Section5.Contracts.sds_slow2 {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κm : ℝ) (T : ℝ → Homogenization.Vec 2 → ℝ) {t : ℝ} (hTt : ContDiff ℝ (↑⊤) (T t)) (hTp : IsZ2Periodic (T t)) (k : ℤ) (a j : Fin 2) : ContDiff ℝ (↑⊤) (section5SlowChoice2 I hΦ m κm T k t a j) ∧ IsZ2Periodic (section5SlowChoice2 I hΦ m κm T k t a j)

theorem AVenhance.Infra.Section5.Contracts.sds_slow3 {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (T : ℝ → Homogenization.Vec 2 → ℝ) {t : ℝ} (hTt : ContDiff ℝ (↑⊤) (T t)) (hTp : IsZ2Periodic (T t)) (k : ℤ) (a j : Fin 2) : ContDiff ℝ (↑⊤) (section5SlowChoice3 I hΦ m T k t a j) ∧ IsZ2Periodic (section5SlowChoice3 I hΦ m T k t a j)