OrbitMinima.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

The least-norm unitary-orbit point is scalar when the coordinate inclusion has scalar commutant.

def OAI.Generator.Tracial.subalgebraUnitaries line 17
def OAI.Generator.Tracial.ambientUnitary line 25
theorem OAI.Generator.Tracial.commutes_of_fixed_unitaries line 29

theorem OAI.Generator.Tracial.scalar_mem_traceOrbitHull line 52

Source documentation

Irreducibility is exactly the coordinate relative-commutant hypothesis. Completeness of P is automatic for a von Neumann subalgebra, and is used only to express its elements as sums of four unitaries.

theorem scalar_mem_traceOrbitHull (P : StarSubalgebra ℂ M.toStarSubalgebra) [CompleteSpace P]
    (hirr : ∀ c : M.toStarSubalgebra, (∀ a : P, (a : M.toStarSubalgebra)*c = c*(a : M.toStarSubalgebra)) →
      ∃ z : ℂ, c = z • (1 : M.toStarSubalgebra)) (b : M.toStarSubalgebra) :
    baseVector τ (τ.trace b • (1 : M.toStarSubalgebra)) ∈ traceOrbitHull τ (subalgebraUnitaries P) b := by
…

Mentions: OAI.Generator.Tracial.baseVector, OAI.Generator.Tracial.traceOrbitHull, OAI.Generator.Tracial.subalgebraUnitaries

theorem OAI.Generator.Tracial.trace_distance_le_unitary_displacement line 65
theorem OAI.Generator.Tracial.baseVector_inner_eq_trace line 89
theorem OAI.Generator.Tracial.orbitHull_trace_test_zero line 97
Source documentation
A continuous trace test vanishing on an orbit vanishes on its closed convex hull.
```
theorem orbitHull_trace_test_zero (G : Subgroup (unitary M.toStarSubalgebra))
    (b d : M.toStarSubalgebra)
    (hd : ∀ u : G, τ.trace (star d * conjugateLinear u.val b)=0)
    {ξ : H} (hξ : ξ ∈ traceOrbitHull τ G b) :
    inner ℂ (baseVector τ d) ξ=0 := by
…
```
Mentions: OAI.Generator.Tracial.conjugateLinear, OAI.Generator.Tracial.traceOrbitHull, OAI.Generator.Tracial.baseVector
theorem OAI.Generator.Tracial.projection_eq_zero_or_eq_zero_of_no_links line 118
Source documentation
Nonzero ambient projections cannot have all their P matrix coefficients zero in an irreducible inclusion. No comparison theorem is assumed.
```
theorem projection_eq_zero_or_eq_zero_of_no_links (r s : AlgebraProjection M)
    (hlink : ∀ a : P, s.val*(a : M.toStarSubalgebra)*r.val=0) :
    r.val=0 ∨ s.val=0 := by
…
```
Mentions: OAI.Generator.Tracial.AlgebraProjection
theorem OAI.Generator.Tracial.corner_commutant_projection_trivial line 147
Source documentation
Every projection commuting with pPp inside pMp is either zero or p.
```
theorem corner_commutant_projection_trivial (p r : AlgebraProjection M)
    (hrp : r ≤ p)
    (hr : ∀ a : P, Commute r.val (p.val*(a : M.toStarSubalgebra)*p.val)) :
    r.val=0 ∨ r.val=p.val := by
…
```
Mentions: OAI.Generator.Tracial.AlgebraProjection