OAI/RingTheory/BassTrace/VolumeBounds.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

Scalar estimates for iterated volume growth and high-dimensional ball bounds.

  1. def OAI.BassTrace.Sparse.dividedPower line 17
  2. def OAI.BassTrace.Sparse.slicingError line 20
  3. lemma OAI.BassTrace.Sparse.continuous_dividedPower line 23
  4. lemma OAI.BassTrace.Sparse.continuous_slicingError line 27
  5. lemma OAI.BassTrace.Sparse.dividedPower_zero line 31
  6. lemma OAI.BassTrace.Sparse.slicingError_zero line 34
  7. lemma OAI.BassTrace.Sparse.dividedPower_one line 37
  8. lemma OAI.BassTrace.Sparse.integral_dividedPower line 40
  9. lemma OAI.BassTrace.Sparse.integral_slicingError line 47
  10. lemma OAI.BassTrace.Sparse.integral_slicing_lower line 56
  11. theorem OAI.BassTrace.Sparse.iterated_slicing_lower_bound line 70
  12. theorem OAI.BassTrace.Sparse.absorb_nonempty_probability line 98
  13. def OAI.BassTrace.Sparse.volumeThreshold line 111
  14. lemma OAI.BassTrace.Sparse.square_succ_le_two_pow line 113
  15. lemma OAI.BassTrace.Sparse.real_sqrt_lt_nat_sqrt_succ line 121
  16. lemma OAI.BassTrace.Sparse.floor_radius_sqrt_bound line 129
  17. theorem OAI.BassTrace.Sparse.exponential_volume_margin line 140
  18. theorem OAI.BassTrace.Sparse.strict_volume_margin line 167
  19. lemma OAI.BassTrace.Sparse.GraphGeometry.sourceTop_connected line 205
  20. lemma OAI.BassTrace.Sparse.GraphGeometry.localOriginalArea_top_le line 212
  21. lemma OAI.BassTrace.Sparse.GraphGeometry.localTops_card_le line 224
  22. lemma OAI.BassTrace.Sparse.GraphGeometry.ballMass_top_bound line 255
  23. lemma OAI.BassTrace.Sparse.real_integral_of_mass_bound line 294
  24. theorem OAI.BassTrace.Sparse.iterated_mass_bound line 307
  25. def OAI.BassTrace.Sparse.GraphGeometry.ballVolumeBound line 367
  26. theorem OAI.BassTrace.Sparse.GraphGeometry.iterated_ball_volume line 372