OAI/Probability/PosteriorReplicas/Regression/SphereGeometry.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PosteriorRegression.ambientSphereLaw line 17
  2. instance OAI.PosteriorRegression.ambientSphereLaw_probability line 19
  3. lemma OAI.PosteriorRegression.ambientSphereLaw_support line 23
  4. lemma OAI.PosteriorRegression.ambientSphereLaw_closedBall line 32
  5. lemma OAI.PosteriorRegression.terminal_cap_mass line 53
  6. lemma OAI.PosteriorRegression.chord_le_arccos line 76
  7. lemma OAI.PosteriorRegression.unitBallLaw_isometry_apply line 89
  8. lemma OAI.PosteriorRegression.ambientSphereLaw_apply line 105
  9. lemma OAI.PosteriorRegression.ambientSphereLaw_isometry line 118
  10. lemma OAI.PosteriorRegression.ambientSphereLaw_ae_norm line 138
  11. lemma OAI.PosteriorRegression.sphere_inner_sq_integrable line 143
  12. lemma OAI.PosteriorRegression.sphere_inner_sq_eq line 152
  13. lemma OAI.PosteriorRegression.sphere_inner_sq_unit line 162
  14. lemma OAI.PosteriorRegression.sphere_projection_sq_integrable line 187
  15. lemma OAI.PosteriorRegression.sphere_projection_sq_integral line 200
  16. def OAI.PosteriorRegression.sphereIsometry line 218
  17. lemma OAI.PosteriorRegression.sphereIsometry_preserving line 224
  18. lemma OAI.PosteriorRegression.reflection_dist line 234
  19. lemma OAI.PosteriorRegression.sphere_projection_large line 244
  20. lemma OAI.PosteriorRegression.sphere_reflection_success_bound line 275