KernelReconstruction.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Reconstructing measurable operator fields from scalar kernels

The coherent countable-core representatives give pointwise bounded operators. Dense scalar tests prove measurability; continuity of the L-infinity kernel then identifies all coefficients.

def OAI.KadisonKastler.ScalarOperatorKernel.reconstructedOperator line 28
Source documentation
The scalar kernel gives a bounded operator at every good point, and zero on the exceptional null set.
```
def reconstructedOperator (x : D) : H →L[ℂ] H := by
…
```
theorem OAI.KadisonKastler.ScalarOperatorKernel.reconstructedOperator_norm_le line 32
theorem OAI.KadisonKastler.ScalarOperatorKernel.reconstructedOperator_core_ae line 39
Source documentation
Every countable-core matrix coefficient is the supplied scalar representative.
```
theorem reconstructedOperator_core_ae (ξ η : C.space) :
    ∀ᵐ x ∂μ, inner ℂ (η : H) (K.reconstructedOperator C x (ξ : H)) = K.coeff ξ η x := by
…
```

theorem OAI.KadisonKastler.ScalarOperatorKernel.reconstructedOperator_measurable line 47

Source documentation

The resulting field and its adjoint have all strongly measurable evaluations.

theorem reconstructedOperator_measurable :
    ∀ ξ : H, AEStronglyMeasurable (fun x => K.reconstructedOperator C x ξ) μ ∧
      AEStronglyMeasurable (fun x => star (K.reconstructedOperator C x) ξ) μ := by
…

def OAI.KadisonKastler.ScalarOperatorKernel.reconstructedRepresentative line 59
Source documentation
A bounded measurable representative reconstructed from the scalar kernel.
```
def reconstructedRepresentative : WeakOperatorRepresentative (H := H) μ :=
…
```
Mentions: OAI.KadisonKastler.WeakOperatorRepresentative
theorem OAI.KadisonKastler.ScalarOperatorKernel.reconstructedRepresentative_norm_le line 65
theorem OAI.KadisonKastler.ScalarOperatorKernel.reconstructedRepresentative_coefficient line 71
Source documentation
Equality on the core extends to equality of all L-infinity coefficients.
```
theorem reconstructedRepresentative_coefficient (ξ η : H) :
    WeakOperatorRepresentative.coefficient (K.reconstructedRepresentative C) ξ η = K.coeff ξ η := by
…
```
Mentions: OAI.KadisonKastler.WeakOperatorRepresentative.coefficient
theorem OAI.KadisonKastler.ScalarOperatorKernel.exists_representative line 84
Source documentation
Bounded scalar sesquilinear kernels have actual measurable operator representatives, with no additional existence premise.
```
theorem exists_representative : ∃ F : WeakOperatorRepresentative (H := H) μ,
…
```
Mentions: OAI.KadisonKastler.WeakOperatorRepresentative