OAI/Analysis/LipschitzHilbert/Fourier/DyadicLineFiniteTail.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The exponential count bound for actual finite maximal dyadic families.

  1. theorem OAI.LipschitzHilbert.DyadicLineGrid.maximal_bad_finite_tail line 17