OAI/MeasureTheory/Falconer/Measures/PairCorePruning.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Core restrictions and density pruning preserve the original pair-cost ledger

  1. theorem OAI.Falconer.product_core_compl_null line 12
  2. theorem OAI.Falconer.pair_core_restriction_cost line 25
  3. theorem OAI.Falconer.density_pruned_pair_cost line 31