AdjointSurjectivity.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.SeparableQuotient.ball_image_closure_of_adjoint_bound line 16

Source documentation

Hahn–Banach ball inclusion with a quantitative lower bound.

theorem ball_image_closure_of_adjoint_bound
    (T : E →L[ℝ] F) (c : ℝ) (_hc : 0 < c)
    (hT : ∀ g : StrongDual ℝ F, c * ‖g‖ ≤ ‖g.comp T‖) :
    closedBall (0 : F) c ⊆ closure (T '' closedBall (0 : E) 1) := by
…

theorem OAI.SeparableQuotient.approximate_lift_of_adjoint_bound line 46

Source documentation

Approximate lifting with a quantitative norm bound.

theorem approximate_lift_of_adjoint_bound
    (T : E →L[ℝ] F) (c : ℝ) (hc : 0 < c)
    (hT : ∀ g : StrongDual ℝ F, c * ‖g‖ ≤ ‖g.comp T‖) (y : F) :
    ∃ x : E, ‖y - T x‖ ≤ (1 / 2 : ℝ) * ‖y‖ ∧ ‖x‖ ≤ c⁻¹ * ‖y‖ := by
…

theorem OAI.SeparableQuotient.exact_lift_of_approximate line 79

Source documentation

The elementary completion argument, with no open-mapping assumption.

theorem exact_lift_of_approximate [CompleteSpace E]
    (T : E →L[ℝ] F) (C : ℝ) (hC : 0 ≤ C)
    (ha : ∀ y : F, ∃ x : E, ‖y - T x‖ ≤ (1 / 2 : ℝ) * ‖y‖ ∧ ‖x‖ ≤ C * ‖y‖)
    (y : F) : ∃ x : E, T x = y ∧ ‖x‖ ≤ 2 * C * ‖y‖ := by
…

theorem OAI.SeparableQuotient.surjective_of_adjoint_bound line 135

Source documentation

Adjoint lower bounds force surjectivity.

theorem surjective_of_adjoint_bound [CompleteSpace E]
    (T : E →L[ℝ] F) (c : ℝ) (hc : 0 < c)
    (hT : ∀ g : StrongDual ℝ F, c * ‖g‖ ≤ ‖g.comp T‖) :
    Function.Surjective T := by
…

theorem OAI.SeparableQuotient.surjective_of_adjoint_bound_rclike line 151

Source documentation

The surjectivity test over either original scalar field.

theorem surjective_of_adjoint_bound_rclike
    (T : E →L[𝕜] F) (c : ℝ) (hc : 0 < c)
    (hT : ∀ g : StrongDual 𝕜 F, c * ‖g‖ ≤ ‖g.comp T‖) :
    Function.Surjective T := by
…