OAI/Probability/SphericalField/Sphere/RadialDensity.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.SphericalPerceptron.RadialSpace line 22
  2. def OAI.SphericalPerceptron.radialNormalizer line 24
  3. def OAI.SphericalPerceptron.canonicalRadialDensity line 26
  4. def OAI.SphericalPerceptron.canonicalRadialMass line 29
  5. lemma OAI.SphericalPerceptron.radialNormalizer_pos line 32
  6. lemma OAI.SphericalPerceptron.canonicalRadialDensity_pos line 36
  7. lemma OAI.SphericalPerceptron.canonicalRadialDensity_continuous line 39
  8. lemma OAI.SphericalPerceptron.integrable_exp_neg_norm_sq line 42
  9. lemma OAI.SphericalPerceptron.canonicalRadialDensity_integrable line 52
  10. lemma OAI.SphericalPerceptron.canonicalRadialDensity_integral line 56
  11. instance OAI.SphericalPerceptron.(instance at line 67) line 67
  12. lemma OAI.SphericalPerceptron.canonicalRadialMass_apply line 76
  13. lemma OAI.SphericalPerceptron.canonicalRadial_mass_le line 83
  14. lemma OAI.SphericalPerceptron.canonicalRadial_upper_tail line 104
  15. lemma OAI.SphericalPerceptron.canonicalRadial_lower_tail line 130
  16. def OAI.SphericalPerceptron.normSquareBand line 156
  17. lemma OAI.SphericalPerceptron.normSquareBand_measurable line 159
  18. lemma OAI.SphericalPerceptron.canonicalRadial_band_compl_le line 163
  19. lemma OAI.SphericalPerceptron.exp_neg_mul_nat_succ_tendsto line 179
  20. lemma OAI.SphericalPerceptron.canonicalRadial_band_eventually_half line 185
  21. lemma OAI.SphericalPerceptron.canonicalRadialMass_real_apply line 207
  22. lemma OAI.SphericalPerceptron.canonicalRadialDensity_tilt line 213
  23. lemma OAI.SphericalPerceptron.normSquareBand_tilt_bounds line 220