RelativeMatrixQuantization.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Relative finite matrix averaging in an irreducible inclusion. The matrix systems stay in the prescribed source algebra throughout the refinement.

theorem OAI.KadisonSimilarity.map_matrix_rankOne line 16
theorem OAI.KadisonSimilarity.matrix_stage_size_le_of_algebra_le line 43
theorem OAI.KadisonSimilarity.exists_relative_matrix_expectation_budget line 51

theorem OAI.KadisonSimilarity.exists_source_rankOne_compression line 65

Source documentation

A small phase-energy budget gives a nonzero compression in the source algebra, with its exact trace retained in the ambient representation.

theorem exists_source_rankOne_compression {I : Type*} [Fintype I]
    (E : FiniteMatrixStage N) (x : I → M.toStarSubalgebra) {δ : ℝ}
    (hbudget : (∑ i,
      (‖(vectorPositiveFunctional M υ.vector).toPreGNS
          ((matrixSystemOfUnits (E.units.map (coordinateInclusion hNM))).expectation (x i))‖ ^ 2 +
        ‖(vectorPositiveFunctional M υ.vector).toPreGNS (x i)‖ ^ 2 / (E.size : ℝ))) < δ) :
    ∃ q : N.toStarSubalgebra, IsStarProjection q ∧ q ≠ 0 ∧
      υ.trace (coordinateInclusion hNM q) = (E.size : ℂ)⁻¹ ∧
      ∀ i, ‖(vectorPositiveFunctional M υ.vector).toPreGNS
        (coordinateInclusion hNM q * x i * coordinateInclusion hNM q)‖ ^ 2 <
          δ * (υ.trace (coordinateInclusion hNM q)).re := by
…

Mentions: OAI.KadisonSimilarity.vectorPositiveFunctional, OAI.KadisonSimilarity.matrixSystemOfUnits

theorem OAI.KadisonSimilarity.exists_source_small_projection line 110

Source documentation

Relative local quantization with a small projection in the prescribed source, using its cofinal family of finite matrix stages.

theorem exists_source_small_projection {I : Type*} [Fintype I]
    (T : ℕ → FiniteMatrixStage N) (hT : ∀ m : ℕ, ∃ j, m < (T j).size)
    (x : I → M.toStarSubalgebra) (hx : ∀ i, υ.trace (x i) = 0)
    {δ η : ℝ} (hδ : 0 < δ) (hη : 0 < η) :
    ∃ q : N.toStarSubalgebra, IsStarProjection q ∧ q ≠ 0 ∧
      (υ.trace (coordinateInclusion hNM q)).re < η ∧
      ∀ i, ‖(vectorPositiveFunctional M υ.vector).toPreGNS
        (coordinateInclusion hNM q * x i * coordinateInclusion hNM q)‖ ^ 2 <
          δ * (υ.trace (coordinateInclusion hNM q)).re := by
…

Mentions: OAI.KadisonSimilarity.vectorPositiveFunctional

theorem OAI.KadisonSimilarity.exists_source_matrix_stage line 155
Source documentation
Every required finite size occurs in the diffuse source; no separable matrix tower is needed for the local estimate.
```
theorem exists_source_matrix_stage (n : ℕ) (hn : 0 < n) :
    ∃ E : FiniteMatrixStage N, E.size = n := by
…
```

theorem OAI.KadisonSimilarity.exists_source_small_projection_of_diffuse line 163

Source documentation

Relative local quantization without a chosen matrix tower.

theorem exists_source_small_projection_of_diffuse {I : Type*} [Fintype I]
    (x : I → M.toStarSubalgebra) (hx : ∀ i, υ.trace (x i) = 0)
    {δ η : ℝ} (hδ : 0 < δ) (hη : 0 < η) :
    ∃ q : N.toStarSubalgebra, IsStarProjection q ∧ q ≠ 0 ∧
      (υ.trace (coordinateInclusion hNM q)).re < η ∧
      ∀ i, ‖(vectorPositiveFunctional M υ.vector).toPreGNS
        (coordinateInclusion hNM q * x i * coordinateInclusion hNM q)‖ ^ 2 <
          δ * (υ.trace (coordinateInclusion hNM q)).re := by
…

Mentions: OAI.KadisonSimilarity.vectorPositiveFunctional