SpectralLogarithm.lean`

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.KervaireSpectral.exists_phaseOperator line 19
def OAI.KervaireSpectral.vectorCLM line 107
Source documentation
The continuous vector functional on all bounded operators.
```
def vectorCLM (ξ : H) : Operator H →L[ℂ] ℂ :=
…
```
Mentions: OAI.KervaireSpectral.Operator
theorem OAI.KervaireSpectral.vectorCLM_apply line 111
theorem OAI.KervaireSpectral.vectorCLM_star line 115
Source documentation
The vector functional respects the star, without a trace assumption.
```
theorem vectorCLM_star (ξ : H) (T : Operator H) :
    vectorCLM ξ (star T) = star (vectorCLM ξ T) := by
…
```
Mentions: OAI.KervaireSpectral.Operator, OAI.KervaireSpectral.vectorCLM
theorem OAI.KervaireSpectral.vectorCLM_complexify_real line 122
Source documentation
Real continuous spectral functions have real vector expectations.
```
theorem vectorCLM_complexify_real (U : Operator H) [hU : IsStarNormal U] (ξ : H)
    (f : C(spectrum ℂ U, ℝ)) :
    (((vectorCLM ξ (cfcHom hU (complexify f))).re : ℝ) : ℂ) =
      vectorCLM ξ (cfcHom hU (complexify f)) := by
…
```
Mentions: OAI.KervaireSpectral.Operator, OAI.KervaireSpectral.vectorCLM, OAI.KervaireSpectral.complexify
theorem OAI.KervaireSpectral.integrable_continuous_map line 134
Source documentation
Every continuous function on the compact spectral space is integrable.
```
theorem integrable_continuous_map {E : Type*} [NormedAddCommGroup E]
    (U : Operator H) [IsStarNormal U] (ξ : H) (f : C(spectrum ℂ U, E)) :
    Integrable f (vectorMeasure U ξ) := by
…
```
Mentions: OAI.KervaireSpectral.Operator, OAI.KervaireSpectral.vectorMeasure
theorem OAI.KervaireSpectral.integral_vectorMeasure_complex line 141
Source documentation
The scalar spectral measure integrates complex functions as well as real ones.
```
theorem integral_vectorMeasure_complex (U : Operator H) [hU : IsStarNormal U] (ξ : H)
    (f : C(spectrum ℂ U, ℂ)) :
    ∫ z, f z ∂vectorMeasure U ξ = vectorCLM ξ (cfcHom hU f) := by
…
```
Mentions: OAI.KervaireSpectral.Operator, OAI.KervaireSpectral.vectorMeasure, OAI.KervaireSpectral.vectorCLM