WeakOperatorCompactness.lean`

11 declarations, 0 contain sorry, 0 declared as axioms

Weak-operator compactness of a norm ball, obtained from compact scalar matrix-coefficient discs and the Hilbert-space representation of bounded forms.

def OAI.KadisonSimilarity.IsOperatorForm line 20
Source documentation
Algebraic identities for a matrix coefficient function, conjugate-linear in the operator's argument and linear in the test vector.
```
def IsOperatorForm (f : H → H → ℂ) : Prop :=
…
```
def OAI.KadisonSimilarity.operatorFormLinear line 26
def OAI.KadisonSimilarity.operatorOfForm line 36
Source documentation
Reconstruct an operator from a bounded sesquilinear matrix coefficient.
```
def operatorOfForm (f : H → H → ℂ) (hf : IsOperatorForm f) (R : ℝ)
    (hb : ∀ x y, ‖f x y‖ ≤ R * ‖x‖ * ‖y‖) : H →L[ℂ] H :=
…
```
Mentions: OAI.KadisonSimilarity.IsOperatorForm
theorem OAI.KadisonSimilarity.operatorOfForm_inner line 41
theorem OAI.KadisonSimilarity.norm_operatorOfForm_le line 46
theorem OAI.KadisonSimilarity.isClosed_operatorForms line 56
def OAI.KadisonSimilarity.boundedOperatorForms line 71
theorem OAI.KadisonSimilarity.isCompact_boundedOperatorForms line 75
def OAI.KadisonSimilarity.boundedFormOperator line 87
theorem OAI.KadisonSimilarity.continuous_boundedFormOperator line 91
theorem OAI.KadisonSimilarity.isCompact_weakOperator_ball line 109
Source documentation
The closed norm ball in bounded operators on a Hilbert space is compact in the weak-operator topology.
```
theorem isCompact_weakOperator_ball (R : ℝ) (hR : 0 ≤ R) :
    IsCompact {T : H →WOT[ℂ] H | ‖toCLM T‖ ≤ R} := by
…
```