OAI/Analysis/LipschitzHilbert/Fourier/DyadicLineCountableTail.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Uniform tails for countably many actual maximal dyadic occurrences.

  1. theorem OAI.LipschitzHilbert.DyadicLineGrid.maximal_bad_countable_tail line 15