FrequencySupport.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Frequency-cut ranges as almost-everywhere support conditions

theorem OAI.KadisonKastler.regularFrequencyProjection_fixed_iff line 19
Source documentation
Being fixed by the actual frequency projection is exactly the usual almost-everywhere support condition on the L² Fourier transform.
```
theorem regularFrequencyProjection_fixed_iff (a : ℝ) (f : RegularCoreHilbert H) :
    regularFrequencyProjection a f = f ↔
      ∀ᵐ t : ℝ, t ≤ a / (2 * Real.pi) → (𝓕 f : RegularCoreHilbert H) t = 0 := by
…
```
Mentions: OAI.KadisonKastler.RegularCoreHilbert, OAI.KadisonKastler.regularFrequencyProjection

theorem OAI.KadisonKastler.frequency_support_of_preserves_nest line 42

Source documentation

A nest-preserving operator preserves every positive-frequency subspace with the corresponding shifted threshold.

theorem frequency_support_of_preserves_nest
    (T : RegularCoreHilbert H →L[ℂ] RegularCoreHilbert H)
    (hT : PreservesProjectionNest regularFrequencyNest T)
    (a : ℝ) (f : RegularCoreHilbert H)
    (hf : ∀ᵐ t : ℝ, t ≤ a / (2 * Real.pi) → (𝓕 f : RegularCoreHilbert H) t = 0) :
    ∀ᵐ t : ℝ, t ≤ a / (2 * Real.pi) → (𝓕 (T f) : RegularCoreHilbert H) t = 0 := by
…

Mentions: OAI.KadisonKastler.RegularCoreHilbert, OAI.KadisonKastler.PreservesProjectionNest, OAI.KadisonKastler.regularFrequencyNest