FiniteBimodularBound.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Bounded-ball tests for bimodular operators

Relative scalar averaging supplies the finite covariance families. The left and right unitary actions then preserve their pairings, so the proved sign-randomization and clipping estimate applies with constant 384.

theorem OAI.KadisonKastler.norm_trace_square_le_one line 22
theorem OAI.KadisonKastler.norm_trace_square_reverse_le_one line 28

theorem OAI.KadisonKastler.exists_finite_bimodular_covariance_families line 36

Source documentation

Irreducibility and bimodularity produce the actual finite families required for covariance testing.

theorem exists_finite_bimodular_covariance_families
    (τ : FaithfulTracialState (Algebra M)) (J : Algebra M →ₗ[ℂ] E)
    (hJ : ∀ x, ‖J x‖ = traceTwoNorm τ x) (hτ : FiniteVectorTrace τ)
    (φ : R →⋆ₐ[ℂ] Algebra M)
    (hirr : ∀ b : Algebra M, (∀ r : R, φ r * b = b * φ r) →
      ∃ c : ℂ, b = c • (1 : Algebra M))
    (V : E →L[ℂ] E) (L Q : unitary R → unitary (E →L[ℂ] E))
    (hL : ∀ (u : unitary R) (x : Algebra M), J (φ u * x) = (L u : E →L[ℂ] E) (J x))
    (hQ : ∀ (u : unitary R) (x : Algebra M), J (x * φ u) = (Q u : E →L[ℂ] E) (J x))
    (hVL : ∀ u, Commute V (L u : E →L[ℂ] E))
    (hVQ : ∀ u, Commute V (Q u : E →L[ℂ] E))
    (a b : Algebra M) (ha : traceTwoNorm τ a ≤ 1) (hb : traceTwoNorm τ b ≤ 1) :
…

Mentions: OAI.KadisonKastler.FaithfulTracialState, OAI.KadisonKastler.Algebra, OAI.KadisonKastler.traceTwoNorm, OAI.KadisonKastler.FiniteVectorTrace

theorem OAI.KadisonKastler.opNorm_le_of_irreducible_bimodular_tests line 93

Source documentation

Unit-ball tests control a bounded bimodular operator on the trace Hilbert realization, with the manuscript's constant 384.

theorem opNorm_le_of_irreducible_bimodular_tests
    (τ : FaithfulTracialState (Algebra M)) (J : Algebra M →ₗ[ℂ] E)
    (hJ : ∀ x, ‖J x‖ = traceTwoNorm τ x) (hJdense : DenseRange J)
    (hτ : FiniteVectorTrace τ) (φ : R →⋆ₐ[ℂ] Algebra M)
    (hirr : ∀ b : Algebra M, (∀ r : R, φ r * b = b * φ r) →
      ∃ c : ℂ, b = c • (1 : Algebra M))
    (V : E →L[ℂ] E) (L Q : unitary R → unitary (E →L[ℂ] E))
    (hL : ∀ (u : unitary R) (x : Algebra M), J (φ u * x) = (L u : E →L[ℂ] E) (J x))
    (hQ : ∀ (u : unitary R) (x : Algebra M), J (x * φ u) = (Q u : E →L[ℂ] E) (J x))
    (hVL : ∀ u, Commute V (L u : E →L[ℂ] E))
    (hVQ : ∀ u, Commute V (Q u : E →L[ℂ] E)) {K : ℝ}
    (hK : ∀ x y : Algebra M, ‖x‖ ≤ 1 → ‖y‖ ≤ 1 →
…

Mentions: OAI.KadisonKastler.FaithfulTracialState, OAI.KadisonKastler.Algebra, OAI.KadisonKastler.traceTwoNorm, OAI.KadisonKastler.FiniteVectorTrace