Order.lean`

11 declarations, 0 contain sorry, 0 declared as axioms

def OAI.PlanarL1.Ordered.running line 11
Source documentation
Running minimum toward a target in the circle cut at its root, index zero. The exceptional root retains its global minimum.
```
noncomputable def running {n : ℕ} (b : Fin (n + 1)) (f : Fin (n + 1) → ℝ)
    (i : Fin (n + 1)) : ℝ :=
…
```
lemma OAI.PlanarL1.Ordered.running_zero line 15
lemma OAI.PlanarL1.Ordered.running_le line 18
lemma OAI.PlanarL1.Ordered.le_running line 25
lemma OAI.PlanarL1.Ordered.running_target line 32
lemma OAI.PlanarL1.Ordered.running_mono_left line 38
lemma OAI.PlanarL1.Ordered.running_mono_right line 51

lemma OAI.PlanarL1.Ordered.running_switch line 72

Source documentation

Collision inequality for a chord is exactly what is needed to make running minima respect its switch, including chords that straddle the target.

lemma running_switch {n : ℕ} (b : Fin (n + 1)) (f : Fin (n + 1) → ℝ)
    (hmin : ∀ i, f 0 ≤ f i) {p q : Fin (n + 1)} (hpq : p < q) (he : f p = f q)
    (hcollision : p ≠ 0 → ∀ z, p ≤ z → z ≤ q → f p ≤ f z) :
    running b f p = running b f q := by
…

Mentions: OAI.PlanarL1.Ordered.running

lemma OAI.PlanarL1.Ordered.finite_inf_lipschitz line 129
lemma OAI.PlanarL1.Ordered.running_lipschitz line 150
lemma OAI.PlanarL1.Ordered.rotate_unimodal_neg line 166