OAI/Probability/GaussianPropeller/Geometry.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.GaussianPropeller.Geometry.pair_factor_le_eight line 41
  2. lemma OAI.GaussianPropeller.Geometry.triple_factor_le_ten line 55
  3. lemma OAI.GaussianPropeller.Geometry.row_two_le line 81
  4. lemma OAI.GaussianPropeller.Geometry.row_determinants_lower line 102
  5. lemma OAI.GaussianPropeller.Geometry.three_correlations_lower line 110
  6. def OAI.GaussianPropeller.Geometry.unitVector line 136
  7. lemma OAI.GaussianPropeller.Geometry.unitVector_norm line 138
  8. lemma OAI.GaussianPropeller.Geometry.unitVector_inner_cancel line 141
  9. lemma OAI.GaussianPropeller.Geometry.unitVector_inner_nonpos line 150
  10. lemma OAI.GaussianPropeller.Geometry.unitVector_inner_bounds line 156
  11. lemma OAI.GaussianPropeller.Geometry.unitVector_variance line 163
  12. lemma OAI.GaussianPropeller.Geometry.gram_det_unitVector line 171
  13. lemma OAI.GaussianPropeller.Geometry.three_gram_determinants_lower line 178
  14. lemma OAI.GaussianPropeller.Geometry.gram_det_nonneg line 188
  15. lemma OAI.GaussianPropeller.Geometry.first_constraint_of_pair_bounds line 193
  16. lemma OAI.GaussianPropeller.Geometry.second_constraint_of_pair_bounds line 213