OAI/MeasureTheory/Falconer/Slicing/SlicePruningRatios.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Cancellation of the dyadic weights in the simultaneous pruning costs

  1. theorem OAI.Falconer.pruning_weight_cancel line 11
  2. theorem OAI.Falconer.pruning_weighted_sum line 19
  3. theorem OAI.Falconer.pruning_weighted_sum_le line 25
  4. theorem OAI.Falconer.pruning_real_weighted_sum line 32