Range.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The surjectivity step in the completely positive criterion

The first paragraph of Proposition 2.4 in the manuscript proves surjectivity from a reverse unit-ball gap strictly below one. The normed-space argument uses Riesz's lemma and requires no operator-algebra perturbation theorem.

theorem OAI.KadisonKastler.eq_top_of_unitBall_approx line 22

Source documentation

A closed complex subspace that uniformly approximates the unit ball to an error strictly below one must be the whole space.

theorem eq_top_of_unitBall_approx (V : Submodule ℂ E)
    (hclosed : IsClosed (V : Set E)) {c : ℝ} (hc : c < 1)
    (happrox : ∀ x : E, ‖x‖ ≤ 1 → ∃ y ∈ V, ‖x - y‖ ≤ c) : V = ⊤ := by
…

theorem OAI.KadisonKastler.surjective_of_closed_range_unitBall_approx line 41

Source documentation

The reverse-gap argument for a continuous linear map with closed range. The domain and codomain may have different norms and need not be algebras.

theorem surjective_of_closed_range_unitBall_approx (F : P →L[ℂ] Q)
    (hclosed : IsClosed (Set.range F)) {c : ℝ} (hc : c < 1)
    (happrox : ∀ y : Q, ‖y‖ ≤ 1 → ∃ x : P, ‖y - F x‖ ≤ c) :
    Function.Surjective F := by
…

theorem OAI.KadisonKastler.bijective_of_close_isometry_and_reverse_gap line 56

Source documentation

The range argument used in the manuscript's UCP criterion. Here ρ and ι are isometric embeddings into one ambient operator space. The reverse gap is expressed with arbitrary positive slack, so no nearest point or compactness hypothesis is hidden in the statement.

theorem bijective_of_close_isometry_and_reverse_gap [CompleteSpace P]
    (ρ : P →L[ℂ] E) (ι : Q →L[ℂ] E) (F : P →L[ℂ] Q)
    (hρ : ∀ x, ‖ρ x‖ = ‖x‖) (hι : ∀ y, ‖ι y‖ = ‖y‖)
    {e g : ℝ} (he : 0 ≤ e) (he1 : e < 1) (hge : g + e < 1)
    (hclose : ∀ x, ‖ι (F x) - ρ x‖ ≤ e * ‖x‖)
    (hgap : ∀ y : Q, ‖y‖ ≤ 1 → ∀ r : ℝ, g < r →
      ∃ x : P, ‖x‖ ≤ 1 ∧ ‖ι y - ρ x‖ < r) :
    Function.Bijective F := by
…