FiniteComparison.lean`

36 declarations, 0 contain sorry, 0 declared as axioms

The closed span of algebra translates of a projection range gives its central support. All operators act on the original Hilbert space; no trace, cyclic vector, separability, finiteness, or comparison theorem is assumed.

def OAI.Generator.Tracial.projectionOrbitVectors line 18
def OAI.Generator.Tracial.projectionOrbitClosure line 21
instance OAI.Generator.Tracial.projectionOrbitClosure_complete line 24
theorem OAI.Generator.Tracial.projectionOrbitClosure_invariant_of_vectors line 28
theorem OAI.Generator.Tracial.projectionOrbitClosure_invariant line 40
theorem OAI.Generator.Tracial.projectionOrbitClosure_commutant_invariant line 46
theorem OAI.Generator.Tracial.projectionOrbitProjection_mem line 60
def OAI.Generator.Tracial.centralSupport line 68
theorem OAI.Generator.Tracial.centralSupport_commutes line 76
theorem OAI.Generator.Tracial.le_centralSupport line 83
theorem OAI.Generator.Tracial.centralSupport_le line 91
theorem OAI.Generator.Tracial.mul_centralSupport_eq_zero_of_no_links line 108

theorem OAI.Generator.Tracial.centralSupport_eq_one_of_factor line 123

Source documentation

Scalar center forces every nonzero projection to have full central support.

theorem centralSupport_eq_one_of_factor
    (hfactor : ∀ c : M.toStarSubalgebra,
      (∀ a : M.toStarSubalgebra, a*c=c*a) → ∃ z : ℂ, c=z • (1 : M.toStarSubalgebra))
    (p : AlgebraProjection M) (hp : p.val≠0) : (centralSupport p).val=1 := by
…

Mentions: OAI.Generator.Tracial.AlgebraProjection, OAI.Generator.Tracial.centralSupport

theorem OAI.Generator.Tracial.traceFree_projection_eq_zero_or_eq_zero_of_no_links line 134

theorem OAI.Generator.Tracial.wot_limit_mul_left line 157

Source documentation

Left multiplication by a fixed operator preserves matrix-coefficient limits.

theorem wot_limit_mul_left {ι : Type*} {l : Filter ι}
    (a : ι → M.toStarSubalgebra) (b c : M.toStarSubalgebra)
    (ht : ∀ x y : H, Tendsto (fun i => inner ℂ y ((a i).val x)) l
      (𝓝 (inner ℂ y (b.val x)))) :
    ∀ x y : H, Tendsto (fun i => inner ℂ y ((c*a i).val x)) l
      (𝓝 (inner ℂ y ((c*b).val x))) := by
…

theorem OAI.Generator.Tracial.wot_limit_mul_right line 170

Source documentation

Right multiplication by a fixed operator preserves matrix-coefficient limits.

theorem wot_limit_mul_right {ι : Type*} {l : Filter ι}
    (a : ι → M.toStarSubalgebra) (b c : M.toStarSubalgebra)
    (ht : ∀ x y : H, Tendsto (fun i => inner ℂ y ((a i).val x)) l
      (𝓝 (inner ℂ y (b.val x)))) :
    ∀ x y : H, Tendsto (fun i => inner ℂ y ((a i*c).val x)) l
      (𝓝 (inner ℂ y ((b*c).val x))) := fun x y => ht (c.val x) y

theorem OAI.Generator.Tracial.wot_limit_unique line 178

Source documentation

Matrix coefficients determine an element of the concrete algebra.

theorem wot_limit_unique {ι : Type*} {l : Filter ι} [l.NeBot]
    (a : ι → M.toStarSubalgebra) (b c : M.toStarSubalgebra)
    (hb : ∀ x y : H, Tendsto (fun i => inner ℂ y ((a i).val x)) l
      (𝓝 (inner ℂ y (b.val x))))
    (hc : ∀ x y : H, Tendsto (fun i => inner ℂ y ((a i).val x)) l
      (𝓝 (inner ℂ y (c.val x)))) : b=c := by
…

theorem OAI.Generator.Tracial.PartialIsometry.traceFree_monotone_upper_bound line 193

Source documentation

Every monotone directed net has a partial-isometry upper bound, retaining any prescribed bounds on its initial and final projections.

theorem traceFree_monotone_upper_bound
    {ι : Type*} [Preorder ι] [IsDirected ι (· ≤ ·)] [Nonempty ι]
    (a : ι → PartialIsometry M) (ha : Monotone a)
    (p q : AlgebraProjection M) (hp : ∀ i, (a i).support ≤ p)
    (hq : ∀ i, (a i).target ≤ q) :
    ∃ v : PartialIsometry M, (∀ i, a i ≤ v) ∧ v.support ≤ p ∧ v.target ≤ q := by
…

Mentions: OAI.Generator.Tracial.PartialIsometry, OAI.Generator.Tracial.AlgebraProjection, OAI.Generator.Tracial.PartialIsometry.target

theorem OAI.Generator.Tracial.PartialIsometry.traceFree_chain_upper_bound line 253
theorem OAI.Generator.Tracial.PartialIsometry.traceFree_exists_maximal_between line 269
theorem OAI.Generator.Tracial.traceFree_exists_nonzero_partialIsometry_between_projections line 299
theorem OAI.Generator.Tracial.traceFree_exists_partialIsometry_comparison line 314
def OAI.Generator.Tracial.PartialIsometry.onProjection line 376
Source documentation
The identity partial isometry on a projection.
```
def onProjection (p : AlgebraProjection M) : PartialIsometry M :=
…
```
Mentions: OAI.Generator.Tracial.AlgebraProjection, OAI.Generator.Tracial.PartialIsometry
theorem OAI.Generator.Tracial.PartialIsometry.onProjection_target line 379
theorem OAI.Generator.Tracial.PartialIsometry.target_eq_support_of_finite line 386
Source documentation
A finite algebra has no partial isometry from a projection onto a proper subprojection of itself. Finiteness is used on v + (1 - p).
```
theorem target_eq_support_of_finite
    (hfinite : ∀ a : M.toStarSubalgebra, star a*a=1 → a*star a=1)
    (v : PartialIsometry M) (hv : v.target ≤ v.support) : v.target=v.support := by
…
```
Mentions: OAI.Generator.Tracial.PartialIsometry
theorem OAI.Generator.Tracial.PartialIsometry.target_eq_support_of_finite_of_le line 414
Source documentation
Finiteness also excludes a proper enlargement equivalent to a projection.
```
theorem target_eq_support_of_finite_of_le
    (hfinite : ∀ a : M.toStarSubalgebra, star a*a=1 → a*star a=1)
    (v : PartialIsometry M) (hv : v.support ≤ v.target) : v.target=v.support := by
…
```
Mentions: OAI.Generator.Tracial.PartialIsometry
theorem OAI.Generator.isII1Factor_projection_comparison line 434
Source documentation
Comparison in the exact original concrete algebra, packaged by its proved bicommutant property. The underlying operators and star subalgebra are unchanged.
```
theorem isII1Factor_projection_comparison
    (S : StarSubalgebra ℂ (H →L[ℂ] H)) (hS : IsII1Factor S)
    (p q : Tracial.AlgebraProjection (vonNeumannOfWOTClosed S hS.weaklyClosed)) :
    ∃ v : Tracial.PartialIsometry (vonNeumannOfWOTClosed S hS.weaklyClosed),
      v.support ≤ p ∧ v.target ≤ q ∧ (v.support=p ∨ v.target=q) := by
…
```
Mentions: OAI.Generator.IsII1Factor, OAI.Generator.Tracial.AlgebraProjection, OAI.Generator.vonNeumannOfWOTClosed, OAI.Generator.Tracial.PartialIsometry
theorem OAI.Generator.isII1Factor_no_proper_self_equivalence line 445
Source documentation
The exact original finite-isometry field makes every projection finite.
```
theorem isII1Factor_no_proper_self_equivalence
    (S : StarSubalgebra ℂ (H →L[ℂ] H)) (hS : IsII1Factor S)
    (v : Tracial.PartialIsometry (vonNeumannOfWOTClosed S hS.weaklyClosed))
    (hv : v.target ≤ v.support) : v.target=v.support :=
…
```
Mentions: OAI.Generator.IsII1Factor, OAI.Generator.Tracial.PartialIsometry, OAI.Generator.vonNeumannOfWOTClosed
theorem OAI.Generator.Tracial.projection_orthogonal_of_le line 461
Source documentation
Orthogonality passes to subprojections in both variables.
```
theorem projection_orthogonal_of_le {p q r s : AlgebraProjection M}
    (h : p.val*q.val=0) (hr : r ≤ p) (hs : s ≤ q) : r.val*s.val=0 := by
…
```
Mentions: OAI.Generator.Tracial.AlgebraProjection
theorem OAI.Generator.Tracial.PartialIsometry.target_mono line 469

theorem OAI.Generator.Tracial.PartialIsometry.traceFree_orthogonal_monotone_upper_bound line 476

Source documentation

A directed increasing family of square-zero partial isometries has an upper bound with orthogonal initial/final projections inside p.

theorem traceFree_orthogonal_monotone_upper_bound
    {ι : Type*} [Preorder ι] [IsDirected ι (· ≤ ·)] [Nonempty ι]
    (a : ι → PartialIsometry M) (ha : Monotone a)
    (p : AlgebraProjection M) (hp : ∀ i, (a i).support ≤ p)
    (hq : ∀ i, (a i).target ≤ p)
    (ho : ∀ i, (a i).support.val*(a i).target.val=0) :
    ∃ v : PartialIsometry M, (∀ i, a i ≤ v) ∧ v.support ≤ p ∧ v.target ≤ p ∧
      v.support.val*v.target.val=0 := by
…

Mentions: OAI.Generator.Tracial.PartialIsometry, OAI.Generator.Tracial.AlgebraProjection, OAI.Generator.Tracial.PartialIsometry.target

theorem OAI.Generator.Tracial.PartialIsometry.traceFree_orthogonal_chain_upper_bound line 546
theorem OAI.Generator.Tracial.PartialIsometry.traceFree_exists_maximal_orthogonal line 565

theorem OAI.Generator.Tracial.PartialIsometry.traceFree_monotone_least_supports line 593

Source documentation

The initial and final projections of this upper bound are the respective least upper bounds of the net's initial and final projections.

theorem traceFree_monotone_least_supports
    {ι : Type*} [Preorder ι] [IsDirected ι (· ≤ ·)] [Nonempty ι]
    (a : ι → PartialIsometry M) (ha : Monotone a) :
    ∃ v : PartialIsometry M, (∀ i, a i ≤ v) ∧
      (∀ p : AlgebraProjection M, (∀ i, (a i).support ≤ p) → v.support ≤ p) ∧
      (∀ q : AlgebraProjection M, (∀ i, (a i).target ≤ q) → v.target ≤ q) := by
…

Mentions: OAI.Generator.Tracial.PartialIsometry, OAI.Generator.Tracial.AlgebraProjection, OAI.Generator.Tracial.PartialIsometry.target

theorem OAI.Generator.Tracial.PartialIsometry.exists_unitary_extension line 662
theorem OAI.Generator.Tracial.exists_unitary_polar_decomposition line 697