WeakFieldKernel.lean`

16 declarations, 0 contain sorry, 0 declared as axioms

Kernel projections of measurable operator fields

Cesàro averages of a positive contraction converge strongly to its kernel projection. Applied pointwise, this proves measurability of the projection without using a measurable selection or Borel functional calculus input.

def OAI.KadisonKastler.WeakOperatorRepresentative.evalHom line 27
Source documentation
Evaluation is a star algebra homomorphism.
```
def evalHom (x : D) : WeakOperatorRepresentative (H := H) μ →⋆ₐ[ℂ] (H →L[ℂ] H) where
…
```
Mentions: OAI.KadisonKastler.WeakOperatorRepresentative
theorem OAI.KadisonKastler.WeakOperatorRepresentative.evalHom_apply line 36
theorem OAI.KadisonKastler.WeakOperatorRepresentative.ext_eval line 41
Source documentation
Pointwise equality determines a representative.
```
theorem ext_eval {F G : WeakOperatorRepresentative (H := H) μ}
…
```
Mentions: OAI.KadisonKastler.WeakOperatorRepresentative
def OAI.KadisonKastler.WeakOperatorRepresentative.kernelAverage line 55
theorem OAI.KadisonKastler.WeakOperatorRepresentative.norm_positive_complement_le line 59
theorem OAI.KadisonKastler.WeakOperatorRepresentative.starProjection_congr line 66
theorem OAI.KadisonKastler.WeakOperatorRepresentative.operator_kernel_averages_tendsto line 72
theorem OAI.KadisonKastler.WeakOperatorRepresentative.kernelAverage_eval line 87
theorem OAI.KadisonKastler.WeakOperatorRepresentative.kernelAverage_tendsto line 95
theorem OAI.KadisonKastler.WeakOperatorRepresentative.kernel_aestronglyMeasurable line 104
Source documentation
Kernel projections of positive contraction fields are measurable.
```
theorem kernel_aestronglyMeasurable (F : WeakOperatorRepresentative (H := H) μ)
…
```
Mentions: OAI.KadisonKastler.WeakOperatorRepresentative
def OAI.KadisonKastler.WeakOperatorRepresentative.kernelProjection line 112
Source documentation
The kernel projection is an actual measurable representative.
```
def kernelProjection (F : WeakOperatorRepresentative (H := H) μ)
…
```
Mentions: OAI.KadisonKastler.WeakOperatorRepresentative
theorem OAI.KadisonKastler.WeakOperatorRepresentative.eval_kernelProjection line 122
theorem OAI.KadisonKastler.WeakOperatorRepresentative.positive_kernel_aestronglyMeasurable line 127
Source documentation
Remove the contraction restriction by a positive scalar rescaling.
```
theorem positive_kernel_aestronglyMeasurable (F : WeakOperatorRepresentative (H := H) μ)
…
```
Mentions: OAI.KadisonKastler.WeakOperatorRepresentative
def OAI.KadisonKastler.WeakOperatorRepresentative.positiveKernelProjection line 147
Source documentation
Kernel projection of a positive measurable field, with no norm restriction.
```
def positiveKernelProjection (F : WeakOperatorRepresentative (H := H) μ)
…
```
Mentions: OAI.KadisonKastler.WeakOperatorRepresentative
theorem OAI.KadisonKastler.WeakOperatorRepresentative.eval_positiveKernelProjection line 157
theorem OAI.KadisonKastler.WeakOperatorRepresentative.positiveKernelProjection_isStarProjection line 162
Source documentation
The pointwise kernel projection is a projection in the representative algebra.
```
theorem positiveKernelProjection_isStarProjection
    (F : WeakOperatorRepresentative (H := H) μ) (hF : 0 ≤ F) :
…
```
Mentions: OAI.KadisonKastler.WeakOperatorRepresentative