OAI/Probability/SphericalField/Fields/BoundedPressure.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SphericalPerceptron.fieldL1 line 14
2. lemma OAI.SphericalPerceptron.fieldL1_nonneg line 16
3. lemma OAI.SphericalPerceptron.fieldL1_symm line 18
4. lemma OAI.SphericalPerceptron.fieldL1_triangle line 21
5. lemma OAI.SphericalPerceptron.BoundedField.round_pair_dist line 28
6. lemma OAI.SphericalPerceptron.BoundedField.round_pressure_cauchy line 39
7. lemma OAI.SphericalPerceptron.boundedSphericalFieldValue_tendsto line 61
8. theorem OAI.SphericalPerceptron.boundedSphericalFieldValue_eq_finite line 65
9. theorem OAI.SphericalPerceptron.boundedSphericalFieldValue_L1_continuous line 79
10. lemma OAI.SphericalPerceptron.boundedSphericalFieldValue_ae_eq line 96