OAI/Probability/Subsphere/Mixture/Latitude.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SubsphereCurrent.Mixture.nested_projection_beta line 17
  2. lemma OAI.SubsphereCurrent.Mixture.nested_perp_beta line 42
  3. lemma OAI.SubsphereCurrent.Mixture.measurable_directionSampler line 71
  4. instance OAI.SubsphereCurrent.Mixture.directionLaw_probability line 77
  5. lemma OAI.SubsphereCurrent.Mixture.directionLaw_unit line 82
  6. lemma OAI.SubsphereCurrent.Mixture.directionLaw_invariant line 91
  7. lemma OAI.SubsphereCurrent.Mixture.directionLaw_beta line 106
  8. lemma OAI.SubsphereCurrent.Mixture.latitude_norm line 126
  9. lemma OAI.SubsphereCurrent.Mixture.latitude_coordinate line 139
  10. lemma OAI.SubsphereCurrent.Mixture.latitude_rank_one line 150
  11. lemma OAI.SubsphereCurrent.Mixture.latitude_coordinate_rank_one line 160
  12. lemma OAI.SubsphereCurrent.Mixture.measurable_latitudeSampler line 169
  13. lemma OAI.SubsphereCurrent.Mixture.latitudeLaw_probability line 178
  14. lemma OAI.SubsphereCurrent.Mixture.latitudeLaw_unit line 185
  15. lemma OAI.SubsphereCurrent.Mixture.latitudeLaw_invariant line 201
  16. lemma OAI.SubsphereCurrent.Mixture.beta_product_preserving line 227
  17. lemma OAI.SubsphereCurrent.Mixture.latitudeLaw_beta_gt_one line 268
  18. lemma OAI.SubsphereCurrent.Mixture.latitudeLaw_beta_one line 315