OAI/Probability/Subsphere/Geometry/Integration.lean

GitHub source file

54 declarations, 0 contain sorry, 0 declared as axioms

Isometric naturality of the exact normalized Haar spherical law.

  1. lemma OAI.SubsphereCurrent.Polar.introducing_radius line 14
  2. lemma OAI.SubsphereCurrent.Polar.lintegral_polar line 27
  3. lemma OAI.SubsphereCurrent.Polar.orthogonal_sum_volume line 35
  4. def OAI.SubsphereCurrent.Polar.unitDirection line 52
  5. def OAI.SubsphereCurrent.Polar.radial line 55
  6. lemma OAI.SubsphereCurrent.Polar.measurable_radial line 61
  7. lemma OAI.SubsphereCurrent.Polar.radial_smul line 78
  8. lemma OAI.SubsphereCurrent.Polar.radial_ball_integral line 91
  9. def OAI.SubsphereCurrent.Polar.sphereMap line 148
  10. lemma OAI.SubsphereCurrent.Polar.sphereMap_preserving line 153
  11. structure OAI.SubsphereCurrent.Slice.Test line 197
  12. def OAI.SubsphereCurrent.Slice.Test.point line 207
  13. lemma OAI.SubsphereCurrent.Slice.Test.measurable_point line 220
  14. lemma OAI.SubsphereCurrent.Slice.orthogonal_radius_norm line 225
  15. def OAI.SubsphereCurrent.Slice.radiusNorm line 236
  16. lemma OAI.SubsphereCurrent.Slice.radiusNorm_pos line 239
  17. lemma OAI.SubsphereCurrent.Slice.radiusNorm_sq line 244
  18. lemma OAI.SubsphereCurrent.Slice.norm_eq_radiusNorm line 248
  19. def OAI.SubsphereCurrent.Slice.scaledTest line 254
  20. lemma OAI.SubsphereCurrent.Slice.radial_on_slice line 270
  21. def OAI.SubsphereCurrent.Slice.Controlled line 286
  22. lemma OAI.SubsphereCurrent.Slice.radial_slice_bound line 290
  23. def OAI.SubsphereCurrent.Weighted.nestedSpaceEquiv line 328
  24. lemma OAI.SubsphereCurrent.Weighted.nestedSpaceEquiv_val line 333
  25. def OAI.SubsphereCurrent.Weighted.nestedTest line 337
  26. lemma OAI.SubsphereCurrent.Weighted.nestedTest_point line 362
  27. lemma OAI.SubsphereCurrent.Weighted.borel_onTest line 373
  28. lemma OAI.SubsphereCurrent.Weighted.radius_le_one line 378
  29. lemma OAI.SubsphereCurrent.Weighted.nested_average line 381
  30. lemma OAI.SubsphereCurrent.Polar.radius_inverse_density line 411
  31. lemma OAI.SubsphereCurrent.Polar.radius_inverse_integral line 425
  32. lemma OAI.SubsphereCurrent.Polar.orthogonal_volume_ratio line 439
  33. lemma OAI.SubsphereCurrent.Slice.sphere_integral_unnormalize line 492
  34. def OAI.SubsphereCurrent.Slice.capFunction line 502
  35. def OAI.SubsphereCurrent.Slice.ballCap line 506
  36. lemma OAI.SubsphereCurrent.Slice.measurable_capFunction line 510
  37. lemma OAI.SubsphereCurrent.Slice.measurable_ballCap line 515
  38. lemma OAI.SubsphereCurrent.Slice.ballCap_le line 520
  39. lemma OAI.SubsphereCurrent.Slice.ballCap_support line 531
  40. lemma OAI.SubsphereCurrent.Slice.angular_ballCap_bound line 576
  41. lemma OAI.SubsphereCurrent.Slice.ballCap_integral line 620
  42. lemma OAI.SubsphereCurrent.Slice.radius_mass_le line 683
  43. lemma OAI.SubsphereCurrent.Slice.controlled_cap_bound line 705
  44. def OAI.SubsphereCurrent.Quarter.twinTurn line 751
  45. lemma OAI.SubsphereCurrent.Quarter.twinTurn_inner line 756
  46. lemma OAI.SubsphereCurrent.Quarter.twinTurn_square line 763
  47. lemma OAI.SubsphereCurrent.Quarter.exists_even_turn line 769
  48. lemma OAI.SubsphereCurrent.Quarter.subspace_dimension line 784
  49. lemma OAI.SubsphereCurrent.Quarter.exists_small_fixed line 793
  50. def OAI.SubsphereCurrent.Quarter.extend line 805
  51. lemma OAI.SubsphereCurrent.Quarter.extend_apply line 809
  52. lemma OAI.SubsphereCurrent.Quarter.extend_fixed line 813
  53. lemma OAI.SubsphereCurrent.Quarter.extend_norm_sq line 818
  54. lemma OAI.SubsphereCurrent.Quarter.extend_square_norm_sq line 833