OAI/MeasureTheory/Falconer/Recursion/LeafMassBins.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PlanarFalconer.massBinCandidates line 11
  2. def OAI.PlanarFalconer.leafMassBin line 15
  3. theorem OAI.PlanarFalconer.massBinCandidates_nonempty line 18
  4. theorem OAI.PlanarFalconer.leafMassBin_le line 23
  5. theorem OAI.PlanarFalconer.leafMassBin_lower line 31
  6. theorem OAI.PlanarFalconer.leafMassBin_upper line 38
  7. def OAI.PlanarFalconer.leafBinEndpoint line 54
  8. theorem OAI.PlanarFalconer.leafBinEndpoint_pos line 56
  9. theorem OAI.PlanarFalconer.leaf_mass_bin_bounds line 59
  10. def OAI.PlanarFalconer.sourceLeafLabel line 72
  11. theorem OAI.PlanarFalconer.sourceLeafLabel_card_le line 75
  12. theorem OAI.PlanarFalconer.retained_leaf_mass_bin_bounds line 86