OAI/MeasureTheory/Falconer/Estimates/DescriptorTestBad.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Original-pair failure of the level-zero tests, before smoothing

  1. def OAI.Falconer.descriptorTestBad line 15
  2. theorem OAI.Falconer.descriptorTestBad_measurable line 20
  3. theorem OAI.Falconer.Regularization.uniform_source_test_bad_mass line 31