OAI/Probability/Subsphere/Regression/Spheres.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SubsphereRegression.unitBallLaw line 21
  2. lemma OAI.SubsphereRegression.unitBallLaw_closedBall line 24
  3. lemma OAI.SubsphereRegression.unitBallLaw_local line 36
  4. lemma OAI.SubsphereRegression.unitBallLaw_support line 41
  5. instance OAI.SubsphereRegression.unitBallLaw_probability line 47
  6. instance OAI.SubsphereRegression.sphereLaw_probability line 55
  7. lemma OAI.SubsphereRegression.sphereLaw_apply line 63
  8. lemma OAI.SubsphereRegression.sphereLaw_cap_raw line 85
  9. instance OAI.SubsphereRegression.ambientSphereLaw_probability line 124
  10. lemma OAI.SubsphereRegression.ambientSphereLaw_support line 128
  11. lemma OAI.SubsphereRegression.ambientSphereLaw_closedBall line 137
  12. lemma OAI.SubsphereRegression.terminal_cap_mass line 158
  13. lemma OAI.SubsphereRegression.chord_le_arccos line 181
  14. lemma OAI.SubsphereRegression.unitBallLaw_isometry_apply line 194
  15. lemma OAI.SubsphereRegression.ambientSphereLaw_apply line 210
  16. lemma OAI.SubsphereRegression.ambientSphereLaw_isometry line 223
  17. lemma OAI.SubsphereRegression.ambientSphereLaw_ae_norm line 243
  18. lemma OAI.SubsphereRegression.sphere_inner_sq_integrable line 248
  19. lemma OAI.SubsphereRegression.sphere_inner_sq_eq line 257
  20. lemma OAI.SubsphereRegression.sphere_inner_sq_unit line 267
  21. lemma OAI.SubsphereRegression.sphere_projection_sq_integrable line 292
  22. lemma OAI.SubsphereRegression.sphere_projection_sq_integral line 305
  23. def OAI.SubsphereRegression.sphereIsometry line 323
  24. lemma OAI.SubsphereRegression.sphereIsometry_preserving line 329
  25. lemma OAI.SubsphereRegression.reflection_dist line 339
  26. lemma OAI.SubsphereRegression.sphere_projection_large line 349
  27. lemma OAI.SubsphereRegression.sphere_reflection_success_bound line 380
  28. lemma OAI.SubsphereRegression.ae_fiber_aemeasurable line 424
  29. lemma OAI.SubsphereRegression.prod_null_set_bound line 432
  30. instance OAI.SubsphereRegression.sampleLaw_probability line 450
  31. instance OAI.SubsphereRegression.uniformSphere_probability line 453