English
For the incidence matrix, the diagonal entry (e,e) of the product incMatrix^T incMatrix is 2 if e is an edge, otherwise 0.
Русский
Для матрицы инцидентности диагональная запись (e,e) произведения incMatrix^T incMatrix равна 2, если e является ребром, иначе 0.
LaTeX
$$$\forall {e} \in Sym2 \alpha,\; (G.incMatrix R)^T * (G.incMatrix R) e e = \begin{cases} 2 & e \in G.edgeSet \\ 0 & e \notin G.edgeSet\end{cases}$$$
Lean4
theorem incMatrix_transpose_mul_diag [Fintype α] [Decidable (e ∈ G.edgeSet)] :
((G.incMatrix R)ᵀ * G.incMatrix R) e e = if e ∈ G.edgeSet then 2 else 0 :=
by
simp only [Matrix.mul_apply, incMatrix_apply', transpose_apply, ite_zero_mul_ite_zero, one_mul, sum_boole,
and_self_iff]
split_ifs with h
· revert h
refine e.ind ?_
intro v w h
rw [← Nat.cast_two, ← card_pair (G.ne_of_adj h)]
simp only [mk'_mem_incidenceSet_iff, G.mem_edgeSet.mp h, true_and]
congr 2
ext u
simp
· revert h
refine e.ind ?_
intro v w h
simp [mk'_mem_incidenceSet_iff, G.mem_edgeSet.not.mp h]
