SpectralApproximation.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

def OAI.KervaireSpectral.spectralLog line 20
Source documentation
The Mercator logarithm is continuous on the unitary spectrum.
```
def spectralLog (U : Operator H) (hU : U ∈ unitary (Operator H)) (a : ℂ)
    (ha : ‖a‖ < 1) : C(spectrum ℂ U, ℂ) :=
…
```
Mentions: OAI.KervaireSpectral.Operator

theorem OAI.KervaireSpectral.hasSum_spectralLog line 33

Source documentation

Uniform absolute convergence of the Mercator expansion in continuous calculus.

theorem hasSum_spectralLog (U : Operator H) (hU : U ∈ unitary (Operator H))
    {a : ℂ} (ha : ‖a‖ < 1) :
    HasSum (fun n : ℕ => (a ^ (n+1) / (n+1)) •
      ((ContinuousMap.id ℂ).restrict (spectrum ℂ U)) ^ (n+1)) (spectralLog U hU a ha) := by
…

Mentions: OAI.KervaireSpectral.Operator, OAI.KervaireSpectral.spectralLog

theorem OAI.KervaireSpectral.traceLog_eq_calculus line 75
Source documentation
Applying any continuous functional to the convergent spectral logarithm commutes with its Mercator expansion.
```
theorem traceLog_eq_calculus (U : Operator H) (hU : U ∈ unitary (Operator H))
    (τ : Operator H →L[ℂ] ℂ) {a : ℂ} (ha : ‖a‖ < 1) :
    let hN := isStarNormal_of_mem_unitary hU
…
```
Mentions: OAI.KervaireSpectral.Operator
def OAI.KervaireSpectral.spectralSmooth line 88
Source documentation
The regularized scalar phase is continuous on the unitary spectrum.
```
def spectralSmooth (U : Operator H) (hU : U ∈ unitary (Operator H))
    (a : ℂ) (ha : ‖a‖ < 1) : C(spectrum ℂ U, ℝ) :=
…
```
Mentions: OAI.KervaireSpectral.Operator
theorem OAI.KervaireSpectral.complexify_one line 98
theorem OAI.KervaireSpectral.integral_one_vectorMeasure line 102
Source documentation
The mass of a vector spectral measure is its value at the identity.
```
theorem integral_one_vectorMeasure (U : Operator H) [IsStarNormal U] (ξ : H) :
    ∫ _z : spectrum ℂ U, (1 : ℝ) ∂vectorMeasure U ξ = (vectorCLM ξ 1).re := by
…
```
Mentions: OAI.KervaireSpectral.Operator, OAI.KervaireSpectral.vectorMeasure, OAI.KervaireSpectral.vectorCLM
theorem OAI.KervaireSpectral.smoothTrace_vectorCLM line 107
Source documentation
Continuous-calculus and scalar-measure versions of the regularization agree.
```
theorem smoothTrace_vectorCLM (U : Operator H) (hU : U ∈ unitary (Operator H))
    (ξ : H) {a : ℂ} (ha : ‖a‖ < 1) :
    let _ := isStarNormal_of_mem_unitary hU
…
```
Mentions: OAI.KervaireSpectral.Operator
theorem OAI.KervaireSpectral.tendsto_smoothTrace_vectorCLM line 132
Source documentation
Dominated convergence reaches the exact value zero at the phase cut.
```
theorem tendsto_smoothTrace_vectorCLM (U : Operator H) (hU : U ∈ unitary (Operator H))
    (ξ : H) :
    let _ := isStarNormal_of_mem_unitary hU
…
```
Mentions: OAI.KervaireSpectral.Operator