OAI/Probability/GaussianReplacement/Sphere.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CurrentProjection.unitBallLaw line 16
  2. def OAI.CurrentProjection.sphereLaw line 19
  3. lemma OAI.CurrentProjection.unitBallLaw_closedBall line 23
  4. lemma OAI.CurrentProjection.unitBallLaw_local line 35
  5. lemma OAI.CurrentProjection.unitBallLaw_support line 40
  6. instance OAI.CurrentProjection.unitBallLaw_probability line 46
  7. instance OAI.CurrentProjection.sphereLaw_probability line 54
  8. lemma OAI.CurrentProjection.sphereLaw_apply line 62
  9. lemma OAI.CurrentProjection.sphereLaw_cap_raw line 84
  10. lemma OAI.CurrentProjection.uniformSphere_growth line 120
  11. lemma OAI.CurrentProjection.dominatedSphere_growth line 142
  12. lemma OAI.CurrentProjection.extended_eq_inverse_rnDeriv line 153
  13. lemma OAI.CurrentProjection.labelLaw_ac_of_finite_extended line 168
  14. lemma OAI.CurrentProjection.measurable_swapped_extended line 187
  15. lemma OAI.CurrentProjection.ae_labelLaw_ac_of_growth line 194
  16. lemma OAI.CurrentProjection.volume_ae_cube_limit line 208
  17. lemma OAI.CurrentProjection.entropy_exp_bound line 229
  18. lemma OAI.CurrentProjection.lintegral_one_add_pow_le line 280