PhaseFaithfulness.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.KervaireRegular.star_leftOperator line 22
theorem OAI.KervaireRegular.leftOperator_mem line 28
theorem OAI.KervaireRegular.groupPhase_eq_zero_iff line 36
Source documentation
The endpoint τ(phase(L(a)))=0 → a=1, on the full arbitrary group. The positive trace faithfulness is proved above, not assumed.
```
theorem groupPhase_eq_zero_iff (a : A) : groupPhase 1 (one_mem _) a = 0 ↔ a = 1 := by
…
```
Mentions: OAI.KervaireRegular.groupPhase

theorem OAI.KervaireRegular.tendsto_groupPhase_rotation line 79

Source documentation

The nonnegative cut convention gives precisely the right-hand continuity used at the distinguished boundary.

theorem tendsto_groupPhase_rotation (a : A) {x : ℕ → ℝ}
    (hx : Filter.Tendsto x Filter.atTop (nhds 0)) (hx0 : ∀ n, 0 ≤ x n) :
    Filter.Tendsto (fun n => groupPhase (scalarRotation (x n)) (scalarRotation_unitary _) a)
      Filter.atTop (nhds (groupPhase 1 (one_mem _) a)) := by
…

Mentions: OAI.KervaireRegular.groupPhase

theorem OAI.KervaireSpectral.vectorPhase_eq_zero_of_fixed line 92
Source documentation
Fixed vectors carry zero phase, including the atom at the phase cut.
```
theorem vectorPhase_eq_zero_of_fixed (U : Operator H) (hU : U ∈ unitary (Operator H))
    (ξ : H) (hξ : U ξ = ξ) :
    let _ := isStarNormal_of_mem_unitary hU
…
```
Mentions: OAI.KervaireSpectral.Operator
theorem OAI.KervaireSpectral.vectorPhase_add_star_le line 110
Source documentation
An inverse pair contributes at most one unit of phase per unit vector.
```
theorem vectorPhase_add_star_le (U : Operator H) (hU : U ∈ unitary (Operator H)) (ξ : H) :
    let _ := isStarNormal_of_mem_unitary hU
…
```
Mentions: OAI.KervaireSpectral.Operator