OAI/Probability/Perceptron/Variational/AmplitudeConvex.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SphericalPerceptronFreeEnergy.sphericalExp_field_holder line 11
  2. lemma OAI.SphericalPerceptronFreeEnergy.decoratedLeafIntegral_mixed_holder line 33
  3. lemma OAI.SphericalPerceptronFreeEnergy.canonicalCoordinateStep_affine line 73
  4. lemma OAI.SphericalPerceptronFreeEnergy.coordinateLeafField_affine line 81
  5. lemma OAI.SphericalPerceptronFreeEnergy.coordinateAngularFactor_amplitude_holder line 86
  6. lemma OAI.SphericalPerceptronFreeEnergy.decoratedLeafIntegral_constant_step line 111
  7. lemma OAI.SphericalPerceptronFreeEnergy.decoratedTerminalTotal_zero_step line 124
  8. lemma OAI.SphericalPerceptronFreeEnergy.quadraticCascadePrecision_add line 133
  9. lemma OAI.SphericalPerceptronFreeEnergy.exists_positive_canonical_precision line 139
  10. lemma OAI.SphericalPerceptronFreeEnergy.coordinateAngularLog_amplitude_convex line 145
  11. def OAI.SphericalPerceptronFreeEnergy.coordinateRootScale line 174
  12. lemma OAI.SphericalPerceptronFreeEnergy.coordinateRootScale_preserving line 178
  13. def OAI.SphericalPerceptronFreeEnergy.amplitudeSphereLog line 193
  14. def OAI.SphericalPerceptronFreeEnergy.amplitudeSphereValue line 197
  15. lemma OAI.SphericalPerceptronFreeEnergy.amplitudeSphereLog_integrable line 200
  16. lemma OAI.SphericalPerceptronFreeEnergy.amplitudeSphereValue_eq line 207
  17. lemma OAI.SphericalPerceptronFreeEnergy.amplitudeSphereLog_nonneg line 216
  18. lemma OAI.SphericalPerceptronFreeEnergy.amplitudeSphereLog_regular line 223
  19. lemma OAI.SphericalPerceptronFreeEnergy.amplitudeSphereValue_convex line 242