OAI/MeasureTheory/Falconer/Measures/FarOriginalSupport.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Far-label elimination under a positive original-law bound

  1. def OAI.Falconer.farDisplacementRegion line 13
  2. theorem OAI.Falconer.farDisplacementRegion_measurable line 19
  3. theorem OAI.Falconer.sum_pair_reassociate line 26
  4. theorem OAI.Falconer.originalFourPoint_lintegral_rows line 35
  5. theorem OAI.Falconer.fourPointChildMeasure_far_support line 48
  6. theorem OAI.Falconer.originalFourPoint_far_rows_le line 114