OAI/Probability/GaussianReplacement/Geometry.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CurrentProjection.inverse_pow_dyadic_majorant line 15
  2. lemma OAI.CurrentProjection.dyadic_power_cancel line 50
  3. theorem OAI.CurrentProjection.inverse_moment_of_tube_bound line 65
  4. def OAI.CurrentProjection.HasLocalMassBound line 116
  5. theorem OAI.CurrentProjection.HasLocalMassBound.any_center line 122
  6. theorem OAI.CurrentProjection.card_le_volume_ratio line 138
  7. theorem OAI.CurrentProjection.exists_net_of_finite_packing_bound line 188
  8. theorem OAI.CurrentProjection.exists_unit_ball_net line 240
  9. theorem OAI.CurrentProjection.exists_affine_tube_cover line 272
  10. theorem OAI.CurrentProjection.HasLocalMassBound.affine_tube line 305
  11. lemma OAI.CurrentProjection.tube_radius_factors line 336
  12. theorem OAI.CurrentProjection.HasLocalMassBound.affine_tube_pow line 344
  13. theorem OAI.CurrentProjection.HasLocalMassBound.affine_inverse_moment line 361
  14. theorem OAI.CurrentProjection.HasLocalMassBound.affine_null line 375