WeakOperatorIntegral.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

Weak operator integrals built from scalar integrals. In particular this permits averaging a strongly continuous unitary action without assuming continuity in the operator norm.

def OAI.KadisonSimilarity.WeaklyIntegrable line 20
Source documentation
Integrability of the scalar matrix coefficients of an operator field.
```
def WeaklyIntegrable (A : X → H →L[ℂ] H) : Prop :=
…
```
def OAI.KadisonSimilarity.integralOperatorForm line 23
theorem OAI.KadisonSimilarity.isOperatorForm_integral line 27
theorem OAI.KadisonSimilarity.norm_integralOperatorForm_le line 44
def OAI.KadisonSimilarity.weakOperatorIntegral line 56
Source documentation
The weak integral of a uniformly bounded, weakly integrable field.
```
def weakOperatorIntegral (A : X → H →L[ℂ] H) (hA : WeaklyIntegrable μ A)
    (R : ℝ) (hbound : ∀ g, ‖A g‖ ≤ R) : H →L[ℂ] H :=
…
```
Mentions: OAI.KadisonSimilarity.WeaklyIntegrable
theorem OAI.KadisonSimilarity.weakOperatorIntegral_inner line 61
theorem OAI.KadisonSimilarity.norm_weakOperatorIntegral_le line 66

theorem OAI.KadisonSimilarity.weakOperatorIntegral_sandwich_inner line 72

Source documentation

Left and right multiplication may be passed through the weak integral.

theorem weakOperatorIntegral_sandwich_inner (A : X → H →L[ℂ] H)
    (hA : WeaklyIntegrable μ A) (R : ℝ) (hbound : ∀ g, ‖A g‖ ≤ R)
    (B C : H →L[ℂ] H) (x y : H) :
    inner ℂ ((B * weakOperatorIntegral μ A hA R hbound * C) x) y =
      ∫ g, inner ℂ ((B * A g * C) x) y ∂μ := by
…

Mentions: OAI.KadisonSimilarity.WeaklyIntegrable, OAI.KadisonSimilarity.weakOperatorIntegral

theorem OAI.KadisonSimilarity.weakOperatorIntegral_commutator_inner line 84

Source documentation

A commutator with a fixed operator may be passed through the weak integral.

theorem weakOperatorIntegral_commutator_inner (A : X → H →L[ℂ] H)
    (hA : WeaklyIntegrable μ A) (R : ℝ) (hbound : ∀ g, ‖A g‖ ≤ R)
    (B : H →L[ℂ] H) (x y : H) :
    inner ℂ (commutator (weakOperatorIntegral μ A hA R hbound) B x) y =
      ∫ g, inner ℂ (commutator (A g) B x) y ∂μ := by
…

Mentions: OAI.KadisonSimilarity.WeaklyIntegrable, OAI.KadisonSimilarity.commutator, OAI.KadisonSimilarity.weakOperatorIntegral

theorem OAI.KadisonSimilarity.norm_commutator_weakOperatorIntegral_le line 97

Source documentation

Uniform commutator bounds are preserved by weak integration.

theorem norm_commutator_weakOperatorIntegral_le (A : X → H →L[ℂ] H)
    (hA : WeaklyIntegrable μ A) (R : ℝ) (hbound : ∀ g, ‖A g‖ ≤ R)
    (B : H →L[ℂ] H) {c : ℝ} (hc : 0 ≤ c)
    (hcomm : ∀ g, ‖commutator (A g) B‖ ≤ c) :
    ‖commutator (weakOperatorIntegral μ A hA R hbound) B‖ ≤ c := by
…

Mentions: OAI.KadisonSimilarity.WeaklyIntegrable, OAI.KadisonSimilarity.commutator, OAI.KadisonSimilarity.weakOperatorIntegral