ScalarOperatorKernel.lean`

13 declarations, 0 contain sorry, 0 declared as axioms

Simultaneous scalar representatives on a countable complex core

An L-infinity-valued bounded sesquilinear kernel has, almost everywhere, a genuinely sesquilinear bounded scalar kernel on the rational core. No uncountable intersection of conull sets is used.

structure OAI.KadisonKastler.ScalarOperatorKernel line 24
Source documentation
The bounded sesquilinear coefficient data from which an operator field is reconstructed. The first vector is the input to the operator.
```
structure ScalarOperatorKernel (H : Type*) [NormedAddCommGroup H]
    [InnerProductSpace ℂ H] (μ : Measure D) where
…
```
theorem OAI.KadisonKastler.ScalarOperatorKernel.add_left_ae line 39
theorem OAI.KadisonKastler.ScalarOperatorKernel.add_right_ae line 45
theorem OAI.KadisonKastler.ScalarOperatorKernel.smul_left_ae line 51
theorem OAI.KadisonKastler.ScalarOperatorKernel.smul_right_ae line 57
theorem OAI.KadisonKastler.ScalarOperatorKernel.bound_ae line 63
def OAI.KadisonKastler.ScalarOperatorKernel.toLinear line 69
Source documentation
Bundle the coefficient identities as a sesquilinear map.
```
def toLinear : H →ₗ[ℂ] H →ₗ⋆[ℂ] ScalarLInfinity μ where
…
```
Mentions: OAI.KadisonKastler.ScalarLInfinity
def OAI.KadisonKastler.ScalarOperatorKernel.toContinuous line 84
Source documentation
The L-infinity coefficient map is jointly continuous.
```
def toContinuous : H →L[ℂ] H →L⋆[ℂ] ScalarLInfinity μ :=
…
```
Mentions: OAI.KadisonKastler.ScalarLInfinity
theorem OAI.KadisonKastler.ScalarOperatorKernel.toContinuous_apply line 88
theorem OAI.KadisonKastler.ScalarOperatorKernel.coeff_eq_of_core line 91
Source documentation
Agreement on the dense core determines the whole kernel.
```
theorem coeff_eq_of_core (L : ScalarOperatorKernel H μ) (C : RationalComplexCore H)
    (h : ∀ ξ η : C.space, K.coeff ξ η = L.coeff ξ η) :
    ∀ ξ η : H, K.coeff ξ η = L.coeff ξ η := by
…
```
Mentions: OAI.KadisonKastler.ScalarOperatorKernel, OAI.KadisonKastler.RationalComplexCore
structure OAI.KadisonKastler.ScalarOperatorKernel.CoherentCore line 110
Source documentation
Pointwise bounded rational sesquilinearity, including the two tests with multiplication by i that force complex sesquilinearity by continuity.
```
structure CoherentCore (C : RationalComplexCore H) (k : C.space → C.space → ℂ) : Prop where
…
```
Mentions: OAI.KadisonKastler.RationalComplexCore
theorem OAI.KadisonKastler.ScalarOperatorKernel.coherentCore_ae line 121
Source documentation
Countability gives one conull set on which every core identity and bound holds at once.
```
theorem coherentCore_ae (C : RationalComplexCore H) :
    ∀ᵐ x ∂μ, K.CoherentCore C (fun ξ η => K.coeff (ξ : H) (η : H) x) := by
…
```
Mentions: OAI.KadisonKastler.RationalComplexCore
def OAI.KadisonKastler.UniformMeasurableOperators.meanKernel line 174
Source documentation
The scalar boundary mean supplies all data of the bounded operator kernel.
```
def UniformMeasurableOperators.meanKernel (T : UniformMeasurableOperators G D H μ)
    {α : NonsingularAction G D μ} (m : ScalarBoundaryMean α) : ScalarOperatorKernel H μ where
…
```
Mentions: OAI.KadisonKastler.UniformMeasurableOperators, OAI.KadisonKastler.NonsingularAction, OAI.KadisonKastler.ScalarBoundaryMean, OAI.KadisonKastler.ScalarOperatorKernel