OAI/Analysis/KadisonKastler/ProbabilityOperatorAlgebra.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.KadisonKastler.integrable_bounded_operator_vector line 17
2. theorem OAI.KadisonKastler.probabilityOperatorIntegral_commutes line 26

   Source documentation

   Every fixed commutation relation passes to the actual vector integral.

   theorem probabilityOperatorIntegral_commutes (μ : Measure S) [IsProbabilityMeasure μ]
       (F : S → H →L[ℂ] H) (hm : ∀ x, AEStronglyMeasurable (fun s => F s x) μ)
       (C : ℝ) (hb : ∀ᵐ s ∂μ, ‖F s‖ ≤ C) (T : H →L[ℂ] H)
       (hT : ∀ᵐ s ∂μ, F s * T = T * F s) :
       probabilityOperatorIntegral μ F hm C hb * T =
         T * probabilityOperatorIntegral μ F hm C hb := by
   …

   Mentions: OAI.KadisonKastler.probabilityOperatorIntegral

3. theorem OAI.KadisonKastler.probabilityOperatorIntegral_mem line 41

   Source documentation

   Von Neumann algebra membership is retained without any norm measurability hypothesis on the field.

   theorem probabilityOperatorIntegral_mem (μ : Measure S) [IsProbabilityMeasure μ]
       (F : S → H →L[ℂ] H) (hm : ∀ x, AEStronglyMeasurable (fun s => F s x) μ)
       (C : ℝ) (hb : ∀ᵐ s ∂μ, ‖F s‖ ≤ C) (M : VonNeumannAlgebra H)
       (hM : ∀ᵐ s ∂μ, F s ∈ M) : probabilityOperatorIntegral μ F hm C hb ∈ M := by
   …

   Mentions: OAI.KadisonKastler.probabilityOperatorIntegral