OAI/MeasureTheory/Falconer/Geometry/EuclideanCross.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Three-dimensional dual directions and the Gram determinant

  1. def OAI.Falconer.euclideanCross line 11
  2. theorem OAI.Falconer.euclidean_inner_dot line 14
  3. theorem OAI.Falconer.inner_self_euclideanCross line 21
  4. theorem OAI.Falconer.inner_euclideanCross_self line 25
  5. theorem OAI.Falconer.euclideanCross_cyclic line 29
  6. theorem OAI.Falconer.euclideanCross_norm_sq line 34
  7. theorem OAI.Falconer.euclideanCross_norm_le_one line 46
  8. theorem OAI.Falconer.gram_eq_rowMatrix_mul_transpose line 56
  9. theorem OAI.Falconer.euclideanCross_triple_sq line 63