OAI/MeasureTheory/Falconer/Estimates/ScalarBunchingTotals.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Total length, discarded weight and retained weight of the actual greedy bunching ledger. The loss and gain use the same covered terminal interval.

  1. theorem OAI.Falconer.ScalarBunchChain.weight_partition line 9
  2. theorem OAI.Falconer.ScalarBunchChain.total_trim line 23
  3. theorem OAI.Falconer.ScalarBunchChain.total_loss line 38
  4. theorem OAI.Falconer.ScalarBunchChain.total_retained line 57
  5. theorem OAI.Falconer.scalar_bunching_total_weights line 76