Multiplication.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Multiplicative defects of maps close to a representation

These estimates are the normed-algebra calculation used in the UCP criterion in §2 of Universal strong Kadison–Kastler stability (2026). They require no positivity theorem: contractivity, where used, is an explicit hypothesis.

theorem OAI.KadisonKastler.norm_image_le_of_close_to_isometric_hom line 21

Source documentation

A map within e of an isometric representation has norm at most 1 + e.

theorem norm_image_le_of_close_to_isometric_hom
    (ρ : A →ₐ[ℂ] B) (F : A →ₗ[ℂ] B) {e : ℝ}
    (hρ : ∀ x, ‖ρ x‖ = ‖x‖)
    (hclose : ∀ x, ‖F x - ρ x‖ ≤ e * ‖x‖) (x : A) :
    ‖F x‖ ≤ (1 + e) * ‖x‖ := by
…

theorem OAI.KadisonKastler.multiplicative_defect_le_three_terms line 33

Source documentation

A three-term defect estimate, keeping the norm of the map on the left factor visible so that contractivity can improve the final bound.

theorem multiplicative_defect_le_three_terms
    (ρ : A →ₐ[ℂ] B) (F : A →ₗ[ℂ] B) {e : ℝ}
    (hρ : ∀ x, ‖ρ x‖ = ‖x‖)
    (hclose : ∀ x, ‖F x - ρ x‖ ≤ e * ‖x‖) (x y : A) :
    ‖F (x * y) - F x * F y‖ ≤
      e * ‖x * y‖ + e * ‖x‖ * ‖y‖ + ‖F x‖ * (e * ‖y‖) := by
…

theorem OAI.KadisonKastler.multiplicative_defect_le_of_close_to_isometric_hom line 64

Source documentation

The general perturbation bound without an assumption that F is contractive.

theorem multiplicative_defect_le_of_close_to_isometric_hom
    (ρ : A →ₐ[ℂ] B) (F : A →ₗ[ℂ] B) {e : ℝ} (he : 0 ≤ e)
    (hρ : ∀ x, ‖ρ x‖ = ‖x‖)
    (hclose : ∀ x, ‖F x - ρ x‖ ≤ e * ‖x‖) (x y : A) :
    ‖F (x * y) - F x * F y‖ ≤ (3 * e + e ^ 2) * ‖x‖ * ‖y‖ := by
…

theorem OAI.KadisonKastler.multiplicative_defect_le_of_contractive_close_to_isometric_hom line 83

Source documentation

Contractivity removes the quadratic term, yielding the 3e estimate used for UCP maps in the manuscript.

theorem multiplicative_defect_le_of_contractive_close_to_isometric_hom
    (ρ : A →ₐ[ℂ] B) (F : A →ₗ[ℂ] B) {e : ℝ} (he : 0 ≤ e)
    (hρ : ∀ x, ‖ρ x‖ = ‖x‖)
    (hclose : ∀ x, ‖F x - ρ x‖ ≤ e * ‖x‖)
    (hcontractive : ∀ x, ‖F x‖ ≤ ‖x‖) (x y : A) :
    ‖F (x * y) - F x * F y‖ ≤ 3 * e * ‖x‖ * ‖y‖ := by
…