RightBoundedVector.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Constructing a commutant operator from a bounded right vector

A bound on the map a Ω ↦ a ξ gives its continuous extension. Density makes the extension commute with the represented algebra and unique. This is the bounded-vector bridge for the modular commutant argument.

def OAI.KadisonKastler.rightVectorOperator line 21
Source documentation
Extension of right multiplication, whenever its algebra-vector bound holds.
```
def rightVectorOperator : H →L[ℂ] H :=
…
```
theorem OAI.KadisonKastler.rightVectorOperator_apply line 29
theorem OAI.KadisonKastler.rightVectorOperator_norm_le line 34
theorem OAI.KadisonKastler.rightVectorOperator_vector line 38
theorem OAI.KadisonKastler.rightVectorOperator_mem_commutant line 43

theorem OAI.KadisonKastler.commutant_operator_eq_of_vector line 59

Source documentation

A commutant operator is determined by its value at a cyclic vector.

theorem commutant_operator_eq_of_vector {S T : H →L[ℂ] H}
    (hS : S ∈ M.commutant) (hT : T ∈ M.commutant) (he : S Ω = T Ω) : S = T := by
…

theorem OAI.KadisonKastler.exists_commutant_operator_iff_vector_bound line 76
Source documentation
The right-vector estimate is equivalent to an actual bounded operator in the commutant.
```
theorem exists_commutant_operator_iff_vector_bound :
    (∃ T : H →L[ℂ] H, T ∈ M.commutant ∧ ‖T‖ ≤ C ∧ T Ω = ξ) ↔
      ∀ a : Algebra M, ‖a.val ξ‖ ≤ C * ‖a.val Ω‖ := by
…
```
Mentions: OAI.KadisonKastler.Algebra