OAI/Probability/Perceptron/Variational/FieldRounding.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.SphericalPerceptronFreeEnergy.BoundedField line 11
  2. instance OAI.SphericalPerceptronFreeEnergy.(instance at line 17) line 17
  3. lemma OAI.SphericalPerceptronFreeEnergy.BoundedField.measurable line 19
  4. lemma OAI.SphericalPerceptronFreeEnergy.BoundedField.bound_nonneg line 21
  5. lemma OAI.SphericalPerceptronFreeEnergy.BoundedField.integrable line 23
  6. def OAI.SphericalPerceptronFreeEnergy.roundLower line 27
  7. lemma OAI.SphericalPerceptronFreeEnergy.roundLower_nonneg line 29
  8. lemma OAI.SphericalPerceptronFreeEnergy.roundLower_monotone line 31
  9. lemma OAI.SphericalPerceptronFreeEnergy.roundLower_le line 36
  10. lemma OAI.SphericalPerceptronFreeEnergy.sub_roundLower_lt line 41
  11. lemma OAI.SphericalPerceptronFreeEnergy.roundLower_measurable line 47
  12. def OAI.SphericalPerceptronFreeEnergy.BoundedField.round line 49
  13. lemma OAI.SphericalPerceptronFreeEnergy.BoundedField.round_error line 55
  14. lemma OAI.SphericalPerceptronFreeEnergy.BoundedField.round_finite line 61
  15. def OAI.SphericalPerceptronFreeEnergy.BoundedField.roundModel line 71
  16. lemma OAI.SphericalPerceptronFreeEnergy.BoundedField.round_abs_integral line 74
  17. def OAI.SphericalPerceptronFreeEnergy.quantileTrial line 81
  18. def OAI.SphericalPerceptronFreeEnergy.quantileTail line 95
  19. lemma OAI.SphericalPerceptronFreeEnergy.quantileTrial_eq_integral line 98
  20. lemma OAI.SphericalPerceptronFreeEnergy.tailIntegral_quantileTrial line 104
  21. lemma OAI.SphericalPerceptronFreeEnergy.quantileTail_integrable line 118
  22. lemma OAI.SphericalPerceptronFreeEnergy.quantileTail_lower line 135
  23. lemma OAI.SphericalPerceptronFreeEnergy.quantileTail_upper line 142
  24. lemma OAI.SphericalPerceptronFreeEnergy.quantileTail_of_le line 148
  25. lemma OAI.SphericalPerceptronFreeEnergy.quantileTail_lipschitz line 155