OAI/Probability/Perceptron/Variational/ProbabilityMaps.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SphericalPerceptronFreeEnergy.probabilityMap_tendsto_of_ae_tendsto line 11
2. lemma OAI.SphericalPerceptronFreeEnergy.FiniteFieldModel.property_of_ae line 32
3. def OAI.SphericalPerceptronFreeEnergy.quantileRoundLaw line 50
4. lemma OAI.SphericalPerceptronFreeEnergy.quantileRoundLaw_tendsto line 54
5. lemma OAI.SphericalPerceptronFreeEnergy.realTail_quantileRoundLaw line 67
6. lemma OAI.SphericalPerceptronFreeEnergy.quantileRoundLaw_support line 76
7. lemma OAI.SphericalPerceptronFreeEnergy.roundTimeValue_support line 86
8. lemma OAI.SphericalPerceptronFreeEnergy.cappedA_nonneg line 98
9. lemma OAI.SphericalPerceptronFreeEnergy.roundTimeValue_profile_exact line 102
10. lemma OAI.SphericalPerceptronFreeEnergy.quantileRoundLaw_stationary line 123