OAI/Probability/Perceptron/Variational/RoundedPairCoefficients.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SphericalPerceptronFreeEnergy.exists_finiteFieldModel_strict line 12
2. def OAI.SphericalPerceptronFreeEnergy.finiteMonotoneExtension line 63
3. lemma OAI.SphericalPerceptronFreeEnergy.finiteMonotoneExtension_mono line 66
4. lemma OAI.SphericalPerceptronFreeEnergy.finiteMonotoneExtension_value line 79
5. lemma OAI.SphericalPerceptronFreeEnergy.finiteMonotoneExtension_bounds line 91
6. lemma OAI.SphericalPerceptronFreeEnergy.monotone_tendsto_of_rat_tendsto line 101
7. theorem OAI.SphericalPerceptronFreeEnergy.bounded_monotone_helly line 123