FieldWeakClosure.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Von Neumann closure of actual operator fields

A common subsequence on countably many constant L² columns turns strong operator convergence into pointwise strong convergence almost everywhere. The uniform norm bound extends convergence from the dense columns to every fiber vector. Bicommutant closure then proves fiber membership.

theorem OAI.KadisonSimilarity.strong_tendsto_of_bounded_dense_columns line 25

Source documentation

Uniformly bounded operators converge strongly once they converge on a fixed countable dense set.

theorem strong_tendsto_of_bounded_dense_columns
    (T : ℕ → H →L[ℂ] H) (S : H →L[ℂ] H) (C : ℝ)
    (hbound : ∀ n, ‖T n‖ ≤ C)
    (hcol : ∀ j, Tendsto (fun n => T n (TopologicalSpace.denseSeq H j))
      atTop (𝓝 (S (TopologicalSpace.denseSeq H j)))) :
    ∀ x : H, Tendsto (fun n => T n x) atTop (𝓝 (S x)) := by
…

theorem OAI.KadisonSimilarity.vonNeumann_mem_of_strong_tendsto line 47

Source documentation

Strong limits preserve von Neumann membership directly by commuting with every member of the commutant.

theorem vonNeumann_mem_of_strong_tendsto
    (P : VonNeumannAlgebra H) (T : ℕ → H →L[ℂ] H) (S : H →L[ℂ] H)
    (hmem : ∀ n, T n ∈ P)
    (hlim : ∀ x : H, Tendsto (fun n => T n x) atTop (𝓝 (S x))) : S ∈ P := by
…

theorem OAI.KadisonSimilarity.ae_field_mem_of_strong_approximation line 70

Source documentation

Fiber membership is inherited from uniformly bounded strong approximants on L². The pointwise action hypotheses are per fixed vector, so no uncountable intersection of conull sets is used.

theorem ae_field_mem_of_strong_approximation
    (P : Ω → VonNeumannAlgebra H)
    (T : ℕ → Lp H 2 μ →L[ℂ] Lp H 2 μ) (S : Lp H 2 μ →L[ℂ] Lp H 2 μ)
    (R : ℕ → Ω → H →L[ℂ] H) (Q : Ω → H →L[ℂ] H)
    (haction : ∀ n (f : Lp H 2 μ), ∀ᵐ a ∂μ, T n f a = R n a (f a))
    (hS : ∀ f : Lp H 2 μ, ∀ᵐ a ∂μ, S f a = Q a (f a))
    (hstrong : ∀ f : Lp H 2 μ, Tendsto (fun n => T n f) atTop (𝓝 (S f)))
    (C : ℝ) (hbound : ∀ n, ∀ᵐ a ∂μ, ‖R n a‖ ≤ C)
    (hmem : ∀ n, ∀ᵐ a ∂μ, R n a ∈ P a) :
    ∀ᵐ a ∂μ, Q a ∈ P a := by
…

theorem OAI.KadisonSimilarity.ae_field_mem_of_norm_bounded_strong_approximation line 110

Source documentation

In applications the uniform bound is a norm bound on the actual approximating operators; the pointwise bound is then derived.

theorem ae_field_mem_of_norm_bounded_strong_approximation
    (P : Ω → VonNeumannAlgebra H)
    (T : ℕ → Lp H 2 μ →L[ℂ] Lp H 2 μ) (S : Lp H 2 μ →L[ℂ] Lp H 2 μ)
    (R : ℕ → Ω → H →L[ℂ] H) (Q : Ω → H →L[ℂ] H)
    (haction : ∀ n (f : Lp H 2 μ), ∀ᵐ a ∂μ, T n f a = R n a (f a))
    (hS : ∀ f : Lp H 2 μ, ∀ᵐ a ∂μ, S f a = Q a (f a))
    (hstrong : ∀ f : Lp H 2 μ, Tendsto (fun n => T n f) atTop (𝓝 (S f)))
    (C : ℝ) (hC : 0 ≤ C) (hbound : ∀ n, ‖T n‖ ≤ C)
    (hmem : ∀ n, ∀ᵐ a ∂μ, R n a ∈ P a) :
    ∀ᵐ a ∂μ, Q a ∈ P a :=
…