OAI/MeasureTheory/Falconer/Estimates/ScalarGroupedTreeGain.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Iterating the grouped porous gain on the original cluster tree. The gain depends on selected local group sizes, not total branching.

  1. theorem OAI.Falconer.ScalarSeparatedTree.grouped_projection_log_gain line 11
  2. theorem OAI.Falconer.ScalarSeparatedTree.grouped_projection_gain line 69