OAI/MeasureTheory/Falconer/Estimates/ScalarBunchTree.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The realized ledger, ordered from fine to coarse scales, is the separated tree consumed by the porous projection estimate.

  1. def OAI.Falconer.scalarBunchBoundary line 10
  2. theorem OAI.Falconer.ScalarBunchChain.boundary_zero line 13
  3. theorem OAI.Falconer.ScalarBunchChain.boundary_edges line 17
  4. theorem OAI.Falconer.ScalarBunchChain.boundary_bounds line 35
  5. theorem OAI.Falconer.scalarBunchValue_at line 46
  6. def OAI.Falconer.Regularization.scalarBunchSeparatedTreeOfLeaves line 54
  7. def OAI.Falconer.Regularization.scalarBunchSeparatedTree line 87