OAI/MeasureTheory/Falconer/Estimates/RetainedPairs.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Exact decomposition into the suffix cells having a witness

Only actual original-law restrictions occur. Empty intersections with the parent's good-pair set contribute zero, so retaining witnessed cells is an exact identity, before their full cell measures are used for comparison.

  1. def OAI.Falconer.testedCellPair line 18
  2. def OAI.Falconer.testedCellDistance line 22
  3. instance OAI.Falconer.testedCellPair_finite line 26
  4. instance OAI.Falconer.testedCellDistance_finite line 32
  5. def OAI.Falconer.retainedCellPairs line 38
  6. theorem OAI.Falconer.testedCellPair_eq_zero line 44
  7. theorem OAI.Falconer.testedCellPair_split line 57
  8. theorem OAI.Falconer.testedCellDistance_split line 78
  9. theorem OAI.Falconer.testedCellDistance_le line 88
  10. theorem OAI.Falconer.full_retained_distance_le line 93