OAI/MeasureTheory/Falconer/Estimates/PlanarTreeUniformization.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

A logarithmic-cost planar block regularization. The existing exact prefix classes preserve the local child counts; only the sharper block-width count and the cardinality selection are needed here.

  1. theorem OAI.Falconer.Regularization.planar_blockLabel_card_le line 12
  2. theorem OAI.Falconer.Regularization.exists_large_planar_block_class line 28
  3. theorem OAI.Falconer.Regularization.planar_block_uniformization line 51