TracialSymmetryDilation.lean`

16 declarations, 0 contain sorry, 0 declared as axioms

Centered symmetry tests for contractions. The selfadjoint two-by-two dilation has opposite diagonal entries, so its normalized trace vanishes for every linear functional. Applying it to the selfadjoint off-diagonal matrix of an arbitrary contraction yields a four-by-four symmetry with the original contraction as one entry. This avoids any extra spectral trace-equality hypothesis.

def OAI.KadisonSimilarity.linearMatrixTrace line 21
Source documentation
The normalized two-by-two matrix extension of a linear functional.
```
def linearMatrixTrace (τ : A →ₗ[ℂ] ℂ) : Mat A →ₗ[ℂ] ℂ where
…
```
theorem OAI.KadisonSimilarity.linearMatrixTrace_apply line 28
def OAI.KadisonSimilarity.selfAdjointSymmetryDilation line 39
Source documentation
The two-by-two symmetry associated to a selfadjoint contraction.
```
def selfAdjointSymmetryDilation (a : A) : Mat A :=
…
```
theorem OAI.KadisonSimilarity.selfAdjointSymmetryDilation_entry line 42
theorem OAI.KadisonSimilarity.selfAdjointSymmetryDilation_star line 46
theorem OAI.KadisonSimilarity.selfAdjoint_defect_nonneg line 52
theorem OAI.KadisonSimilarity.selfAdjoint_defect_sqrt_commutes line 60
theorem OAI.KadisonSimilarity.selfAdjointSymmetryDilation_sq line 67
def OAI.KadisonSimilarity.selfAdjointSymmetryUnitary line 78
Source documentation
The symmetry as an actual unitary, with no existence assumption.
```
def selfAdjointSymmetryUnitary (a : A) (ha : IsSelfAdjoint a) (hn : ‖a‖ ≤ 1) :
    unitary (Mat A) :=
…
```
theorem OAI.KadisonSimilarity.linearMatrixTrace_selfAdjointSymmetryDilation line 87
Source documentation
Opposite diagonal entries make the dilation centered without any centering condition on its input.
```
theorem linearMatrixTrace_selfAdjointSymmetryDilation (τ : A →ₗ[ℂ] ℂ) (a : A) :
    linearMatrixTrace τ (selfAdjointSymmetryDilation a) = 0 := by
…
```
Mentions: OAI.KadisonSimilarity.linearMatrixTrace, OAI.KadisonSimilarity.selfAdjointSymmetryDilation
def OAI.KadisonSimilarity.contractionSymmetryUnitary line 93
Source documentation
A centered four-by-four symmetry containing an arbitrary contraction. The blocks use the existing selfadjoint off-diagonal contraction lemma.
```
def contractionSymmetryUnitary (a : A) (ha : ‖a‖ ≤ 1) : unitary (Mat (Mat A)) :=
…
```
theorem OAI.KadisonSimilarity.contractionSymmetryUnitary_star line 97
theorem OAI.KadisonSimilarity.contractionSymmetryUnitary_sq line 101
theorem OAI.KadisonSimilarity.contractionSymmetryUnitary_entry line 105
theorem OAI.KadisonSimilarity.linearMatrixTrace_contractionSymmetryUnitary line 111
theorem OAI.KadisonSimilarity.exists_centered_symmetry_dilation line 117