OAI/MeasureTheory/Falconer/Estimates/AllDimensionalRegularizationLabels.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

Upward regularization labels in arbitrary dimension

The label-preservation argument applies to all-dimensional dyadic paths. Each extension retains or removes a whole previous child group.

  1. abbrev OAI.Falconer.Regularization.CellPath line 15
  2. def OAI.Falconer.Regularization.labeledChildren line 18
  3. def OAI.Falconer.Regularization.extendLabel line 23
  4. def OAI.Falconer.Regularization.upwardLabels line 27
  5. theorem OAI.Falconer.Regularization.take_eq_of_take_eq line 32
  6. theorem OAI.Falconer.Regularization.labeledChildren_eq line 37
  7. theorem OAI.Falconer.Regularization.labeledChildren_nonempty line 43
  8. theorem OAI.Falconer.Regularization.extendLabel_old line 49
  9. theorem OAI.Falconer.Regularization.extendLabel_local line 53
  10. theorem OAI.Falconer.Regularization.upwardLabels_old line 61
  11. theorem OAI.Falconer.Regularization.upwardLabels_local line 68
  12. theorem OAI.Falconer.Regularization.final_labeledChildren_eq line 78
  13. theorem OAI.Falconer.Regularization.final_child_count_bin line 94
  14. theorem OAI.Falconer.Regularization.final_child_count_bounds line 105