OAI/MeasureTheory/Falconer/Estimates/CellClassifier.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Countable Borel labels for the actual endpoint masks

Every descriptor anchored above a fixed depth is constant on that depth's cells. The label also records points outside the original cube.

  1. instance OAI.Falconer.cellLabelMeasurableSpace line 18
  2. instance OAI.Falconer.cellLabelMeasurableSingletonClass line 20
  3. def OAI.Falconer.cellLabel line 24
  4. theorem OAI.Falconer.cellLabel_eq_some_iff line 28
  5. theorem OAI.Falconer.cellLabel_eq_none_iff line 52
  6. theorem OAI.Falconer.cellLabel_measurable line 56
  7. def OAI.Falconer.descriptorClassProduct line 79
  8. theorem OAI.Falconer.descriptorClassProduct_contDiff line 87
  9. theorem OAI.Falconer.descriptorAmbientProduct_eq_class line 97