OAI/Analysis/KadisonKastler/ClosedExponentialGenerator.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Recovering a small exponential generator in a closed subalgebra

The radius is absolute, independent of the ambient complex Banach algebra. This is the logarithm-series step needed for a small exact normalizer.

  1. theorem OAI.KadisonKastler.exponentialRemainder_zero line 22
  2. theorem OAI.KadisonKastler.norm_exponentialRemainder_le_third line 25
  3. theorem OAI.KadisonKastler.mem_closedSubalgebra_of_exp_mem line 34

    Source documentation

    A small element belongs to every closed complex subalgebra containing its exponential. The contraction argument supplies a uniform inverse radius.

    theorem mem_closedSubalgebra_of_exp_mem (S : Subalgebra ℂ A)
    (hS : IsClosed (S : Set A)) (x : A) (hx : ‖x‖ ≤ 1 / 16)
    (hexp : NormedSpace.exp x ∈ S) : x ∈ S := by
…