OAI/Probability/Perceptron/Sphere/SphereBridge.lean

GitHub source file

40 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SphericalPerceptronFreeEnergy.decoratedLeafIntegral line 12
  2. lemma OAI.SphericalPerceptronFreeEnergy.decoratedLeafIntegral_exp line 21
  3. lemma OAI.SphericalPerceptronFreeEnergy.decoratedLeafIntegral_measurable line 30
  4. lemma OAI.SphericalPerceptronFreeEnergy.decoratedLeafIntegral_param_measurable line 45
  5. lemma OAI.SphericalPerceptronFreeEnergy.decoratedLeafIntegral_mono line 66
  6. lemma OAI.SphericalPerceptronFreeEnergy.decoratedLeafIntegral_const_mul line 75
  7. lemma OAI.SphericalPerceptronFreeEnergy.decoratedLeafIntegral_lintegral line 86
  8. def OAI.SphericalPerceptronFreeEnergy.decoratedFieldFactor line 116
  9. def OAI.SphericalPerceptronFreeEnergy.decoratedAngularFactor line 121
  10. lemma OAI.SphericalPerceptronFreeEnergy.decoratedFieldFactor_measurable line 127
  11. lemma OAI.SphericalPerceptronFreeEnergy.decoratedAngularFactor_eq line 142
  12. lemma OAI.SphericalPerceptronFreeEnergy.decoratedAngularFactor_mono line 163
  13. lemma OAI.SphericalPerceptronFreeEnergy.decoratedAngularFactor_mass_le line 172
  14. theorem OAI.SphericalPerceptronFreeEnergy.decoratedCanonical_band_bounds line 181
  15. lemma OAI.SphericalPerceptronFreeEnergy.canonicalRadialDensity_complete_square line 215
  16. lemma OAI.SphericalPerceptronFreeEnergy.canonicalRadial_linear_integral line 229
  17. def OAI.SphericalPerceptronFreeEnergy.coordinateLeafField line 247
  18. lemma OAI.SphericalPerceptronFreeEnergy.coordinateLeafField_measurable line 250
  19. lemma OAI.SphericalPerceptronFreeEnergy.coordinateLeafField_norm_sq line 256
  20. lemma OAI.SphericalPerceptronFreeEnergy.canonicalCoordinatePotential_eq_norm line 261
  21. theorem OAI.SphericalPerceptronFreeEnergy.canonicalCoordinateTotalE_eq_radial line 268
  22. def OAI.SphericalPerceptronFreeEnergy.sphericalCoordinateLog line 291
  23. lemma OAI.SphericalPerceptronFreeEnergy.canonicalCoordinateLog_eq_radial line 297
  24. lemma OAI.SphericalPerceptronFreeEnergy.decoratedLeafIntegral_holder line 306
  25. lemma OAI.SphericalPerceptronFreeEnergy.ofReal_exp_affine line 348
  26. lemma OAI.SphericalPerceptronFreeEnergy.sphericalExp_holder line 354
  27. lemma OAI.SphericalPerceptronFreeEnergy.decoratedAngularFactor_holder line 376
  28. lemma OAI.SphericalPerceptronFreeEnergy.decoratedTerminalTotal_pos_of_fractional line 391
  29. lemma OAI.SphericalPerceptronFreeEnergy.decoratedTerminalTotal_zero_pos line 409
  30. def OAI.SphericalPerceptronFreeEnergy.coordinateCascadeLaw line 421
  31. instance OAI.SphericalPerceptronFreeEnergy.coordinateCascadeLaw_probability line 426
  32. lemma OAI.SphericalPerceptronFreeEnergy.canonicalCoordinateTotal_pos line 431
  33. lemma OAI.SphericalPerceptronFreeEnergy.canonicalCoordinateBase_pos line 450
  34. lemma OAI.SphericalPerceptronFreeEnergy.sphericalExp_le_gaussian line 467
  35. lemma OAI.SphericalPerceptronFreeEnergy.decoratedAngularFactor_le_canonical line 486
  36. def OAI.SphericalPerceptronFreeEnergy.coordinateAngularLog line 502
  37. lemma OAI.SphericalPerceptronFreeEnergy.coordinateAngularLog_regular line 508
  38. lemma OAI.SphericalPerceptronFreeEnergy.coordinateAngularLog_convex line 545
  39. lemma OAI.SphericalPerceptronFreeEnergy.coordinateAngularLog_measurable line 573
  40. lemma OAI.SphericalPerceptronFreeEnergy.coordinateAngularLog_integrable line 592