OAI/MeasureTheory/Falconer/Incidence/BlockRegularization.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

All-dimensional block regularization

The upward labels preserve complete child groups at every selected depth. Count bins cost d*N+1 possibilities and leaf mass bins cost (d+2)*N+1.

  1. abbrev OAI.Falconer.Regularization.blockDepth line 16
  2. def OAI.Falconer.Regularization.blockLabel line 18
  3. theorem OAI.Falconer.Regularization.blockDepth_antitone line 23
  4. theorem OAI.Falconer.Regularization.blockDepth_gap line 27
  5. theorem OAI.Falconer.Regularization.blockDepth_terminal line 32
  6. theorem OAI.Falconer.Regularization.blockLabel_old line 39
  7. theorem OAI.Falconer.Regularization.blockLabel_local line 53
  8. theorem OAI.Falconer.Regularization.block_final_children line 71
  9. theorem OAI.Falconer.Regularization.block_final_bin_eq line 88
  10. theorem OAI.Falconer.Regularization.blockLabel_card_le line 98
  11. def OAI.Falconer.Regularization.regularizationLeaves line 115
  12. def OAI.Falconer.Regularization.regularizationLabel line 118
  13. theorem OAI.Falconer.Regularization.regularization_label_count line 122
  14. theorem OAI.Falconer.Regularization.regularization_label_mass_bin line 130