OAI/Probability/SphericalField/Sphere/Bridge.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SphericalPerceptron.decoratedLeafIntegral_exp line 14
  2. lemma OAI.SphericalPerceptron.decoratedLeafIntegral_measurable line 23
  3. lemma OAI.SphericalPerceptron.decoratedLeafIntegral_param_measurable line 38
  4. lemma OAI.SphericalPerceptron.decoratedLeafIntegral_mono line 59
  5. lemma OAI.SphericalPerceptron.decoratedLeafIntegral_const_mul line 68
  6. lemma OAI.SphericalPerceptron.decoratedLeafIntegral_lintegral line 79
  7. lemma OAI.SphericalPerceptron.decoratedFieldFactor_measurable line 109
  8. lemma OAI.SphericalPerceptron.decoratedAngularFactor_eq line 124
  9. lemma OAI.SphericalPerceptron.decoratedAngularFactor_mono line 145
  10. lemma OAI.SphericalPerceptron.decoratedAngularFactor_mass_le line 154
  11. theorem OAI.SphericalPerceptron.decoratedCanonical_band_bounds line 163
  12. lemma OAI.SphericalPerceptron.canonicalRadialDensity_complete_square line 197
  13. lemma OAI.SphericalPerceptron.canonicalRadial_linear_integral line 211
  14. lemma OAI.SphericalPerceptron.coordinateLeafField_measurable line 229
  15. lemma OAI.SphericalPerceptron.coordinateLeafField_norm_sq line 235
  16. lemma OAI.SphericalPerceptron.canonicalCoordinatePotential_eq_norm line 240
  17. theorem OAI.SphericalPerceptron.canonicalCoordinateTotalE_eq_radial line 247
  18. def OAI.SphericalPerceptron.sphericalCoordinateLog line 270
  19. lemma OAI.SphericalPerceptron.canonicalCoordinateLog_eq_radial line 276
  20. lemma OAI.SphericalPerceptron.decoratedLeafIntegral_holder line 285
  21. lemma OAI.SphericalPerceptron.ofReal_exp_affine line 327
  22. lemma OAI.SphericalPerceptron.sphericalExp_holder line 333
  23. lemma OAI.SphericalPerceptron.decoratedAngularFactor_holder line 355
  24. lemma OAI.SphericalPerceptron.decoratedTerminalTotal_pos_of_fractional line 370
  25. lemma OAI.SphericalPerceptron.decoratedTerminalTotal_zero_pos line 388
  26. instance OAI.SphericalPerceptron.coordinateCascadeLaw_probability line 400
  27. lemma OAI.SphericalPerceptron.canonicalCoordinateTotal_pos line 405
  28. lemma OAI.SphericalPerceptron.canonicalCoordinateBase_pos line 424
  29. lemma OAI.SphericalPerceptron.sphericalExp_le_gaussian line 441
  30. lemma OAI.SphericalPerceptron.decoratedAngularFactor_le_canonical line 460
  31. lemma OAI.SphericalPerceptron.coordinateAngularLog_regular line 476
  32. lemma OAI.SphericalPerceptron.coordinateAngularLog_convex line 513
  33. lemma OAI.SphericalPerceptron.coordinateAngularLog_measurable line 541
  34. lemma OAI.SphericalPerceptron.coordinateAngularLog_integrable line 560