OAI/Probability/SphericalField/Heat/Grid.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SphericalPerceptron.gaussianGrid line 17
2. lemma OAI.SphericalPerceptron.gaussianGrid_lipschitz line 20
3. lemma OAI.SphericalPerceptron.gaussianGrid_succ line 29
4. lemma OAI.SphericalPerceptron.gaussianGrid_zero line 34
5. lemma OAI.SphericalPerceptron.gaussianGrid_absorb line 44
6. def OAI.SphericalPerceptron.gridVariance line 86
7. lemma OAI.SphericalPerceptron.gridVariance_nonneg line 89
8. lemma OAI.SphericalPerceptron.gridVariance_below line 99
9. lemma OAI.SphericalPerceptron.gridVariance_cons line 106
10. lemma OAI.SphericalPerceptron.gaussianBackward_compress line 115