Slices.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.ExactModuli.exists_unit_near_opNorm line 15
lemma OAI.ExactModuli.daugavet_normalized_slice line 29
theorem OAI.ExactModuli.daugavet_unitSlice line 73
Source documentation
Forward half of the actual rank-one/slice equivalence, with a unit-sphere witness.
```
theorem daugavet_unitSlice (hd : Daugavet X) : UnitSliceProperty X := by
…
```
Mentions: OAI.ExactModuli.Daugavet, OAI.ExactModuli.UnitSliceProperty
lemma OAI.ExactModuli.exposed_support_approx line 101
lemma OAI.ExactModuli.closure_convexHull_exposed line 135

lemma OAI.ExactModuli.exposed_small_slice line 147

Source documentation

Compactness shrinks a slice about its uniquely exposed maximizer.

lemma exposed_small_slice {K : Set Y} (hK : IsCompact K) {p : Y}
    (hp : p ∈ K.exposedPoints ℝ) {r : ℝ} (hr : 0 < r) :
    ∃ (ell : Y →L[ℝ] ℝ) (β : ℝ), β < ell p ∧
      ∀ q ∈ K, β < ell q → ‖q - p‖ < r := by
…

lemma OAI.ExactModuli.bourgain_image line 180

Source documentation

Bourgain's finite-dimensional slice-combination lemma, in the exact form needed for finite-quotient neighborhoods. Zero weights are harmless and allowed.

lemma bourgain_image (T : X →L[ℝ] Y) {u : X} (hu : ‖u‖ ≤ 1) {r : ℝ} (hr : 0 < r) :
    ∃ (ι : Type) (_ : Fintype ι) (a : ι → ℝ) (ell : ι → X →L[ℝ] ℝ) (β : ι → ℝ),
      (∀ i, 0 ≤ a i) ∧ (∑ i, a i = 1) ∧
      (∀ i, ∃ y : X, ‖y‖ ≤ 1 ∧ β i < ell i y) ∧
      ∀ y : ι → X, (∀ i, ‖y i‖ ≤ 1 ∧ β i < ell i (y i)) →
        ‖T (∑ i, a i • y i) - T u‖ < r := by
…