OAI/Probability/SphericalField/Sphere/Polar.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SphericalPerceptron.polar_lintegral line 28
  2. lemma OAI.SphericalPerceptron.polar_lintegral_swap line 49
  3. def OAI.SphericalPerceptron.normalizedAngular line 57
  4. def OAI.SphericalPerceptron.haarRadiusMeasure line 60
  5. lemma OAI.SphericalPerceptron.angular_total_ne_zero line 63
  6. lemma OAI.SphericalPerceptron.polar_lintegral_normalized line 66
  7. lemma OAI.SphericalPerceptron.polar_radial_lintegral line 76
  8. lemma OAI.SphericalPerceptron.polar_weighted_lintegral line 87
  9. lemma OAI.SphericalPerceptron.polar_weighted_bounds line 100
  10. def OAI.SphericalPerceptron.linearFieldFactor line 125
  11. def OAI.SphericalPerceptron.angularFieldFactor line 128
  12. lemma OAI.SphericalPerceptron.linearFieldFactor_measurable line 132
  13. lemma OAI.SphericalPerceptron.angularFieldFactor_eq line 137
  14. lemma OAI.SphericalPerceptron.angularFieldFactor_mono line 148
  15. lemma OAI.SphericalPerceptron.one_le_angularFieldFactor line 154
  16. def OAI.SphericalPerceptron.canonicalBandRadiusWeight line 162
  17. lemma OAI.SphericalPerceptron.canonicalBandRadiusWeight_measurable line 166
  18. lemma OAI.SphericalPerceptron.canonicalBandRadiusWeight_integral line 172
  19. lemma OAI.SphericalPerceptron.canonicalBandRadiusWeight_mass line 184