FrequencyCovariance.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Characters permute the concrete frequency nest

theorem OAI.KadisonKastler.regularFrequencyProjection_character_intertwine line 20
Source documentation
The sign and the 2*pi normalization in the frequency shift.
```
theorem regularFrequencyProjection_character_intertwine (a s : ℝ) :
    regularFrequencyProjection (H := H) a *
…
```
Mentions: OAI.KadisonKastler.regularFrequencyProjection
theorem OAI.KadisonKastler.regularFrequencyProjection_character_conj line 62
Source documentation
Conjugation by a character sends one upper-frequency cut to another.
```
theorem regularFrequencyProjection_character_conj (a s : ℝ) :
    unitaryConj (regularCharacterUnitary (H := H) (2 * Real.pi * s))
…
```
Mentions: OAI.KadisonKastler.unitaryConj, OAI.KadisonKastler.regularCharacterUnitary
theorem OAI.KadisonKastler.regularFrequencyNest_character_perm line 73
Source documentation
The constructed increasing nest meets the character-permutation hypothesis of invariant nest averaging, for every real character.
```
theorem regularFrequencyNest_character_perm (a b : ℝ) :
    ∃ c, regularFrequencyNest (H := H) a =
…
```
Mentions: OAI.KadisonKastler.regularFrequencyNest

theorem OAI.KadisonKastler.exists_frequency_nest_multiplier line 86

Source documentation

Actual Fourier cuts can now be used directly in the multiplier construction; no abstract projection-chain or permutation input remains.

theorem exists_frequency_nest_multiplier [TopologicalSpace.SeparableSpace H]
    (hNest : PublishedRealNestDistance.{u})
    (hSpectral : PublishedRealSpectralCommutant.{u})
    (hDiagonal : PublishedRealDiagonalDecomposition.{u})
    (F : ℝ → H →L[ℂ] H) (hF : ∀ x, AEStronglyMeasurable (fun t => F t x) volume)
    {C : ℝ} (hC0 : 0 ≤ C) (hC : ∀ᵐ t, ‖F t‖ ≤ C)
    {δ : ℝ} (hδ : 0 < δ)
    (hdefect : ∀ a, ‖(1 - regularFrequencyNest a) *
      regularFieldOperator volume F hF C hC * regularFrequencyNest a‖ ≤ δ) :
    ∃ (B : ℝ → H →L[ℂ] H) (S : RegularCoreHilbert H →L[ℂ] RegularCoreHilbert H),
      PreservesProjectionNest regularFrequencyNest S ∧
      (∀ x, AEStronglyMeasurable (fun t => B t x) volume) ∧
…

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