RescaledAnnularSymbol.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The fixed angular enlargement is an exact change of normalized coordinates. The annular cutoff and the compact master symbol are still one on every contributing frequency.

theorem OAI.LipschitzHilbert.PacketRepresentation.rescaled_symbol_coordinates line 11
theorem OAI.LipschitzHilbert.PacketRepresentation.rescaled_localized_symbol_eq line 20
theorem OAI.LipschitzHilbert.PacketRepresentation.vertical_annulus_from_window line 56
Source documentation
A vertical frequency window inherits the original annulus from its center and width, with the exact endpoint allowance.
```
theorem vertical_annulus_from_window (w W center eta B c C : ℝ)
    (hw : 0<w) (hW : 0<W)
    (hlo : c+B*(w/W)≤w*center) (hhi : w*center+B*(w/W)≤C)
    (hY : |symbolY W eta center|≤B) : c≤w*eta ∧ w*eta≤C := by
…
```
Mentions: OAI.LipschitzHilbert.PacketRepresentation.symbolY