OAI/Probability/SphericalField/Cascade/CoordinateBounds.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SphericalPerceptron.cascadeLogFluctuationConstant line 17
2. lemma OAI.SphericalPerceptron.cascadeLogFluctuationConstant_nonneg line 20
3. lemma OAI.SphericalPerceptron.decoratedCascade_log_second_moment_bound line 24
4. lemma OAI.SphericalPerceptron.decoratedCascade_log_deviation_le line 81
5. lemma OAI.SphericalPerceptron.finiteCascade_terminal_log_deviation_le line 103
6. lemma OAI.SphericalPerceptron.fractional_log_moment_sum_pi line 119
7. theorem OAI.SphericalPerceptron.finiteCascade_sum_pi line 131
8. theorem OAI.SphericalPerceptron.finiteCascade_quadratic_coordinates line 162