OAI/Probability/SphericalField/Fields/Rounding.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SphericalPerceptron.BoundedField.bound_nonneg line 13
2. lemma OAI.SphericalPerceptron.BoundedField.integrable line 15
3. lemma OAI.SphericalPerceptron.sub_roundLower_lt line 19
4. lemma OAI.SphericalPerceptron.roundLower_measurable line 26
5. lemma OAI.SphericalPerceptron.BoundedField.round_error line 28
6. lemma OAI.SphericalPerceptron.BoundedField.round_abs_integral line 34