OAI/MeasureTheory/Falconer/Incidence/RadialBlockDepths.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

A dyadic block schedule with two initial blocks reserved for freezing

  1. def OAI.Falconer.radialBlockSize line 10
  2. def OAI.Falconer.radialBlockDepth line 12
  3. theorem OAI.Falconer.radialBlockSize_total line 15
  4. theorem OAI.Falconer.radialBlockDepth_le line 18
  5. theorem OAI.Falconer.radialBlockDepth_final line 27
  6. theorem OAI.Falconer.radialBlockDepth_step line 33
  7. theorem OAI.Falconer.radialBlockDepth_mono line 38
  8. theorem OAI.Falconer.radialBlockDepth_two_blocks line 43
  9. theorem OAI.Falconer.radialBlockDepth_initial_upper line 51