OAI/MeasureTheory/Falconer/Incidence/LeafMassBins.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Original leaf mass bins with the dimension-dependent cutoff

  1. def OAI.Falconer.Regularization.massBinCandidates line 14
  2. def OAI.Falconer.Regularization.leafMassBin line 18
  3. theorem OAI.Falconer.Regularization.massBinCandidates_nonempty line 21
  4. theorem OAI.Falconer.Regularization.leafMassBin_le line 26
  5. theorem OAI.Falconer.Regularization.leafMassBin_lower line 34
  6. theorem OAI.Falconer.Regularization.leafMassBin_upper line 41
  7. def OAI.Falconer.Regularization.leafBinEndpoint line 57
  8. theorem OAI.Falconer.Regularization.leafBinEndpoint_pos line 59
  9. theorem OAI.Falconer.Regularization.leaf_mass_bin_bounds line 62
  10. def OAI.Falconer.Regularization.sourceLeafLabel line 75
  11. theorem OAI.Falconer.Regularization.sourceLeafLabel_card_le line 78
  12. theorem OAI.Falconer.Regularization.retained_leaf_mass_bin_bounds line 89