OAI/Probability/Perceptron/Variational/LabelProfileSingleReference.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SphericalPerceptronFreeEnergy.labelProfile_single_reference_exists line 13
2. lemma OAI.SphericalPerceptronFreeEnergy.rootPathMean_bound line 87
3. lemma OAI.SphericalPerceptronFreeEnergy.labelSingleCoefficient_bound line 96
4. lemma OAI.SphericalPerceptronFreeEnergy.labelSingleCoefficient_one line 112
5. def OAI.SphericalPerceptronFreeEnergy.roundedSingleCoeff line 127
6. lemma OAI.SphericalPerceptronFreeEnergy.roundedSingleCoeff_bound line 133
7. lemma OAI.SphericalPerceptronFreeEnergy.roundedSingleCoeff_one line 137
8. theorem OAI.SphericalPerceptronFreeEnergy.rounded_single_reference_exists line 141