OAI/Analysis/LipschitzHilbert/Fourier/DyadicLineRootCount.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The count in one grid agrees on a root with the count of its selected descendants.

  1. abbrev OAI.LipschitzHilbert.DyadicLineGrid.GridOccurrence line 17
  2. def OAI.LipschitzHilbert.DyadicLineGrid.maximalCell line 19
  3. def OAI.LipschitzHilbert.DyadicLineGrid.gridCount line 23
  4. def OAI.LipschitzHilbert.DyadicLineGrid.RootOccurrence line 26
  5. theorem OAI.LipschitzHilbert.DyadicLineGrid.selectedCount_eq_gridCounts line 30
  6. theorem OAI.LipschitzHilbert.DyadicLineGrid.gridCount_eq_rootCount line 55
  7. theorem OAI.LipschitzHilbert.DyadicLineGrid.gridCount_root_tail line 80