§4.6, p. 63 — isometry invariance: a deformation of the mesh preserving ℓ does not change the cotangent Laplacian
ProvedGeomDL.Cotangent.isometry_invariancecotangent-laplaciangeometric-deep-learningisometry-invariancep2o-batch-pfp2ap2o-gran-per-chapterp2o-plan-bookp2o-v1
Let be the faces of a manifold triangular mesh on the nodes , and let and be two embeddings of the nodes in a Euclidean space that induce the same metric on the mesh: for every face ,
Then the cotangent Laplacians of (24) with the weights (25), computed from and from , are equal.
Hence everything computed from the Laplacian, such as its eigenvalues and eigenvectors, is unchanged by a deformation that does not stretch or squeeze the edges.
Formalization Note No non-degeneracy hypothesis is needed: the angles and areas of every face are determined by its three side lengths, including the junk values Lean assigns to degenerate triangles.
Preamble
import Mathlib import Definitions.Def_GeomDL_Cotangent_Defs open EuclideanGeometry
Formal statement
namespace GeomDL.Cotangent
variable {V P : Type*} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P]
[NormedAddTorsor V P]
/-- §4.6, p. 63, isometry invariance: two embeddings `x, x'` of the same mesh that give every
edge of every face the same length `ℓ` have the same cotangent Laplacian (24)–(25),
under the section's manifold-mesh assumption. -/
theorem isometry_invariance {n : ℕ} (M : TriMesh n) (x x' : Fin n → P)
(hmesh : IsManifoldMesh M) (hℓ : ∀ t ∈ M.faces,
edgeLength x t.1 t.2.1 = edgeLength x' t.1 t.2.1 ∧
edgeLength x t.2.1 t.2.2 = edgeLength x' t.2.1 t.2.2 ∧
edgeLength x t.1 t.2.2 = edgeLength x' t.1 t.2.2) :
cotLaplacian M x = cotLaplacian M x' := by sorry
end GeomDL.Cotangent
Source
Bronstein et al., Geometric Deep Learning (arXiv:2104.13478v2), §4.6, p. 63, "any deformation of the mesh that does not affect the metric ℓ … does not change the Laplacian"
Human review
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.