OAI/Probability/Perceptron/Cavity/CavityRoundedLower.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SphericalPerceptronFreeEnergy.cavityProfileMoment line 13
2. def OAI.SphericalPerceptronFreeEnergy.roundedProfileMoment line 16
3. lemma OAI.SphericalPerceptronFreeEnergy.roundedProfileMoment_tendsto line 21
4. lemma OAI.SphericalPerceptronFreeEnergy.roundedCavityValue_lower line 45
5. lemma OAI.SphericalPerceptronFreeEnergy.markedTimePair_eq_map line 95
6. lemma OAI.SphericalPerceptronFreeEnergy.marked_cappedA_identification line 104