OAI/Analysis/LipschitzHilbert/Phase/SourceAngularGridRebase.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Dropping dyadic packet scales rebases the same angular grid. The alternating shift changes the grid sign at odd starting levels.

  1. theorem OAI.LipschitzHilbert.scaledAngularCell_eq_Ico line 13
  2. theorem OAI.LipschitzHilbert.angular_shift_rebase line 20
  3. theorem OAI.LipschitzHilbert.angular_left_rebase line 25
  4. theorem OAI.LipschitzHilbert.scaledAngularCell_rebase line 32
  5. theorem OAI.LipschitzHilbert.SourceLabeledLattice.dropScales_angularCell line 44