OAI/Probability/GaussianReplacement/CriticalGeometry.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CurrentProjection.CriticalComparisonMain line 12

    Also declared: ComparatorChallenges/GaussianReplacement.lean:237 (same declaration text).

  2. def OAI.CurrentProjection.criticalRadius line 24
  3. lemma OAI.CurrentProjection.criticalRadius_pos line 26
  4. lemma OAI.CurrentProjection.criticalRadius_le_two line 30
  5. lemma OAI.CurrentProjection.criticalRadius_tendsto line 34
  6. def OAI.CurrentProjection.ballRatio line 39
  7. lemma OAI.CurrentProjection.sphere_dist_le_two line 42
  8. lemma OAI.CurrentProjection.ballRatio_zero line 49
  9. lemma OAI.CurrentProjection.ballRatio_nonneg line 58
  10. lemma OAI.CurrentProjection.measurable_ballRatio line 61
  11. lemma OAI.CurrentProjection.ballRatio_le_growth line 68
  12. lemma OAI.CurrentProjection.ballRatio_tendsto_zero line 81
  13. lemma OAI.CurrentProjection.exists_max_of_tendsto_zero line 88
  14. lemma OAI.CurrentProjection.ballRatio_has_max line 97
  15. def OAI.CurrentProjection.criticalIndex line 105
  16. def OAI.CurrentProjection.criticalMass line 109
  17. def OAI.CurrentProjection.criticalLevel line 112
  18. lemma OAI.CurrentProjection.criticalIndex_max line 115
  19. lemma OAI.CurrentProjection.criticalIndex_least line 123
  20. lemma OAI.CurrentProjection.measurable_criticalIndex line 131
  21. lemma OAI.CurrentProjection.measurable_criticalMass line 168
  22. lemma OAI.CurrentProjection.measurable_criticalLevel line 178
  23. lemma OAI.CurrentProjection.criticalMass_pos line 181
  24. lemma OAI.CurrentProjection.criticalMass_log_bounds line 188
  25. lemma OAI.CurrentProjection.criticalLevel_bounds line 203
  26. lemma OAI.CurrentProjection.criticalIndex_bound line 218
  27. def OAI.CurrentProjection.criticalClass line 252
  28. lemma OAI.CurrentProjection.measurableSet_criticalClass line 255
  29. lemma OAI.CurrentProjection.criticalClass_mass_upper line 260
  30. lemma OAI.CurrentProjection.criticalClass_mass_lower line 275
  31. lemma OAI.CurrentProjection.exists_criticalRadius line 293
  32. lemma OAI.CurrentProjection.criticalClass_restrict_growth line 305
  33. def OAI.CurrentProjection.criticalPosterior line 343
  34. lemma OAI.CurrentProjection.criticalPosterior_growth line 346
  35. lemma OAI.CurrentProjection.criticalClass_packing line 365
  36. lemma OAI.CurrentProjection.criticalClass_cover line 404