OAI/Probability/SphericalField/Perceptron/Variance.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SphericalPerceptron.continuous_integral_of_bounded line 23
2. lemma OAI.SphericalPerceptron.abs_integral_of_bounded line 38
3. lemma OAI.SphericalPerceptron.variance_prod_le line 44
4. lemma OAI.SphericalPerceptron.variance_le_of_oscillation line 85
5. lemma OAI.SphericalPerceptron.continuous_fin_cons line 98
6. lemma OAI.SphericalPerceptron.measurePreserving_fin_cons line 108
7. lemma OAI.SphericalPerceptron.measurableEmbedding_fin_cons line 116
8. theorem OAI.SphericalPerceptron.variance_pi_le_of_bounded_differences line 122
9. lemma OAI.SphericalPerceptron.abs_hamiltonian_update_sub_le line 178
10. lemma OAI.SphericalPerceptron.abs_pressure_update_sub_le line 197
11. lemma OAI.SphericalPerceptron.variance_pressure_le line 215
12. lemma OAI.SphericalPerceptron.variance_pressure_le_rate line 222
13. lemma OAI.SphericalPerceptron.pressure_deviation_le line 237