CountableFiberTests.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

One conull set for the scalar fiber estimates

A countable family of contraction tests gives a common conull set. Weak operator density then extends the bound to every contraction in each fiber. This is the countability step in the central-decomposition argument; the existence and density of the measurable sections remain explicit data.

theorem OAI.KadisonSimilarity.commutator_bound_of_weak_closure line 22

Source documentation

A commutator bound extends from a set of operators to its weak closure.

theorem commutator_bound_of_weak_closure (Y T : H →L[ℂ] H)
    (S : Set (H →L[ℂ] H)) {c : ℝ} (hc : 0 ≤ c)
    (hbound : ∀ X ∈ S, ‖commutator Y X‖ ≤ c)
    (hT : ofCLM T ∈ closure (ofCLM '' S)) : ‖commutator Y T‖ ≤ c := by
…

Mentions: OAI.KadisonSimilarity.commutator

theorem OAI.KadisonSimilarity.scalarCommutatorNorm_le_of_weak_dense_tests line 34

Source documentation

Weakly dense contraction tests control the full scalar commutator norm.

theorem scalarCommutatorNorm_le_of_weak_dense_tests
    (P : VonNeumannAlgebra H) (Y : H →L[ℂ] H)
    (test : ℕ → H →L[ℂ] H)
    (hdense : ∀ X : H →L[ℂ] H, X ∈ P → ‖X‖ ≤ 1 →
      ofCLM X ∈ closure (Set.range fun n => ofCLM (test n)))
    {c : ℝ} (hc : 0 ≤ c) (hbound : ∀ n, ‖commutator Y (test n)‖ ≤ c) :
    scalarCommutatorNorm P Y ≤ c := by
…

Mentions: OAI.KadisonSimilarity.commutator, OAI.KadisonSimilarity.scalarCommutatorNorm

theorem OAI.KadisonSimilarity.ae_scalarCommutatorNorm_le_of_countable_tests line 57

Source documentation

Countably many almost-everywhere test inequalities hold simultaneously. Density on each remaining fiber gives its full scalar commutator bound.

theorem ae_scalarCommutatorNorm_le_of_countable_tests
    (P : ∀ a, VonNeumannAlgebra (K a))
    (Y : ∀ a, K a →L[ℂ] K a) (test : ∀ a, ℕ → K a →L[ℂ] K a)
    (hdense : ∀ᵐ a ∂μ, ∀ X : K a →L[ℂ] K a, X ∈ P a → ‖X‖ ≤ 1 →
      ofCLM X ∈ closure (Set.range fun n => ofCLM (test a n)))
    {c : ℝ} (hc : 0 ≤ c)
    (hbound : ∀ n, ∀ᵐ a ∂μ, ‖commutator (Y a) (test a n)‖ ≤ c) :
    ∀ᵐ a ∂μ, scalarCommutatorNorm (P a) (Y a) ≤ c := by
…

Mentions: OAI.KadisonSimilarity.commutator, OAI.KadisonSimilarity.scalarCommutatorNorm