Mathlib.Algebra.Order.Group.MinMax

max_one_div_max_inv_one_eq_self theorem

(a : α) : max a 1 / max a⁻¹ 1 = a

Full source

@[to_additive (attr := simp)]
theorem max_one_div_max_inv_one_eq_self (a : α) : max a 1 / max a⁻¹ 1 = a := by
  rcases le_total a 1 with (h | h) <;> simp [h]

Ratio of Maxima Equals Original Element in Ordered Group

Informal description

For any element $a$ in a linearly ordered group $\alpha$, the ratio of the maximum of $a$ and $1$ to the maximum of $a^{-1}$ and $1$ equals $a$, i.e., \[ \frac{\max(a, 1)}{\max(a^{-1}, 1)} = a. \]

max_inv_one theorem

(a : α) : max a⁻¹ 1 = a⁻¹ * max a 1

Full source

@[to_additive]
lemma max_inv_one (a : α) : max a⁻¹ 1 = a⁻¹ * max a 1 := by
  rw [eq_inv_mul_iff_mul_eq, ← eq_div_iff_mul_eq', max_one_div_max_inv_one_eq_self]

Max-Inv-One Identity: $\max(a^{-1}, 1) = a^{-1} \cdot \max(a, 1)$

Informal description

For any element $a$ in a linearly ordered group $\alpha$, the maximum of $a^{-1}$ and $1$ equals the product of $a^{-1}$ and the maximum of $a$ and $1$, i.e., \[ \max(a^{-1}, 1) = a^{-1} \cdot \max(a, 1). \]

min_inv_inv' theorem

(a b : α) : min a⁻¹ b⁻¹ = (max a b)⁻¹

Full source

@[to_additive min_neg_neg]
theorem min_inv_inv' (a b : α) : min a⁻¹ b⁻¹ = (max a b)⁻¹ :=
  Eq.symm <| (@Monotone.map_max α αᵒᵈ _ _ Inv.inv a b) fun _ _ =>
    inv_le_inv_iff.mpr

Minimum of Inverses Equals Inverse of Maximum in Ordered Group

Informal description

For any elements $a$ and $b$ in a linearly ordered group $\alpha$, the minimum of their inverses $a^{-1}$ and $b^{-1}$ is equal to the inverse of the maximum of $a$ and $b$, i.e., \[ \min(a^{-1}, b^{-1}) = (\max(a, b))^{-1}. \]

max_inv_inv' theorem

(a b : α) : max a⁻¹ b⁻¹ = (min a b)⁻¹

Full source

@[to_additive max_neg_neg]
theorem max_inv_inv' (a b : α) : max a⁻¹ b⁻¹ = (min a b)⁻¹ :=
  Eq.symm <| (@Monotone.map_min α αᵒᵈ _ _ Inv.inv a b) fun _ _ =>
    inv_le_inv_iff.mpr

Maximum of Inverses Equals Inverse of Minimum in Ordered Group

Informal description

For any elements $a$ and $b$ in a linearly ordered group $\alpha$, the maximum of their inverses $a^{-1}$ and $b^{-1}$ is equal to the inverse of the minimum of $a$ and $b$, i.e., \[ \max(a^{-1}, b^{-1}) = (\min(a, b))^{-1}. \]

min_div_div_right' theorem

(a b c : α) : min (a / c) (b / c) = min a b / c

Full source

@[to_additive min_sub_sub_right]
theorem min_div_div_right' (a b c : α) : min (a / c) (b / c) = min a b / c := by
  simpa only [div_eq_mul_inv] using min_mul_mul_right a b c⁻¹

Min-Max Identity: $\min(a/c, b/c) = \min(a, b)/c$ in Ordered Groups

Informal description

For any elements $a, b, c$ in a linearly ordered group $\alpha$, the minimum of $a/c$ and $b/c$ is equal to the minimum of $a$ and $b$ divided by $c$, i.e., $\min(a/c, b/c) = \min(a, b)/c$.

max_div_div_right' theorem

(a b c : α) : max (a / c) (b / c) = max a b / c

Full source

@[to_additive max_sub_sub_right]
theorem max_div_div_right' (a b c : α) : max (a / c) (b / c) = max a b / c := by
  simpa only [div_eq_mul_inv] using max_mul_mul_right a b c⁻¹

Maximum of Quotients Equals Quotient of Maximums in Ordered Group

Informal description

For any elements $a, b, c$ in a linearly ordered group $\alpha$, the maximum of the quotients $a/c$ and $b/c$ is equal to the quotient of the maximum of $a$ and $b$ by $c$, i.e., \[ \max\left(\frac{a}{c}, \frac{b}{c}\right) = \frac{\max(a, b)}{c}. \]

min_div_div_left' theorem

(a b c : α) : min (a / b) (a / c) = a / max b c

Full source

@[to_additive min_sub_sub_left]
theorem min_div_div_left' (a b c : α) : min (a / b) (a / c) = a / max b c := by
  simp only [div_eq_mul_inv, min_mul_mul_left, min_inv_inv']

Minimum of Quotients Equals Quotient by Maximum in Ordered Group

Informal description

For any elements $a, b, c$ in a linearly ordered group $\alpha$, the minimum of the quotients $a/b$ and $a/c$ is equal to $a$ divided by the maximum of $b$ and $c$, i.e., \[ \min\left(\frac{a}{b}, \frac{a}{c}\right) = \frac{a}{\max(b, c)}. \]

max_div_div_left' theorem

(a b c : α) : max (a / b) (a / c) = a / min b c

Full source

@[to_additive max_sub_sub_left]
theorem max_div_div_left' (a b c : α) : max (a / b) (a / c) = a / min b c := by
  simp only [div_eq_mul_inv, max_mul_mul_left, max_inv_inv']

Maximum of Quotients Equals Quotient by Minimum in Ordered Group

Informal description

For any elements $a, b, c$ in a linearly ordered group $\alpha$, the maximum of the quotients $a/b$ and $a/c$ is equal to $a$ divided by the minimum of $b$ and $c$, i.e., \[ \max\left(\frac{a}{b}, \frac{a}{c}\right) = \frac{a}{\min(b, c)}. \]

max_sub_max_le_max theorem

(a b c d : α) : max a b - max c d ≤ max (a - c) (b - d)

Full source

theorem max_sub_max_le_max (a b c d : α) : max a b - max c d ≤ max (a - c) (b - d) := by
  simp only [sub_le_iff_le_add, max_le_iff]; constructor
  · calc
    a = a - c + c := (sub_add_cancel a c).symm
    _ ≤ max (a - c) (b - d) + max c d := add_le_add (le_max_left _ _) (le_max_left _ _)
  · calc
    b = b - d + d := (sub_add_cancel b d).symm
    _ ≤ max (a - c) (b - d) + max c d := add_le_add (le_max_right _ _) (le_max_right _ _)

Inequality for Differences of Maxima in Linearly Ordered Groups

Informal description

For any elements $a, b, c, d$ in a linearly ordered group $\alpha$, the difference between the maxima $\max(a, b) - \max(c, d)$ is less than or equal to the maximum of the differences $\max(a - c, b - d)$.

abs_max_sub_max_le_max theorem

(a b c d : α) : |max a b - max c d| ≤ max |a - c| |b - d|

Full source

theorem abs_max_sub_max_le_max (a b c d : α) : |max a b - max c d| ≤ max |a - c| |b - d| := by
  refine abs_sub_le_iff.2 ⟨?_, ?_⟩
  · exact (max_sub_max_le_max _ _ _ _).trans (max_le_max (le_abs_self _) (le_abs_self _))
  · rw [abs_sub_comm a c, abs_sub_comm b d]
    exact (max_sub_max_le_max _ _ _ _).trans (max_le_max (le_abs_self _) (le_abs_self _))

Absolute Difference of Maxima Bounded by Maximum of Absolute Differences

Informal description

For any elements $a, b, c, d$ in a linearly ordered group $\alpha$, the absolute difference between the maxima $\max(a, b)$ and $\max(c, d)$ is less than or equal to the maximum of the absolute differences $\max(|a - c|, |b - d|)$, i.e., \[ |\max(a, b) - \max(c, d)| \leq \max(|a - c|, |b - d|). \]

abs_min_sub_min_le_max theorem

(a b c d : α) : |min a b - min c d| ≤ max |a - c| |b - d|

Full source

theorem abs_min_sub_min_le_max (a b c d : α) : |min a b - min c d| ≤ max |a - c| |b - d| := by
  simpa only [max_neg_neg, neg_sub_neg, abs_sub_comm] using
    abs_max_sub_max_le_max (-a) (-b) (-c) (-d)

Absolute Difference of Minima Bounded by Maximum of Absolute Differences

Informal description

For any elements $a, b, c, d$ in a linearly ordered group $\alpha$, the absolute difference between the minima $\min(a, b)$ and $\min(c, d)$ is less than or equal to the maximum of the absolute differences $\max(|a - c|, |b - d|)$, i.e., \[ |\min(a, b) - \min(c, d)| \leq \max(|a - c|, |b - d|). \]

abs_max_sub_max_le_abs theorem

(a b c : α) : |max a c - max b c| ≤ |a - b|

Full source

theorem abs_max_sub_max_le_abs (a b c : α) : |max a c - max b c| ≤ |a - b| := by
  simpa only [sub_self, abs_zero, max_eq_left (abs_nonneg (a - b))]
    using abs_max_sub_max_le_max a c b c

Absolute Difference of Maxima with Common Term Bounded by Absolute Difference

Informal description

For any elements $a, b, c$ in a linearly ordered group $\alpha$, the absolute difference between $\max(a, c)$ and $\max(b, c)$ is less than or equal to the absolute difference between $a$ and $b$, i.e., \[ |\max(a, c) - \max(b, c)| \leq |a - b|. \]