OAI/Probability/SphericalField/Fields/Words.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SphericalPerceptron.cascadeHeatWord_eq_ofFn line 15
  2. def OAI.SphericalPerceptron.fieldVariances line 28
  3. def OAI.SphericalPerceptron.fieldExponents line 31
  4. lemma OAI.SphericalPerceptron.fieldVariances_nonneg line 34
  5. lemma OAI.SphericalPerceptron.fieldVariances_sum line 40
  6. lemma OAI.SphericalPerceptron.fieldExponents_nonneg line 47
  7. lemma OAI.SphericalPerceptron.fieldExponents_lt_one line 51
  8. lemma OAI.SphericalPerceptron.fieldExponents_strictMono line 55
  9. lemma OAI.SphericalPerceptron.stepFieldIncrement_reverse line 64
  10. lemma OAI.SphericalPerceptron.fieldWord_eq line 73
  11. def OAI.SphericalPerceptron.sphericalHeatValue line 79
  12. lemma OAI.SphericalPerceptron.finiteSphericalFieldValue_eq_heat line 83
  13. def OAI.SphericalPerceptron.varianceLevels line 102
  14. lemma OAI.SphericalPerceptron.varianceLevels_zero line 105
  15. lemma OAI.SphericalPerceptron.varianceLevels_last line 108
  16. lemma OAI.SphericalPerceptron.varianceLevels_increment line 112
  17. lemma OAI.SphericalPerceptron.fieldVariances_varianceLevels line 132
  18. lemma OAI.SphericalPerceptron.varianceLevels_monotone line 139
  19. lemma OAI.SphericalPerceptron.varianceLevels_nonneg line 146
  20. lemma OAI.SphericalPerceptron.gaussianGrid_spherical_last line 153