Divergence/nondivergence split of twistie4ND, twistie5ND

The proofs use the helper modules TermCenteredSplitCalculus (product rule), TermCenteredSplitFields (smoothness/periodicity of the defect matrices), TermCenteredSplitFlux (generic finite-support flux calculus) and TermCenteredSplitAlgebra (component forms).

theorem AVenhance.Infra.Section5.Contracts.twistie4ND_split {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) {m : ℕ} (hm : 1 ≤ m) (κm : ℝ) (T : ℝ → Homogenization.Vec 2 → ℝ) {t : ℝ} (hTt : ContDiff ℝ (↑⊤) (T t)) (x : Homogenization.Vec 2) : twistie4ND I hΦ m κm T t x = twistie4Nd I hΦ m κm T t x - vecDiv (twistie4Flux I hΦ m κm T t) x

e.monster.twistie4.split for the earlier body: twistie4ND = (nondivergence part) - div (flux). (In the corrected form, twistie4 itself is -div (flux): twistie4_eq_neg_div_flux.)

theorem AVenhance.Infra.Section5.Contracts.twistie5ND_split {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) {m : ℕ} (hm : 1 ≤ m) (κm : ℝ) (T : ℝ → Homogenization.Vec 2 → ℝ) {t : ℝ} (hTt : ContDiff ℝ (↑⊤) (T t)) (x : Homogenization.Vec 2) : twistie5ND I hΦ m κm T t x = twistie5Nd I hΦ m κm T t x - vecDiv (twistie5Flux I hΦ m κm T t) x

e.monster.twistie5.split for the earlier body twistie5ND.

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

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

theorem AVenhance.Infra.Section5.Contracts.twistie4Nd_continuous {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) {m : ℕ} (hm : 1 ≤ m) (κm : ℝ) (T : ℝ → Homogenization.Vec 2 → ℝ) {t : ℝ} (hTt : ContDiff ℝ (↑⊤) (T t)) : Continuous (twistie4Nd I hΦ m κm T t)

The nondivergence parts are continuous in x (finite sums of continuous terms).

theorem AVenhance.Infra.Section5.Contracts.twistie5Nd_continuous {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) {m : ℕ} (hm : 1 ≤ m) (κm : ℝ) (T : ℝ → Homogenization.Vec 2 → ℝ) {t : ℝ} (hTt : ContDiff ℝ (↑⊤) (T t)) : Continuous (twistie5Nd I hΦ m κm T t)

theorem AVenhance.Infra.Section5.Contracts.twistie4Nd_eq_sum {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) {m : ℕ} (hm : 1 ≤ m) (κm : ℝ) (T : ℝ → Homogenization.Vec 2 → ℝ) (t : ℝ) (S : Finset { k : ℤ // Odd k }) (hS : ∀ (k : { k : ℤ // Odd k }), I.xiMK m (↑k) t ≠ 0 → k ∈ S) (x : Homogenization.Vec 2) : twistie4Nd I hΦ m κm T t x = ∑ k ∈ S, ∑ a : Fin 2, ∑ j : Fin 2, sdFast4 I κm m (↑k) t a j (I.xFlowInv hΦ m (lIdx β I.Λ m ↑k) t x) * section5SlowChoice2 I hΦ m κm T (↑k) t a j x

Component form of the nondivergence part of twistie4: Σ_k ξ_k D_k : ∇G_k = Σ_k Σ_{a,j} (∂_aΧ_{k,j} ∘ X_k⁻¹) · f_{k,aj} (choice 2).

theorem AVenhance.Infra.Section5.Contracts.twistie5Nd_eq_sum {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) {m : ℕ} (hm : 1 ≤ m) (κm : ℝ) (T : ℝ → Homogenization.Vec 2 → ℝ) (t : ℝ) (S : Finset { k : ℤ // Odd k }) (hS : ∀ (k : { k : ℤ // Odd k }), I.xiMK m (↑k) t ≠ 0 → k ∈ S) (x : Homogenization.Vec 2) : twistie5Nd I hΦ m κm T t x = ∑ k ∈ S, ∑ a : Fin 2, ∑ j : Fin 2, sdFast5 I κm m (↑k) t a j (I.xFlowInv hΦ m (lIdx β I.Λ m ↑k) t x) * section5SlowChoice3 I hΦ m T (↑k) t a j x

Component form of the nondivergence part of twistie5 (choice 3).