OAI/Probability/SphericalField/Entropy/StationaryExistence.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SphericalPerceptron.stepTailSum line 14
  2. lemma OAI.SphericalPerceptron.stepTailSum_zero line 17
  3. lemma OAI.SphericalPerceptron.stepTailSum_last line 20
  4. lemma OAI.SphericalPerceptron.stepTailSum_difference line 26
  5. lemma OAI.SphericalPerceptron.stepTailSum_nonneg line 46
  6. lemma OAI.SphericalPerceptron.stepTailSum_le_zero line 52
  7. def OAI.SphericalPerceptron.finitePrecisionShift line 59
  8. def OAI.SphericalPerceptron.finitePrecisionTail line 62
  9. def OAI.SphericalPerceptron.finiteOverlapIncrement line 65
  10. def OAI.SphericalPerceptron.finiteStationarityMass line 69
  11. lemma OAI.SphericalPerceptron.finitePrecisionShift_le_root line 73
  12. lemma OAI.SphericalPerceptron.finitePrecisionTail_pos line 79
  13. lemma OAI.SphericalPerceptron.finitePrecisionTail_gap line 84
  14. lemma OAI.SphericalPerceptron.finiteOverlapIncrement_nonneg line 99
  15. lemma OAI.SphericalPerceptron.finiteStationarityMass_ge_root line 105
  16. lemma OAI.SphericalPerceptron.finiteStationarityMass_continuousOn line 124
  17. lemma OAI.SphericalPerceptron.finiteStationarityMass_tendsto line 139
  18. theorem OAI.SphericalPerceptron.exists_finite_normalizing_precision line 152
  19. theorem OAI.SphericalPerceptron.exists_finite_stationary_quantile line 167
  20. theorem OAI.SphericalPerceptron.finiteSphericalFieldValue_pointwise_dual line 240