KaplanskySelfAdjoint.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Self-adjoint strong approximation

This is the first step in discharging bounded density. The existing bicommutant theorem gives unbounded strong approximation. Taking real parts preserves weak convergence; orthogonal complements of the finite tuple orbit then recover strong approximation by self-adjoint elements.

theorem OAI.KadisonKastler.inner_realPart line 26

theorem OAI.KadisonKastler.tendsto_inner_realPart_of_strong line 38

Source documentation

Strong convergence implies weak convergence of the real parts, even when no uniform norm bound on the original net is available.

theorem tendsto_inner_realPart_of_strong
    {ι : Type*} {l : Filter ι} {a : ι → H →L[ℂ] H} {T : H →L[ℂ] H}
    (ha : ∀ x, Tendsto (fun i => a i x) l (𝓝 (T x))) (x y : H) :
    Tendsto (fun i => inner ℂ y ((realPart (a i) : H →L[ℂ] H) x)) l
      (𝓝 (inner ℂ y ((realPart T : H →L[ℂ] H) x))) := by
…

def OAI.KadisonKastler.selfAdjointTupleMap line 47

theorem OAI.KadisonKastler.selfAdjoint_bicommutant_tuple_mem_closure line 59

Source documentation

The finite tuple of values of a self-adjoint bicommutant element lies in the real-linear closure of the self-adjoint algebra orbit.

theorem selfAdjoint_bicommutant_tuple_mem_closure
    {ι : Type*} [Fintype ι] (A : StarSubalgebra ℂ (H →L[ℂ] H))
    (T : H →L[ℂ] H) (hT : T ∈ Set.centralizer (Set.centralizer (A : Set (H →L[ℂ] H))))
    (hsa : IsSelfAdjoint T) (x : FiniteHilbert ι H) :
    diagonalOperator T x ∈ (selfAdjointTupleMap A x).range.topologicalClosure := by
…

Mentions: OAI.KadisonKastler.selfAdjointTupleMap

theorem OAI.KadisonKastler.selfAdjoint_bicommutant_finite_strong_approximation line 98

Source documentation

Finite strong tests can be met by a self-adjoint element of the original algebra. This step has no bounded-density hypothesis.

theorem selfAdjoint_bicommutant_finite_strong_approximation
    (A : StarSubalgebra ℂ (H →L[ℂ] H)) (T : H →L[ℂ] H)
    (hT : T ∈ Set.centralizer (Set.centralizer (A : Set (H →L[ℂ] H))))
    (hsa : IsSelfAdjoint T) (V : Finset H) {ε : ℝ} (hε : 0 < ε) :
    ∃ a : A, IsSelfAdjoint (a : H →L[ℂ] H) ∧
      ∀ x ∈ V, ‖T x - (a : H →L[ℂ] H) x‖ < ε := by
…

theorem OAI.KadisonKastler.selfAdjoint_bicommutant_exists_strong_net line 118

Source documentation

A self-adjoint strongly convergent net, indexed independently of any norm bound. Bounded transforms will supply the missing norm control.

theorem selfAdjoint_bicommutant_exists_strong_net
    (A : StarSubalgebra ℂ (H →L[ℂ] H)) (T : H →L[ℂ] H)
    (hT : T ∈ Set.centralizer (Set.centralizer (A : Set (H →L[ℂ] H))))
    (hsa : IsSelfAdjoint T) :
    ∃ a : Finset H × ℕ → A,
      (∀ i, IsSelfAdjoint (a i : H →L[ℂ] H)) ∧
      ∀ x : H, Tendsto (fun i => (a i : H →L[ℂ] H) x) atTop (𝓝 (T x)) := by
…