OAI/MeasureTheory/Falconer/Estimates/PreparedPair.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Original starting pairs with the complete finite-filter interface

The pair and its Frostman gap are fixed before the coarse loss is chosen. All cap bounds and partitions concern the original marginal laws.

  1. structure OAI.Falconer.PreparedOriginalPair line 15
  2. theorem OAI.Falconer.even_prepared_original_pair line 31