UpperBounds.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.ExactModuli.half_envelope line 14
lemma OAI.ExactModuli.cofinite_direction_upper line 21
theorem OAI.ExactModuli.averaged_upper_bound line 41
Source documentation
Matching averaged upper curve, from one family of cofinite directions.
```
theorem averaged_upper_bound (hsp : UnitSliceProperty X) {x : X} (hx : ‖x‖ = 1)
    {t : ℝ} (ht : 0 ≤ t) : H (normSeminorm ℝ X) x t ≤ max (t / 2) (t - 1) := by
…
```
Mentions: OAI.ExactModuli.UnitSliceProperty, OAI.ExactModuli.H
theorem OAI.ExactModuli.oneSided_upper_bound line 63
Source documentation
Matching one-sided upper curve, including the radius-two corner.
```
theorem oneSided_upper_bound (hsp : UnitSliceProperty X) {x : X} (hx : ‖x‖ = 1)
    {t : ℝ} (ht : 0 ≤ t) : D (normSeminorm ℝ X) x t ≤ max 0 (t - 2) := by
…
```
Mentions: OAI.ExactModuli.UnitSliceProperty, OAI.ExactModuli.D
theorem OAI.ExactModuli.exact_pointwise line 82

theorem OAI.ExactModuli.exact_center_infima line 93

Source documentation

The infimum over centers is a separate conclusion, not an identification of definitions.

theorem exact_center_infima (E : Submodule ℝ (Lp ℝ 1 μ))
    (hdim : ¬ FiniteDimensional ℝ E) (hpre : MeasurePrecompactBall μ E) (hd : Daugavet E)
    {t : ℝ} (ht : 0 < t) :
    averagedModulus (normSeminorm ℝ E) t = max (t / 2) (t - 1) ∧
    oneSidedModulus (normSeminorm ℝ E) t = max 0 (t - 2) := by
…

Mentions: OAI.ExactModuli.MeasurePrecompactBall, OAI.ExactModuli.Daugavet, OAI.ExactModuli.averagedModulus, OAI.ExactModuli.oneSidedModulus