OAI/MeasureTheory/Falconer/Incidence/BlockChordRegularity.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The actual block classes inherit regularity from each selected profile interval. All losses are retained in the exponent.

  1. theorem OAI.Falconer.Regularization.blockClass_chord_frostman line 11
  2. theorem OAI.Falconer.Regularization.blockClass_chord_covering line 40