CountableStrongMembership.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Countable finite-vector tests for algebra membership

For contractions, approximation on finite prefixes of a dense vector sequence is equivalent to membership in the strongly closed target algebra, provided the test family is strongly dense in its unit ball.

theorem OAI.KadisonKastler.norm_le_iff_dense_vector_tests line 22
def OAI.KadisonKastler.CountableStrongTests line 34
theorem OAI.KadisonKastler.exists_strong_sequence_of_countable_tests line 38
theorem OAI.KadisonKastler.countableStrongTests_of_strong_sequence line 54

theorem OAI.KadisonKastler.mem_iff_countableStrongTests line 71

Source documentation

The countably quantified test predicate exactly recognizes the contractive elements of the target algebra.

theorem mem_iff_countableStrongTests (N : VonNeumannAlgebra H)
    (ξ : ℕ → H) (hξ : DenseRange ξ) (F : Set (H →L[ℂ] H))
    (hFN : F ⊆ unitBall N)
    (hFdense : ∀ T ∈ unitBall N, ∃ S : ℕ → H →L[ℂ] H,
      (∀ n, S n ∈ F) ∧ ∀ x, Tendsto (fun n => S n x) atTop (𝓝 (T x)))
    (T : H →L[ℂ] H) (hT : ‖T‖ ≤ 1) :
    T ∈ N ↔ CountableStrongTests ξ F T := by
…

Mentions: OAI.KadisonKastler.unitBall, OAI.KadisonKastler.CountableStrongTests