OAI/Analysis/KadisonKastler/FiniteCovariancePairing.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.KadisonKastler.normalized_sign_second_moment_le_one line 21
2. theorem OAI.KadisonKastler.pairing_le_of_finite_covariances line 34

   Source documentation

   A balanced family has a bounded fourth moment after sign randomization. Clipping then controls its common pairing by unit-ball tests.

   theorem pairing_le_of_finite_covariances (τ : FaithfulTracialState A)
       (J : A →ₗ[ℂ] H) (hJ : ∀ x, ‖J x‖ = traceTwoNorm τ x)
       (V : H →L[ℂ] H) (a b : ι → A) {z : ℂ} {K : ℝ}
       (hK : ∀ x y : A, ‖x‖ ≤ 1 → ‖y‖ ≤ 1 → ‖inner ℂ (V (J x)) (J y)‖ ≤ K)
       (ha : ∀ i, traceTwoNorm τ (a i) ≤ 1)
       (hb : ∀ i, traceTwoNorm τ (b i) ≤ 1)
       (hQa : traceTwoNorm τ (finiteSignRightCovariance a) ≤ 2)
       (hLa : traceTwoNorm τ (finiteSignLeftCovariance a) ≤ 2)
       (hQb : traceTwoNorm τ (finiteSignRightCovariance b) ≤ 2)
       (hLb : traceTwoNorm τ (finiteSignLeftCovariance b) ≤ 2)
       (hz : ∀ i, inner ℂ (V (J (a i))) (J (b i)) = z) :
       ‖z‖ ≤ 192 * K + ‖V‖ / 2 := by
   …

   Mentions: OAI.KadisonKastler.FaithfulTracialState, OAI.KadisonKastler.traceTwoNorm, OAI.KadisonKastler.finiteSignRightCovariance, OAI.KadisonKastler.finiteSignLeftCovariance

3. theorem OAI.KadisonKastler.opNorm_le_of_finite_covariance_families line 62

   Source documentation

   Once finite families with the stated covariance bounds have been constructed for each pair of tracial unit vectors, the bounded-ball test constant is 384. The family construction is kept as a separate task.

   theorem opNorm_le_of_finite_covariance_families (τ : FaithfulTracialState A)
       (J : A →ₗ[ℂ] H) (hJ : ∀ x, ‖J x‖ = traceTwoNorm τ x)
       (hJdense : DenseRange J) (V : H →L[ℂ] H) {K : ℝ}
       (hK : ∀ x y : A, ‖x‖ ≤ 1 → ‖y‖ ≤ 1 → ‖inner ℂ (V (J x)) (J y)‖ ≤ K)
       (hfamilies : ∀ a b : A, traceTwoNorm τ a ≤ 1 → traceTwoNorm τ b ≤ 1 →
         ∃ n : ℕ, 0 < n ∧ ∃ f g : Fin n → A,
           (∀ i, traceTwoNorm τ (f i) ≤ 1) ∧
           (∀ i, traceTwoNorm τ (g i) ≤ 1) ∧
           traceTwoNorm τ (finiteSignRightCovariance f) ≤ 2 ∧
           traceTwoNorm τ (finiteSignLeftCovariance f) ≤ 2 ∧
           traceTwoNorm τ (finiteSignRightCovariance g) ≤ 2 ∧
           traceTwoNorm τ (finiteSignLeftCovariance g) ≤ 2 ∧
   …

   Mentions: OAI.KadisonKastler.FaithfulTracialState, OAI.KadisonKastler.traceTwoNorm, OAI.KadisonKastler.finiteSignRightCovariance, OAI.KadisonKastler.finiteSignLeftCovariance