OAI/MeasureTheory/Falconer/Measures/ScalarSubsetMass.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Relative ball bounds and projection covers under the actual scalar pruning. The sole cost is the ratio of the numbers of retained leaves.

  1. theorem OAI.Falconer.scalarBallMass_mono line 10
  2. theorem OAI.Falconer.scalar_projection_cover_mono line 15
  3. theorem OAI.Falconer.Regularization.scalar_leaf_center_card line 23
  4. theorem OAI.Falconer.Regularization.scalar_pruned_ball_bound line 28