PhaseDimension.lean`

21 declarations, 0 contain sorry, 0 declared as axioms

def OAI.KervaireSpectral.orthogonalPairBasis line 25

Source documentation

A basis adapted to a subspace and its orthogonal complement.

def orthogonalPairBasis (E : Submodule ℂ H) :
    Module.Basis (Fin (Module.finrank ℂ E) ⊕ Fin (Module.finrank ℂ Eᗮ)) ℂ H :=
…

theorem OAI.KervaireSpectral.orthogonalPairBasis_inl line 30
theorem OAI.KervaireSpectral.orthogonalPairBasis_inr line 35
theorem OAI.KervaireSpectral.orthogonalPairBasis_orthonormal line 40

def OAI.KervaireSpectral.orthogonalPairONB line 57

Source documentation

The normalized basis is orthonormal.

def orthogonalPairONB (E : Submodule ℂ H) :
    OrthonormalBasis (Fin (Module.finrank ℂ E) ⊕ Fin (Module.finrank ℂ Eᗮ)) ℂ H :=
…

theorem OAI.KervaireSpectral.orthogonalPairONB_inl line 61
theorem OAI.KervaireSpectral.orthogonalPairONB_inr line 65
theorem OAI.KervaireSpectral.vectorSum_onb line 79
Source documentation
The sum of vector functionals over an ONB is precisely algebraic trace.
```
theorem vectorSum_onb (b : OrthonormalBasis ι ℂ H) (T : Operator H) :
    vectorSum b T = LinearMap.trace ℂ H T.toLinearMap := by
…
```
Mentions: OAI.KervaireSpectral.Operator, OAI.KervaireSpectral.vectorSum

theorem OAI.KervaireSpectral.sumPhase_onb_eq line 85

Source documentation

The spectral phase of a finite-dimensional unitary does not depend on ONB.

theorem sumPhase_onb_eq (U : Operator H) (hU : U ∈ unitary (Operator H))
    (b : OrthonormalBasis ι ℂ H) (c : OrthonormalBasis κ ℂ H) :
    let _ := isStarNormal_of_mem_unitary hU
…

Mentions: OAI.KervaireSpectral.Operator

theorem OAI.KervaireSpectral.star_fixed_of_fixed line 94
Source documentation
A unitary and its adjoint fix exactly the same vectors.
```
theorem star_fixed_of_fixed (U : Operator H) (hU : U ∈ unitary (Operator H))
    (v : H) (hv : U v = v) : star U v = v := by
…
```
Mentions: OAI.KervaireSpectral.Operator

theorem OAI.KervaireSpectral.sumPhase_add_star_le_codim line 101

Source documentation

Inverse-pair phases are bounded by codimension of any common fixed space.

theorem sumPhase_add_star_le_codim (U : Operator H) (hU : U ∈ unitary (Operator H))
    (b : OrthonormalBasis ι ℂ H) (E : Submodule ℂ H)
    (hE : ∀ v : E, U (v : H) = (v : H)) :
    let _ := isStarNormal_of_mem_unitary hU
…

Mentions: OAI.KervaireSpectral.Operator

theorem OAI.KervaireSpectral.unitary_conj_pow line 142
Source documentation
Powers telescope under a unitary conjugation.
```
theorem unitary_conj_pow (U Q : Operator H) (hQ : Q ∈ unitary (Operator H)) (n : ℕ) :
    (Q * U * star Q)^n = Q * U^n * star Q := by
…
```
Mentions: OAI.KervaireSpectral.Operator
theorem OAI.KervaireSpectral.vectorSum_onb_mul_comm line 155
Source documentation
The finite-vector trace of an ONB is cyclic.
```
theorem vectorSum_onb_mul_comm (b : OrthonormalBasis ι ℂ H) (T S : Operator H) :
    vectorSum b (T*S) = vectorSum b (S*T) := by
…
```
Mentions: OAI.KervaireSpectral.Operator, OAI.KervaireSpectral.vectorSum

theorem OAI.KervaireSpectral.sumPhase_unitary_conj line 161

Source documentation

Conjugation preserves the exact, possibly discontinuous, spectral phase.

theorem sumPhase_unitary_conj (U Q : Operator H)
    (hU : U ∈ unitary (Operator H)) (hQ : Q ∈ unitary (Operator H))
    (b : OrthonormalBasis ι ℂ H) :
    let _ := isStarNormal_of_mem_unitary hU
…

Mentions: OAI.KervaireSpectral.Operator

theorem OAI.KervaireSpectral.sumPhase_le_half_codim line 175

Source documentation

Inverse-symmetric spectrum divides the codimension bound by two.

theorem sumPhase_le_half_codim (U Q : Operator H)
    (hU : U ∈ unitary (Operator H)) (hQ : Q ∈ unitary (Operator H))
    (hconj : Q*U*star Q = star U)
    (b : OrthonormalBasis ι ℂ H) (E : Submodule ℂ H)
    (hE : ∀ v : E, U (v : H) = (v : H)) :
    let _ := isStarNormal_of_mem_unitary hU
…

Mentions: OAI.KervaireSpectral.Operator

theorem OAI.KervaireMatrix.scalarTensor_pow line 202
theorem OAI.KervaireMatrix.vectorSum_toEuclideanCLM line 211
Source documentation
The ordinary finite-dimensional operator trace has the matrix entries used by the amplification trace; no normalization is introduced here.
```
theorem vectorSum_toEuclideanCLM (M : Matrix D D ℂ) :
    vectorSum (EuclideanSpace.basisFun D ℂ) ((Matrix.toEuclideanCLM (n := D) (𝕜 := ℂ)) M) = Matrix.trace M := by
…
```
theorem OAI.KervaireMatrix.phase_scalarTensor line 221
Source documentation
The cut-sensitive phase of a scalar amplification is the ordinary finite-dimensional phase, proved through every nonnegative power moment.
```
theorem phase_scalarTensor (M : Matrix D D ℂ) (hM : M ∈ Matrix.unitaryGroup D ℂ) :
    let _ := isStarNormal_of_mem_unitary (scalarTensor_mem_unitary (A := A) hM)
…
```
Mentions: OAI.KervaireMatrix.scalarTensor_mem_unitary
theorem OAI.KervaireSpectral.spectrum_involution line 242
Source documentation
A scalar point of the spectrum of an involution is exactly a sign.
```
theorem spectrum_involution {U : Operator H} (hU : U ^ 2 = 1) (z : spectrum ℂ U) :
    (z : ℂ) = 1 ∨ (z : ℂ) = -1 := by
…
```
Mentions: OAI.KervaireSpectral.Operator
theorem OAI.KervaireSpectral.vectorPhase_involution line 251
Source documentation
Spectral phase on a self-adjoint unitary is one half of its negative projection.
```
theorem vectorPhase_involution (U : Operator H) (hU : U ∈ unitary (Operator H))
    (hUU : U ^ 2 = 1) (ξ : H) :
    let _ := isStarNormal_of_mem_unitary hU
…
```
Mentions: OAI.KervaireSpectral.Operator

theorem OAI.KervaireSpectral.sumPhase_involution line 277

Source documentation

The unnormalized matrix version used for the involution SJ.

theorem sumPhase_involution {ι : Type*} [Fintype ι]
    (U : Operator H) (hU : U ∈ unitary (Operator H)) (hUU : U ^ 2 = 1) (ξ : ι → H) :
    let _ := isStarNormal_of_mem_unitary hU
…

Mentions: OAI.KervaireSpectral.Operator