Defect matrices, fluxes and nondivergence parts of twistie4, twistie5

In the corrected form, the slots are the divergences twistie4 = -div(twistie4Flux) and twistie5 = -div(twistie5Flux) (twistie4_eq_neg_div_flux, twistie5_eq_neg_div_flux); the earlier bodies are twistie4ND, twistie5ND.

twistie4ND = -Σ_k ξ_k G_k · Div D_k with the Lagrangian defect matrix D_k = κ_m (∇X⁻¹ - I)(∇Χ_{m,k} ∘ X⁻¹), and twistie5 = -Σ_k ξ_k G_k · Div E_k with E_k = (I - (∇X∘X⁻¹)ᵀ)(ζ̂ζ ψ_{m,k}∘X⁻¹ σ + κ_m ∇Χ_{m,k}∘X⁻¹). Integrating the divergence by parts (source e.monster.twistie4.split, e.monster.twistie5.split) gives twistie = (nondivergence part) - div (flux), with flux = Σ_k ξ_k D_k G_k and nondivergence part = Σ_k ξ_k D_k : ∇G_k.

noncomputable def AVenhance.Infra.Section5.Contracts.sdDefect4 {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κm : ℝ) (k : ℤ) (t : ℝ) (y : Homogenization.Vec 2) : Matrix (Fin 2) (Fin 2) ℝ

The Lagrangian defect matrix D_k of twistie4.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def AVenhance.Infra.Section5.Contracts.sdDefect5 {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κm : ℝ) (k : ℤ) (t : ℝ) (y : Homogenization.Vec 2) : Matrix (Fin 2) (Fin 2) ℝ

The push-forward defect matrix E_k of twistie5.

Equations

• One or more equations did not get rendered due to their size.

theorem AVenhance.Infra.Section5.Contracts.twistie4ND_eq_defect {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κm : ℝ) (T : ℝ → Homogenization.Vec 2 → ℝ) (t : ℝ) (x : Homogenization.Vec 2) : twistie4ND I hΦ m κm T t x = -∑' (k : { k : ℤ // Odd k }), I.xiMK m (↑k) t * Homogenization.vecDot (G I hΦ m T (lIdx β I.Λ m ↑k) t x) (matDiv (sdDefect4 I hΦ m κm (↑k) t) x)

theorem AVenhance.Infra.Section5.Contracts.twistie5ND_eq_defect {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κm : ℝ) (T : ℝ → Homogenization.Vec 2 → ℝ) (t : ℝ) (x : Homogenization.Vec 2) : twistie5ND I hΦ m κm T t x = -∑' (k : { k : ℤ // Odd k }), I.xiMK m (↑k) t * Homogenization.vecDot (G I hΦ m T (lIdx β I.Λ m ↑k) t x) (matDiv (sdDefect5 I hΦ m κm (↑k) t) x)

noncomputable def AVenhance.Infra.Section5.Contracts.twistie4Flux {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κm : ℝ) (T : ℝ → Homogenization.Vec 2 → ℝ) (t : ℝ) (x : Homogenization.Vec 2) : Homogenization.Vec 2

The vector flux Σ_k ξ_k D_k G_k under the divergence in the split of twistie4.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def AVenhance.Infra.Section5.Contracts.twistie5Flux {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κm : ℝ) (T : ℝ → Homogenization.Vec 2 → ℝ) (t : ℝ) (x : Homogenization.Vec 2) : Homogenization.Vec 2

The vector flux Σ_k ξ_k E_k G_k under the divergence in the split of twistie5.

Equations

• One or more equations did not get rendered due to their size.

theorem AVenhance.Infra.Section5.Contracts.twistie4_eq_neg_div_flux {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κm : ℝ) (T : ℝ → Homogenization.Vec 2 → ℝ) (t : ℝ) (x : Homogenization.Vec 2) : twistie4 I hΦ m κm T t x = -vecDiv (twistie4Flux I hΦ m κm T t) x

In the corrected form, twistie4 is the divergence of its flux.

theorem AVenhance.Infra.Section5.Contracts.twistie5_eq_neg_div_flux {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κm : ℝ) (T : ℝ → Homogenization.Vec 2 → ℝ) (t : ℝ) (x : Homogenization.Vec 2) : twistie5 I hΦ m κm T t x = -vecDiv (twistie5Flux I hΦ m κm T t) x

In the corrected form, twistie5 is the divergence of its flux.

noncomputable def AVenhance.Infra.Section5.Contracts.twistie4Nd {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κm : ℝ) (T : ℝ → Homogenization.Vec 2 → ℝ) (t : ℝ) (x : Homogenization.Vec 2) : ℝ

The nondivergence part Σ_k ξ_k D_k : ∇G_k of twistie4ND.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def AVenhance.Infra.Section5.Contracts.twistie5Nd {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κm : ℝ) (T : ℝ → Homogenization.Vec 2 → ℝ) (t : ℝ) (x : Homogenization.Vec 2) : ℝ

The nondivergence part Σ_k ξ_k E_k : ∇G_k of twistie5ND.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def AVenhance.Infra.Section5.Contracts.sdFast4 {β : ℝ} (I : Ingredients β) (κm : ℝ) (m : ℕ) (k : ℤ) (t : ℝ) (a j : Fin 2) (y : Homogenization.Vec 2) : ℝ

Fast factor ∂_aΧ_{m,k,j} (a 1/ε_m-periodic function) of the nondivergence part of twistie4.

Equations

• AVenhance.Infra.Section5.Contracts.sdFast4 I κm m k t a j y = AVenhance.gradMatrix (fun (z : Homogenization.Vec 2) => I.chiMK κm m k t z) y a j

noncomputable def AVenhance.Infra.Section5.Contracts.sdFast5 {β : ℝ} (I : Ingredients β) (κm : ℝ) (m : ℕ) (k : ℤ) (t : ℝ) (a j : Fin 2) (y : Homogenization.Vec 2) : ℝ

Fast factor ζ̂ζ ψ_{m,k} σ_{aj} + κ_m ∂_aΧ_{m,k,j} of the nondivergence part of twistie5.

Equations

• One or more equations did not get rendered due to their size.