PublishedFock.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

The published faithful free-product representation input

The only input here is the standard faithful reduced-free-product representation of a scalar-free family with a faithful tracial state. The creation, annihilation and preservation formulas are those of Ricard–Xu, Khintchine type inequalities for reduced free products and applications, J. reine angew. Math. 599 (2006), §1 and Fact 2.6 (arXiv:math/0505302v2, printed pp. 3 and 7).

We use only finite diagonal algebras with equal trace projections. The input supplies their representation and structural identities, without assuming any projection-word norm estimate. The latter has been proved in FreeProjectionWords from those identities.

structure OAI.KadisonKastler.FaithfulTracialState line 32
Source documentation
The state data needed for faithful reduced free products.
```
structure FaithfulTracialState (B : Type u) [CStarAlgebra B] where
…
```
def OAI.KadisonKastler.generatedDiagonal line 41
Source documentation
The norm-closed algebra generated by the diagonal projections.
```
def generatedDiagonal {B : Type u} [CStarAlgebra B] {r d : ℕ}
    (e : Fin r → Fin d → B) : StarSubalgebra ℂ B :=
…
```
instance OAI.KadisonKastler.generatedDiagonalCStarAlgebra line 45
theorem OAI.KadisonKastler.mem_generatedDiagonal line 49
def OAI.KadisonKastler.generatedDiagonalProjection line 54
def OAI.KadisonKastler.ScalarFreeDiagonal line 60
Source documentation
Scalar freeness, specialized to the span of each finite diagonal partition. Adjacent copy indices differ; every letter has zero trace.
```
def ScalarFreeDiagonal {B : Type u} [CStarAlgebra B] {r d : ℕ}
    (τ : FaithfulTracialState B) (e : Fin r → Fin d → B) : Prop :=
…
```
Mentions: OAI.KadisonKastler.FaithfulTracialState
def OAI.KadisonKastler.PublishedDiagonalFockRepresentation line 69
Source documentation
A precise specialization of the faithful reduced-free-product representation, with no quantitative word bounds in its conclusion.
```
def PublishedDiagonalFockRepresentation : Prop :=
…
```

theorem OAI.KadisonKastler.norm_sum_diagonalWords_eq line 84

Source documentation

Faithful representation transfers every finite sum of diagonal words, including sums with repeated labels, without changing its norm.

theorem norm_sum_diagonalWords_eq {B : Type u} [CStarAlgebra B] {r d : ℕ}
    {K : Type*} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K]
    [NeZero d] (e : Fin r → Fin d → B) (M : FreeDiagonalModel (Fin r) (Fin d) K)
    (π : generatedDiagonal e →⋆ₐ[ℂ] (K →L[ℂ] K)) (hπ : Function.Injective π)
    (he : ∀ i a, π (generatedDiagonalProjection e i a) = M.e i a)
    {T : Type*} (s : Finset T) (label : T → Fin r → Fin d) :
    ‖∑ t ∈ s, (List.ofFn (fun i => e i (label t i))).prod‖ =
      ‖∑ t ∈ s, M.projectionWord id (label t)‖ := by
…

Mentions: OAI.KadisonKastler.FreeDiagonalModel, OAI.KadisonKastler.generatedDiagonal, OAI.KadisonKastler.generatedDiagonalProjection

theorem OAI.KadisonKastler.norm_freeProjectionWords_le_of_published line 108

Source documentation

The manuscript's projection-word estimate, conditional only on the standard faithful Fock representation of the scalar-free diagonals.

theorem norm_freeProjectionWords_le_of_published
    (hFock : PublishedDiagonalFockRepresentation.{u})
    {B : Type u} [CStarAlgebra B] {r d : ℕ} [NeZero d]
    (τ : FaithfulTracialState B) (e : Fin r → Fin d → B)
    (hprojection : ∀ i a, IsStarProjection (e i a))
    (horthogonal : ∀ i a b, a ≠ b → e i a * e i b = 0)
    (hsum : ∀ i, ∑ a, e i a = 1)
    (htrace : ∀ i a, τ.toLinearMap (e i a) = (d : ℂ)⁻¹)
    (hfree : ScalarFreeDiagonal τ e)
    (hr : 1 ≤ r) (hd : freeWordThreshold r ≤ d) (s : Sym (Fin d) r) :
    ‖∑ t : PrescribedLabelTuple s, (List.ofFn (fun i => e i (t.val i))).prod‖ ≤
      projectionWordWeight (freeWordC r) s := by
…

Mentions: OAI.KadisonKastler.FaithfulTracialState, OAI.KadisonKastler.ScalarFreeDiagonal, OAI.KadisonKastler.freeWordThreshold, OAI.KadisonKastler.PrescribedLabelTuple, OAI.KadisonKastler.projectionWordWeight, OAI.KadisonKastler.freeWordC