OAI/Probability/Perceptron/Cavity/FreshGGUniqueness.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SphericalPerceptronFreeEnergy.CompactSpinGeometry line 12
2. def OAI.SphericalPerceptronFreeEnergy.compactSpinTop line 16
3. lemma OAI.SphericalPerceptronFreeEnergy.compactSpinCode_geometry line 18
4. lemma OAI.SphericalPerceptronFreeEnergy.compactSpinCode_block_law_unique line 48
5. lemma OAI.SphericalPerceptronFreeEnergy.compactSpinCode_integral_unique line 66
6. lemma OAI.SphericalPerceptronFreeEnergy.compactSpinCode_integral_tendsto line 80
7. theorem OAI.SphericalPerceptronFreeEnergy.scalarGram_eq_of_pair_law line 103
8. theorem OAI.SphericalPerceptronFreeEnergy.freshReplicaKernel_eq_of_pair_law line 123