OAI/MeasureTheory/Falconer/Estimates/PrefixCounting.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

All-dimensional prefix counts for regularized original measures

  1. def OAI.Falconer.Regularization.prefixFiber line 12
  2. def OAI.Falconer.Regularization.prefixChildren line 16
  3. theorem OAI.Falconer.Regularization.prefixFiber_zero line 19
  4. theorem OAI.Falconer.Regularization.prefixFiber_leaf line 23
  5. theorem OAI.Falconer.Regularization.prefixFiber_nonempty line 36
  6. theorem OAI.Falconer.Regularization.prefixChildren_mem_image line 42
  7. theorem OAI.Falconer.Regularization.prefixFiber_parent_filter line 48
  8. theorem OAI.Falconer.Regularization.prefixFiber_card_sum line 61
  9. theorem OAI.Falconer.Regularization.prefixFiber_count_bounds line 71
  10. theorem OAI.Falconer.Regularization.prefixChildren_class_eq line 89