OAI/Geometry/NodalSets/Elliptic/CoordinateMatrixEllipticity.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Yau.Geometry.coordMatrixForm line 12
2. lemma OAI.Yau.Geometry.coordMatrixForm_apply line 15
3. lemma OAI.Yau.Geometry.coordMatrixForm_positive line 19
4. lemma OAI.Yau.Geometry.coordMatrixForm_continuous line 24
5. lemma OAI.Yau.Geometry.coord_norm_sq_le_sum_sq line 32
6. lemma OAI.Yau.Geometry.coord_sum_sq_le_four_norm_sq line 38
7. theorem OAI.Yau.Geometry.compact_matrix_uniform_ellipticity line 44