FrequencyNest.lean`

11 declarations, 0 contain sorry, 0 declared as axioms

The concrete Fourier frequency projections

The Fourier transform uses mathlib's exp(-2*pi*i*t*ξ) convention. Thus the cut of the generator -i d/dt at a is the Fourier multiplier of Ioi (a/(2*pi)). The upper frequency cuts decrease with a; negating the index gives the increasing chain used by the nest distance theorem.

def OAI.KadisonKastler.regularIndicatorProjection line 24
Source documentation
Multiplication by the indicator of a measurable subset of the line.
```
def regularIndicatorProjection (s : Set ℝ) (hs : MeasurableSet s) :
    RegularCoreHilbert H →L[ℂ] RegularCoreHilbert H :=
…
```
Mentions: OAI.KadisonKastler.RegularCoreHilbert
theorem OAI.KadisonKastler.regularIndicatorProjection_apply_ae line 32
theorem OAI.KadisonKastler.regularIndicatorProjection_mul_of_subset line 49
theorem OAI.KadisonKastler.regularIndicatorProjection_isStarProjection line 68
def OAI.KadisonKastler.regularFrequencyProjection line 83
Source documentation
The positive-frequency cut of the actual L² Fourier transform.
```
def regularFrequencyProjection (a : ℝ) :
    RegularCoreHilbert H →L[ℂ] RegularCoreHilbert H :=
…
```
Mentions: OAI.KadisonKastler.RegularCoreHilbert
theorem OAI.KadisonKastler.regularFrequencyProjection_isStarProjection line 88
theorem OAI.KadisonKastler.regularFrequencyProjection_apply_fourier line 94
theorem OAI.KadisonKastler.regularFrequencyProjection_mul line 105
Source documentation
Upper frequency cuts decrease as the threshold increases.
```
theorem regularFrequencyProjection_mul (a b : ℝ) (hab : a ≤ b) :
    regularFrequencyProjection (H := H) b * regularFrequencyProjection a =
…
```
Mentions: OAI.KadisonKastler.regularFrequencyProjection
def OAI.KadisonKastler.regularFrequencyNest line 115
Source documentation
Reindexing the upper cuts produces an increasing real-indexed nest.
```
def regularFrequencyNest (a : ℝ) :
    RegularCoreHilbert H →L[ℂ] RegularCoreHilbert H := regularFrequencyProjection (-a)
```
Mentions: OAI.KadisonKastler.RegularCoreHilbert, OAI.KadisonKastler.regularFrequencyProjection
theorem OAI.KadisonKastler.regularFrequencyNest_isStarProjection line 118
theorem OAI.KadisonKastler.regularFrequencyNest_mono line 122