RectangularDerivations.lean`

36 declarations, 0 contain sorry, 0 declared as axioms

Rectangular derivations and the row/column estimate

def OAI.KadisonSimilarity.rectangularMatrixOperator line 16
Source documentation
Finite rectangular operator matrices act between the two Hilbert sums.
```
def rectangularMatrixOperator {p q : ℕ}
    (X : Matrix (Fin p) (Fin q) (K →L[ℂ] F)) :
    HilbertCopies K q →L[ℂ] HilbertCopies F p :=
…
```
Mentions: OAI.KadisonSimilarity.HilbertCopies
theorem OAI.KadisonSimilarity.rectangularMatrixOperator_apply line 23
theorem OAI.KadisonSimilarity.rectangularMatrixOperator_zero line 29
theorem OAI.KadisonSimilarity.rectangularMatrixOperator_smul line 34
def OAI.KadisonSimilarity.mapCopies line 41
Source documentation
Coordinatewise amplification of a bounded operator between different spaces.
```
def mapCopies (T : K →L[ℂ] F) (n : ℕ) : HilbertCopies K n →L[ℂ] HilbertCopies F n :=
…
```
Mentions: OAI.KadisonSimilarity.HilbertCopies
theorem OAI.KadisonSimilarity.mapCopies_apply line 45
theorem OAI.KadisonSimilarity.norm_mapCopies_le line 49
abbrev OAI.KadisonSimilarity.RectangularSum line 68
Source documentation
The Hilbert direct sum used in the rectangular triangular representation.
```
abbrev RectangularSum (F K : Type*) := WithLp 2 (F × K)
```
def OAI.KadisonSimilarity.rectangularInl line 70
def OAI.KadisonSimilarity.rectangularInr line 74
theorem OAI.KadisonSimilarity.rectangularInl_apply line 78
theorem OAI.KadisonSimilarity.rectangularInr_apply line 82
theorem OAI.KadisonSimilarity.norm_rectangularInr_le_one line 86
theorem OAI.KadisonSimilarity.norm_rectangularFst_le_one line 92

theorem OAI.KadisonSimilarity.rectangularMatrixOperator_corner line 98

Source documentation

Matrix amplification respects compression to the upper-right corner.

theorem rectangularMatrixOperator_corner {p q : ℕ}
    (X : Matrix (Fin p) (Fin q)
      (RectangularSum F K →L[ℂ] RectangularSum F K)) :
    rectangularMatrixOperator (fun i j => (WithLp.fstL 2 ℂ F K).comp
      ((X i j).comp rectangularInr)) =
      (mapCopies (WithLp.fstL 2 ℂ F K) p).comp
        ((rectangularMatrixOperator X).comp (mapCopies rectangularInr q)) := by
…

Mentions: OAI.KadisonSimilarity.RectangularSum, OAI.KadisonSimilarity.rectangularMatrixOperator, OAI.KadisonSimilarity.rectangularInr, OAI.KadisonSimilarity.mapCopies

theorem OAI.KadisonSimilarity.norm_compression_le line 122
theorem OAI.KadisonSimilarity.norm_rectangularCorner_le line 142
Source documentation
Compression to the upper-right corner of every entry does not increase the norm of a rectangular operator matrix.
```
theorem norm_rectangularCorner_le {p q : ℕ}
    (X : Matrix (Fin p) (Fin q)
      (RectangularSum F K →L[ℂ] RectangularSum F K)) :
    ‖rectangularMatrixOperator (fun i j => (WithLp.fstL 2 ℂ F K).comp
      ((X i j).comp rectangularInr))‖ ≤ ‖rectangularMatrixOperator X‖ := by
…
```
Mentions: OAI.KadisonSimilarity.RectangularSum, OAI.KadisonSimilarity.rectangularMatrixOperator, OAI.KadisonSimilarity.rectangularInr
def OAI.KadisonSimilarity.rectangularTriangular line 159
Source documentation
The diagonal plus one upper-right block.
```
def rectangularTriangular (ρ : F →L[ℂ] F) (δ : K →L[ℂ] F) (σ : K →L[ℂ] K) :
    RectangularSum F K →L[ℂ] RectangularSum F K :=
…
```
Mentions: OAI.KadisonSimilarity.RectangularSum
theorem OAI.KadisonSimilarity.rectangularTriangular_fst line 165
theorem OAI.KadisonSimilarity.rectangularTriangular_snd line 170

theorem OAI.KadisonSimilarity.norm_rectangularDiagonal_le line 176

Source documentation

Contractive diagonal blocks give a contractive diagonal operator.

theorem norm_rectangularDiagonal_le (ρ : F →L[ℂ] F) (σ : K →L[ℂ] K)
    {c : ℝ} (hc : 0 ≤ c) (hρ : ‖ρ‖ ≤ c) (hσ : ‖σ‖ ≤ c) :
    ‖rectangularTriangular ρ 0 σ‖ ≤ c := by
…

Mentions: OAI.KadisonSimilarity.rectangularTriangular

theorem OAI.KadisonSimilarity.norm_rectangularOffDiagonal_le line 197
Source documentation
The off-diagonal corner has the same norm bound as its sole block.
```
theorem norm_rectangularOffDiagonal_le (δ : K →L[ℂ] F) :
    ‖rectangularTriangular 0 δ 0‖ ≤ ‖δ‖ := by
…
```
Mentions: OAI.KadisonSimilarity.rectangularTriangular

theorem OAI.KadisonSimilarity.norm_rectangularTriangular_le line 209

Source documentation

The pointwise triangular estimate used before applying Dickson.

theorem norm_rectangularTriangular_le (ρ : F →L[ℂ] F) (δ : K →L[ℂ] F)
    (σ : K →L[ℂ] K) {c : ℝ} (hc : 0 ≤ c) (hρ : ‖ρ‖ ≤ c) (hσ : ‖σ‖ ≤ c) :
    ‖rectangularTriangular ρ δ σ‖ ≤ c + ‖δ‖ := by
…

Mentions: OAI.KadisonSimilarity.rectangularTriangular

theorem OAI.KadisonSimilarity.rectangularDerivation_map_one line 227

Source documentation

A rectangular derivation vanishes at the identity.

theorem rectangularDerivation_map_one (ρ : A →⋆ₐ[ℂ] (F →L[ℂ] F))
    (σ : A →⋆ₐ[ℂ] (K →L[ℂ] K)) (δ : A →L[ℂ] (K →L[ℂ] F))
    (hδ : ∀ a b, δ (a * b) = (ρ a).comp (δ b) + (δ a).comp (σ b)) : δ 1 = 0 := by
…

def OAI.KadisonSimilarity.rectangularRepresentation line 237

Source documentation

The bounded unital triangular homomorphism of a rectangular derivation.

def rectangularRepresentation (ρ : A →⋆ₐ[ℂ] (F →L[ℂ] F))
    (σ : A →⋆ₐ[ℂ] (K →L[ℂ] K)) (δ : A →L[ℂ] (K →L[ℂ] F))
    (hδ : ∀ a b, δ (a * b) = (ρ a).comp (δ b) + (δ a).comp (σ b)) :
    BoundedUnitalHom A (RectangularSum F K) := by
…

Mentions: OAI.KadisonSimilarity.BoundedUnitalHom, OAI.KadisonSimilarity.RectangularSum

theorem OAI.KadisonSimilarity.norm_rectangularRepresentation_apply line 274

Source documentation

The norm estimate which gives norm at most two after normalization.

theorem norm_rectangularRepresentation_apply (ρ : A →⋆ₐ[ℂ] (F →L[ℂ] F))
    (σ : A →⋆ₐ[ℂ] (K →L[ℂ] K)) (δ : A →L[ℂ] (K →L[ℂ] F))
    (hδ : ∀ a b, δ (a * b) = (ρ a).comp (δ b) + (δ a).comp (σ b)) (a : A) :
    ‖(rectangularRepresentation ρ σ δ hδ).1 a‖ ≤ (1 + ‖δ‖) * ‖a‖ := by
…

Mentions: OAI.KadisonSimilarity.rectangularRepresentation

def OAI.KadisonSimilarity.normalizedRectangularDerivation line 287
Source documentation
Rescaling the derivation before forming the triangular representation.
```
def normalizedRectangularDerivation (δ : A →L[ℂ] (K →L[ℂ] F)) :
    A →L[ℂ] (K →L[ℂ] F) := ((‖δ‖⁻¹ : ℝ) : ℂ) • δ
…
```
theorem OAI.KadisonSimilarity.norm_normalizedRectangularDerivation_le line 291
theorem OAI.KadisonSimilarity.normalizedRectangularDerivation_leibniz line 300
def OAI.KadisonSimilarity.normalizedRectangularRepresentation line 309

theorem OAI.KadisonSimilarity.norm_normalizedRectangularRepresentation_le_two line 317

Source documentation

The normalized triangular representation meets Dickson's norm-two hypothesis.

theorem norm_normalizedRectangularRepresentation_le_two
    (ρ : A →⋆ₐ[ℂ] (F →L[ℂ] F)) (σ : A →⋆ₐ[ℂ] (K →L[ℂ] K))
    (δ : A →L[ℂ] (K →L[ℂ] F))
    (hδ : ∀ a b, δ (a * b) = (ρ a).comp (δ b) + (δ a).comp (σ b)) (a : A) :
    ‖(rectangularRepresentation ρ σ (normalizedRectangularDerivation δ)
      (normalizedRectangularDerivation_leibniz ρ σ δ hδ)).1 a‖ ≤ 2 * ‖a‖ := by
…

Mentions: OAI.KadisonSimilarity.rectangularRepresentation, OAI.KadisonSimilarity.normalizedRectangularDerivation, OAI.KadisonSimilarity.normalizedRectangularDerivation_leibniz

def OAI.KadisonSimilarity.RowBound line 332
Source documentation
Uniform row-amplification bound with the rectangular C-star matrix norm.
```
def RowBound (f : A → (K →L[ℂ] F)) (C : ℝ) : Prop :=
…
```
def OAI.KadisonSimilarity.ColumnBound line 337
Source documentation
Uniform column-amplification bound with the rectangular C-star matrix norm.
```
def ColumnBound (f : A → (K →L[ℂ] F)) (C : ℝ) : Prop :=
…
```
def OAI.KadisonSimilarity.DicksonTwoBound line 343
Source documentation
The norm-two specialization of Dickson (2014), Lemma 2.9, Eq. (19), including its column form obtained by taking adjoints.
```
def DicksonTwoBound (H : Type*) [NormedAddCommGroup H]
    [InnerProductSpace ℂ H] [CompleteSpace H] : Prop :=
…
```

theorem OAI.KadisonSimilarity.rectangularDerivation_matrix_bound_of_triangular line 350

Source documentation

The upper-right corner transfers any matrix estimate for the normalized triangular representation to the original derivation.

theorem rectangularDerivation_matrix_bound_of_triangular
    (ρ : A →⋆ₐ[ℂ] (F →L[ℂ] F)) (σ : A →⋆ₐ[ℂ] (K →L[ℂ] K))
    (δ : A →L[ℂ] (K →L[ℂ] F))
    (hδ : ∀ a b, δ (a * b) = (ρ a).comp (δ b) + (δ a).comp (σ b))
    {p q : ℕ} (X : Matrix (Fin p) (Fin q) A) {C : ℝ}
    (htri : ‖rectangularMatrixOperator
      (X.map (normalizedRectangularRepresentation ρ σ δ hδ).1)‖ ≤
        C * ‖CStarMatrix.ofMatrix X‖) :
    ‖rectangularMatrixOperator (X.map δ)‖ ≤ (C * ‖δ‖) * ‖CStarMatrix.ofMatrix X‖ := by
…

Mentions: OAI.KadisonSimilarity.rectangularMatrixOperator, OAI.KadisonSimilarity.normalizedRectangularRepresentation

theorem OAI.KadisonSimilarity.rectangularDerivation_row_column line 403

Source documentation

The manuscript's row/column derivation estimate, conditional only on the norm-two specialization of the published Dickson estimate.

theorem rectangularDerivation_row_column
    (ρ : A →⋆ₐ[ℂ] (F →L[ℂ] F)) (σ : A →⋆ₐ[ℂ] (K →L[ℂ] K))
    (δ : A →L[ℂ] (K →L[ℂ] F))
    (hδ : ∀ a b, δ (a * b) = (ρ a).comp (δ b) + (δ a).comp (σ b))
    (dickson : DicksonTwoBound (A := A) (RectangularSum F K)) :
…

Mentions: OAI.KadisonSimilarity.DicksonTwoBound, OAI.KadisonSimilarity.RectangularSum