WeakOperatorFields.lean`

45 declarations, 0 contain sorry, 0 declared as axioms

Essentially bounded weak operator fields

The representatives are bounded operator-valued functions with measurable evaluations of the function and its adjoint. Their closed C-star algebra is quotiented by the closed star ideal of almost-everywhere zero fields. The resulting norm is bounded by every essential operator-norm bound.

abbrev OAI.KadisonKastler.RawOperatorField line 27
Source documentation
The discrete topology is used only to package arbitrary bounded families; all measurable assertions use the original measure space.
```
abbrev RawOperatorField (D H : Type*) [NormedAddCommGroup H]
    [InnerProductSpace ℂ H] [CompleteSpace H] :=
…
```
instance OAI.KadisonKastler.rawOperatorFieldCStar line 31
def OAI.KadisonKastler.rawOperatorEval line 33
theorem OAI.KadisonKastler.rawOperatorEval_zero line 37
theorem OAI.KadisonKastler.rawOperatorEval_one line 40
theorem OAI.KadisonKastler.rawOperatorEval_add line 43
theorem OAI.KadisonKastler.rawOperatorEval_mul line 47
theorem OAI.KadisonKastler.rawOperatorEval_smul line 51
theorem OAI.KadisonKastler.rawOperatorEval_star line 55
theorem OAI.KadisonKastler.rawOperatorEval_continuous line 58
def OAI.KadisonKastler.rawOperatorVectorEval line 62
theorem OAI.KadisonKastler.rawOperatorVectorEval_apply line 67
def OAI.KadisonKastler.IsMeasurableOperatorField line 72
def OAI.KadisonKastler.measurableOperatorSubalgebra line 78
Source documentation
Measurable operator fields form a star subalgebra.
```
def measurableOperatorSubalgebra : StarSubalgebra ℂ (RawOperatorField D H) where
…
```
Mentions: OAI.KadisonKastler.RawOperatorField
instance OAI.KadisonKastler.measurableOperatorSubalgebra_closed line 117
Source documentation
The measurability condition is preserved by operator-norm limits.
```
instance measurableOperatorSubalgebra_closed :
    IsClosed (measurableOperatorSubalgebra (H := H) μ : Set (RawOperatorField D H)) := by
…
```
Mentions: OAI.KadisonKastler.measurableOperatorSubalgebra, OAI.KadisonKastler.RawOperatorField
abbrev OAI.KadisonKastler.WeakOperatorRepresentative line 130
instance OAI.KadisonKastler.weakOperatorRepresentativeCStar line 132
def OAI.KadisonKastler.WeakOperatorRepresentative.eval line 139
theorem OAI.KadisonKastler.WeakOperatorRepresentative.eval_zero line 143
theorem OAI.KadisonKastler.WeakOperatorRepresentative.eval_one line 146
theorem OAI.KadisonKastler.WeakOperatorRepresentative.eval_add line 149
theorem OAI.KadisonKastler.WeakOperatorRepresentative.eval_mul line 153
theorem OAI.KadisonKastler.WeakOperatorRepresentative.eval_sub line 157
theorem OAI.KadisonKastler.WeakOperatorRepresentative.eval_neg line 161
theorem OAI.KadisonKastler.WeakOperatorRepresentative.eval_smul line 165
theorem OAI.KadisonKastler.WeakOperatorRepresentative.eval_star line 169
theorem OAI.KadisonKastler.WeakOperatorRepresentative.eval_aestronglyMeasurable line 172
theorem OAI.KadisonKastler.WeakOperatorRepresentative.star_eval_aestronglyMeasurable line 175
theorem OAI.KadisonKastler.WeakOperatorRepresentative.eval_norm_le line 178
theorem OAI.KadisonKastler.WeakOperatorRepresentative.eval_continuous line 181

def OAI.KadisonKastler.WeakOperatorRepresentative.mk line 186

Source documentation

Bundle any uniformly bounded measurable operator field.

def mk (f : D → H →L[ℂ] H) (C : ℝ) (hC : ∀ x, ‖f x‖ ≤ C)
    (hf : ∀ ξ, AEStronglyMeasurable (fun x => f x ξ) μ)
    (hfstar : ∀ ξ, AEStronglyMeasurable (fun x => star (f x) ξ) μ) :
    WeakOperatorRepresentative (H := H) μ :=
…

Mentions: OAI.KadisonKastler.WeakOperatorRepresentative

theorem OAI.KadisonKastler.WeakOperatorRepresentative.eval_mk line 195
theorem OAI.KadisonKastler.WeakOperatorRepresentative.norm_mk_le line 200
def OAI.KadisonKastler.operatorRepresentativeConst line 210
Source documentation
Constant operators as measurable fields.
```
def operatorRepresentativeConst : (H →L[ℂ] H) →⋆ₐ[ℂ] WeakOperatorRepresentative (H := H) μ where
…
```
Mentions: OAI.KadisonKastler.WeakOperatorRepresentative
theorem OAI.KadisonKastler.operatorRepresentativeConst_eval line 226
def OAI.KadisonKastler.operatorFieldAERel line 230
Source documentation
Equality almost everywhere is an algebra congruence.
```
def operatorFieldAERel : RingCon (WeakOperatorRepresentative (H := H) μ) where
…
```
Mentions: OAI.KadisonKastler.WeakOperatorRepresentative
def OAI.KadisonKastler.operatorFieldZeroIdeal line 237
Source documentation
The zero fields form a closed two-sided star ideal.
```
def operatorFieldZeroIdeal :
    CuntzPureness.ClosedStarIdeal (WeakOperatorRepresentative (H := H) μ) where
…
```
Mentions: OAI.CuntzPureness.ClosedStarIdeal, OAI.KadisonKastler.WeakOperatorRepresentative
abbrev OAI.KadisonKastler.WeakOperatorField line 265
instance OAI.KadisonKastler.weakOperatorFieldCStar line 267
def OAI.KadisonKastler.operatorFieldQuotient line 269
theorem OAI.KadisonKastler.operatorFieldQuotient_surjective line 272
theorem OAI.KadisonKastler.operatorFieldQuotient_eq_iff line 275
theorem OAI.KadisonKastler.operatorFieldQuotient_norm_le line 281
def OAI.KadisonKastler.operatorFieldConst line 284
theorem OAI.KadisonKastler.operatorFieldQuotient_norm_le_of_ae line 290
Source documentation
An essential operator-norm bound bounds the actual quotient norm. The exceptional-set replacement is legitimate even when that set itself has not been supplied as a measurable set.
```
theorem operatorFieldQuotient_norm_le_of_ae
    (F : WeakOperatorRepresentative (H := H) μ) {C : ℝ} (hC : 0 ≤ C)
…
```
Mentions: OAI.KadisonKastler.WeakOperatorRepresentative