OAI/MeasureTheory/Falconer/Estimates/ComparableBands.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Borel dyadic bands for the two original comparable displacements

The finite cover has the exact constants used by the far-cell partner geometry. Nonnegative integration only needs a cover, so no arbitrary choice of a depth or additional measurability hypothesis is introduced.

  1. def OAI.Falconer.comparableLengthBand line 16
  2. theorem OAI.Falconer.comparableLengthBand_measurable line 23
  3. def OAI.Falconer.comparableFarRegion line 34
  4. theorem OAI.Falconer.comparableFarRegion_measurable line 42
  5. theorem OAI.Falconer.comparableFarRegion_covered line 54
  6. theorem OAI.Falconer.comparableLengthBand_dist_lower line 61
  7. theorem OAI.Falconer.descendant_common_band_scale line 72
  8. theorem OAI.Falconer.comparableLengthBand_descendants line 78
  9. theorem OAI.Falconer.lintegral_comparable_bands_le line 90