OAI/Probability/Perceptron/Variational/UniformQuantileCells.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SphericalPerceptronFreeEnergy.uniformQuantileGrid line 11
  2. lemma OAI.SphericalPerceptronFreeEnergy.uniformQuantileGrid_strict line 15
  3. lemma OAI.SphericalPerceptronFreeEnergy.uniformQuantileGrid_zero line 20
  4. lemma OAI.SphericalPerceptronFreeEnergy.uniformQuantileGrid_last line 24
  5. def OAI.SphericalPerceptronFreeEnergy.uniformQuantileCell line 30
  6. lemma OAI.SphericalPerceptronFreeEnergy.uniformQuantileCell_mono line 33
  7. lemma OAI.SphericalPerceptronFreeEnergy.uniformQuantileCell_measurable line 38
  8. lemma OAI.SphericalPerceptronFreeEnergy.uniformQuantileCell_floor line 41
  9. lemma OAI.SphericalPerceptronFreeEnergy.uniformQuantileCell_bounds line 51
  10. lemma OAI.SphericalPerceptronFreeEnergy.uniformQuantileCell_atom line 74
  11. lemma OAI.SphericalPerceptronFreeEnergy.uniformQuantileCell_weight line 85
  12. lemma OAI.SphericalPerceptronFreeEnergy.uniformQuantileCell_integral line 100
  13. lemma OAI.SphericalPerceptronFreeEnergy.uniformQuantileCell_upper line 105
  14. lemma OAI.SphericalPerceptronFreeEnergy.uniformQuantileCell_tail_integral line 112
  15. def OAI.SphericalPerceptronFreeEnergy.compactSpinTime line 126
  16. lemma OAI.SphericalPerceptronFreeEnergy.compactSpinTime_continuous line 129
  17. lemma OAI.SphericalPerceptronFreeEnergy.compactSpinTime_mono line 133
  18. def OAI.SphericalPerceptronFreeEnergy.compactSpinCode line 139
  19. lemma OAI.SphericalPerceptronFreeEnergy.compactSpinCode_measurable line 142
  20. lemma OAI.SphericalPerceptronFreeEnergy.compactSpinCode_mono line 145
  21. def OAI.SphericalPerceptronFreeEnergy.compactSpinDecode line 149
  22. lemma OAI.SphericalPerceptronFreeEnergy.compactSpinDecode_error line 152
  23. lemma OAI.SphericalPerceptronFreeEnergy.compactSpinDecode_tendsto line 166