Commit 2024-02-28 12:44 30f06274

View on Github →

feat: Laplacian matrix of a simple graph (#8594) Contains the definition of the graph laplacian and proofs of some its properties, including that it is positive semidefinite and that the dimension of its nullspace equals the number of connected components of the graph.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Ring/Defs.lean

added theorem ite_add_ite

added theorem ite_sub_ite

Modified Mathlib/Combinatorics/SimpleGraph/AdjMatrix.lean

added theorem SimpleGraph.dotProduct_mulVec_adjMatrix

Created Mathlib/Combinatorics/SimpleGraph/LapMatrix.lean

added theorem SimpleGraph.card_ConnectedComponent_eq_rank_ker_lapMatrix

added def SimpleGraph.degMatrix

added theorem SimpleGraph.degMatrix_mulVec_apply

added theorem SimpleGraph.degree_eq_sum_if_adj

added theorem SimpleGraph.dotProduct_mulVec_degMatrix

added theorem SimpleGraph.isSymm_degMatrix

added theorem SimpleGraph.isSymm_lapMatrix

added def SimpleGraph.lapMatrix

added def SimpleGraph.lapMatrix_ker_basis_aux

added theorem SimpleGraph.lapMatrix_mulVec_apply

added theorem SimpleGraph.lapMatrix_mulVec_const_eq_zero

added theorem SimpleGraph.lapMatrix_toLin'_apply_eq_zero_iff_forall_adj

added theorem SimpleGraph.lapMatrix_toLin'_apply_eq_zero_iff_forall_reachable

added theorem SimpleGraph.lapMatrix_toLinearMap₂'

added theorem SimpleGraph.lapMatrix_toLinearMap₂'_apply'_eq_zero_iff_forall_adj

added theorem SimpleGraph.lapMatrix_toLinearMap₂'_apply'_eq_zero_iff_forall_reachable

added theorem SimpleGraph.linearIndependent_lapMatrix_ker_basis_aux

added theorem SimpleGraph.mem_ker_toLin'_lapMatrix_of_connectedComponent

added theorem SimpleGraph.posSemidef_lapMatrix

added theorem SimpleGraph.top_le_span_range_lapMatrix_ker_basis_aux