TomiyamaNormGeometry.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Norm geometry used in the projection theorem

A quadratic norm bound at the identity of a corner forces the real first-order term to vanish. This is the elementary norm argument in Tomiyama's proof, separated from any operator-field representation.

theorem OAI.KadisonKastler.le_zero_of_inverse_bounds line 27
theorem OAI.KadisonKastler.corner_real_term_nonpos line 34

theorem OAI.KadisonKastler.corner_skewAdjoint_of_quadratic_bound line 87

Source documentation

A quadratic norm bound at a projection makes a corner element skew-adjoint. This also applies to the zero corner.

theorem corner_skewAdjoint_of_quadratic_bound (p x : B) (hp : IsStarProjection p)
    (hpx : p * x = x) (hxp : x * p = x) (C : ℝ)
    (h : ∀ t : ℝ, ‖p + t • x‖ ^ 2 ≤ 1 + C * t ^ 2) :
    star x = -x := by
…

theorem OAI.KadisonKastler.isSelfAdjoint_of_quadratic_norm_bound line 102
Source documentation
Applying the tangent argument to the imaginary multiple detects self-adjointness using only the norm.
```
theorem isSelfAdjoint_of_quadratic_norm_bound (x : B) (C : ℝ)
    (h : ∀ t : ℝ, ‖1 + t • (Complex.I • x)‖ ^ 2 ≤ 1 + C * t ^ 2) :
    IsSelfAdjoint x := by
…
```