OAI/Analysis/LipschitzHilbert/Phase/AngularNormalization.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Choose the fixed enlargement used by the manuscript's angular cells. Enlarging the auxiliary angular width rescales the annulus and selector constants together and preserves their separation.

  1. theorem OAI.LipschitzHilbert.PacketRepresentation.exists_angular_normalization line 12
  2. theorem OAI.LipschitzHilbert.PacketRepresentation.rescaled_vertical_annulus line 36
  3. theorem OAI.LipschitzHilbert.PacketRepresentation.exists_uniform_lattice_multiplicity line 43