OAI/MeasureTheory/Falconer/Measures/ScalarTaggedPruning.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Selecting a common geometric tag while retaining whole child fibers. The loss is the number of tags times the local pruning loss.

  1. theorem OAI.Falconer.scalar_tagged_child_pruning line 9
  2. theorem OAI.Falconer.scalar_equal_fiber_card line 43