OAI/MeasureTheory/Falconer/Estimates/ScalarPathNodes.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Translating actual scalar prefix nodes into their distinct centers. This is the coordinate bridge to the separated-tree projection estimate.

  1. def OAI.Falconer.Regularization.scalarPrefixPath line 10
  2. def OAI.Falconer.Regularization.scalarPrefixPoints line 13
  3. def OAI.Falconer.Regularization.scalarPrefixChildren line 16
  4. theorem OAI.Falconer.Regularization.scalar_prefix_path_mem line 19
  5. theorem OAI.Falconer.Regularization.scalar_prefix_path_center line 25
  6. theorem OAI.Falconer.Regularization.scalar_prefix_path_eq line 31
  7. theorem OAI.Falconer.Regularization.scalar_prefix_points_eq line 41
  8. theorem OAI.Falconer.Regularization.scalar_prefix_children_eq line 48
  9. theorem OAI.Falconer.Regularization.prefixFiber_children_union line 55
  10. theorem OAI.Falconer.Regularization.scalar_prefix_points_children line 68
  11. theorem OAI.Falconer.Regularization.scalar_prefix_points_leaf line 92
  12. theorem OAI.Falconer.Regularization.ScalarBranchingLevel.separated line 105