Finite decomposition of twistie1

At fixed t, twistie1(t) = ∑_{k ∈ s} ∑_j f_{k,j} · (χ_{m,k,j} ∘ X_{m-1,l_k}⁻¹) over the finite set s of odd k with ξ_{m,k}(t) ≠ 0 (at most three), f_{k,j} the slow factor of e.fg.choice.1 (section5SlowChoice1).

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

The vector field ∇ ∇·((K_m + s_{m-1}) ∇T) at time t.

Equations

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

theorem AVenhance.Infra.Section5.Contracts.seGd_apply {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κ : ℝ) (T : ℝ → Homogenization.Vec 2 → ℝ) (t : ℝ) (x : Homogenization.Vec 2) (i : Fin 2) : seGd I hΦ m κ T t x i = slowFactorGradDiv (fun (y : Homogenization.Vec 2) => I.Kmat κ m t + I.sMat hΦ m κ t y) (T t) i x

theorem AVenhance.Infra.Section5.Contracts.se_memL2On_of_continuous {f : Homogenization.Vec 2 → ℝ} (hf : Continuous f) : Homogenization.MemL2On unitCube f

theorem AVenhance.Infra.Section5.Contracts.se_xi_support {β : ℝ} (I : Ingredients β) (m : ℕ) (t : ℝ) : ∃ (s : Finset { k : ℤ // Odd k }), s.card ≤ 3 ∧ (∀ q ∈ s, I.xiMK m (↑q) t ≠ 0) ∧ ∀ q ∉ s, I.xiMK m (↑q) t = 0

ξ_{m,k}(t) ≠ 0 for k in a finite set.

theorem AVenhance.Infra.Section5.Contracts.se_twistie1_eq_sum {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κ : ℝ) (T : ℝ → Homogenization.Vec 2 → ℝ) (t : ℝ) (s : Finset { k : ℤ // Odd k }) (hs : ∀ q ∉ s, I.xiMK m (↑q) t = 0) : twistie1 I hΦ m κ T t = fun (x : Homogenization.Vec 2) => ∑ q ∈ s, ∑ j : Fin 2, section5SlowChoice1 I hΦ m κ T (↑q) t j x * I.chiTilde hΦ m κ (↑q) t x j

The finite decomposition of twistie1(t).