OAI/Analysis/Daugavet/Diameter.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ExactModuli.dual_apply_le_norm line 14
2. lemma OAI.ExactModuli.slice_add_almost line 21

   Source documentation

   One induction step in the diametral argument, with additive rather than multiplicative error.

   lemma slice_add_almost (hsp : UnitSliceProperty X) {w₀ : X} (hw₀ : ‖w₀‖ = 1)
       (ell : X →L[ℝ] ℝ) (β : ℝ) (hne : ∃ y : X, ‖y‖ ≤ 1 ∧ β < ell y)
       (z : X) {a δ : ℝ} (ha : 0 ≤ a) (hδ : 0 < δ) :
       ∃ y : X, ‖y‖ = 1 ∧ β < ell y ∧ ‖z‖ + a - δ ≤ ‖z + a • y‖ := by
   …

   Mentions: OAI.ExactModuli.UnitSliceProperty

3. lemma OAI.ExactModuli.slices_finite_sum line 54
4. theorem OAI.ExactModuli.diametral_finite_image line 93

   Source documentation

   The weak-open diametral lemma in finite-dimensional coordinates.

   theorem diametral_finite_image (hsp : UnitSliceProperty X) {x u : X} (hx : ‖x‖ = 1)
       (hu : ‖u‖ ≤ 1) (T : X →L[ℝ] Y) {r δ : ℝ} (hr : 0 < r) (hδ : 0 < δ) :
       ∃ v : X, ‖v‖ ≤ 1 ∧ ‖T v - T u‖ < r ∧ 2 - δ ≤ ‖v - x‖ := by
   …

   Mentions: OAI.ExactModuli.UnitSliceProperty

5. lemma OAI.ExactModuli.diametral_finite_norm line 113
6. lemma OAI.ExactModuli.cofinite_diametral_correction line 136

   Source documentation

   Finite quotient correction, retaining the small error vector for equivalent-norm estimates.

   lemma cofinite_diametral_correction (hsp : UnitSliceProperty X) {x : X} (hx : ‖x‖ = 1)
       {F : Submodule ℝ X} (hF : Cofinite F) {ε : ℝ} (hε : 0 < ε) :
       ∃ v e : X, ‖v‖ ≤ 1 ∧ ‖e‖ < ε ∧ v - x - e ∈ F ∧ 2 - ε ≤ ‖v - x‖ := by
   …

   Mentions: OAI.ExactModuli.UnitSliceProperty, OAI.ExactModuli.Cofinite

7. lemma OAI.ExactModuli.cofinite_antipodal_endpoint line 151