DicksonAdjoint.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

The adjoint homomorphism and the exact row-to-column transfer.

def OAI.KadisonSimilarity.sharpHom line 14
Source documentation
Taking adjoints in both source and target preserves the algebra map.
```
def sharpHom (π : BoundedUnitalHom A H) : BoundedUnitalHom A H :=
…
```
Mentions: OAI.KadisonSimilarity.BoundedUnitalHom
theorem OAI.KadisonSimilarity.sharpHom_apply line 28
theorem OAI.KadisonSimilarity.sharpHom_bound line 32
Source documentation
Every pointwise operator bound is preserved by the sharp operation.
```
theorem sharpHom_bound (π : BoundedUnitalHom A H) {C : ℝ}
    (hπ : ∀ a, ‖π.1 a‖ ≤ C * ‖a‖) (a : A) :
    ‖(sharpHom π).1 a‖ ≤ C * ‖a‖ := by
…
```
Mentions: OAI.KadisonSimilarity.BoundedUnitalHom, OAI.KadisonSimilarity.sharpHom

theorem OAI.KadisonSimilarity.rectangularMatrixOperator_adjoint line 38

Source documentation

The concrete finite rectangular adjoint is entrywise adjoint and transpose.

theorem rectangularMatrixOperator_adjoint {F K : Type*}
    [NormedAddCommGroup F] [InnerProductSpace ℂ F] [CompleteSpace F]
    [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K]
    {p q : ℕ} (X : Matrix (Fin p) (Fin q) (K →L[ℂ] F)) :
    (rectangularMatrixOperator X).adjoint =
      rectangularMatrixOperator (fun i j => (X j i).adjoint) := by
…

Mentions: OAI.KadisonSimilarity.rectangularMatrixOperator

theorem OAI.KadisonSimilarity.columnBound_of_sharp_rowBound line 60
Source documentation
A row estimate for the sharp map is the same column estimate for the original homomorphism, with the native rectangular C-star matrix norm.
```
theorem columnBound_of_sharp_rowBound (π : BoundedUnitalHom A H) {C : ℝ}
    (hrow : RowBound (sharpHom π).1 C) : ColumnBound π.1 C := by
…
```
Mentions: OAI.KadisonSimilarity.BoundedUnitalHom, OAI.KadisonSimilarity.RowBound, OAI.KadisonSimilarity.sharpHom, OAI.KadisonSimilarity.ColumnBound
theorem OAI.KadisonSimilarity.dicksonTwoBound_of_row line 79
Source documentation
Only the row half of Dickson's estimate needs an analytic proof.
```
theorem dicksonTwoBound_of_row
    (hrow : ∀ π : BoundedUnitalHom A H, (∀ a, ‖π.1 a‖ ≤ 2 * ‖a‖) →
      RowBound π.1 (4 * Real.sqrt 2)) : DicksonTwoBound (A := A) H := by
…
```
Mentions: OAI.KadisonSimilarity.BoundedUnitalHom, OAI.KadisonSimilarity.RowBound, OAI.KadisonSimilarity.DicksonTwoBound