pith. machine review for the scientific record. sign in
theorem proved tactic proof

laplacianCoefficient_row_sum

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 593theorem laplacianCoefficient_row_sum {n : ℕ} (A : Fin n → Fin n → ℝ) :
 594    ∀ i : Fin n, ∑ j : Fin n, laplacianCoefficient A i j = 0 := by

proof body

Tactic-mode proof.

 595  intro i
 596  unfold laplacianCoefficient
 597  rw [Finset.sum_sub_distrib]
 598  have hdiag :
 599      (∑ j : Fin n, (if i = j then ∑ k : Fin n, A i k else 0))
 600        = ∑ k : Fin n, A i k := by
 601    rw [Finset.sum_eq_single i]
 602    · simp
 603    · intro b _ hb
 604      have hne : i ≠ b := fun h => hb h.symm
 605      simp [hne]
 606    · intro hi
 607      exact (hi (Finset.mem_univ i)).elim
 608  rw [hdiag]
 609  ring
 610
 611/-- The weak-field Regge data whose bilinear coefficient is the graph
 612    Laplacian associated with `A`. We put the whole coefficient into
 613    `dDeficit`; `dArea = 1` is a harmless normalization because only the
 614    product `dArea · dDeficit` enters the second variation. -/

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (8)

Lean names referenced from this declaration's body.