PhaseNaturality.lean`

15 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.KervaireSpectral.vectorPhase_cfcHom line 23
Source documentation
The cut-sensitive phase has the expected scalar-measure pullback under continuous functional calculus. This is proved from triangular approximants.
```
theorem vectorPhase_cfcHom (U : Operator H) [hN : IsStarNormal U]
    (f : C(spectrum ℂ U, ℂ)) (hf : cfcHom hN f ∈ unitary (Operator H)) (ξ : H) :
    let _ := isStarNormal_of_mem_unitary hf
…
```
Mentions: OAI.KervaireSpectral.Operator
theorem OAI.KervaireSpectral.vectorPhase_star line 57
Source documentation
Naturality for taking the inverse of a unitary.
```
theorem vectorPhase_star (U : Operator H) (hU : U ∈ unitary (Operator H)) (ξ : H) :
    let _ := isStarNormal_of_mem_unitary hU
…
```
Mentions: OAI.KervaireSpectral.Operator
theorem OAI.KervaireSpectral.vectorPhase_pow line 71
Source documentation
Naturality for positive powers, needed for the boundary-cycle calculation.
```
theorem vectorPhase_pow (U : Operator H) (hU : U ∈ unitary (Operator H)) (n : ℕ) (ξ : H) :
    let _ := isStarNormal_of_mem_unitary hU
…
```
Mentions: OAI.KervaireSpectral.Operator
def OAI.KervaireSpectral.scalarRotation line 86
theorem OAI.KervaireSpectral.scalarRotation_zero line 88
theorem OAI.KervaireSpectral.norm_scalarRotation line 90
theorem OAI.KervaireSpectral.scalarRotation_add line 93
theorem OAI.KervaireSpectral.star_scalarRotation line 97
theorem OAI.KervaireSpectral.scalarRotation_unitary line 104
theorem OAI.KervaireSpectral.phase_rotation line 109
theorem OAI.KervaireSpectral.phase_star line 116
theorem OAI.KervaireSpectral.phase_add_star_le_one line 122

theorem OAI.KervaireSpectral.tendsto_phase_rotation line 129

Source documentation

The exact one-sided convergence used at the exceptional boundary circle.

theorem tendsto_phase_rotation {ι : Type*} {l : Filter ι} {a : ι → ℝ}
    (ha : Tendsto a l (𝓝 0)) (ha0 : ∀ᶠ i in l, 0 ≤ a i)
    {z : ℂ} (hz : ‖z‖ = 1) :
    Tendsto (fun i => phase (scalarRotation (a i) * z)) l (𝓝 (phase z)) := by
…

Mentions: OAI.KervaireSpectral.phase, OAI.KervaireSpectral.scalarRotation

theorem OAI.KervaireSpectral.vectorPhase_rotation line 144
Source documentation
The scalar-rotation formula for the exact spectral measure.
```
theorem vectorPhase_rotation (U : Operator H) (hU : U ∈ unitary (Operator H))
    (x : ℝ) (ξ : H) :
    let _ := isStarNormal_of_mem_unitary hU
…
```
Mentions: OAI.KervaireSpectral.Operator

theorem OAI.KervaireSpectral.tendsto_vectorPhase_rotation line 164

Source documentation

Bounded convergence at the phase cut from the nonnegative-shift side.

theorem tendsto_vectorPhase_rotation (U : Operator H) (hU : U ∈ unitary (Operator H))
    (ξ : H) {a : ℕ → ℝ} (ha : Tendsto a atTop (𝓝 0)) (ha0 : ∀ n, 0 ≤ a n) :
    let _ := isStarNormal_of_mem_unitary hU
…

Mentions: OAI.KervaireSpectral.Operator