SpectralMeasures.lean`

46 declarations, 0 contain sorry, 0 declared as axioms

abbrev OAI.KervaireSpectral.Operator line 16
def OAI.KervaireSpectral.complexify line 19
Source documentation
Embed a real-valued function into complex-valued functions.
```
def complexify {X : Type*} [TopologicalSpace X] (f : C(X, ℝ)) : C(X, ℂ) :=
…
```
theorem OAI.KervaireSpectral.complexify_apply line 22
theorem OAI.KervaireSpectral.complexify_add line 25
theorem OAI.KervaireSpectral.complexify_smul line 28
def OAI.KervaireSpectral.vectorFunctional line 33
Source documentation
A vector functional restricted to the continuous calculus of a normal operator.
```
def vectorFunctional (U : Operator H) [hU : IsStarNormal U] (ξ : H) :
    C_c(spectrum ℂ U, ℝ) →ₚ[ℝ] ℝ := .mk₀ {
…
```
Mentions: OAI.KervaireSpectral.Operator
def OAI.KervaireSpectral.vectorMeasure line 54
Source documentation
The finite scalar spectral measure of a vector, on the actual spectrum.
```
def vectorMeasure (U : Operator H) [IsStarNormal U] (ξ : H) : Measure (spectrum ℂ U) :=
…
```
Mentions: OAI.KervaireSpectral.Operator
instance OAI.KervaireSpectral.vectorMeasure_finite line 57
theorem OAI.KervaireSpectral.integral_vectorMeasure line 63
Source documentation
The defining integration identity for the scalar spectral measure.
```
theorem integral_vectorMeasure (U : Operator H) [hU : IsStarNormal U] (ξ : H)
    (f : C(spectrum ℂ U, ℝ)) :
    ∫ z, f z ∂vectorMeasure U ξ = (inner ℂ ξ (cfcHom hU (complexify f) ξ)).re := by
…
```
Mentions: OAI.KervaireSpectral.Operator, OAI.KervaireSpectral.vectorMeasure, OAI.KervaireSpectral.complexify
def OAI.KervaireSpectral.normSqMap line 70
Source documentation
Squared modulus of a continuous complex function, kept real-valued.
```
def normSqMap {X : Type*} [TopologicalSpace X] (f : C(X, ℂ)) : C(X, ℝ) :=
…
```
theorem OAI.KervaireSpectral.integral_normSqMap line 74
Source documentation
The scalar measure gives squared norms of arbitrary continuous-calculus vectors.
```
theorem integral_normSqMap (U : Operator H) [hU : IsStarNormal U] (ξ : H)
    (f : C(spectrum ℂ U, ℂ)) :
    ∫ z, normSqMap f z ∂vectorMeasure U ξ = ‖cfcHom hU f ξ‖ ^ 2 := by
…
```
Mentions: OAI.KervaireSpectral.Operator, OAI.KervaireSpectral.normSqMap, OAI.KervaireSpectral.vectorMeasure
def OAI.KervaireSpectral.phase line 85
theorem OAI.KervaireSpectral.phase_one line 87
theorem OAI.KervaireSpectral.phase_nonneg line 89
theorem OAI.KervaireSpectral.phase_lt_one line 91
theorem OAI.KervaireSpectral.measurable_phase line 93
theorem OAI.KervaireSpectral.phase_eq_zero_iff line 97
Source documentation
On the unit circle only the identity has phase zero.
```
theorem phase_eq_zero_iff {z : ℂ} (hz : z ∈ unitary ℂ) : phase z = 0 ↔ z = 1 := by
…
```
Mentions: OAI.KervaireSpectral.phase
theorem OAI.KervaireSpectral.integrable_phase line 114
Source documentation
A bounded measurable phase is integrable for every scalar spectral measure.
```
theorem integrable_phase (U : Operator H) [IsStarNormal U] (ξ : H) :
    Integrable (fun z : spectrum ℂ U => phase z) (vectorMeasure U ξ) := by
…
```
Mentions: OAI.KervaireSpectral.Operator, OAI.KervaireSpectral.phase, OAI.KervaireSpectral.vectorMeasure
def OAI.KervaireSpectral.vectorPhase line 121
theorem OAI.KervaireSpectral.vectorPhase_nonneg line 124
def OAI.KervaireSpectral.distanceSq line 128
Source documentation
The continuous squared distance to one on the spectrum.
```
def distanceSq (U : Operator H) : C(spectrum ℂ U, ℝ) :=
…
```
Mentions: OAI.KervaireSpectral.Operator
theorem OAI.KervaireSpectral.distanceSq_calculus line 133
Source documentation
Its calculus is the positive square of U - I.
```
theorem distanceSq_calculus (U : Operator H) [hU : IsStarNormal U] :
    cfcHom hU (complexify (distanceSq U)) = star (U - 1) * (U - 1) := by
…
```
Mentions: OAI.KervaireSpectral.Operator, OAI.KervaireSpectral.complexify, OAI.KervaireSpectral.distanceSq
theorem OAI.KervaireSpectral.integral_distanceSq line 144
Source documentation
The scalar spectral measure recovers the norm of the displacement.
```
theorem integral_distanceSq (U : Operator H) [hU : IsStarNormal U] (ξ : H) :
    ∫ z, distanceSq U z ∂vectorMeasure U ξ = ‖U ξ - ξ‖ ^ 2 := by
…
```
Mentions: OAI.KervaireSpectral.Operator, OAI.KervaireSpectral.distanceSq, OAI.KervaireSpectral.vectorMeasure
theorem OAI.KervaireSpectral.fixed_of_vectorPhase_eq_zero line 153
Source documentation
Zero vector phase forces this vector to be fixed. No spectral projection or Borel operator calculus is assumed in this implication.
```
theorem fixed_of_vectorPhase_eq_zero (U : Operator H) (hU : U ∈ unitary (Operator H))
    (ξ : H) (h : letI := isStarNormal_of_mem_unitary hU; vectorPhase U ξ = 0) :
…
```
Mentions: OAI.KervaireSpectral.Operator, OAI.KervaireSpectral.vectorPhase

theorem OAI.KervaireSpectral.cauchySeq_calculus line 171

Source documentation

Bounded pointwise convergence of continuous spectral functions is strongly Cauchy. The proof is scalar dominated convergence, applied to squared distances.

theorem cauchySeq_calculus (U : Operator H) [hU : IsStarNormal U]
    (f : ℕ → C(spectrum ℂ U, ℂ)) (g : spectrum ℂ U → ℂ)
    (C : ℝ) (_hC : 0 ≤ C) (hb : ∀ n z, ‖f n z‖ ≤ C)
    (ht : ∀ z, Tendsto (fun n => f n z) atTop (𝓝 (g z))) (ξ : H) :
    CauchySeq (fun n => cfcHom hU (f n) ξ) := by
…

Mentions: OAI.KervaireSpectral.Operator

theorem OAI.KervaireSpectral.exists_strongLimit line 210

Source documentation

A uniformly bounded convergent continuous approximation defines a bounded operator, without a separability restriction on the Hilbert space.

theorem exists_strongLimit (U : Operator H) [hU : IsStarNormal U]
    (f : ℕ → C(spectrum ℂ U, ℂ)) (g : spectrum ℂ U → ℂ)
    (C : ℝ) (hC : 0 ≤ C) (hb : ∀ n z, ‖f n z‖ ≤ C)
    (ht : ∀ z, Tendsto (fun n => f n z) atTop (𝓝 (g z))) :
    ∃ T : Operator H, (∀ ξ, Tendsto (fun n => cfcHom hU (f n) ξ) atTop (𝓝 (T ξ))) ∧
      ‖T‖ ≤ C := by
…

Mentions: OAI.KervaireSpectral.Operator

theorem OAI.KervaireSpectral.phase_exp line 230
theorem OAI.KervaireSpectral.phase_exp_normalized line 239
def OAI.KervaireSpectral.phaseTriangle line 246
Source documentation
A continuous triangular cutoff on the chosen angle interval.
```
def phaseTriangle (n : ℕ) (x : ℝ) : ℝ := min x ((n : ℝ) * (1 - x))
```
theorem OAI.KervaireSpectral.continuous_phaseTriangle line 248
theorem OAI.KervaireSpectral.phaseTriangle_zero line 252
theorem OAI.KervaireSpectral.phaseTriangle_one line 255
theorem OAI.KervaireSpectral.continuous_clippedPhase line 259
Source documentation
Although phase is discontinuous, this clipped phase is continuous on the circle.
```
theorem continuous_clippedPhase (n : ℕ) :
    Continuous (fun z : Circle => phaseTriangle n (phase z)) := by
…
```
Mentions: OAI.KervaireSpectral.phaseTriangle, OAI.KervaireSpectral.phase
theorem OAI.KervaireSpectral.phaseTriangle_nonneg line 267
theorem OAI.KervaireSpectral.phaseTriangle_le_self line 271
theorem OAI.KervaireSpectral.tendsto_phaseTriangle line 273
def OAI.KervaireSpectral.phaseApprox line 282
Source documentation
Continuous lower approximations to phase on a unitary spectrum.
```
def phaseApprox (U : Operator H) (hU : U ∈ unitary (Operator H)) (n : ℕ) :
    C(spectrum ℂ U, ℝ) :=
…
```
Mentions: OAI.KervaireSpectral.Operator
theorem OAI.KervaireSpectral.phaseApprox_nonneg line 289
theorem OAI.KervaireSpectral.phaseApprox_le_one line 293
theorem OAI.KervaireSpectral.tendsto_phaseApprox line 297
theorem OAI.KervaireSpectral.tendsto_integral_phaseApprox line 301
theorem OAI.KervaireSpectral.exp_phase line 317
Source documentation
Exponentiating the chosen phase recovers a point on the unit circle.
```
theorem exp_phase {z : ℂ} (hz : ‖z‖ = 1) :
    Complex.exp ((2 * Real.pi * phase z : ℝ) * Complex.I) = z := by
…
```
Mentions: OAI.KervaireSpectral.phase

theorem OAI.KervaireSpectral.tendsto_calculus line 329

Source documentation

An already continuous pointwise limit is identified by the scalar measures.

theorem tendsto_calculus (U : Operator H) [hU : IsStarNormal U]
    (f : ℕ → C(spectrum ℂ U, ℂ)) (g : C(spectrum ℂ U, ℂ))
    (C : ℝ) (_hC : 0 ≤ C) (hb : ∀ n z, ‖f n z‖ ≤ C)
    (ht : ∀ z, Tendsto (fun n => f n z) atTop (𝓝 (g z))) (ξ : H) :
    Tendsto (fun n => cfcHom hU (f n) ξ) atTop (𝓝 (cfcHom hU g ξ)) := by
…

Mentions: OAI.KervaireSpectral.Operator

def OAI.KervaireSpectral.expMap line 360
Source documentation
Pointwise exponential of a continuous complex-valued function.
```
def expMap {X : Type*} [TopologicalSpace X] (f : C(X, ℂ)) : C(X, ℂ) :=
…
```
theorem OAI.KervaireSpectral.expMap_eq_exp line 364
Source documentation
The normed-ring exponential on continuous functions is pointwise.
```
theorem expMap_eq_exp {X : Type*} [TopologicalSpace X] [CompactSpace X]
    (f : C(X, ℂ)) : expMap f = NormedSpace.exp f := by
…
```
Mentions: OAI.KervaireSpectral.expMap
theorem OAI.KervaireSpectral.calculus_expMap line 373
Source documentation
The continuous functional calculus respects the operator exponential.
```
theorem calculus_expMap (U : Operator H) [hU : IsStarNormal U]
    (f : C(spectrum ℂ U, ℂ)) :
    cfcHom hU (expMap f) = NormedSpace.exp (cfcHom hU f) := by
…
```
Mentions: OAI.KervaireSpectral.Operator, OAI.KervaireSpectral.expMap