OAI/Probability/Perceptron/Cavity/BulkMarkedTangentLimit.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SphericalPerceptronFreeEnergy.bulkScale_sq_div line 11
2. lemma OAI.SphericalPerceptronFreeEnergy.bulk_tangent_error_tendsto line 19
3. lemma OAI.SphericalPerceptronFreeEnergy.marked_tangent_continuous line 32
4. lemma OAI.SphericalPerceptronFreeEnergy.bulk_marked_tangent_limit line 43
5. lemma OAI.SphericalPerceptronFreeEnergy.exists_nat_perm_pair line 67
6. lemma OAI.SphericalPerceptronFreeEnergy.compact_exchangeable_offdiag_ae line 83
7. lemma OAI.SphericalPerceptronFreeEnergy.bulkMarkedArray_limit_overlap line 99
8. theorem OAI.SphericalPerceptronFreeEnergy.bulkMarkedArray_identification line 110