NormalizerLogarithm.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

The logarithm of a small normalizer preserves the algebra

The bounded operators preserving a closed linear subspace form a closed subalgebra. Uniform exponential inversion recovers the commutator generator inside that subalgebra.

def OAI.KadisonKastler.preservingOperatorAlgebra line 21
Source documentation
Bounded maps on the ambient operator algebra preserving P.
```
def preservingOperatorAlgebra (P : VonNeumannAlgebra H) :
    Subalgebra ℂ ((H →L[ℂ] H) →L[ℂ] (H →L[ℂ] H)) where
…
```
theorem OAI.KadisonKastler.preservingOperatorAlgebra_isClosed line 33

theorem OAI.KadisonKastler.commutator_mem_of_small_expUnitary_normalizes line 47

Source documentation

In the absolute logarithm radius, conjugation invariance implies invariance under the bounded commutator.

theorem commutator_mem_of_small_expUnitary_normalizes
    (P : VonNeumannAlgebra H) (h : selfAdjoint (H →L[ℂ] H))
    (hsmall : ‖(h : H →L[ℂ] H)‖ ≤ 1 / 32)
    (hnormalizes : Conjugates (H := H) (selfAdjoint.expUnitary h) P P) :
…

Mentions: OAI.KadisonKastler.Conjugates

theorem OAI.KadisonKastler.exists_small_normalizer_log line 81
Source documentation
The controlled principal logarithm of a sufficiently small exact normalizer implements a derivation of the algebra.
```
theorem exists_small_normalizer_log (P : VonNeumannAlgebra H)
    (v : unitary (H →L[ℂ] H)) (hv : Conjugates (H := H) v P P)
…
```
Mentions: OAI.KadisonKastler.Conjugates