OAI/Probability/Perceptron/Variational/FiniteGaussianRow.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SphericalPerceptronFreeEnergy.finiteGaussianRow line 14
  2. def OAI.SphericalPerceptronFreeEnergy.finiteGaussianRowLength line 17
  3. lemma OAI.SphericalPerceptronFreeEnergy.finiteGaussianRow_key line 20
  4. lemma OAI.SphericalPerceptronFreeEnergy.finiteGaussianRow_zero line 25
  5. lemma OAI.SphericalPerceptronFreeEnergy.finiteGaussianRow_key_lt line 29
  6. lemma OAI.SphericalPerceptronFreeEnergy.finiteGaussianRow_tail line 33
  7. lemma OAI.SphericalPerceptronFreeEnergy.finiteGaussianRow_sum line 40
  8. lemma OAI.SphericalPerceptronFreeEnergy.finiteGaussianRow_field line 58
  9. lemma OAI.SphericalPerceptronFreeEnergy.finiteGaussianRow_norm line 63
  10. def OAI.SphericalPerceptronFreeEnergy.indexedGaussianRowKey line 70
  11. lemma OAI.SphericalPerceptronFreeEnergy.indexedGaussianRowKey_injective line 73
  12. def OAI.SphericalPerceptronFreeEnergy.indexedGaussianRow line 81
  13. def OAI.SphericalPerceptronFreeEnergy.indexedGaussianRowLength line 85
  14. lemma OAI.SphericalPerceptronFreeEnergy.indexedGaussianRow_measurable line 88
  15. lemma OAI.SphericalPerceptronFreeEnergy.indexedGaussianRowLength_measurable line 102
  16. lemma OAI.SphericalPerceptronFreeEnergy.indexedGaussianRow_field line 108
  17. lemma OAI.SphericalPerceptronFreeEnergy.indexedGaussianRow_norm line 120
  18. lemma OAI.SphericalPerceptronFreeEnergy.indexedGaussianRow_norm_le line 133