OAI/Analysis/LipschitzHilbert/Estimates/PopularTopCountPowers.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The count exponent C_as + 3 max(k,C_as) in the manuscript follows from the actual witness density and a common polynomial base dilation.

  1. theorem OAI.LipschitzHilbert.popular_top_count_powers line 13