OAI/Probability/Perceptron/Cavity/BulkEmpiricalLimit.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SphericalPerceptronFreeEnergy.bulk_density_factors line 11
2. lemma OAI.SphericalPerceptronFreeEnergy.bulkPairAverage_first_limit line 32
3. lemma OAI.SphericalPerceptronFreeEnergy.bulkPairAverage_second_limit line 48
4. theorem OAI.SphericalPerceptronFreeEnergy.bulk_marked_empirical_limits line 72
5. lemma OAI.SphericalPerceptronFreeEnergy.bulk_pair_restoration_exact line 98
6. lemma OAI.SphericalPerceptronFreeEnergy.bulk_full_pair_tendsto line 120
7. lemma OAI.SphericalPerceptronFreeEnergy.bulk_limit_geometry line 134
8. lemma OAI.SphericalPerceptronFreeEnergy.bulk_full_omitted_pair_integral line 152