OAI/Probability/SphericalField/Cascade/Concentration.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SphericalPerceptron.canonical_coordinate_converges line 17
2. lemma OAI.SphericalPerceptron.exponential_ratio_converges line 46
3. theorem OAI.SphericalPerceptron.canonical_ratio_converges line 79
4. lemma OAI.SphericalPerceptron.canonical_stationary_tail_rates line 97
5. lemma OAI.SphericalPerceptron.integrable_prod_of_conditional_square line 133
6. lemma OAI.SphericalPerceptron.finiteCascade_terminal_log_second_moment_bound line 165
7. theorem OAI.SphericalPerceptron.canonical_coordinate_joint_mean line 181
8. lemma OAI.SphericalPerceptron.expected_eventually_gt_of_probability_lower line 235