RegularWeightedIntegral.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Integrable scalar weights on bounded operator fields

Vectorwise integration needs only strong measurability on each vector. An integrable scalar weight therefore defines a bounded operator, and commutation and von Neumann algebra membership pass to this operator. This applies in particular to the compactly weighted convolution operators in the regular representation.

theorem OAI.KadisonKastler.integrable_weighted_operator_vector line 24
theorem OAI.KadisonKastler.norm_integral_weighted_operator_vector_le line 40

def OAI.KadisonKastler.weightedOperatorIntegral line 56

Source documentation

Integrating an integrably weighted, uniformly bounded field on vectors.

def weightedOperatorIntegral
    (μ : Measure S) (w : S → ℂ) (hw : Integrable w μ)
    (F : S → H →L[ℂ] H)
    (hm : ∀ x, AEStronglyMeasurable (fun t => F t x) μ)
    (C : ℝ) (hb : ∀ᵐ t ∂μ, ‖F t‖ ≤ C) : H →L[ℂ] H :=
…

theorem OAI.KadisonKastler.weightedOperatorIntegral_apply line 75
theorem OAI.KadisonKastler.norm_weightedOperatorIntegral_le line 83
theorem OAI.KadisonKastler.weightedOperatorIntegral_commutes line 93

theorem OAI.KadisonKastler.weightedOperatorIntegral_mem line 112

Source documentation

Membership is checked against the commutant, with no norm-topology measurability assumption on the operator field.

theorem weightedOperatorIntegral_mem
    (μ : Measure S) (w : S → ℂ) (hw : Integrable w μ)
    (F : S → H →L[ℂ] H)
    (hm : ∀ x, AEStronglyMeasurable (fun t => F t x) μ)
    (C : ℝ) (hb : ∀ᵐ t ∂μ, ‖F t‖ ≤ C) (M : VonNeumannAlgebra H)
    (hM : ∀ᵐ t ∂μ, F t ∈ M) :
    weightedOperatorIntegral μ w hw F hm C hb ∈ M := by
…

Mentions: OAI.KadisonKastler.weightedOperatorIntegral