The divergence remainder as a weighted gradient contraction.

theorem AVenhance.Infra.Section5.ResidualR46.frob_add_right (A B C : Matrix (Fin 2) (Fin 2) ℝ) : frob A (B + C) = frob A B + frob A C

theorem AVenhance.Infra.Section5.ResidualR46.frob_smul_right (A B : Matrix (Fin 2) (Fin 2) ℝ) (c : ℝ) : frob A (c • B) = c * frob A B

theorem AVenhance.Infra.Section5.ResidualR46.frob_finite_weighted_sum {ι : Type u_1} (S : Finset ι) (A : Matrix (Fin 2) (Fin 2) ℝ) (c : ι → ℝ) (B : ι → Matrix (Fin 2) (Fin 2) ℝ) : frob A (∑ k ∈ S, c k • B k) = ∑ k ∈ S, c k * frob A (B k)