QuantitativeImplementation.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Quantitative implementation from a triangular similarity

Conjugating an orthogonal projection gives the implementing corner directly. The norm bound is the condition number of the given similarity.

theorem OAI.KadisonSimilarity.exists_commuting_projection_norm line 20

Source documentation

A fixed similarity gives a commuting projection with norm bounded by its condition number.

theorem exists_commuting_projection_norm (π : BoundedUnitalHom A H)
    (S : (H →L[ℂ] H)ˣ)
    (hS : ∀ a : A, (S : H →L[ℂ] H) * π.1 (star a) * (↑S⁻¹ : H →L[ℂ] H) =
      star ((S : H →L[ℂ] H) * π.1 a * (↑S⁻¹ : H →L[ℂ] H)))
    (M : ClosedSubmodule ℂ H) (hM : ∀ a x, x ∈ M → π.1 a x ∈ M) :
    ∃ P : H →L[ℂ] H, (∀ x, P x ∈ M) ∧
      (∀ x, x ∈ M → P x = x) ∧ (∀ a, Commute P (π.1 a)) ∧
      ‖P‖ ≤ ‖(S : H →L[ℂ] H)‖ * ‖(↑S⁻¹ : H →L[ℂ] H)‖ := by
…

Mentions: OAI.KadisonSimilarity.BoundedUnitalHom

theorem OAI.KadisonSimilarity.rectangular_inner_of_similarity_norm line 75

Source documentation

The implementing upper-right corner inherits the condition-number bound.

theorem rectangular_inner_of_similarity_norm
    (ρ : A →⋆ₐ[ℂ] (F →L[ℂ] F)) (σ : A →⋆ₐ[ℂ] (K →L[ℂ] K))
    (δ : A →L[ℂ] (K →L[ℂ] F))
    (hδ : ∀ a b, δ (a * b) = (ρ a).comp (δ b) + (δ a).comp (σ b))
    (S : (RectangularSum F K →L[ℂ] RectangularSum F K)ˣ)
    (hS : ∀ a : A,
      (S : RectangularSum F K →L[ℂ] RectangularSum F K) *
        (rectangularRepresentation ρ σ δ hδ).1 (star a) * ↑S⁻¹ =
      star ((S : RectangularSum F K →L[ℂ] RectangularSum F K) *
        (rectangularRepresentation ρ σ δ hδ).1 a * ↑S⁻¹)) :
    ∃ V : K →L[ℂ] F, (∀ a, δ a = V.comp (σ a) - (ρ a).comp V) ∧
      ‖V‖ ≤ ‖(S : RectangularSum F K →L[ℂ] RectangularSum F K)‖ *
…

Mentions: OAI.KadisonSimilarity.RectangularSum, OAI.KadisonSimilarity.rectangularRepresentation