Subfactors.lean`

33 declarations, 0 contain sorry, 0 declared as axioms

The actual von Neumann algebra of operators in N commuting with a finite projection partition. Its double-commutant identity and completeness are proved, so spectral approximation can be performed inside this algebra.

def OAI.Generator.Tracial.CornerPartition.blockStarAlgebra line 22
theorem OAI.Generator.Tracial.CornerPartition.blockStarAlgebra_bicommutant line 41
def OAI.Generator.Tracial.CornerPartition.blockVonNeumann line 58
theorem OAI.Generator.Tracial.CornerPartition.blockVonNeumann_le line 62
theorem OAI.Generator.Tracial.CornerPartition.blockVonNeumann_mem_iff line 65
theorem OAI.Generator.Tracial.CornerPartition.piece_commute line 73
theorem OAI.Generator.Tracial.CornerPartition.piece_mem_blockVonNeumann line 79
theorem OAI.Generator.Tracial.CornerPartition.compression_mem_blockVonNeumann line 84

theorem OAI.Generator.Tracial.selfAdjoint_corner_commutant_scalar line 122

Source documentation

A self-adjoint element of the relative corner commutant is scalar in that corner, including the zero corner.

theorem selfAdjoint_corner_commutant_scalar (p : AlgebraProjection M)
    (c : M.toStarSubalgebra) (hc : IsSelfAdjoint c)
    (hl : p.val*c=c) (hr : c*p.val=c)
    (hcomm : ∀ a : P, Commute c (p.val*(a : M.toStarSubalgebra)*p.val)) :
    ∃ z : ℂ, c=z • p.val := by
…

Mentions: OAI.Generator.Tracial.AlgebraProjection

theorem OAI.Generator.Tracial.corner_commutant_star line 156

Source documentation

Taking adjoints preserves the supported relative-commutant condition.

theorem corner_commutant_star (p : AlgebraProjection M) (c : M.toStarSubalgebra)
    (hcomm : ∀ a : P, Commute c (p.val*(a : M.toStarSubalgebra)*p.val)) :
    ∀ a : P, Commute (star c) (p.val*(a : M.toStarSubalgebra)*p.val) := by
…

Mentions: OAI.Generator.Tracial.AlgebraProjection

theorem OAI.Generator.Tracial.corner_commutant_scalar line 171
Source documentation
Exact irreducibility in pMp, stated in ambient coordinates. The scalar is the normalized corner trace when p is nonzero.
```
theorem corner_commutant_scalar (p : AlgebraProjection M) (c : M.toStarSubalgebra)
    (hl : p.val*c=c) (hr : c*p.val=c)
    (hcomm : ∀ a : P, Commute c (p.val*(a : M.toStarSubalgebra)*p.val)) :
    ∃ z : ℂ, c=z • p.val := by
…
```
Mentions: OAI.Generator.Tracial.AlgebraProjection
theorem OAI.Generator.Tracial.CornerPartition.pinch_eq_self_of_commutes line 213
theorem OAI.Generator.Tracial.CornerPartition.block_commutant_scalar_blocks line 223
theorem OAI.Generator.Tracial.CornerPartition.block_commutant_mem_subalgebra line 255
def OAI.Generator.Tracial.TraceOrthogonal line 282
theorem OAI.Generator.Tracial.TraceOrthogonal.trace_zero line 290
theorem OAI.Generator.Tracial.TraceOrthogonal.compression line 292
theorem OAI.Generator.Tracial.TraceOrthogonal.conjugate line 302
theorem OAI.Generator.Tracial.TraceOrthogonal.pinch line 311
theorem OAI.Generator.Tracial.TraceOrthogonal.cornerScalar_zero line 318
theorem OAI.Generator.Tracial.TraceOrthogonal.scalarEnergy_zero line 322

theorem OAI.Generator.Tracial.zero_mem_orbitHull_of_orthogonal line 332

Source documentation

If an orthogonal operator is averaged by subalgebra unitaries and all fixed points lie in the subalgebra, the actual least-norm orbit point is zero.

theorem zero_mem_orbitHull_of_orthogonal
    (P : StarSubalgebra ℂ M.toStarSubalgebra)
    (G : Subgroup (unitary M.toStarSubalgebra))
    (hG : ∀ u : G,(u.val : M.toStarSubalgebra) ∈ P)
    (hfixed : ∀ c : M.toStarSubalgebra,
      (∀ u : G,conjugateLinear u.val c=c) → c ∈ P)
    (x : M.toStarSubalgebra) (hx : TraceOrthogonal τ P x) :
    (0 : H) ∈ traceOrbitHull τ G x := by
…

Mentions: OAI.Generator.Tracial.conjugateLinear, OAI.Generator.Tracial.TraceOrthogonal, OAI.Generator.Tracial.traceOrbitHull

theorem OAI.Generator.Tracial.CornerPartition.scalarEnergy_le_energy line 353
theorem OAI.Generator.Tracial.CornerPartition.cornerScalar_eq_of_orthogonal_difference line 363
theorem OAI.Generator.Tracial.CornerPartition.scalarEnergy_eq_of_orthogonal_difference line 371
theorem OAI.Generator.Tracial.CornerPartition.refinement_scalarEnergy_le_component line 383
Source documentation
All later scalar terms are bounded by the already controlled coarse energy of the subalgebra component. There is no claim that global centering provides this bound.
```
theorem refinement_scalarEnergy_le_component
    (P : StarSubalgebra ℂ M.toStarSubalgebra) (R : CornerPartition p)
    (hR : ∀ i,(R.piece i).val ∈ P) (hQR : Q.Refines R)
    (x y : M.toStarSubalgebra) (hxy : TraceOrthogonal τ P (x-y)) :
    R.scalarEnergy τ x ≤ τ.norm₂ (Q.pinch y)^2 := by
…
```
Mentions: OAI.Generator.Tracial.CornerPartition, OAI.Generator.Tracial.TraceOrthogonal
theorem OAI.Generator.Tracial.CornerPartition.pinch_mem line 393

theorem OAI.Generator.Tracial.CornerPartition.orthogonal_component_energy line 399

Source documentation

Pythagoras separates the orthogonal component from the component in P.

theorem orthogonal_component_energy
    (P : StarSubalgebra ℂ M.toStarSubalgebra) (hQ : ∀ i,(Q.piece i).val ∈ P)
    (x y : M.toStarSubalgebra) (hy : y ∈ P) (hxy : TraceOrthogonal τ P (x-y)) :
    τ.norm₂ (Q.pinch x)^2 = τ.norm₂ (Q.pinch (x-y))^2+τ.norm₂ (Q.pinch y)^2 := by
…

Mentions: OAI.Generator.Tracial.TraceOrthogonal

theorem OAI.Generator.Tracial.selfAdjoint_corner_scalar_of_projections line 425
theorem OAI.Generator.Tracial.corner_scalar_of_projections line 445
theorem OAI.Generator.Tracial.irreducible_subalgebra_diffuse line 472
theorem OAI.Generator.Tracial.tracial_isometry_coisometry line 515
theorem OAI.Generator.Tracial.tracial_nonzero line 530