OAI/MeasureTheory/Falconer/Radial/RadialProfileProduct.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Quantitative telescoping for the constructed regularization profile

  1. theorem OAI.Falconer.Regularization.sourceProfile_depth_upper line 14
  2. theorem OAI.Falconer.Regularization.radial_profile_product_bound line 23