OAI/Geometry/NodalSets/Spectral/FiniteVariationalEigenframe.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Yau.Analysis.real_orthogonal_span_range line 10
2. theorem OAI.Yau.Analysis.real_orthonormal_snoc line 21
3. theorem OAI.Yau.Analysis.compact_positive_finite_variational_eigenframe line 35