ConjugatedDiagonal.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

Diagonal partitions conjugated by powers of a unitary

Conjugation preserves the projection partition and its tracial values. Consequently the published faithful Fock representation applies to the actual conjugated copies used in the phase coefficients, once scalar freeness of those copies is supplied.

theorem OAI.KadisonKastler.conjugatedCopy_mul line 28
theorem OAI.KadisonKastler.conjugatedCopy_isStarProjection line 40
theorem OAI.KadisonKastler.conjugatedCopy_orthogonal line 51
theorem OAI.KadisonKastler.sum_conjugatedCopy line 56
def OAI.KadisonKastler.conjugatedDiagonal line 66
Source documentation
The finite family appearing in a word of length r.
```
def conjugatedDiagonal (e : α → A) (v : A) (r : ℕ) (i : Fin r) (a : α) : A :=
…
```
theorem OAI.KadisonKastler.conjugatedProjectionWord_eq_diagonalWord line 69

theorem OAI.KadisonKastler.trace_conjugatedCopy line 81

Source documentation

Traciality removes both factors of the conjugation.

theorem trace_conjugatedCopy (τ : FaithfulTracialState B) (e : α → B) (v : B)
    (hv : v ∈ unitary B) (n : ℕ) (a : α) :
    τ.toLinearMap (conjugatedCopy e v n a) = τ.toLinearMap (e a) := by
…

Mentions: OAI.KadisonKastler.FaithfulTracialState, OAI.KadisonKastler.conjugatedCopy

theorem OAI.KadisonKastler.norm_positivePhaseCoefficient_le_of_published line 97

Source documentation

The positive phase coefficient satisfies the actual projection-word bound, conditional only on the published Fock input and scalar freeness of these specific conjugated diagonal copies.

theorem norm_positivePhaseCoefficient_le_of_published
    (hFock : PublishedDiagonalFockRepresentation.{u})
    (τ : FaithfulTracialState B) (e : Fin d → B) (v : B) (hv : v ∈ unitary B)
    (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 : ScalarFreeDiagonal τ (conjugatedDiagonal e v r))
    (hr : 1 ≤ r) (hd : freeWordThreshold r ≤ d) (s : Sym (Fin d) r) :
    ‖positivePhaseCoefficient e v r s‖ ≤ projectionWordWeight (freeWordC r) s := by
…

Mentions: OAI.KadisonKastler.FaithfulTracialState, OAI.KadisonKastler.ScalarFreeDiagonal, OAI.KadisonKastler.conjugatedDiagonal, OAI.KadisonKastler.freeWordThreshold, OAI.KadisonKastler.positivePhaseCoefficient, OAI.KadisonKastler.projectionWordWeight, OAI.KadisonKastler.freeWordC

theorem OAI.KadisonKastler.norm_negativePhaseCoefficient_le_of_published line 118

Source documentation

The adjoint formula gives the identical bound for negative powers.

theorem norm_negativePhaseCoefficient_le_of_published
    (hFock : PublishedDiagonalFockRepresentation.{u})
    (τ : FaithfulTracialState B) (e : Fin d → B) (v : B) (hv : v ∈ unitary B)
    (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 : ScalarFreeDiagonal τ (conjugatedDiagonal e v r))
    (hr : 1 ≤ r) (hd : freeWordThreshold r ≤ d) (s : Sym (Fin d) r) :
    ‖negativePhaseCoefficient e v r s‖ ≤ projectionWordWeight (freeWordC r) s := by
…

Mentions: OAI.KadisonKastler.FaithfulTracialState, OAI.KadisonKastler.ScalarFreeDiagonal, OAI.KadisonKastler.conjugatedDiagonal, OAI.KadisonKastler.freeWordThreshold, OAI.KadisonKastler.negativePhaseCoefficient, OAI.KadisonKastler.projectionWordWeight, OAI.KadisonKastler.freeWordC