Fixed-time smoothness and periodicity of the flux ingredients

At a fixed time the ξ-sums are finite, ψTilde_m and the diffusion matrix are smooth and ℤ²-periodic (actual flow and inverse flow are lattice equivariant), and G_l, ∇G_l, uShear ∘ X⁻¹ are smooth and periodic when the temperature slice is.

The generic flux form at a fixed time

theorem AVenhance.Infra.Section5.Contracts.tfFlux_slice_contDiff (c : { k : ℤ // Odd k } → ℝ → ℝ) (D : ℝ → Homogenization.Vec 2 → Matrix (Fin 2) (Fin 2) ℝ) (W : { k : ℤ // Odd k } → ℝ → Homogenization.Vec 2 → Homogenization.Vec 2) (t : ℝ) (hfin : {k : { k : ℤ // Odd k } | c k t ≠ 0}.Finite) (hD : ∀ (i j : Fin 2), ContDiff ℝ ↑⊤ fun (x : Homogenization.Vec 2) => D t x i j) (hW : ∀ (k : { k : ℤ // Odd k }) (j : Fin 2), ContDiff ℝ ↑⊤ fun (x : Homogenization.Vec 2) => W k t x j) : ContDiff ℝ (↑⊤) (tfFlux c D W t)

theorem AVenhance.Infra.Section5.Contracts.tfFlux_periodic (c : { k : ℤ // Odd k } → ℝ → ℝ) (D : ℝ → Homogenization.Vec 2 → Matrix (Fin 2) (Fin 2) ℝ) (W : { k : ℤ // Odd k } → ℝ → Homogenization.Vec 2 → Homogenization.Vec 2) (t : ℝ) (hD : IsZ2Periodic (D t)) (hW : ∀ (k : { k : ℤ // Odd k }), IsZ2Periodic (W k t)) : IsZ2Periodic (tfFlux c D W t)

The diffusion matrix at a fixed time

theorem AVenhance.Infra.Section5.Contracts.tf_sin_shift (a : ℝ) (z : ℤ) : Real.sin (2 * Real.pi * (a + ↑z)) = Real.sin (2 * Real.pi * a)

theorem AVenhance.Infra.Section5.Contracts.tf_psi_periodic {β : ℝ} (I : Ingredients β) (m : ℕ) (k : ℤ) : IsZ2Periodic (psi β I.Λ m k)

theorem AVenhance.Infra.Section5.Contracts.tf_psiTilde_periodic {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (t : ℝ) : IsZ2Periodic (psiTilde I hΦ m t)

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

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

G_l, ∇G_l, the pulled-back shear

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

theorem AVenhance.Infra.Section5.Contracts.tf_G_slice_periodic {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (T : ℝ → Homogenization.Vec 2 → ℝ) (t : ℝ) (l : ℤ) (hT : IsZ2Periodic (T t)) : IsZ2Periodic (G I hΦ m T l t)

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

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

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

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

The three fluxes at a fixed time

theorem AVenhance.Infra.Section5.Contracts.tf_twistie3Flux_slice {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) {m : ℕ} (hm : 1 ≤ m) (κm : ℝ) (T : ℝ → Homogenization.Vec 2 → ℝ) (t : ℝ) (hs : ContDiff ℝ (↑⊤) (T t)) (hp : IsZ2Periodic (T t)) : ContDiff ℝ (↑⊤) (twistie3Flux I hΦ m κm T t) ∧ IsZ2Periodic (twistie3Flux I hΦ m κm T t)

theorem AVenhance.Infra.Section5.Contracts.tf_normie1Flux_slice {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) {m : ℕ} (hm : 1 ≤ m) (κm : ℝ) (T : ℝ → Homogenization.Vec 2 → ℝ) (t : ℝ) (hs : ContDiff ℝ (↑⊤) (T t)) (hp : IsZ2Periodic (T t)) : ContDiff ℝ (↑⊤) (normie1Flux I hΦ m κm T t) ∧ IsZ2Periodic (normie1Flux I hΦ m κm T t)

theorem AVenhance.Infra.Section5.Contracts.tf_normie2Flux_slice {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κm : ℝ) (T : ℝ → Homogenization.Vec 2 → ℝ) (t : ℝ) (hs : ContDiff ℝ (↑⊤) (I.Hm hΦ m κm T t)) (hp : IsZ2Periodic (I.Hm hΦ m κm T t)) : ContDiff ℝ (↑⊤) (normie2Flux I hΦ m κm T t) ∧ IsZ2Periodic (normie2Flux I hΦ m κm T t)