OAI/MeasureTheory/Falconer/Recursion/ProfileIncrementFrostman.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Turning a contact-interval profile inequality into actual conditional ball bounds

  1. theorem OAI.Falconer.Regularization.profileDrop_le_of_increment line 12
  2. theorem OAI.Falconer.Regularization.sourceClass_conditional_frostman_of_increment line 26