PhaseQuotient.lean`

13 declarations, 0 contain sorry, 0 declared as axioms

Phase coefficients in a tracial sequence quotient

The multiset coefficients are finite noncommutative polynomials. Their bounded-sequence versions therefore descend exactly to the coefficients of the constant partition and the quotient unitary. The free-word estimate therefore applies to those quotient coefficients.

theorem OAI.KadisonKastler.map_positivePhaseCoefficient line 26

Source documentation

Positive phase coefficients commute with star algebra homomorphisms.

theorem map_positivePhaseCoefficient (φ : A →⋆ₐ[ℂ] B) (e : ι → A) (w : A)
    (r : ℕ) (s : Sym ι r) :
    φ (positivePhaseCoefficient e w r s) =
      positivePhaseCoefficient (fun a => φ (e a)) (φ w) r s := by
…

Mentions: OAI.KadisonKastler.positivePhaseCoefficient

theorem OAI.KadisonKastler.map_negativePhaseCoefficient line 37

Source documentation

Negative phase coefficients have the same functoriality.

theorem map_negativePhaseCoefficient (φ : A →⋆ₐ[ℂ] B) (e : ι → A) (w : A)
    (r : ℕ) (s : Sym ι r) :
    φ (negativePhaseCoefficient e w r s) =
      negativePhaseCoefficient (fun a => φ (e a)) (φ w) r s := by
…

Mentions: OAI.KadisonKastler.negativePhaseCoefficient

def OAI.KadisonKastler.positivePhaseCoefficientSequence line 44
Source documentation
The actual positive coefficient bounded sequence.
```
def positivePhaseCoefficientSequence (e : ι → A) (w : BoundedSequence A)
    (r : ℕ) (s : Sym ι r) : BoundedSequence A :=
…
```
Mentions: OAI.KadisonKastler.BoundedSequence
def OAI.KadisonKastler.negativePhaseCoefficientSequence line 49
Source documentation
The actual negative coefficient bounded sequence.
```
def negativePhaseCoefficientSequence (e : ι → A) (w : BoundedSequence A)
    (r : ℕ) (s : Sym ι r) : BoundedSequence A :=
…
```
Mentions: OAI.KadisonKastler.BoundedSequence
theorem OAI.KadisonKastler.positivePhaseCoefficientSequence_apply line 54
theorem OAI.KadisonKastler.negativePhaseCoefficientSequence_apply line 61
theorem OAI.KadisonKastler.quotient_positivePhaseCoefficientSequence line 68
Source documentation
Quotients preserve the actual positive coefficient sequence exactly.
```
theorem quotient_positivePhaseCoefficientSequence (π : BoundedSequence A →⋆ₐ[ℂ] B)
    (e : ι → A) (w : BoundedSequence A) (r : ℕ) (s : Sym ι r) :
    π (positivePhaseCoefficientSequence e w r s) =
      positivePhaseCoefficient (fun a => π (boundedSequenceConst (e a))) (π w) r s :=
…
```
Mentions: OAI.KadisonKastler.BoundedSequence, OAI.KadisonKastler.positivePhaseCoefficientSequence, OAI.KadisonKastler.positivePhaseCoefficient, OAI.KadisonKastler.boundedSequenceConst
theorem OAI.KadisonKastler.quotient_negativePhaseCoefficientSequence line 75
Source documentation
Quotients preserve the actual negative coefficient sequence exactly.
```
theorem quotient_negativePhaseCoefficientSequence (π : BoundedSequence A →⋆ₐ[ℂ] B)
    (e : ι → A) (w : BoundedSequence A) (r : ℕ) (s : Sym ι r) :
    π (negativePhaseCoefficientSequence e w r s) =
      negativePhaseCoefficient (fun a => π (boundedSequenceConst (e a))) (π w) r s :=
…
```
Mentions: OAI.KadisonKastler.BoundedSequence, OAI.KadisonKastler.negativePhaseCoefficientSequence, OAI.KadisonKastler.negativePhaseCoefficient, OAI.KadisonKastler.boundedSequenceConst
theorem OAI.KadisonKastler.map_phaseSupport line 83
Source documentation
The support sum is also preserved by a star algebra homomorphism.
```
theorem map_phaseSupport (φ : A →⋆ₐ[ℂ] B) (e : ι → A) (s : Multiset ι) :
    φ (phaseSupport e s) = phaseSupport (fun a => φ (e a)) s := by
…
```
Mentions: OAI.KadisonKastler.phaseSupport

theorem OAI.KadisonKastler.phaseCoefficientSequence_right_support line 88

Source documentation

Coordinate coefficients retain their actual right support.

theorem phaseCoefficientSequence_right_support
    (e : ι → A) (w : BoundedSequence A)
    (he : ∀ a, star (e a) = e a)
    (hmul : ∀ a b, e a * e b = if a = b then e a else 0)
    (r : ℕ) (s : Sym ι (r + 1)) (j : ℕ) :
    positivePhaseCoefficientSequence e w (r + 1) s j * phaseSupport e (s : Multiset ι) =
        positivePhaseCoefficientSequence e w (r + 1) s j ∧
      negativePhaseCoefficientSequence e w (r + 1) s j * phaseSupport e (s : Multiset ι) =
        negativePhaseCoefficientSequence e w (r + 1) s j := by
…

Mentions: OAI.KadisonKastler.BoundedSequence, OAI.KadisonKastler.positivePhaseCoefficientSequence, OAI.KadisonKastler.phaseSupport, OAI.KadisonKastler.negativePhaseCoefficientSequence

theorem OAI.KadisonKastler.phaseCoefficientSequence_column_norm line 107

Source documentation

Both signs of the actual coordinate coefficient family are isometric columns after applying any Hilbert-space star representation.

theorem phaseCoefficientSequence_column_norm
    (ρ : A →⋆ₐ[ℂ] (H →L[ℂ] H)) (e : ι → A)
    (w : unitary (BoundedSequence A))
    (he : ∀ a, star (e a) = e a)
    (hmul : ∀ a b, e a * e b = if a = b then e a else 0)
    (hsum : ∑ a, e a = 1) (r : ℕ) (j : ℕ) (ξ : H) :
    ‖WithLp.toLp 2 (fun s : Sym ι (r + 1) =>
      ρ (positivePhaseCoefficientSequence e (w : BoundedSequence A) (r + 1) s j) ξ)‖ = ‖ξ‖ ∧
    ‖WithLp.toLp 2 (fun s : Sym ι (r + 1) =>
      ρ (negativePhaseCoefficientSequence e (w : BoundedSequence A) (r + 1) s j) ξ)‖ = ‖ξ‖ := by
…

Mentions: OAI.KadisonKastler.BoundedSequence, OAI.KadisonKastler.positivePhaseCoefficientSequence, OAI.KadisonKastler.negativePhaseCoefficientSequence

theorem OAI.KadisonKastler.TraceQuotientMap.trace_boundedSequenceConst line 146
Source documentation
Constant traces are preserved for arbitrary source C⋆-algebras.
```
theorem TraceQuotientMap.trace_boundedSequenceConst (Q : TraceQuotientMap τ σ ω) (a : A) :
    σ.toLinearMap (Q.quotient (boundedSequenceConst a)) = τ.toLinearMap a :=
…
```
Mentions: OAI.KadisonKastler.TraceQuotientMap, OAI.KadisonKastler.boundedSequenceConst

theorem OAI.KadisonKastler.phaseCoefficientSequence_quotient_norm_bounds line 152

Source documentation

The free-word estimates bound both signs of the actual sequence coefficients after quotienting; no coefficient norm estimate is assumed.

theorem phaseCoefficientSequence_quotient_norm_bounds
    (hFock : PublishedDiagonalFockRepresentation.{v})
    (Q : TraceQuotientMap τ σ ω) {d r : ℕ} [NeZero d]
    (e : Fin d → A) (w : unitary (BoundedSequence A))
    (hprojection : ∀ a, IsStarProjection (e a))
    (horthogonal : ∀ a b, a ≠ b → e a * e b = 0)
    (hsum : ∑ a, e a = 1)
    (htrace : ∀ a, τ.toLinearMap (e a) = (d : ℂ)⁻¹)
    (hfree : FreeHaarMoments σ (Q.quotient.comp boundedSequenceConst).range
      (Unitary.map (StarMonoidHom.ofClass Q.quotient) w))
    (hr : 1 ≤ r) (hd : freeWordThreshold r ≤ d) :
    (∀ s : Sym (Fin d) r,
…

Mentions: OAI.KadisonKastler.TraceQuotientMap, OAI.KadisonKastler.BoundedSequence, OAI.KadisonKastler.FreeHaarMoments, OAI.KadisonKastler.boundedSequenceConst, OAI.KadisonKastler.freeWordThreshold