ClippedPairingBound.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Averaged pairings controlled by bounded algebra elements

theorem OAI.KadisonKastler.pairing_le_of_unitBall line 21

Source documentation

Rescaling the two algebra arguments extends a unit-ball pairing bound to any fixed operator-norm ball.

theorem pairing_le_of_unitBall (J : A →ₗ[ℂ] H) (V : H →L[ℂ] H) {K s : ℝ}
    (hK : ∀ a b : A, ‖a‖ ≤ 1 → ‖b‖ ≤ 1 → ‖inner ℂ (V (J a)) (J b)‖ ≤ K)
    (hs : 0 < s) (a b : A) (ha : ‖a‖ ≤ s) (hb : ‖b‖ ≤ s) :
    ‖inner ℂ (V (J a)) (J b)‖ ≤ s ^ 2 * K := by
…

theorem OAI.KadisonKastler.averaged_pairing_le_of_fourth_moments line 51

Source documentation

The two tracial clipping errors are controlled in root mean square, while the retained pairing is tested entirely on bounded elements.

theorem averaged_pairing_le_of_fourth_moments (τ : FaithfulTracialState A)
    (J : A →ₗ[ℂ] H) (hJ : ∀ a, ‖J a‖ = traceTwoNorm τ a)
    (V : H →L[ℂ] H) (a b : ι → A) {K s : ℝ} (hs : 0 < s)
    (hK : ∀ x y : A, ‖x‖ ≤ 1 → ‖y‖ ≤ 1 → ‖inner ℂ (V (J x)) (J y)‖ ≤ K)
    (ha₂ : (𝔼 i, traceTwoNorm τ (a i) ^ 2) ≤ 1)
    (hb₂ : (𝔼 i, traceTwoNorm τ (b i) ^ 2) ≤ 1)
    (ha₄ : (𝔼 i, (τ.toLinearMap ((star (a i) * a i) ^ 2)).re) ≤ 12)
    (hb₄ : (𝔼 i, (τ.toLinearMap ((star (b i) * b i) ^ 2)).re) ≤ 12) :
    ‖𝔼 i, inner ℂ (V (J (a i))) (J (b i))‖ ≤
      s ^ 2 * K + (2 * Real.sqrt 12 / s) * ‖V‖ := by
…

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

theorem OAI.KadisonKastler.averaged_pairing_le_one_ninety_two line 132

Source documentation

The cutoff 4 * sqrt 12 makes the two error terms half of the operator norm, with retained-pairing coefficient 192.

theorem averaged_pairing_le_one_ninety_two (τ : FaithfulTracialState A)
    (J : A →ₗ[ℂ] H) (hJ : ∀ a, ‖J a‖ = traceTwoNorm τ a)
    (V : H →L[ℂ] H) (a b : ι → A) {K : ℝ}
    (hK : ∀ x y : A, ‖x‖ ≤ 1 → ‖y‖ ≤ 1 → ‖inner ℂ (V (J x)) (J y)‖ ≤ K)
    (ha₂ : (𝔼 i, traceTwoNorm τ (a i) ^ 2) ≤ 1)
    (hb₂ : (𝔼 i, traceTwoNorm τ (b i) ^ 2) ≤ 1)
    (ha₄ : (𝔼 i, (τ.toLinearMap ((star (a i) * a i) ^ 2)).re) ≤ 12)
    (hb₄ : (𝔼 i, (τ.toLinearMap ((star (b i) * b i) ^ 2)).re) ≤ 12) :
    ‖𝔼 i, inner ℂ (V (J (a i))) (J (b i))‖ ≤ 192 * K + ‖V‖ / 2 := by
…

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