OAI/Probability/SphericalField/Sphere/AmplitudeConvex.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SphericalPerceptron.sphericalExp_field_holder line 13
2. lemma OAI.SphericalPerceptron.decoratedLeafIntegral_mixed_holder line 35
3. lemma OAI.SphericalPerceptron.canonicalCoordinateStep_affine line 75
4. lemma OAI.SphericalPerceptron.coordinateLeafField_affine line 83
5. lemma OAI.SphericalPerceptron.coordinateAngularFactor_amplitude_holder line 88
6. lemma OAI.SphericalPerceptron.decoratedLeafIntegral_constant_step line 113
7. lemma OAI.SphericalPerceptron.decoratedTerminalTotal_zero_step line 126
8. lemma OAI.SphericalPerceptron.quadraticCascadePrecision_add line 135
9. lemma OAI.SphericalPerceptron.exists_positive_canonical_precision line 141
10. lemma OAI.SphericalPerceptron.coordinateAngularLog_amplitude_convex line 147
11. def OAI.SphericalPerceptron.coordinateRootScale line 176
12. lemma OAI.SphericalPerceptron.coordinateRootScale_preserving line 180
13. def OAI.SphericalPerceptron.amplitudeSphereLog line 195
14. def OAI.SphericalPerceptron.amplitudeSphereValue line 199
15. lemma OAI.SphericalPerceptron.amplitudeSphereLog_integrable line 202
16. lemma OAI.SphericalPerceptron.amplitudeSphereValue_eq line 209
17. lemma OAI.SphericalPerceptron.amplitudeSphereLog_nonneg line 218
18. lemma OAI.SphericalPerceptron.amplitudeSphereLog_regular line 225
19. lemma OAI.SphericalPerceptron.amplitudeSphereValue_convex line 244