OAI/Probability/SphericalField/Quantiles/RoundGrid.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SphericalPerceptron.gridFloor line 13
2. def OAI.SphericalPerceptron.gridCeil line 20
3. lemma OAI.SphericalPerceptron.gridFloor_mono line 26
4. lemma OAI.SphericalPerceptron.gridCeil_mono line 31
5. lemma OAI.SphericalPerceptron.gridFloor_le_gridCeil line 36
6. lemma OAI.SphericalPerceptron.gridCeil_le_gridFloor_add_one line 39
7. lemma OAI.SphericalPerceptron.uniformExponents_gridFloor_le line 42
8. lemma OAI.SphericalPerceptron.le_uniformExponents_gridCeil line 47
9. lemma OAI.SphericalPerceptron.gaussianBackward_ofFn_mono line 52
10. lemma OAI.SphericalPerceptron.sphericalHeatValue_ofFn_mono line 81
11. lemma OAI.SphericalPerceptron.sphericalGridValue_round_bracket line 91