OAI/Probability/GaussianRegression/Sphere.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

Normalized spherical surface measure, cap bounds, and rotational symmetry.

  1. def OAI.NoiselessRegression.unitBallLaw line 24
  2. lemma OAI.NoiselessRegression.unitBallLaw_closedBall line 27
  3. lemma OAI.NoiselessRegression.unitBallLaw_local line 39
  4. lemma OAI.NoiselessRegression.unitBallLaw_support line 44
  5. instance OAI.NoiselessRegression.unitBallLaw_probability line 50
  6. instance OAI.NoiselessRegression.sphereLaw_probability line 58
  7. lemma OAI.NoiselessRegression.sphereLaw_apply line 66
  8. lemma OAI.NoiselessRegression.sphereLaw_cap_raw line 88
  9. instance OAI.NoiselessRegression.ambientSphereLaw_probability line 126
  10. lemma OAI.NoiselessRegression.ambientSphereLaw_support line 129
  11. lemma OAI.NoiselessRegression.ambientSphereLaw_closedBall line 138
  12. lemma OAI.NoiselessRegression.terminal_cap_mass line 159
  13. lemma OAI.NoiselessRegression.chord_le_arccos line 182
  14. lemma OAI.NoiselessRegression.unitBallLaw_isometry_apply line 195
  15. lemma OAI.NoiselessRegression.ambientSphereLaw_apply line 211
  16. lemma OAI.NoiselessRegression.ambientSphereLaw_isometry line 224
  17. lemma OAI.NoiselessRegression.ambientSphereLaw_ae_norm line 244
  18. lemma OAI.NoiselessRegression.sphere_inner_sq_integrable line 249
  19. lemma OAI.NoiselessRegression.sphere_inner_sq_eq line 258
  20. lemma OAI.NoiselessRegression.sphere_inner_sq_unit line 268
  21. lemma OAI.NoiselessRegression.sphere_projection_sq_integrable line 293
  22. lemma OAI.NoiselessRegression.sphere_projection_sq_integral line 306
  23. def OAI.NoiselessRegression.sphereIsometry line 324
  24. lemma OAI.NoiselessRegression.sphereIsometry_preserving line 330
  25. lemma OAI.NoiselessRegression.reflection_dist line 340
  26. lemma OAI.NoiselessRegression.sphere_projection_large line 350
  27. lemma OAI.NoiselessRegression.sphere_reflection_success_bound line 381