OAI/Probability/SphericalField/Fields/UniformGrid.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SphericalPerceptron.uniformWeights line 13
  2. def OAI.SphericalPerceptron.uniformExponents line 14
  3. lemma OAI.SphericalPerceptron.uniformWeights_pos line 16
  4. lemma OAI.SphericalPerceptron.uniformWeights_sum line 20
  5. lemma OAI.SphericalPerceptron.uniformExponents_nonneg line 24
  6. lemma OAI.SphericalPerceptron.uniformExponents_last line 28
  7. lemma OAI.SphericalPerceptron.stepCumulative_uniformWeights line 32
  8. lemma OAI.SphericalPerceptron.uniformExponents_castSucc line 43
  9. def OAI.SphericalPerceptron.sphericalGridValue line 49
  10. def OAI.SphericalPerceptron.sphericalGridDual line 52
  11. lemma OAI.SphericalPerceptron.sphericalGridValue_eq line 56
  12. lemma OAI.SphericalPerceptron.varianceLevels_continuous line 84
  13. lemma OAI.SphericalPerceptron.sphericalGridValue_compact_uniform line 93
  14. lemma OAI.SphericalPerceptron.gridVariance_weighted_sum line 111
  15. lemma OAI.SphericalPerceptron.gridVariance_sum line 121
  16. lemma OAI.SphericalPerceptron.sphericalGridValue_compress line 125