NormalizedBandSymbol.lean`

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

The normalized coordinates and support geometry in the packet representation of the annular band multiplier (§2).

def OAI.LipschitzHilbert.PacketRepresentation.symbolX line 13
def OAI.LipschitzHilbert.PacketRepresentation.symbolY line 14
def OAI.LipschitzHilbert.PacketRepresentation.symbolU line 15
theorem OAI.LipschitzHilbert.PacketRepresentation.normalized_symbol_identity line 17
theorem OAI.LipschitzHilbert.PacketRepresentation.normalized_vertical_identity line 23
theorem OAI.LipschitzHilbert.PacketRepresentation.normalized_selector_lower line 31
Source documentation
The annular multiplier and the narrow horizontal frequency support force the normalized selector away from zero, uniformly in the scales.
```
theorem normalized_selector_lower (X V U c C : ℝ)
    (_hc : 0<c) (hC : 0<C) (hV0 : 0≤V) (hV : V≤C)
    (hX : |X|≤c/4) (hAnnulus : c≤|X+V*U|) :
    3*c/(4*C)≤|U| := by
…
```
theorem OAI.LipschitzHilbert.PacketRepresentation.normalized_selector_upper line 43
Source documentation
The positive vertical annulus also bounds the normalized selector above; no scale or bin count enters the bound.
```
theorem normalized_selector_upper (X V U c C M : ℝ)
    (hc : 0<c) (hV : c≤V) (hX : |X|≤C/4) (hAnnulus : |X+V*U|≤M) :
    |U|≤(M+C/4)/c := by
…
```
theorem OAI.LipschitzHilbert.PacketRepresentation.bounded_contributing_slope line 57
theorem OAI.LipschitzHilbert.PacketRepresentation.frequency_slope_margin line 71
Source documentation
The wave slopes stay in a fixed multiple of the angular scale around the lattice label.
```
theorem frequency_slope_margin (l w xi eta theta c C : ℝ)
    (hl : 0<l) (hw : 0<w) (hc : 0<c) (hC : 0≤C)
    (hV : c≤w*eta) (hX : |symbolX l xi eta theta|≤C) :
    |(-xi/eta)-theta|≤(C/c)*(w/l) := by
…
```
Mentions: OAI.LipschitzHilbert.PacketRepresentation.symbolX