Differentiability-based linearity of the classical divergence.

theorem AVenhance.Infra.Section5.DivergenceLinearity.vecDiv_eq_fderivAt {V : Homogenization.Vec 2 → Homogenization.Vec 2} {x : Homogenization.Vec 2} {L : Homogenization.Vec 2 →L[ℝ] Homogenization.Vec 2} (hV : HasFDerivAt V L x) : vecDiv V x = ∑ i : Fin 2, L (Homogenization.basisVec i) i

theorem AVenhance.Infra.Section5.vecDiv_add_of_hasFDerivAt {V W : Homogenization.Vec 2 → Homogenization.Vec 2} {x : Homogenization.Vec 2} {LV LW : Homogenization.Vec 2 →L[ℝ] Homogenization.Vec 2} (hV : HasFDerivAt V LV x) (hW : HasFDerivAt W LW x) : vecDiv (fun (y : Homogenization.Vec 2) => V y + W y) x = vecDiv V x + vecDiv W x

Divergence is additive under explicit local derivative hypotheses.

theorem AVenhance.Infra.Section5.vecDiv_finite_weighted_sum {ι : Type u_1} (S : Finset ι) (c : ι → ℝ) (F : ι → Homogenization.Vec 2 → Homogenization.Vec 2) (x : Homogenization.Vec 2) {LF : ι → Homogenization.Vec 2 →L[ℝ] Homogenization.Vec 2} (hF : ∀ i ∈ S, HasFDerivAt (F i) (LF i) x) : vecDiv (fun (y : Homogenization.Vec 2) => ∑ i ∈ S, c i • F i y) x = ∑ i ∈ S, c i * vecDiv (F i) x

A finite weighted sum may be passed through the divergence when each summand has the displayed derivative at the point.