OAI/Analysis/LipschitzHilbert/Fourier/ShortLineVariation.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Summing the actual short-scale packet boxes on one reference interval.

  1. theorem OAI.LipschitzHilbert.short_line_variation line 17