OAI/MeasureTheory/Falconer/Measures/ScalarPruningPreservation.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Pruning nonempty collections of whole children preserves every coarser prefix and every finer branch above an occupied retained node.

  1. theorem OAI.Falconer.Regularization.prefixChildren_eq_filter line 9
  2. theorem OAI.Falconer.Regularization.scalarPruneLeaves_lift line 24
  3. theorem OAI.Falconer.Regularization.scalarPruneLeaves_upper_prefixes line 38
  4. theorem OAI.Falconer.Regularization.scalarPruneLeaves_upper_children line 50
  5. theorem OAI.Falconer.Regularization.scalarPruneLeaves_nonempty line 58
  6. theorem OAI.Falconer.Regularization.scalar_single_child_choice line 66
  7. theorem OAI.Falconer.Regularization.prefixFiber_total_card line 79