The polygon inequality in either index order

The polygon inequality edist_le_Ico_sum_edist of Mathlib bounds the distance between two terms of a sequence by the sum of the steps between them when the first index is the smaller. Here the two indices may come in either order, and the indices may be the ceilings of scaled times, as for the piecewise constant interpolant of a time discretization.

Main results

• TauCeti.edist_le_Ico_min_max_sum_edist: the distance between two terms of a sequence is at most the sum of the steps taken between them, whichever index is larger.
• TauCeti.edist_ceil_div_le_Ico_sum_edist: the same for the terms at the ceilings of a / τ and b / τ.

theorem TauCeti.edist_le_Ico_min_max_sum_edist {X : Type u_1} [TopologicalSpace X] [WeakPseudoEMetricSpace X] (f : ℕ → X) (m n : ℕ) : edist (f m) (f n) ≤ ∑ i ∈ Finset.Ico (min m n) (max m n), edist (f i) (f (i + 1))

The polygon inequality for two indices in either order. The distance between two terms of a sequence is at most the sum of the steps taken between them.

theorem TauCeti.edist_ceil_div_le_Ico_sum_edist {X : Type u_1} [TopologicalSpace X] [WeakPseudoEMetricSpace X] {K : Type u_2} [Semifield K] [LinearOrder K] [IsStrictOrderedRing K] [FloorSemiring K] {τ : K} (hτ : 0 ≤ τ) (U : ℕ → X) (a b : K) : edist (U ⌈a / τ⌉₊) (U ⌈b / τ⌉₊) ≤ ∑ n ∈ Finset.Ico ⌈min a b / τ⌉₊ ⌈max a b / τ⌉₊, edist (U n) (U (n + 1))

The distance between the terms of a sequence at the ceilings of a / τ and b / τ is at most the sum of the steps taken between them.