ProbabilityOperatorRelations.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Linear relations and commutator bounds under vector integration

The operator fields are only assumed measurable on each vector. Fixed left and right multiplication commute with their probability integral; essential operator-norm commutator bounds therefore pass to the integral.

theorem OAI.KadisonKastler.ae_norm_operator_sandwich_le line 23

Source documentation

An explicit bound for a fixed sandwich of a bounded field.

theorem ae_norm_operator_sandwich_le
    (μ : Measure S) (F : S → H →L[ℂ] H) {C : ℝ}
    (hF : ∀ᵐ s ∂μ, ‖F s‖ ≤ C) (A B : H →L[ℂ] H) :
    ∀ᵐ s ∂μ, ‖A * F s * B‖ ≤ ‖A‖ * C * ‖B‖ := by
…

theorem OAI.KadisonKastler.probabilityOperatorIntegral_sandwich line 35

Source documentation

Fixed operator multiplication commutes with the actual vector integral.

theorem probabilityOperatorIntegral_sandwich
    (μ : Measure S) [IsProbabilityMeasure μ]
    (F : S → H →L[ℂ] H) (hF : ∀ x, AEStronglyMeasurable (fun s => F s x) μ)
    (C : ℝ) (hC : ∀ᵐ s ∂μ, ‖F s‖ ≤ C) (A B : H →L[ℂ] H) :
    probabilityOperatorIntegral μ (fun s => A * F s * B)
      (fun x => A.continuous.comp_aestronglyMeasurable (hF (B x)))
      (‖A‖ * C * ‖B‖) (ae_norm_operator_sandwich_le μ F hC A B) =
      A * probabilityOperatorIntegral μ F hF C hC * B := by
…

Mentions: OAI.KadisonKastler.probabilityOperatorIntegral, OAI.KadisonKastler.ae_norm_operator_sandwich_le

theorem OAI.KadisonKastler.norm_probabilityOperatorIntegral_commutator_le line 49

Source documentation

A uniform almost-everywhere commutator bound survives vector integration.

theorem norm_probabilityOperatorIntegral_commutator_le
    (μ : Measure S) [IsProbabilityMeasure μ]
    (F : S → H →L[ℂ] H) (hF : ∀ x, AEStronglyMeasurable (fun s => F s x) μ)
    (C : ℝ) (hC : ∀ᵐ s ∂μ, ‖F s‖ ≤ C) (A : H →L[ℂ] H)
    {ε : ℝ} (hε : 0 ≤ ε)
    (hcomm : ∀ᵐ s ∂μ, ‖F s * A - A * F s‖ ≤ ε) :
    ‖probabilityOperatorIntegral μ F hF C hC * A -
      A * probabilityOperatorIntegral μ F hF C hC‖ ≤ ε := by
…

Mentions: OAI.KadisonKastler.probabilityOperatorIntegral

theorem OAI.KadisonKastler.norm_commutator_of_near_commuting line 73

Source documentation

An algebra approximation bounds every commutator with its commutant.

theorem norm_commutator_of_near_commuting
    (T b A : H →L[ℂ] H) {δ : ℝ} (hTb : ‖T - b‖ ≤ δ)
    (hbA : b * A = A * b) : ‖T * A - A * T‖ ≤ 2 * δ * ‖A‖ := by
…

theorem OAI.KadisonKastler.norm_probabilityOperatorIntegral_commutator_of_near line 90

Source documentation

This estimate requires no measurable choice of nearby algebra elements.

theorem norm_probabilityOperatorIntegral_commutator_of_near
    (μ : Measure S) [IsProbabilityMeasure μ]
    (F : S → H →L[ℂ] H) (hF : ∀ x, AEStronglyMeasurable (fun s => F s x) μ)
    (C : ℝ) (hC : ∀ᵐ s ∂μ, ‖F s‖ ≤ C) (A : H →L[ℂ] H)
    {δ : ℝ} (hδ : 0 ≤ δ)
    (hnear : ∀ᵐ s ∂μ, ∃ b : H →L[ℂ] H, b * A = A * b ∧ ‖F s - b‖ ≤ δ) :
    ‖probabilityOperatorIntegral μ F hF C hC * A -
      A * probabilityOperatorIntegral μ F hF C hC‖ ≤ 2 * δ * ‖A‖ := by
…

Mentions: OAI.KadisonKastler.probabilityOperatorIntegral