Clamping and medians in ordered additive groups

In a linearly ordered additive group, clamping to a symmetric interval is bounded by its height and does not increase absolute value. Clamping t to [0, a + b], for 0 ≤ a and 0 ≤ b, is the sum of clamping t to [0, a] and clamping the remaining time t - a to [0, b]. This is how a constant-speed run along a segment of duration a + b splits into its runs along the two pieces of durations a and b.

The median max 0 (min a b) + min 0 (max a b) of 0, a and b is the common initial segment of a and b, viewed as segments from 0 on the line: it lies between 0 and each of them, and twice its absolute value is |a| + |b| - |b - a|.

Main results

• TauCeti.max_zero_min_add: max 0 (min t (a + b)) = max 0 (min t a) + max 0 (min (t - a) b).
• TauCeti.abs_max_min_le: the max-min clipping formula is bounded by |M| for any height M.
• TauCeti.abs_max_min_le_abs: clipping at a nonnegative height does not increase absolute value.
• TauCeti.add_max_neg_min_nonneg: clamping two elements with nonnegative sum to [-r, r] leaves a nonnegative sum.
• TauCeti.abs_max_zero_min_add_min_zero_max_add_abs_sub: the median u of 0, a and b satisfies |u| + |a - u| = |a|.
• TauCeti.two_nsmul_abs_max_zero_min_add_min_zero_max: 2 • |u| = |a| + |b| - |b - a|.

theorem TauCeti.max_zero_min_add {α : Type u_1} [AddCommGroup α] [LinearOrder α] [IsOrderedAddMonoid α] {a b : α} (ha : 0 ≤ a) (hb : 0 ≤ b) (t : α) : max 0 (min t (a + b)) = max 0 (min t a) + max 0 (min (t - a) b)

Clamping t to [0, a + b] is the sum of clamping t to [0, a] and clamping the remaining time t - a to [0, b].

theorem TauCeti.abs_max_min_le {α : Type u_1} [AddCommGroup α] [LinearOrder α] [IsOrderedAddMonoid α] (M x : α) : |max (-M) (min M x)| ≤ |M|

The max-min clipping formula is bounded by the absolute value of its height, including when the height is negative.

theorem TauCeti.abs_max_min_le_abs {α : Type u_1} [AddCommGroup α] [LinearOrder α] [IsOrderedAddMonoid α] {M : α} (hM : 0 ≤ M) (x : α) : |max (-M) (min M x)| ≤ |x|

Clipping to a symmetric interval does not increase absolute value.

theorem TauCeti.add_max_neg_min_nonneg {α : Type u_1} [AddCommGroup α] [LinearOrder α] [IsOrderedAddMonoid α] {r a b : α} (h : 0 ≤ a + b) : 0 ≤ max (-r) (min a r) + max (-r) (min b r)

Clamping two elements with nonnegative sum to [-r, r] leaves a nonnegative sum.

theorem TauCeti.abs_max_zero_min_add_min_zero_max_add_abs_sub {α : Type u_1} [AddCommGroup α] [LinearOrder α] [IsOrderedAddMonoid α] (a b : α) : |max 0 (min a b) + min 0 (max a b)| + |a - (max 0 (min a b) + min 0 (max a b))| = |a|

The median u = max 0 (min a b) + min 0 (max a b) of 0, a and b lies between 0 and a: |u| + |a - u| = |a|.

theorem TauCeti.two_nsmul_abs_max_zero_min_add_min_zero_max {α : Type u_1} [AddCommGroup α] [LinearOrder α] [IsOrderedAddMonoid α] (a b : α) : 2 • |max 0 (min a b) + min 0 (max a b)| = |a| + |b| - |b - a|

Twice the absolute value of the median u = max 0 (min a b) + min 0 (max a b) of 0, a and b is |a| + |b| - |b - a|: u is the common initial segment of a and b.