CommutantTopology.lean`

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Hyperinvariant.mem_commutant_iff line 15
Source documentation
Membership is commutation in all bounded operators on H.
```
theorem mem_commutant_iff (T A : H →L[ℂ] H) :
    A ∈ commutant T ↔ A * T = T * A := by
…
```
Mentions: OAI.Hyperinvariant.commutant
theorem OAI.Hyperinvariant.commutant_isClosed_strong line 21
Source documentation
The ordinary commutant is closed for the pointwise-norm strong-operator topology.
```
theorem commutant_isClosed_strong [CompleteSpace H] (T : H →L[ℂ] H) :
    @IsClosed (H →L[ℂ] H) strongOperatorTopology (commutant T : Set (H →L[ℂ] H)) := by
…
```
Mentions: OAI.Hyperinvariant.strongOperatorTopology, OAI.Hyperinvariant.commutant
theorem OAI.Hyperinvariant.scalar_of_commutant_top line 42
Source documentation
If an operator commutes with every bounded operator, it is scalar. The center is scalar because the continuous dual separates points.
```
theorem scalar_of_commutant_top [CompleteSpace H] (T : H →L[ℂ] H)
    (h : commutant T = ⊤) :
    ∃ c : ℂ, algebraMap ℂ (H →L[ℂ] H) c = T := by
…
```
Mentions: OAI.Hyperinvariant.commutant
theorem OAI.Hyperinvariant.commutant_ne_top_of_nonzero_quasinilpotent line 56
Source documentation
Nonzero norm-quasinilpotence excludes scalar bounded operators. This uses the actual root-norm limit from the statement, not a spectral surrogate.
```
theorem commutant_ne_top_of_nonzero_quasinilpotent [CompleteSpace H] [Nontrivial H]
    (T : H →L[ℂ] H) (hT : T ≠ 0)
    (hlim : Tendsto (fun n : ℕ => ‖T ^ n‖ ^ (1 / (n : ℝ))) atTop (𝓝 0)) :
    commutant T ≠ ⊤ := by
…
```
Mentions: OAI.Hyperinvariant.commutant
theorem OAI.Hyperinvariant.fullClaim_of_mainClaim line 78
Source documentation
Adds the two generic commutant conclusions to a genuine main witness.
```
theorem fullClaim_of_mainClaim [Nontrivial H] (h : MainClaim (H := H)) :
…
```
Mentions: OAI.Hyperinvariant.MainClaim