CoreKernelOperator.lean`

19 declarations, 0 contain sorry, 0 declared as axioms

Reconstruction of a bounded operator from a coherent core kernel

Riesz representation first reconstructs the image of every vector in the countable rational core. The complex-linear extension preserves the bound.

def OAI.KadisonKastler.ScalarOperatorKernel.CoherentCore.conjugateFunctional line 30
Source documentation
Conjugating the test-vector slot makes it rational-linear.
```
def conjugateFunctional (ξ : C.space) : C.space →ₗ[ℚ] ℂ :=
…
```
theorem OAI.KadisonKastler.ScalarOperatorKernel.CoherentCore.conjugateFunctional_bound line 38
theorem OAI.KadisonKastler.ScalarOperatorKernel.CoherentCore.conjugateFunctional_mulI line 43
def OAI.KadisonKastler.ScalarOperatorKernel.CoherentCore.extendedFunctional line 51
Source documentation
The continuous scalar functional associated with a core input.
```
def extendedFunctional (ξ : C.space) : H →L[ℂ] ℂ :=
…
```
theorem OAI.KadisonKastler.ScalarOperatorKernel.CoherentCore.extendedFunctional_coe line 56
def OAI.KadisonKastler.ScalarOperatorKernel.CoherentCore.coreVector line 63
Source documentation
Riesz representation supplies the image of a core vector.
```
def coreVector (ξ : C.space) : H :=
…
```
theorem OAI.KadisonKastler.ScalarOperatorKernel.CoherentCore.coreVector_inner line 66
theorem OAI.KadisonKastler.ScalarOperatorKernel.CoherentCore.coreVector_bound line 76
theorem OAI.KadisonKastler.ScalarOperatorKernel.CoherentCore.coreVector_add line 84
theorem OAI.KadisonKastler.ScalarOperatorKernel.CoherentCore.coreVector_rat_smul line 93
theorem OAI.KadisonKastler.ScalarOperatorKernel.CoherentCore.coreVector_mulI line 104
def OAI.KadisonKastler.ScalarOperatorKernel.CoherentCore.coreLinearMap line 113
Source documentation
The Riesz images form a rational-linear map on the core.
```
def coreLinearMap : C.space →ₗ[ℚ] H where
…
```
theorem OAI.KadisonKastler.ScalarOperatorKernel.CoherentCore.coreLinearMap_bound line 118
theorem OAI.KadisonKastler.ScalarOperatorKernel.CoherentCore.coreLinearMap_mulI line 121
def OAI.KadisonKastler.ScalarOperatorKernel.CoherentCore.toOperator line 125
Source documentation
The bounded complex-linear operator reconstructed from the kernel.
```
def toOperator : H →L[ℂ] H :=
…
```
theorem OAI.KadisonKastler.ScalarOperatorKernel.CoherentCore.toOperator_norm_le line 128
theorem OAI.KadisonKastler.ScalarOperatorKernel.CoherentCore.toOperator_inner line 132
theorem OAI.KadisonKastler.ScalarOperatorKernel.CoherentCore.eq_toOperator line 138
Source documentation
The core matrix coefficients uniquely determine the reconstructed operator.
```
theorem eq_toOperator (T : H →L[ℂ] H)
    (hT : ∀ ξ η : C.space, inner ℂ (η : H) (T (ξ : H)) = k ξ η) :
    T = hk.toOperator := by
…
```
theorem OAI.KadisonKastler.ScalarOperatorKernel.CoherentCore.exists_operator line 153
Source documentation
A coherent scalar core kernel is represented by an operator with the same bound; no measurable selection is involved in this construction.
```
theorem exists_operator :
    ∃ T : H →L[ℂ] H, ‖T‖ ≤ K.bound ∧
      ∀ ξ η : C.space, inner ℂ (η : H) (T (ξ : H)) = k ξ η :=
…
```