OAI/MeasureTheory/Falconer/Estimates/ScalarForwardRegularization.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The initial scalar regularization in increasing geometric depth. Exact full blocks are the form used in the porous/nonporous dichotomy.

  1. theorem OAI.Falconer.Regularization.blockDepth_product line 9
  2. theorem OAI.Falconer.Regularization.scalar_forward_regularization line 14