OAI/Probability/GaussianPropeller/Coordinates.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.GaussianPropeller.Coords.CS line 39
  2. def OAI.GaussianPropeller.Coords.split line 41
  3. def OAI.GaussianPropeller.Coords.join line 43
  4. lemma OAI.GaussianPropeller.Coords.split_join line 46
  5. lemma OAI.GaussianPropeller.Coords.join_split line 50
  6. lemma OAI.GaussianPropeller.Coords.continuous_split line 54
  7. lemma OAI.GaussianPropeller.Coords.continuous_join line 59
  8. def OAI.GaussianPropeller.Coords.splitEquiv line 68
  9. lemma OAI.GaussianPropeller.Coords.split_measure line 76
  10. lemma OAI.GaussianPropeller.Coords.measurePreserving_split line 90
  11. lemma OAI.GaussianPropeller.Coords.integral_split line 94
  12. lemma OAI.GaussianPropeller.Coords.norm_join_sq line 99
  13. lemma OAI.GaussianPropeller.Coords.norm_join line 103
  14. lemma OAI.GaussianPropeller.Coords.join_zero line 106
  15. lemma OAI.GaussianPropeller.Coords.exists_basis_zero line 108