FourierCompression.lean`

13 declarations, 0 contain sorry, 0 declared as axioms

Fourier transport of the scalar compression of the modular core. This produces a unital completely positive contraction commuting with every character multiplier. It does not postulate a core trace.

def OAI.WeakPureInfiniteness.modularFourierInclusion line 19
Source documentation
The scalar inclusion in Fourier coordinates is an actual Hilbert-space isometry, rather than a formal change of spectral variables.
```
def modularFourierInclusion : Lp ℂ 2 (volume : Measure ℝ) →ₗᵢ[ℂ]
    Lp H 2 (volume : Measure ℝ) :=
…
```
lemma OAI.WeakPureInfiniteness.modularFourierInclusion_apply line 24
lemma OAI.WeakPureInfiniteness.modularFourierInclusion_adjoint line 27

def OAI.WeakPureInfiniteness.modularFourierCompression line 37

Source documentation

Scalar compression after Fourier diagonalization.

def modularFourierCompression : (Lp H 2 (volume : Measure ℝ) →L[ℂ]
    Lp H 2 (volume : Measure ℝ)) →L[ℂ]
      (Lp ℂ 2 (volume : Measure ℝ) →L[ℂ] Lp ℂ 2 (volume : Measure ℝ)) :=
…

lemma OAI.WeakPureInfiniteness.modularFourierCompression_apply line 42
lemma OAI.WeakPureInfiniteness.modularFourierCompression_conjugate line 49
theorem OAI.WeakPureInfiniteness.modularFourierCompression_cp line 57
theorem OAI.WeakPureInfiniteness.modularFourierCompression_contractive line 60
theorem OAI.WeakPureInfiniteness.modularFourierCompression_one line 69
lemma OAI.WeakPureInfiniteness.fourierConjugation_translation line 72
theorem OAI.WeakPureInfiniteness.modularFourierCompression_commutes line 86
Source documentation
The Fourier compression of every core element commutes with every character multiplier, including on the full von Neumann closure.
```
theorem modularFourierCompression_commutes (T : Lp H 2 (volume : Measure ℝ) →L[ℂ]
    Lp H 2 (volume : Measure ℝ))
    (hT : T ∈ modularCrossedProduct (volume : Measure ℝ) S) (r : ℝ) :
    Commute (modularFourierCompression S T)
      (modularDualUnitary (H := ℂ) (volume : Measure ℝ) r :
…
```
Mentions: OAI.WeakPureInfiniteness.modularCrossedProduct, OAI.WeakPureInfiniteness.modularFourierCompression, OAI.WeakPureInfiniteness.modularDualUnitary
lemma OAI.WeakPureInfiniteness.modularScalarCompression_coefficient_translate line 106
lemma OAI.WeakPureInfiniteness.modularFourierCompression_coefficient_translate line 127
Source documentation
The Fourier coefficient of a crossed-product monomial is the original vector-state coefficient times the corresponding character multiplier.
```
lemma modularFourierCompression_coefficient_translate (T : H →L[ℂ] H) (s : ℝ) :
    modularFourierCompression S
      (modularLpRepresentation volume S.D T *
        (modularLpTranslateEquiv (H := H) volume s :
…
```
Mentions: OAI.WeakPureInfiniteness.modularFourierCompression, OAI.WeakPureInfiniteness.modularLpRepresentation, OAI.WeakPureInfiniteness.modularLpTranslateEquiv