OAI/Probability/Perceptron/Variational/StationaryExistence.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SphericalPerceptronFreeEnergy.stepTailSum line 12
  2. lemma OAI.SphericalPerceptronFreeEnergy.stepTailSum_zero line 15
  3. lemma OAI.SphericalPerceptronFreeEnergy.stepTailSum_last line 18
  4. lemma OAI.SphericalPerceptronFreeEnergy.stepTailSum_difference line 24
  5. lemma OAI.SphericalPerceptronFreeEnergy.stepTailSum_nonneg line 44
  6. lemma OAI.SphericalPerceptronFreeEnergy.stepTailSum_le_zero line 50
  7. def OAI.SphericalPerceptronFreeEnergy.finitePrecisionShift line 57
  8. def OAI.SphericalPerceptronFreeEnergy.finitePrecisionTail line 60
  9. def OAI.SphericalPerceptronFreeEnergy.finiteOverlapIncrement line 63
  10. def OAI.SphericalPerceptronFreeEnergy.finiteStationarityMass line 67
  11. lemma OAI.SphericalPerceptronFreeEnergy.finitePrecisionShift_le_root line 71
  12. lemma OAI.SphericalPerceptronFreeEnergy.finitePrecisionTail_pos line 77
  13. lemma OAI.SphericalPerceptronFreeEnergy.finitePrecisionTail_gap line 82
  14. lemma OAI.SphericalPerceptronFreeEnergy.finiteOverlapIncrement_nonneg line 97
  15. lemma OAI.SphericalPerceptronFreeEnergy.finiteStationarityMass_ge_root line 103
  16. lemma OAI.SphericalPerceptronFreeEnergy.finiteStationarityMass_continuousOn line 122
  17. lemma OAI.SphericalPerceptronFreeEnergy.finiteStationarityMass_tendsto line 137
  18. theorem OAI.SphericalPerceptronFreeEnergy.exists_finite_normalizing_precision line 150
  19. theorem OAI.SphericalPerceptronFreeEnergy.exists_finite_stationary_quantile line 165
  20. def OAI.SphericalPerceptronFreeEnergy.finiteSphericalDualObjective line 238
  21. def OAI.SphericalPerceptronFreeEnergy.finiteSphericalDualValues line 242
  22. theorem OAI.SphericalPerceptronFreeEnergy.finiteSphericalFieldValue_pointwise_dual line 247