Supports.lean`

30 declarations, 0 contain sorry, 0 declared as axioms

Kernel and range projections constructed in the actual von Neumann algebra. Membership follows from commutant invariance, with no spectral theorem assumed.

theorem OAI.Generator.Tracial.kernelProjection_mem line 22
Source documentation
The orthogonal projection onto an operator's kernel belongs to its von Neumann algebra. This uses the actual double-commutant definition.
```
theorem kernelProjection_mem (x : M.toStarSubalgebra) :
    (x.val.ker).starProjection ∈ M := by
…
```
def OAI.Generator.Tracial.kernelProjection line 35
theorem OAI.Generator.Tracial.kernelProjection_apply line 45
theorem OAI.Generator.Tracial.mul_kernelProjection line 48
theorem OAI.Generator.Tracial.kernelProjection_fixes line 53
theorem OAI.Generator.Tracial.le_kernelProjection_iff line 58
Source documentation
This is the largest algebra projection annihilated on the left by x.
```
theorem le_kernelProjection_iff (x : M.toStarSubalgebra) (q : AlgebraProjection M) :
    q ≤ kernelProjection x ↔ x*q.val=0 := by
…
```
Mentions: OAI.Generator.Tracial.AlgebraProjection, OAI.Generator.Tracial.kernelProjection
def OAI.Generator.Tracial.rangeProjection line 72
Source documentation
The projection onto the closed range of x, expressed via ker(x*).
```
def rangeProjection (x : M.toStarSubalgebra) : AlgebraProjection M :=
…
```
Mentions: OAI.Generator.Tracial.AlgebraProjection
theorem OAI.Generator.Tracial.rangeProjection_mul line 75
theorem OAI.Generator.Tracial.rangeProjection_le_iff line 83
Source documentation
Minimality retains any prescribed corner supporting x.
```
theorem rangeProjection_le_iff (x : M.toStarSubalgebra) (q : AlgebraProjection M) :
    rangeProjection x ≤ q ↔ q.val*x=x := by
…
```
Mentions: OAI.Generator.Tracial.AlgebraProjection, OAI.Generator.Tracial.rangeProjection
theorem OAI.Generator.Tracial.kernelProjection_mul_of_mul_eq_zero line 107
Source documentation
Kernel projections fix the range of every operator they annihilate.
```
theorem kernelProjection_mul_of_mul_eq_zero (x y : M.toStarSubalgebra) (h : x*y=0) :
    (kernelProjection x).val*y=y := by
…
```
Mentions: OAI.Generator.Tracial.kernelProjection
theorem OAI.Generator.Tracial.rangeProjection_mul_eq_zero line 115
Source documentation
For self-adjoint x, its range projection kills every y killed by x.
```
theorem rangeProjection_mul_eq_zero (x y : M.toStarSubalgebra) (hx : IsSelfAdjoint x)
    (h : x*y=0) : (rangeProjection x).val*y=0 := by
…
```
Mentions: OAI.Generator.Tracial.rangeProjection
def OAI.Generator.Tracial.positiveSupport line 136
theorem OAI.Generator.Tracial.positiveSupport_mul_pos line 138
theorem OAI.Generator.Tracial.positiveSupport_mul_neg line 141
theorem OAI.Generator.Tracial.positiveSupport_mul line 146
theorem OAI.Generator.Tracial.mul_positiveSupport line 152
theorem OAI.Generator.Tracial.positiveSupport_commutes line 158
theorem OAI.Generator.Tracial.positiveSupport_compression line 163
theorem OAI.Generator.Tracial.positiveSupport_complement_mul line 167
theorem OAI.Generator.Tracial.positiveSupport_complement_compression line 173
def OAI.Generator.Tracial.spectralCut line 182
theorem OAI.Generator.Tracial.spectralShift_selfAdjoint line 185

theorem OAI.Generator.Tracial.spectralCut_lower line 192

Source documentation

The high spectral corner has nonnegative shifted compression.

theorem spectralCut_lower (x : M.toStarSubalgebra) (hx : IsSelfAdjoint x) (t : ℝ) :
    0 ≤ (spectralCut x t).val*(x-(t : ℂ) • (1 : M.toStarSubalgebra))*(spectralCut x t).val := by
…

Mentions: OAI.Generator.Tracial.spectralCut

theorem OAI.Generator.Tracial.spectralCut_upper_complement line 198

Source documentation

Its complement has nonpositive shifted compression.

theorem spectralCut_upper_complement (x : M.toStarSubalgebra) (hx : IsSelfAdjoint x) (t : ℝ) :
    (1-(spectralCut x t).val)*(x-(t : ℂ) • (1 : M.toStarSubalgebra))*
      (1-(spectralCut x t).val) ≤ 0 := by
…

Mentions: OAI.Generator.Tracial.spectralCut

theorem OAI.Generator.Tracial.exists_isometric_range_factor line 212
theorem OAI.Generator.Tracial.rangeProjection_eq_closure_projection line 281
theorem OAI.Generator.Tracial.mul_closure_range_projection_eq_zero line 291
theorem OAI.Generator.Tracial.exists_polar_decomposition line 301
theorem OAI.Generator.Tracial.sqrt_rangeProjection line 353
theorem OAI.Generator.Tracial.exists_polar_with_supports line 370