OAI/Probability/Perceptron/Cavity/CavityShellSubexp.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SphericalPerceptronFreeEnergy.cavityShell_subset_closedBall line 11
2. lemma OAI.SphericalPerceptronFreeEnergy.cavityShell_volume_ne_top line 17
3. lemma OAI.SphericalPerceptronFreeEnergy.cavity_sqrt_power_gap line 22
4. lemma OAI.SphericalPerceptronFreeEnergy.cavityShell_volume_lower line 48
5. lemma OAI.SphericalPerceptronFreeEnergy.cavityShell_density_lower line 72
6. lemma OAI.SphericalPerceptronFreeEnergy.cavity_band_density_upper line 87
7. lemma OAI.SphericalPerceptronFreeEnergy.cavity_sqrt_pow_exp line 113
8. lemma OAI.SphericalPerceptronFreeEnergy.cavityShell_band_comparison line 126
9. lemma OAI.SphericalPerceptronFreeEnergy.cavityShell_log_lower line 162
10. lemma OAI.SphericalPerceptronFreeEnergy.cavityShell_log_error_tendsto line 176
11. theorem OAI.SphericalPerceptronFreeEnergy.cavityShell_log_sublinear line 193