TomiyamaCornerGeometry.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Orthogonal-corner norm calculations

These are the elementary norm estimates behind Tomiyama's projection argument. They do not assume positivity or a representation of the algebra.

theorem OAI.KadisonKastler.norm_projection_compression_le line 18
Source documentation
Compression by a star projection is contractive.
```
theorem norm_projection_compression_le (e x : A) (he : IsStarProjection e) :
    ‖e * x * e‖ ≤ ‖x‖ := by
…
```

theorem OAI.KadisonKastler.norm_add_eq_max_of_orthogonal_products line 28

Source documentation

Two mutually orthogonal operator blocks have the maximum norm.

theorem norm_add_eq_max_of_orthogonal_products (a b : A)
    (hab : star a * b = 0) (hab' : a * star b = 0) :
    ‖a + b‖ = max ‖a‖ ‖b‖ := by
…

theorem OAI.KadisonKastler.norm_two_projection_compression_le line 57

Source documentation

The norm estimate also holds with two different projections.

theorem norm_two_projection_compression_le (e f x : A)
    (he : IsStarProjection e) (hf : IsStarProjection f) :
    ‖e * x * f‖ ≤ ‖x‖ := by
…

theorem OAI.KadisonKastler.norm_add_eq_max_opposite_corners line 70

Source documentation

An upper and a lower off-diagonal block have maximum norm.

theorem norm_add_eq_max_opposite_corners (e a b : A) (he : IsSelfAdjoint e)
    (hea : e * a = a) (hae : a * e = 0)
    (heb : e * b = 0) (hbe : b * e = b) :
    ‖a + b‖ = max ‖a‖ ‖b‖ := by
…

theorem OAI.KadisonKastler.norm_projection_add_sq_le line 87

Source documentation

A zero product with a projection gives a quadratic perturbation bound.

theorem norm_projection_add_sq_le (e z : A) (he : IsStarProjection e)
    (hze : z * e = 0) (t : ℝ) :
    ‖e + t • z‖ ^ 2 ≤ 1 + ‖z‖ ^ 2 * t ^ 2 := by
…

theorem OAI.KadisonKastler.norm_projection_add_sq_le' line 108

Source documentation

The left-product version follows by adjoints.

theorem norm_projection_add_sq_le' (e z : A) (he : IsStarProjection e)
    (hez : e * z = 0) (t : ℝ) :
    ‖e + t • z‖ ^ 2 ≤ 1 + ‖z‖ ^ 2 * t ^ 2 := by
…

theorem OAI.KadisonKastler.corner_eq_zero_of_quadratic_bounds line 121

Source documentation

Testing both real and imaginary perturbations forces a compressed first-order term to vanish.

theorem corner_eq_zero_of_quadratic_bounds (e x : A) (he : IsStarProjection e)
    (hex : e * x = x) (hxe : x * e = x) (C : ℝ)
    (h : ∀ t : ℝ, ‖e + t • x‖ ^ 2 ≤ 1 + C * t ^ 2)
    (hi : ∀ t : ℝ, ‖e + t • (Complex.I • x)‖ ^ 2 ≤ 1 + C * t ^ 2) :
    x = 0 := by
…