OAI/Analysis/LipschitzHilbert/Fourier/GlobalAnnularVariation.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Exhaust the line by growing roots while keeping the comparison mesh fixed. The annular variation constant is independent of the root size.

  1. def OAI.LipschitzHilbert.expandingGrid line 15
  2. theorem OAI.LipschitzHilbert.expandingGrid_root line 23
  3. theorem OAI.LipschitzHilbert.expandingGrid_mesh line 29
  4. theorem OAI.LipschitzHilbert.expandingGrid_mono line 34
  5. theorem OAI.LipschitzHilbert.expandingGrid_cover line 41
  6. theorem OAI.LipschitzHilbert.scalar_annular_variation line 49