OAI/Probability/Subsphere/Geometry/Affine.lean

GitHub source file

53 declarations, 0 contain sorry, 0 declared as axioms

Exact Gaussian reconstruction for an affine-sphere test. The complementary rows are independent random parameters, not an extra sample channel to a learner.

  1. def OAI.SubsphereCurrent.Affine.AllAffineEstimate line 13
  2. abbrev OAI.SubsphereCurrent.Fixed.Stream.Tape line 46
  3. def OAI.SubsphereCurrent.Fixed.Stream.tapeLaw line 48
  4. instance OAI.SubsphereCurrent.Fixed.Stream.tapeLaw_probability line 52
  5. instance OAI.SubsphereCurrent.Fixed.Stream.estimateLaw_probability line 57
  6. def OAI.SubsphereCurrent.Fixed.Stream.stepPMF line 62
  7. def OAI.SubsphereCurrent.Fixed.Stream.stepDet line 66
  8. lemma OAI.SubsphereCurrent.Fixed.Stream.stepDet_measurable line 70
  9. lemma OAI.SubsphereCurrent.Fixed.Stream.stepDet_map line 75
  10. lemma OAI.SubsphereCurrent.Fixed.Stream.run_eq_bind_chain line 80
  11. def OAI.SubsphereCurrent.Fixed.Stream.tapeEstimate line 89
  12. lemma OAI.SubsphereCurrent.Fixed.Stream.measurable_detChain_param line 92
  13. lemma OAI.SubsphereCurrent.Fixed.Stream.measurable_tapeEstimate line 111
  14. lemma OAI.SubsphereCurrent.Fixed.Stream.lintegral_tapeEstimate line 121
  15. def OAI.SubsphereCurrent.Fixed.Stream.tapeTransition line 149
  16. lemma OAI.SubsphereCurrent.Fixed.Stream.tapeTransition_measurable line 154
  17. lemma OAI.SubsphereCurrent.Fixed.Stream.streamRoute_eq_detChain line 159
  18. lemma OAI.SubsphereCurrent.Fixed.Stream.tapeEstimate_eq_route line 174
  19. instance OAI.SubsphereCurrent.Fixed.sphereLaw_probability line 191
  20. instance OAI.SubsphereCurrent.Fixed.rowsLaw_probability line 193
  21. def OAI.SubsphereCurrent.Fixed.euclideanTest line 197
  22. lemma OAI.SubsphereCurrent.Fixed.measurable_euclideanTest line 200
  23. lemma OAI.SubsphereCurrent.Fixed.Stream.euclideanSuccess_eq_integral_tape line 212
  24. lemma OAI.SubsphereCurrent.Fixed.Stream.measurable_euclideanSuccess line 221
  25. lemma OAI.SubsphereCurrent.Fixed.Stream.average_euclideanSuccess_bound line 228
  26. lemma OAI.SubsphereCurrent.Fixed.Stream.average_euclideanSuccess_le_one line 268
  27. lemma OAI.SubsphereCurrent.stdGaussian_prod_map line 288
  28. lemma OAI.SubsphereCurrent.gaussian_orthogonal_sum line 305
  29. lemma OAI.SubsphereCurrent.gaussian_orthogonal_rows line 316
  30. lemma OAI.SubsphereCurrent.Affine.Test.measurable_point line 340
  31. lemma OAI.SubsphereCurrent.Affine.Test.norm_point line 342
  32. def OAI.SubsphereCurrent.Affine.Test.project line 354
  33. lemma OAI.SubsphereCurrent.Affine.Test.measurable_project line 357
  34. lemma OAI.SubsphereCurrent.Affine.Test.project_point line 359
  35. lemma OAI.SubsphereCurrent.Affine.Test.project_error line 363
  36. lemma OAI.SubsphereCurrent.Affine.Test.angular_project_error line 374
  37. lemma OAI.SubsphereCurrent.Affine.Test.observation_identity line 385
  38. def OAI.SubsphereCurrent.Affine.Simulation.stream line 399
  39. lemma OAI.SubsphereCurrent.Affine.Simulation.borel line 410
  40. lemma OAI.SubsphereCurrent.Affine.Simulation.run_eq line 415
  41. lemma OAI.SubsphereCurrent.Affine.Simulation.success_le line 431
  42. def OAI.SubsphereCurrent.Fixed.angularTest line 462
  43. lemma OAI.SubsphereCurrent.Fixed.measurable_angularTest line 465
  44. lemma OAI.SubsphereCurrent.Fixed.Stream.angularSuccess_eq_integral_tape line 476
  45. lemma OAI.SubsphereCurrent.Fixed.Stream.measurable_angularSuccess line 485
  46. lemma OAI.SubsphereCurrent.Fixed.Stream.average_euclideanSuccess_zero_bound line 492
  47. lemma OAI.SubsphereCurrent.Affine.Simulation.reconstruct_preserving line 545
  48. lemma OAI.SubsphereCurrent.Affine.Simulation.integral_reconstruct line 562
  49. lemma OAI.SubsphereCurrent.Affine.Simulation.measurable_angular_onTest line 574
  50. lemma OAI.SubsphereCurrent.Affine.Simulation.average_le_of_simulated line 585
  51. def OAI.SubsphereCurrent.Weighted.pullObservation line 620
  52. lemma OAI.SubsphereCurrent.Weighted.measurable_pullObservation line 626
  53. lemma OAI.SubsphereCurrent.Weighted.block_reconstruct line 630