OAI/Probability/SphericalField/Gibbs/GaussianField.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SphericalPerceptron.measurable_tiltMean line 19
2. def OAI.SphericalPerceptron.gaussianField line 26
3. lemma OAI.SphericalPerceptron.gaussianField_measurable line 29
4. lemma OAI.SphericalPerceptron.gaussianField_bound line 36
5. lemma OAI.SphericalPerceptron.gaussianField_insertNth line 47
6. lemma OAI.SphericalPerceptron.tilt_mean_mulObservable line 56
7. lemma OAI.SphericalPerceptron.gaussian_field_coordinate_ibp line 63
8. lemma OAI.SphericalPerceptron.ennreal_rpow_sum_le line 135
9. lemma OAI.SphericalPerceptron.ennreal_rpow_tsum_le line 144
10. lemma OAI.SphericalPerceptron.finitePoissonLaw_rpow_lintegral_le line 152
11. lemma OAI.SphericalPerceptron.countablePoissonLaw_rpow_lintegral_le line 168