OAI/Probability/SphericalField/Sphere/Shell.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SphericalPerceptron.canonicalWeighted_compl_band_le line 14
2. lemma OAI.SphericalPerceptron.exp_log_quotient_mul line 33
3. def OAI.SphericalPerceptron.canonicalCoordinateBandTotalE line 40
4. lemma OAI.SphericalPerceptron.canonicalCoordinateBandTotalE_le line 46
5. lemma OAI.SphericalPerceptron.canonicalCoordinate_half_band line 55
6. theorem OAI.SphericalPerceptron.canonicalCoordinate_bad_half_band_tendsto_zero line 117
7. lemma OAI.SphericalPerceptron.canonicalCoordinate_shell_log_upper line 164
8. lemma OAI.SphericalPerceptron.canonicalCoordinate_shell_log_lower line 193
9. lemma OAI.SphericalPerceptron.convex_nonneg_radius_transfer line 226
10. lemma OAI.SphericalPerceptron.sqrt_radius_band line 254
11. lemma OAI.SphericalPerceptron.coordinateAngularLog_unit_radius_bounds line 272
12. lemma OAI.SphericalPerceptron.canonicalCoordinate_unitSphere_upper line 299
13. lemma OAI.SphericalPerceptron.canonicalCoordinate_unitSphere_lower line 313