OAI/MeasureTheory/Falconer/Estimates/ScalarTreeAmplification.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Finite iteration of the actual weighted child inequalities. The coefficient is shared by all levels and all branches.

  1. theorem OAI.Falconer.scalar_tree_log_growth line 9
  2. theorem OAI.Falconer.scalar_tree_average_growth line 46