OAI/MeasureTheory/Falconer/Estimates/RegularizationSubpower.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PlanarFalconer.regularization_fixed_count_bound line 11
2. theorem OAI.PlanarFalconer.fixed_polynomial_subpower line 24
3. theorem OAI.PlanarFalconer.regularization_class_count_subpower line 45
4. theorem OAI.PlanarFalconer.thin_leaf_loss_identity line 58