RadialPerturbation.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Small radial perturbations from strict support signs

Compactness is used only on the continuous dual of the span of two vectors. The public result has no finite-dimensional or completeness hypothesis on the ambient real normed space.

theorem OAI.Tingley.exists_dual_gap_of_supportAt_neg line 21
theorem OAI.Tingley.exists_radial_perturbation_lt_finiteDimensional line 53

theorem OAI.Tingley.exists_radial_perturbation_lt line 87

Source documentation

Strict negativity on the perturbing vector for every support at a unit vector makes all sufficiently small positive radial perturbations shorter. Only the span of the two specified vectors is made finite-dimensional.

theorem exists_radial_perturbation_lt
    {X : Type*} [NormedAddCommGroup X] [NormedSpace ℝ X]
    {v y : X} {p : ℝ} (hv : ‖v‖ = 1) (hp : 0 < p)
    (hneg : ∀ φ : X →L[ℝ] ℝ, SupportAt φ v → φ y < 0) :
    ∃ δ : ℝ, 0 < δ ∧ ∀ η : ℝ, 0 < η → η < δ →
      ‖p • v + η • y‖ < p := by
…

Mentions: OAI.Tingley.SupportAt

theorem OAI.Tingley.exists_radial_perturbation_lt_with_cap line 110

Source documentation

The perturbation may also be chosen below any prescribed positive cap.

theorem exists_radial_perturbation_lt_with_cap
    {X : Type*} [NormedAddCommGroup X] [NormedSpace ℝ X]
    {v y : X} {p t : ℝ} (hv : ‖v‖ = 1) (hp : 0 < p) (ht : 0 < t)
    (hneg : ∀ φ : X →L[ℝ] ℝ, SupportAt φ v → φ y < 0) :
    ∃ η : ℝ, 0 < η ∧ η < t ∧ ‖p • v + η • y‖ < p := by
…

Mentions: OAI.Tingley.SupportAt