Smoothness and periodicity of Σ_k ξ_k D_k G_k at a fixed time

The generic flux form with k-dependent matrices, a finite set of nonvanishing weights.

theorem AVenhance.Infra.Section5.Contracts.sd_tsum_flux_eq_sum (c : { k : ℤ // Odd k } → ℝ) (hfin : {k : { k : ℤ // Odd k } | c k ≠ 0}.Finite) (F : { k : ℤ // Odd k } → Homogenization.Vec 2 → Homogenization.Vec 2) (x : Homogenization.Vec 2) : ∑' (k : { k : ℤ // Odd k }), c k • F k x = ∑ k ∈ hfin.toFinset, c k • F k x

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

theorem AVenhance.Infra.Section5.Contracts.sd_flux_periodic (c : { k : ℤ // Odd k } → ℝ) (D : { k : ℤ // Odd k } → Homogenization.Vec 2 → Matrix (Fin 2) (Fin 2) ℝ) (W : { k : ℤ // Odd k } → Homogenization.Vec 2 → Homogenization.Vec 2) (hD : ∀ (k : { k : ℤ // Odd k }), IsZ2Periodic (D k)) (hW : ∀ (k : { k : ℤ // Odd k }), IsZ2Periodic (W k)) : IsZ2Periodic fun (x : Homogenization.Vec 2) => ∑' (k : { k : ℤ // Odd k }), c k • (D k x).mulVec (W k x)

theorem AVenhance.Infra.Section5.Contracts.sd_tsum_eq_sum_of_support (c : { k : ℤ // Odd k } → ℝ) (hfin : {k : { k : ℤ // Odd k } | c k ≠ 0}.Finite) (f : { k : ℤ // Odd k } → ℝ) (hf : ∀ (k : { k : ℤ // Odd k }), c k = 0 → f k = 0) : ∑' (k : { k : ℤ // Odd k }), f k = ∑ k ∈ hfin.toFinset, f k

theorem AVenhance.Infra.Section5.Contracts.sd_split_odd (c : { k : ℤ // Odd k } → ℝ) (hfin : {k : { k : ℤ // Odd k } | c k ≠ 0}.Finite) (D : { k : ℤ // Odd k } → Homogenization.Vec 2 → Matrix (Fin 2) (Fin 2) ℝ) (g : { k : ℤ // Odd k } → Homogenization.Vec 2 → Homogenization.Vec 2) (hD : ∀ (k : { k : ℤ // Odd k }) (i j : Fin 2), ContDiff ℝ ↑⊤ fun (x : Homogenization.Vec 2) => D k x i j) (hg : ∀ (k : { k : ℤ // Odd k }) (j : Fin 2), ContDiff ℝ ↑⊤ fun (x : Homogenization.Vec 2) => g k x j) (x : Homogenization.Vec 2) : -∑' (k : { k : ℤ // Odd k }), c k * Homogenization.vecDot (g k x) (matDiv (D k) x) = ∑' (k : { k : ℤ // Odd k }), c k * frob (D k x) (Matrix.of fun (i j : Fin 2) => spaceGrad (fun (y : Homogenization.Vec 2) => g k y j) x i) - vecDiv (fun (y : Homogenization.Vec 2) => ∑' (k : { k : ℤ // Odd k }), c k • (D k y).mulVec (g k y)) x

The split -Σ_k c_k g_k · Div D_k = Σ_k c_k D_k : ∇g_k - div (Σ_k c_k D_k g_k) for a finite set of nonvanishing weights and smooth data.

theorem AVenhance.Infra.Section5.Contracts.sd_nd_continuous (c : { k : ℤ // Odd k } → ℝ) (hfin : {k : { k : ℤ // Odd k } | c k ≠ 0}.Finite) (D A : { k : ℤ // Odd k } → Homogenization.Vec 2 → Matrix (Fin 2) (Fin 2) ℝ) (hD : ∀ (k : { k : ℤ // Odd k }) (i j : Fin 2), Continuous fun (x : Homogenization.Vec 2) => D k x i j) (hA : ∀ (k : { k : ℤ // Odd k }) (i j : Fin 2), Continuous fun (x : Homogenization.Vec 2) => A k x i j) : Continuous fun (x : Homogenization.Vec 2) => ∑' (k : { k : ℤ // Odd k }), c k * frob (D k x) (A k x)