Amplification.lean`

26 declarations, 0 contain sorry, 0 declared as axioms

Matrix amplification and the main statements

Matrices act on finite Hilbert sums with their ℓ² norm. Consequently the norm in CommutatorEstimate is the concrete operator matrix norm, rather than the coordinatewise supremum norm of a matrix. No main estimate is assumed here.

abbrev OAI.KadisonSimilarity.HilbertCopies line 25
Source documentation
The Hilbert direct sum of n copies of H.
Also declared: ComparatorChallenges/KadisonSimilarity.lean:42 (same declaration text).
```
abbrev HilbertCopies (H : Type u) (n : ℕ) := PiLp 2 (fun _ : Fin n => H)
```
def OAI.KadisonSimilarity.matrixOperator line 28
Source documentation
An operator matrix acts by matrix-vector multiplication on the Hilbert sum.
Also declared: ComparatorChallenges/KadisonSimilarity.lean:44 (same declaration text).
```
def matrixOperator {n : ℕ} (X : Matrix (Fin n) (Fin n) (H →L[ℂ] H)) :
    HilbertCopies H n →L[ℂ] HilbertCopies H n :=
…
```
Mentions: OAI.KadisonSimilarity.HilbertCopies
theorem OAI.KadisonSimilarity.matrixOperator_apply line 34
def OAI.KadisonSimilarity.amplify line 40
Source documentation
The diagonal amplification of one operator.
Also declared: ComparatorChallenges/KadisonSimilarity.lean:50 (same declaration text).
```
def amplify (Y : H →L[ℂ] H) (n : ℕ) :
    HilbertCopies H n →L[ℂ] HilbertCopies H n :=
…
```
Mentions: OAI.KadisonSimilarity.HilbertCopies
theorem OAI.KadisonSimilarity.amplify_apply line 45
theorem OAI.KadisonSimilarity.norm_amplify_le line 50
Source documentation
Hilbert amplification does not increase the operator norm.
```
theorem norm_amplify_le (Y : H →L[ℂ] H) (n : ℕ) : ‖amplify Y n‖ ≤ ‖Y‖ := by
…
```
Mentions: OAI.KadisonSimilarity.amplify
theorem OAI.KadisonSimilarity.norm_amplify line 69
Source documentation
Positive finite amplification preserves the operator norm.
```
theorem norm_amplify (Y : H →L[ℂ] H) {n : ℕ} (hn : 0 < n) :
    ‖amplify Y n‖ = ‖Y‖ := by
…
```
Mentions: OAI.KadisonSimilarity.amplify
theorem OAI.KadisonSimilarity.commutator_amplify_matrixOperator line 86
Source documentation
Matrix amplification of an inner derivation agrees with the commutator of the amplified operator and the matrix operator.
```
theorem commutator_amplify_matrixOperator (Y : H →L[ℂ] H) {n : ℕ}
    (X : Matrix (Fin n) (Fin n) (H →L[ℂ] H)) :
    commutator (amplify Y n) (matrixOperator X) =
      matrixOperator (fun i j => commutator Y (X i j)) := by
…
```
Mentions: OAI.KadisonSimilarity.commutator, OAI.KadisonSimilarity.amplify, OAI.KadisonSimilarity.matrixOperator
def OAI.KadisonSimilarity.innerDerivation line 94
Source documentation
Inner derivation on the full bounded-operator algebra.
Distinct definitions of this name: ComparatorChallenges/KadisonSimilarity.lean:55 (same statement text; different proof or body). Qualify references as OAI.KadisonSimilarity.innerDerivation@path.
```
def innerDerivation (Y : H →L[ℂ] H) :
    (H →L[ℂ] H) →L[ℂ] (H →L[ℂ] H) :=
…
```
theorem OAI.KadisonSimilarity.innerDerivation_apply line 99
def OAI.KadisonSimilarity.scalarCommutatorNorm line 106
Source documentation
The scalar commutator seminorm g_P(Y), expressed as the norm of the bounded linear map a ↦ Ya - aY on the represented algebra.
Also declared: ComparatorChallenges/KadisonSimilarity.lean:62 (same declaration text).
```
def scalarCommutatorNorm (P : VonNeumannAlgebra H) (Y : H →L[ℂ] H) : ℝ := by
…
```
theorem OAI.KadisonSimilarity.scalarCommutatorNorm_nonneg line 111
theorem OAI.KadisonSimilarity.norm_commutator_le_scalarCommutatorNorm line 119
Source documentation
The defining operator norm controls every scalar commutator.
```
theorem norm_commutator_le_scalarCommutatorNorm (P : VonNeumannAlgebra H)
    (Y T : H →L[ℂ] H) (hT : T ∈ P) :
    ‖commutator Y T‖ ≤ scalarCommutatorNorm P Y * ‖T‖ := by
…
```
Mentions: OAI.KadisonSimilarity.commutator, OAI.KadisonSimilarity.scalarCommutatorNorm

theorem OAI.KadisonSimilarity.scalarCommutatorNorm_le_iff line 128

Source documentation

Characterization of the scalar commutator norm by homogeneous bounds.

theorem scalarCommutatorNorm_le_iff (P : VonNeumannAlgebra H)
    (Y : H →L[ℂ] H) {c : ℝ} (hc : 0 ≤ c) :
    scalarCommutatorNorm P Y ≤ c ↔
      ∀ T : H →L[ℂ] H, T ∈ P → ‖commutator Y T‖ ≤ c * ‖T‖ := by
…

Mentions: OAI.KadisonSimilarity.scalarCommutatorNorm, OAI.KadisonSimilarity.commutator

theorem OAI.KadisonSimilarity.scalarCommutatorNorm_le line 144
Source documentation
The scalar seminorm is finite with the elementary commutator bound.
```
theorem scalarCommutatorNorm_le (P : VonNeumannAlgebra H) (Y : H →L[ℂ] H) :
    scalarCommutatorNorm P Y ≤ 2 * ‖Y‖ := by
…
```
Mentions: OAI.KadisonSimilarity.scalarCommutatorNorm
theorem OAI.KadisonSimilarity.scalarCommutatorNorm_perturb line 153
Source documentation
The averaging perturbation estimate for the scalar commutator seminorm.
```
theorem scalarCommutatorNorm_perturb (P : VonNeumannAlgebra H)
    (Y Z : H →L[ℂ] H) :
    scalarCommutatorNorm P Y ≤ scalarCommutatorNorm P Z + 2 * ‖Y - Z‖ := by
…
```
Mentions: OAI.KadisonSimilarity.scalarCommutatorNorm
def OAI.KadisonSimilarity.CommutatorEstimate line 171
Source documentation
The fixed-algebra conclusion of the manuscript's uniform estimate.
Also declared: ComparatorChallenges/KadisonSimilarity.lean:67 (same declaration text).
```
def CommutatorEstimate (P : VonNeumannAlgebra H) (C : ℝ) : Prop :=
…
```
def OAI.KadisonSimilarity.UniformCommutatorEstimate line 178
Source documentation
The exact universal quantifiers of Theorem thm:universal.
Also declared: ComparatorChallenges/KadisonSimilarity.lean:73 (same declaration text).
```
def UniformCommutatorEstimate (C : ℝ) : Prop :=
…
```
def OAI.KadisonSimilarity.UniversalCommutatorTheorem line 183
Source documentation
The existence of a single numerical constant in Theorem thm:universal.
Also declared: ComparatorChallenges/KadisonSimilarity.lean:77 (same declaration text).
```
def UniversalCommutatorTheorem : Prop := ∃ C : ℝ, 0 ≤ C ∧ UniformCommutatorEstimate.{u} C
```
def OAI.KadisonSimilarity.SimilarityTheorem line 186
Source documentation
The exact unrestricted similarity statement, Theorem thm:similarity.
Also declared: ComparatorChallenges/KadisonSimilarity.lean:79 (same declaration text).
```
def SimilarityTheorem : Prop :=
…
```
abbrev OAI.KadisonSimilarity.CommutantProjection line 192
Source documentation
The projections indexing the usual off-diagonal distance seminorm.
Also declared: ComparatorChallenges/KadisonSimilarity.lean:84 (same declaration text).
```
abbrev CommutantProjection (M : VonNeumannAlgebra H) :=
…
```
def OAI.KadisonSimilarity.offDiagonalSeminorm line 196
Source documentation
The off-diagonal distance seminorm from Corollary cor:hyperreflexivity.
Also declared: ComparatorChallenges/KadisonSimilarity.lean:87 (same declaration text).
```
def offDiagonalSeminorm (M : VonNeumannAlgebra H) (T : H →L[ℂ] H) : ℝ :=
…
```
theorem OAI.KadisonSimilarity.norm_projection_le_one line 201
Source documentation
Orthogonal projections are contractions, including the zero projection.
```
theorem norm_projection_le_one (e : H →L[ℂ] H) (hstar : star e = e)
    (hsq : e * e = e) : ‖e‖ ≤ 1 := by
…
```
theorem OAI.KadisonSimilarity.norm_one_sub_projection_le_one line 207
theorem OAI.KadisonSimilarity.offDiagonalSeminorm_le line 216
Source documentation
The off-diagonal supremum is bounded by the operator norm.
```
theorem offDiagonalSeminorm_le (M : VonNeumannAlgebra H) (T : H →L[ℂ] H) :
    offDiagonalSeminorm M T ≤ ‖T‖ := by
…
```
Mentions: OAI.KadisonSimilarity.offDiagonalSeminorm
def OAI.KadisonSimilarity.UniversalHyperreflexivity line 237
Source documentation
The quantitative conclusion of Corollary cor:hyperreflexivity, with the same constant as the universal commutator theorem.
Also declared: ComparatorChallenges/KadisonSimilarity.lean:91 (same declaration text).
```
def UniversalHyperreflexivity (C : ℝ) : Prop :=
…
```