Product rule for matrix-vector fluxes

Pointwise calculus for the integration by parts in e.monster.twistie4.split: for differentiable D, g, div (D g) = D : ∇g + g · Div D, and the divergence of a finite weighted sum is the weighted sum of the divergences.

theorem AVenhance.Infra.Section5.Contracts.sd_spaceGrad_add {f g : Homogenization.Vec 2 → ℝ} {x : Homogenization.Vec 2} (hf : DifferentiableAt ℝ f x) (hg : DifferentiableAt ℝ g x) (i : Fin 2) : spaceGrad (fun (y : Homogenization.Vec 2) => f y + g y) x i = spaceGrad f x i + spaceGrad g x i

theorem AVenhance.Infra.Section5.Contracts.sd_spaceGrad_mul {f g : Homogenization.Vec 2 → ℝ} {x : Homogenization.Vec 2} (hf : DifferentiableAt ℝ f x) (hg : DifferentiableAt ℝ g x) (i : Fin 2) : spaceGrad (fun (y : Homogenization.Vec 2) => f y * g y) x i = f x * spaceGrad g x i + g x * spaceGrad f x i

theorem AVenhance.Infra.Section5.Contracts.sd_spaceGrad_const_mul {f : Homogenization.Vec 2 → ℝ} {x : Homogenization.Vec 2} (c : ℝ) (hf : DifferentiableAt ℝ f x) (i : Fin 2) : spaceGrad (fun (y : Homogenization.Vec 2) => c * f y) x i = c * spaceGrad f x i

theorem AVenhance.Infra.Section5.Contracts.sd_spaceGrad_sum {ι : Type u_1} (S : Finset ι) {f : ι → Homogenization.Vec 2 → ℝ} {x : Homogenization.Vec 2} (hf : ∀ k ∈ S, DifferentiableAt ℝ (f k) x) (i : Fin 2) : spaceGrad (fun (y : Homogenization.Vec 2) => ∑ k ∈ S, f k y) x i = ∑ k ∈ S, spaceGrad (f k) x i

theorem AVenhance.Infra.Section5.Contracts.sd_vecDiv_mulVec {D : Homogenization.Vec 2 → Matrix (Fin 2) (Fin 2) ℝ} {g : Homogenization.Vec 2 → Homogenization.Vec 2} {x : Homogenization.Vec 2} (hD : ∀ (i j : Fin 2), DifferentiableAt ℝ (fun (y : Homogenization.Vec 2) => D y i j) x) (hg : ∀ (j : Fin 2), DifferentiableAt ℝ (fun (y : Homogenization.Vec 2) => g y j) x) : vecDiv (fun (y : Homogenization.Vec 2) => (D y).mulVec (g y)) x = frob (D x) (Matrix.of fun (i j : Fin 2) => spaceGrad (fun (y : Homogenization.Vec 2) => g y j) x i) + Homogenization.vecDot (g x) (matDiv D x)

Product rule for div (D g).

theorem AVenhance.Infra.Section5.Contracts.sd_vecDiv_finset_sum {ι : Type u_1} (S : Finset ι) (c : ι → ℝ) {V : ι → Homogenization.Vec 2 → Homogenization.Vec 2} {x : Homogenization.Vec 2} (hV : ∀ k ∈ S, ∀ (j : Fin 2), DifferentiableAt ℝ (fun (y : Homogenization.Vec 2) => V k y j) x) : vecDiv (fun (y : Homogenization.Vec 2) => ∑ k ∈ S, c k • V k y) x = ∑ k ∈ S, c k * vecDiv (V k) x

The divergence of a finite weighted sum of fluxes.

theorem AVenhance.Infra.Section5.Contracts.sd_split_finset {ι : Type u_1} (S : Finset ι) (c : ι → ℝ) (D : ι → Homogenization.Vec 2 → Matrix (Fin 2) (Fin 2) ℝ) (g : ι → Homogenization.Vec 2 → Homogenization.Vec 2) (x : Homogenization.Vec 2) (hD : ∀ k ∈ S, ∀ (i j : Fin 2), DifferentiableAt ℝ (fun (y : Homogenization.Vec 2) => D k y i j) x) (hg : ∀ k ∈ S, ∀ (j : Fin 2), DifferentiableAt ℝ (fun (y : Homogenization.Vec 2) => g k y j) x) : -∑ k ∈ S, c k * Homogenization.vecDot (g k x) (matDiv (D k) x) = ∑ k ∈ S, 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 ∈ S, c k • (D k y).mulVec (g k y)) x

The finite-sum form of the split.