PhaseSubadditivity.lean`

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

abbrev OAI.KervaireCentralizer.Operator line 18
def OAI.KervaireCentralizer.algebra line 21
Source documentation
The strongly closed algebra in which the phase comparison is performed.
```
def algebra (S : Set (Operator (H := H))) : StarSubalgebra ℂ (Operator (H := H)) :=
…
```
Mentions: OAI.KervaireCentralizer.Operator
instance OAI.KervaireCentralizer.(instance at line 24) line 24
def OAI.KervaireCentralizer.inclusion line 28
Source documentation
The inclusion is continuous for the inherited operator norm.
```
def inclusion (S : Set (Operator (H := H))) : algebra S →L[ℂ] Operator (H := H) :=
…
```
Mentions: OAI.KervaireCentralizer.Operator, OAI.KervaireCentralizer.algebra
theorem OAI.KervaireCentralizer.sqrt_mem line 35
Source documentation
The right-translation commutants are closed under continuous square roots.
```
theorem sqrt_mem (S : Set (Operator (H := H))) {X : Operator (H := H)}
…
```
Mentions: OAI.KervaireCentralizer.Operator
instance OAI.KervaireCentralizer.orderedRing line 44
Source documentation
The inherited positive-operator order, not a replacement order.
```
instance orderedRing (S : Set (Operator (H := H))) : StarOrderedRing (algebra S) := by
…
```
Mentions: OAI.KervaireCentralizer.Operator, OAI.KervaireCentralizer.algebra
theorem OAI.KervaireCentralizer.inclusion_apply line 64
theorem OAI.KervaireCentralizer.unitary_iff line 68
Source documentation
Unitarity is unchanged when an operator is viewed in its centralizer.
```
theorem unitary_iff (S : Set (Operator (H := H))) (X : algebra S) :
…
```
Mentions: OAI.KervaireCentralizer.Operator, OAI.KervaireCentralizer.algebra
def OAI.KervaireSpectral.vectorSum line 85
Source documentation
The unnormalized finite sum of vector functionals used for matrix traces.
```
def vectorSum (ξ : ι → H) : Operator H →L[ℂ] ℂ := ∑ j, vectorCLM (ξ j)
…
```
Mentions: OAI.KervaireSpectral.Operator, OAI.KervaireSpectral.vectorCLM
theorem OAI.KervaireSpectral.vectorSum_apply line 88
def OAI.KervaireSpectral.sumPhase line 92
Source documentation
The phase measured by a finite family of vectors.
```
def sumPhase (U : Operator H) [IsStarNormal U] (ξ : ι → H) : ℝ :=
…
```
Mentions: OAI.KervaireSpectral.Operator
theorem OAI.KervaireSpectral.smoothTrace_vectorSum line 96
Source documentation
Regularized tracial phases distribute over a finite vector family.
```
theorem smoothTrace_vectorSum (U : Operator H) (hU : U ∈ unitary (Operator H))
    (ξ : ι → H) {a : ℂ} (ha : ‖a‖ < 1) :
    smoothTrace (vectorSum ξ) a U = ∑ j, smoothTrace (vectorCLM (ξ j)) a U := by
…
```
Mentions: OAI.KervaireSpectral.Operator, OAI.KervaireSpectral.vectorSum, OAI.KervaireSpectral.vectorCLM
theorem OAI.KervaireSpectral.tendsto_smoothTrace_vectorSum line 104
Source documentation
Bounded convergence for the precise matrix-trace phase.
```
theorem tendsto_smoothTrace_vectorSum (U : Operator H) (hU : U ∈ unitary (Operator H))
    (ξ : ι → H) :
    let _ := isStarNormal_of_mem_unitary hU
…
```
Mentions: OAI.KervaireSpectral.Operator
theorem OAI.KervaireSpectral.vectorSum_star_mul_nonneg line 114
Source documentation
Finite vector functionals are positive on squares.
```
theorem vectorSum_star_mul_nonneg (ξ : ι → H) (T : Operator H) :
    0 ≤ (vectorSum ξ (star T * T)).re := by
…
```
Mentions: OAI.KervaireSpectral.Operator, OAI.KervaireSpectral.vectorSum
theorem OAI.KervaireSpectral.vectorSum_star line 126
Source documentation
Finite vector functionals respect adjoints.
```
theorem vectorSum_star (ξ : ι → H) (T : Operator H) :
    vectorSum ξ (star T) = star (vectorSum ξ T) := by
…
```
Mentions: OAI.KervaireSpectral.Operator, OAI.KervaireSpectral.vectorSum
def OAI.KervaireCentralizer.trace line 139
Source documentation
The vector sum restricted to the correct finite-trace algebra.
```
def trace (S : Set (Operator (H := H))) (ξ : ι → H) : algebra S →L[ℂ] ℂ :=
…
```
Mentions: OAI.KervaireCentralizer.Operator, OAI.KervaireCentralizer.algebra
theorem OAI.KervaireCentralizer.trace_apply line 142
theorem OAI.KervaireCentralizer.traceLog_inclusion line 146
Source documentation
The logarithm trace commutes with the centralizer inclusion.
```
theorem traceLog_inclusion (S : Set (Operator (H := H))) (ξ : ι → H)
…
```
Mentions: OAI.KervaireCentralizer.Operator
theorem OAI.KervaireCentralizer.smoothTrace_inclusion line 155
Source documentation
The smooth trace computed internally is the same operator trace.
```
theorem smoothTrace_inclusion (S : Set (Operator (H := H))) (ξ : ι → H)
…
```
Mentions: OAI.KervaireCentralizer.Operator
theorem OAI.KervaireCentralizer.exists_phaseOperator_mem line 161
Source documentation
The bounded phase logarithm stays in every operator centralizer.
```
theorem exists_phaseOperator_mem (S : Set (Operator (H := H))) (U : algebra S)
…
```
Mentions: OAI.KervaireCentralizer.Operator, OAI.KervaireCentralizer.algebra
theorem OAI.KervaireCentralizer.phase_subadditive line 188
Source documentation
Spectral phase subadditivity in a finite-vector tracial centralizer. The trace property will be proved for the arbitrary-group matrix representation.
```
theorem phase_subadditive [Nontrivial H] (S : Set (Operator (H := H))) (ξ : ι → H)
…
```
Mentions: OAI.KervaireCentralizer.Operator