Mathlib.Algebra.Order.Ring.Basic

IsSquare.nonneg theorem

 [Semiring R] [LinearOrder R] [IsRightCancelAdd R] [ZeroLEOneClass R] [ExistsAddOfLE R] [PosMulMono R]
  [AddLeftStrictMono R] {x : R} (h : IsSquare x) : 0 ≤ x

Full source

theorem IsSquare.nonneg [Semiring R] [LinearOrder R] [IsRightCancelAdd R]
    [ZeroLEOneClass R] [ExistsAddOfLE R] [PosMulMono R] [AddLeftStrictMono R]
    {x : R} (h : IsSquare x) : 0 ≤ x := by
  rcases h with ⟨y, rfl⟩
  exact mul_self_nonneg y

Nonnegativity of Squares in Ordered Semirings

Informal description

Let $R$ be a linearly ordered semiring with the following properties: - Addition is right-cancellative - $0 \leq 1$ - For any $a \leq b$, there exists $c$ such that $b = a + c$ - Left multiplication by nonnegative elements is monotone - Addition is strictly monotone on the left Then for any element $x \in R$ that is a square (i.e., there exists $y \in R$ such that $x = y^2$), we have $0 \leq x$.

MonoidHom.map_neg_one theorem

: f (-1) = 1

Full source

theorem map_neg_one : f (-1) = 1 :=
  (pow_eq_one_iff (Nat.succ_ne_zero 1)).1 <| by rw [← map_pow, neg_one_sq, map_one]

Image of Negative One under Monoid Homomorphism is One

Informal description

For any monoid homomorphism $f$ from a linearly ordered ring $R$ to another monoid, the image of $-1$ under $f$ is $1$, i.e., $f(-1) = 1$.

MonoidHom.map_neg theorem

(x : R) : f (-x) = f x

Full source

@[simp]
theorem map_neg (x : R) : f (-x) = f x := by rw [← neg_one_mul, map_mul, map_neg_one, one_mul]

Monoid Homomorphism Preserves Negation: $f(-x) = f(x)$

Informal description

For any monoid homomorphism $f$ from a linearly ordered ring $R$ to another monoid, and for any element $x \in R$, the image of $-x$ under $f$ equals the image of $x$, i.e., $f(-x) = f(x)$.

MonoidHom.map_sub_swap theorem

(x y : R) : f (x - y) = f (y - x)

Full source

theorem map_sub_swap (x y : R) : f (x - y) = f (y - x) := by rw [← map_neg, neg_sub]

Monoid Homomorphism Preserves Subtraction Swap: $f(x - y) = f(y - x)$

Informal description

For any monoid homomorphism $f$ from a linearly ordered ring $R$ to another monoid, and for any elements $x, y \in R$, the image of $x - y$ under $f$ equals the image of $y - x$, i.e., $f(x - y) = f(y - x)$.

pow_add_pow_le theorem

(hx : 0 ≤ x) (hy : 0 ≤ y) (hn : n ≠ 0) : x ^ n + y ^ n ≤ (x + y) ^ n

Full source

theorem pow_add_pow_le (hx : 0 ≤ x) (hy : 0 ≤ y) (hn : n ≠ 0) : x ^ n + y ^ n ≤ (x + y) ^ n := by
  rcases Nat.exists_eq_add_one_of_ne_zero hn with ⟨k, rfl⟩
  induction k with
  | zero => simp only [zero_add, pow_one, le_refl]
  | succ k ih =>
    let n := k.succ
    have h1 := add_nonneg (mul_nonneg hx (pow_nonneg hy n)) (mul_nonneg hy (pow_nonneg hx n))
    have h2 := add_nonneg hx hy
    calc
      x ^ (n + 1) + y ^ (n + 1) ≤ x * x ^ n + y * y ^ n + (x * y ^ n + y * x ^ n) := by
        rw [pow_succ' _ n, pow_succ' _ n]
        exact le_add_of_nonneg_right h1
      _ = (x + y) * (x ^ n + y ^ n) := by
        rw [add_mul, mul_add, mul_add, add_comm (y * x ^ n), ← add_assoc, ← add_assoc,
          add_assoc (x * x ^ n) (x * y ^ n), add_comm (x * y ^ n) (y * y ^ n), ← add_assoc]
      _ ≤ (x + y) ^ (n + 1) := by
        rw [pow_succ' _ n]
        exact mul_le_mul_of_nonneg_left (ih (Nat.succ_ne_zero k)) h2

Sum of Powers Inequality: $x^n + y^n \leq (x + y)^n$ for Nonnegative $x, y$ and $n \neq 0$

Informal description

For any elements $x$ and $y$ in a linearly ordered semiring $R$ with $x \geq 0$ and $y \geq 0$, and for any nonzero natural number $n$, the sum of their $n$-th powers is less than or equal to the $n$-th power of their sum, i.e., $x^n + y^n \leq (x + y)^n$.

pow_le_pow_left theorem

{a b : R} (ha : 0 ≤ a) (hab : a ≤ b) : ∀ n, a ^ n ≤ b ^ n

Full source

@[deprecated pow_le_pow_left₀ (since := "2024-11-13")]
theorem pow_le_pow_left {a b : R} (ha : 0 ≤ a) (hab : a ≤ b) : ∀ n, a ^ n ≤ b ^ n :=
  pow_le_pow_left₀ ha hab

Monotonicity of Powers: $a^n \leq b^n$ when $0 \leq a \leq b$

Informal description

For any elements $a$ and $b$ in an ordered semiring $R$ with $0 \leq a \leq b$, and for any natural number $n$, we have $a^n \leq b^n$.

pow_add_pow_le' theorem

(ha : 0 ≤ a) (hb : 0 ≤ b) : a ^ n + b ^ n ≤ 2 * (a + b) ^ n

Full source

lemma pow_add_pow_le' (ha : 0 ≤ a) (hb : 0 ≤ b) : a ^ n + b ^ n ≤ 2 * (a + b) ^ n := by
  rw [two_mul]
  exact add_le_add (pow_le_pow_left₀ ha (le_add_of_nonneg_right hb) _)
    (pow_le_pow_left₀ hb (le_add_of_nonneg_left ha) _)

Sum of Powers Inequality with Factor Two: $a^n + b^n \leq 2(a + b)^n$ for Nonnegative $a, b$

Informal description

For any nonnegative elements $a$ and $b$ in a linearly ordered semiring $R$, and for any natural number $n$, the sum of their $n$-th powers is less than or equal to twice the $n$-th power of their sum, i.e., $a^n + b^n \leq 2(a + b)^n$.

pow_lt_pow_left theorem

(h : x < y) (hx : 0 ≤ x) : ∀ {n : ℕ}, n ≠ 0 → x ^ n < y ^ n

Full source

@[deprecated pow_lt_pow_left₀ (since := "2024-11-13")]
theorem pow_lt_pow_left (h : x < y) (hx : 0 ≤ x) : ∀ {n : ℕ}, n ≠ 0 → x ^ n < y ^ n :=
  pow_lt_pow_left₀ h hx

Strict Monotonicity of Powers: $x < y \land x \geq 0 \implies x^n < y^n$ for $n \neq 0$

Informal description

For any elements $x$ and $y$ in a strict ordered semiring $R$ such that $x < y$ and $x \geq 0$, and for any nonzero natural number $n$, we have $x^n < y^n$.

pow_left_strictMonoOn theorem

(hn : n ≠ 0) : StrictMonoOn (· ^ n : R → R) {a | 0 ≤ a}

Full source

@[deprecated pow_left_strictMonoOn₀ (since := "2024-11-13")]
lemma pow_left_strictMonoOn (hn : n ≠ 0) : StrictMonoOn (· ^ n : R → R) {a | 0 ≤ a} :=
  pow_left_strictMonoOn₀ hn

Strict Monotonicity of Power Function on Nonnegative Elements for $n \neq 0$

Informal description

For any nonzero natural number $n$, the power function $x \mapsto x^n$ is strictly increasing on the set of nonnegative elements $\{x \in R \mid 0 \leq x\}$ in a strict ordered semiring $R$.

pow_right_strictMono theorem

(h : 1 < a) : StrictMono (a ^ ·)

Full source

@[deprecated pow_right_strictMono₀ (since := "2024-11-13")]
lemma pow_right_strictMono (h : 1 < a) : StrictMono (a ^ ·) :=
  pow_right_strictMono₀ h

Strict Monotonicity of Powers: $a > 1 \implies n \mapsto a^n$ is strictly increasing

Informal description

For any element $a > 1$ in a strict ordered semiring $R$, the power function $n \mapsto a^n$ is strictly increasing on natural numbers $n$.

pow_lt_pow_right theorem

(h : 1 < a) (hmn : m < n) : a ^ m < a ^ n

Full source

@[deprecated pow_lt_pow_right₀ (since := "2024-11-13")]
theorem pow_lt_pow_right (h : 1 < a) (hmn : m < n) : a ^ m < a ^ n :=
  pow_lt_pow_right₀ h hmn

Strict Monotonicity of Powers: $a > 1 \implies a^m < a^n$ for $m < n$

Informal description

For any element $a > 1$ in a strict ordered semiring $R$ and natural numbers $m < n$, we have $a^m < a^n$.

pow_lt_pow_iff_right theorem

(h : 1 < a) : a ^ n < a ^ m ↔ n < m

Full source

@[deprecated pow_lt_pow_iff_right₀ (since := "2024-11-13")]
lemma pow_lt_pow_iff_right (h : 1 < a) : a ^ n < a ^ m ↔ n < m := pow_lt_pow_iff_right₀ h

Strict Monotonicity of Powers: $a^n < a^m \leftrightarrow n < m$ for $a > 1$

Informal description

For any element $a > 1$ in a strict ordered semiring $R$, and for any natural numbers $n$ and $m$, we have $a^n < a^m$ if and only if $n < m$.

pow_le_pow_iff_right theorem

(h : 1 < a) : a ^ n ≤ a ^ m ↔ n ≤ m

Full source

@[deprecated pow_le_pow_iff_right₀ (since := "2024-11-13")]
lemma pow_le_pow_iff_right (h : 1 < a) : a ^ n ≤ a ^ m ↔ n ≤ m := pow_le_pow_iff_right₀ h

Power Inequality Comparison for $a > 1$: $a^n \leq a^m \leftrightarrow n \leq m$

Informal description

For any element $a > 1$ in a preorder with multiplication, the inequality $a^n \leq a^m$ holds if and only if $n \leq m$ for natural numbers $n$ and $m$.

lt_self_pow theorem

(h : 1 < a) (hm : 1 < m) : a < a ^ m

Full source

@[deprecated lt_self_pow₀ (since := "2024-11-13")]
theorem lt_self_pow (h : 1 < a) (hm : 1 < m) : a < a ^ m := lt_self_pow₀ h hm

Strict inequality for powers: $a < a^m$ when $a > 1$ and $m > 1$

Informal description

For any element $a > 1$ in a strict ordered semiring and any natural number $m > 1$, we have $a < a^m$.

pow_right_strictAnti theorem

(h₀ : 0 < a) (h₁ : a < 1) : StrictAnti (a ^ ·)

Full source

@[deprecated pow_right_strictAnti₀ (since := "2024-11-13")]
theorem pow_right_strictAnti (h₀ : 0 < a) (h₁ : a < 1) : StrictAnti (a ^ ·) :=
  pow_right_strictAnti₀ h₀ h₁

Strict Antitonicity of Powers for $0 < a < 1$

Informal description

For any element $a$ in a preorder with a multiplication operation, if $0 < a < 1$, then the function $n \mapsto a^n$ is strictly antitone (i.e., for any natural numbers $m < n$, we have $a^n < a^m$).

pow_lt_pow_iff_right_of_lt_one theorem

(h₀ : 0 < a) (h₁ : a < 1) : a ^ m < a ^ n ↔ n < m

Full source

@[deprecated pow_lt_pow_iff_right_of_lt_one₀ (since := "2024-11-13")]
theorem pow_lt_pow_iff_right_of_lt_one (h₀ : 0 < a) (h₁ : a < 1) : a ^ m < a ^ n ↔ n < m :=
  pow_lt_pow_iff_right_of_lt_one₀ h₀ h₁

Inequality for Powers with Base $0 < a < 1$: $a^m < a^n \leftrightarrow n < m$

Informal description

For any element $a$ in a strict ordered semiring $R$ such that $0 < a < 1$, the inequality $a^m < a^n$ holds if and only if $n < m$.

pow_lt_pow_right_of_lt_one theorem

(h₀ : 0 < a) (h₁ : a < 1) (hmn : m < n) : a ^ n < a ^ m

Full source

@[deprecated pow_lt_pow_right_of_lt_one₀ (since := "2024-11-13")]
theorem pow_lt_pow_right_of_lt_one (h₀ : 0 < a) (h₁ : a < 1) (hmn : m < n) : a ^ n < a ^ m :=
  pow_lt_pow_right_of_lt_one₀ h₀ h₁ hmn

Strict Antitonicity of Powers for $0 < a < 1$: $a^n < a^m$ when $m < n$

Informal description

For any element $a$ in a strict ordered semiring $R$ such that $0 < a < 1$, and for any natural numbers $m < n$, the inequality $a^n < a^m$ holds.

pow_lt_self_of_lt_one theorem

(h₀ : 0 < a) (h₁ : a < 1) (hn : 1 < n) : a ^ n < a

Full source

@[deprecated pow_lt_self_of_lt_one₀ (since := "2024-11-13")]
theorem pow_lt_self_of_lt_one (h₀ : 0 < a) (h₁ : a < 1) (hn : 1 < n) : a ^ n < a :=
  pow_lt_self_of_lt_one₀ h₀ h₁ hn

Strict Antitonicity of Powers for $0 < a < 1$: $a^n < a$ when $n > 1$

Informal description

For any element $a$ in a strict ordered semiring $R$ such that $0 < a < 1$, and for any natural number $n > 1$, the inequality $a^n < a$ holds.

sq_pos_of_neg theorem

(ha : a < 0) : 0 < a ^ 2

Full source

lemma sq_pos_of_neg (ha : a < 0) : 0 < a ^ 2 := by rw [sq]; exact mul_pos_of_neg_of_neg ha ha

Square of Negative Element is Positive

Informal description

For any element $a$ in an ordered ring, if $a < 0$, then its square is positive, i.e., $0 < a^2$.

pow_le_pow_iff_left theorem

(ha : 0 ≤ a) (hb : 0 ≤ b) (hn : n ≠ 0) : a ^ n ≤ b ^ n ↔ a ≤ b

Full source

@[deprecated pow_le_pow_iff_left₀ (since := "2024-11-12")]
lemma pow_le_pow_iff_left (ha : 0 ≤ a) (hb : 0 ≤ b) (hn : n ≠ 0) : a ^ n ≤ b ^ n ↔ a ≤ b :=
  pow_le_pow_iff_left₀ ha hb hn

Power Inequality Equivalence for Nonnegative Elements: $a^n \leq b^n \leftrightarrow a \leq b$ when $n \neq 0$

Informal description

For any nonnegative elements $a$ and $b$ in a linearly ordered semiring with $0 \leq a$ and $0 \leq b$, and any nonzero natural number $n$, the inequality $a^n \leq b^n$ holds if and only if $a \leq b$.

pow_lt_pow_iff_left theorem

(ha : 0 ≤ a) (hb : 0 ≤ b) (hn : n ≠ 0) : a ^ n < b ^ n ↔ a < b

Full source

@[deprecated pow_lt_pow_iff_left₀ (since := "2024-11-12")]
lemma pow_lt_pow_iff_left (ha : 0 ≤ a) (hb : 0 ≤ b) (hn : n ≠ 0) : a ^ n < b ^ n ↔ a < b :=
  pow_lt_pow_iff_left₀ ha hb hn

Strict Monotonicity of Power Function: $a^n < b^n \leftrightarrow a < b$ for $n \neq 0$

Informal description

For any elements $a, b$ in a linearly ordered semiring with $0 \leq a$ and $0 \leq b$, and any nonzero natural number $n \neq 0$, we have $a^n < b^n$ if and only if $a < b$.

pow_right_injective theorem

(ha₀ : 0 < a) (ha₁ : a ≠ 1) : Injective (a ^ ·)

Full source

@[deprecated pow_right_injective₀ (since := "2024-11-12")]
lemma pow_right_injective (ha₀ : 0 < a) (ha₁ : a ≠ 1) : Injective (a ^ ·) :=
  pow_right_injective₀ ha₀ ha₁

Injectivity of Power Function for $0 < a \neq 1$ in Ordered Semirings

Informal description

For any element $a > 0$ with $a \neq 1$ in a linearly ordered semiring, the power function $n \mapsto a^n$ is injective. That is, for any natural numbers $m$ and $n$, if $a^m = a^n$, then $m = n$.

pow_right_inj theorem

(ha₀ : 0 < a) (ha₁ : a ≠ 1) : a ^ m = a ^ n ↔ m = n

Full source

@[deprecated pow_right_inj₀ (since := "2024-11-12")]
lemma pow_right_inj (ha₀ : 0 < a) (ha₁ : a ≠ 1) : a ^ m = a ^ n ↔ m = n := pow_right_inj₀ ha₀ ha₁

Power Equality Condition: $a^m = a^n \leftrightarrow m = n$ for $0 < a \neq 1$

Informal description

For any element $a > 0$ with $a \neq 1$ in a linearly ordered semiring, the equality $a^m = a^n$ holds if and only if $m = n$ for any natural numbers $m$ and $n$.

sq_le_one_iff theorem

{a : R} (ha : 0 ≤ a) : a ^ 2 ≤ 1 ↔ a ≤ 1

Full source

@[deprecated sq_le_one_iff₀ (since := "2024-11-12")]
theorem sq_le_one_iff {a : R} (ha : 0 ≤ a) : a ^ 2 ≤ 1 ↔ a ≤ 1 := sq_le_one_iff₀ ha

Square Inequality for Nonnegative Elements: $a^2 \leq 1 \leftrightarrow a \leq 1$

Informal description

For any nonnegative element $a$ in a linearly ordered semiring or ring (i.e., $0 \leq a$), the inequality $a^2 \leq 1$ holds if and only if $a \leq 1$.

sq_lt_one_iff theorem

{a : R} (ha : 0 ≤ a) : a ^ 2 < 1 ↔ a < 1

Full source

@[deprecated sq_lt_one_iff₀ (since := "2024-11-12")]
theorem sq_lt_one_iff {a : R} (ha : 0 ≤ a) : a ^ 2 < 1 ↔ a < 1 := sq_lt_one_iff₀ ha

Square Inequality for Nonnegative Elements: $a^2 < 1 \leftrightarrow a < 1$

Informal description

For any nonnegative element $a$ in a linearly ordered semiring or ring (i.e., $0 \leq a$), the inequality $a^2 < 1$ holds if and only if $a < 1$.

one_le_sq_iff theorem

{a : R} (ha : 0 ≤ a) : 1 ≤ a ^ 2 ↔ 1 ≤ a

Full source

@[deprecated one_le_sq_iff₀ (since := "2024-11-12")]
theorem one_le_sq_iff {a : R} (ha : 0 ≤ a) : 1 ≤ a ^ 2 ↔ 1 ≤ a := one_le_sq_iff₀ ha

Square Inequality for Nonnegative Elements: $1 \leq a^2 \leftrightarrow 1 \leq a$

Informal description

For any nonnegative element $a$ in a linearly ordered semiring or ring (i.e., $0 \leq a$), the inequality $1 \leq a^2$ holds if and only if $1 \leq a$.

one_lt_sq_iff theorem

{a : R} (ha : 0 ≤ a) : 1 < a ^ 2 ↔ 1 < a

Full source

@[deprecated one_lt_sq_iff₀ (since := "2024-11-12")]
theorem one_lt_sq_iff {a : R} (ha : 0 ≤ a) : 1 < a ^ 2 ↔ 1 < a := one_lt_sq_iff₀ ha

Square Inequality for Nonnegative Elements: $1 < a^2 \leftrightarrow 1 < a$

Informal description

For any nonnegative element $a$ in a linearly ordered semiring or ring (i.e., $0 \leq a$), the inequality $1 < a^2$ holds if and only if $1 < a$.

lt_of_pow_lt_pow_left theorem

(n : ℕ) (hb : 0 ≤ b) (h : a ^ n < b ^ n) : a < b

Full source

@[deprecated lt_of_pow_lt_pow_left₀ (since := "2024-11-12")]
theorem lt_of_pow_lt_pow_left (n : ℕ) (hb : 0 ≤ b) (h : a ^ n < b ^ n) : a < b :=
  lt_of_pow_lt_pow_left₀ n hb h

Strict Inequality Preservation Under Powers: $a^n < b^n$ implies $a < b$ for $b \geq 0$

Informal description

For any natural number $n$ and elements $a, b$ in a linearly ordered semiring or ring, if $b \geq 0$ and $a^n < b^n$, then $a < b$.

le_of_pow_le_pow_left theorem

(hn : n ≠ 0) (hb : 0 ≤ b) (h : a ^ n ≤ b ^ n) : a ≤ b

Full source

@[deprecated le_of_pow_le_pow_left₀ (since := "2024-11-12")]
theorem le_of_pow_le_pow_left (hn : n ≠ 0) (hb : 0 ≤ b) (h : a ^ n ≤ b ^ n) : a ≤ b :=
  le_of_pow_le_pow_left₀ hn hb h

Inequality Preservation Under Powers: $a^n \leq b^n$ implies $a \leq b$ for $b \geq 0$ and $n \neq 0$

Informal description

For any natural number $n \neq 0$ and elements $a, b$ in a linearly ordered semiring or ring, if $b \geq 0$ and $a^n \leq b^n$, then $a \leq b$.

sq_eq_sq theorem

{a b : R} (ha : 0 ≤ a) (hb : 0 ≤ b) : a ^ 2 = b ^ 2 ↔ a = b

Full source

@[deprecated sq_eq_sq₀ (since := "2024-11-12")]
theorem sq_eq_sq {a b : R} (ha : 0 ≤ a) (hb : 0 ≤ b) : a ^ 2 = b ^ 2 ↔ a = b := sq_eq_sq₀ ha hb

Square Equality for Nonnegative Elements: $a^2 = b^2 \leftrightarrow a = b$

Informal description

For any nonnegative elements $a$ and $b$ in an ordered semiring $R$, the squares of $a$ and $b$ are equal if and only if $a$ and $b$ themselves are equal, i.e., $a^2 = b^2 \leftrightarrow a = b$.

lt_of_mul_self_lt_mul_self theorem

(hb : 0 ≤ b) : a * a < b * b → a < b

Full source

@[deprecated lt_of_mul_self_lt_mul_self₀ (since := "2024-11-12")]
theorem lt_of_mul_self_lt_mul_self (hb : 0 ≤ b) : a * a < b * b → a < b :=
  lt_of_mul_self_lt_mul_self₀ hb

Strict inequality preservation under squaring: $a^2 < b^2 \Rightarrow a < b$ for $b \geq 0$

Informal description

For any elements $a$ and $b$ in an ordered semiring $R$, if $b \geq 0$ and $a^2 < b^2$, then $a < b$.

IsNonarchimedean definition

{α : Type*} [Add α] (f : α → R) : Prop

Full source

/-- A function `f : α → R` is nonarchimedean if it satisfies the ultrametric inequality
  `f (a + b) ≤ max (f a) (f b)` for all `a b : α`. -/
def IsNonarchimedean {α : Type*} [Add α] (f : α → R) : Prop := ∀ a b : α, f (a + b) ≤ f a ⊔ f b

Nonarchimedean function

Informal description

A function $f \colon \alpha \to R$ is called *nonarchimedean* if it satisfies the ultrametric inequality $f(a + b) \leq \max(f(a), f(b))$ for all $a, b \in \alpha$.

add_sq_le theorem

: (a + b) ^ 2 ≤ 2 * (a ^ 2 + b ^ 2)

Full source

lemma add_sq_le : (a + b) ^ 2 ≤ 2 * (a ^ 2 + b ^ 2) := by
  calc
    (a + b) ^ 2 = a ^ 2 + b ^ 2 + (a * b + b * a) := by
        simp_rw [pow_succ', pow_zero, mul_one, add_mul, mul_add, add_comm (b * a), add_add_add_comm]
    _ ≤ a ^ 2 + b ^ 2 + (a * a + b * b) := add_le_add_left ?_ _
    _ = _ := by simp_rw [pow_succ', pow_zero, mul_one, two_mul]
  cases le_total a b
  · exact mul_add_mul_le_mul_add_mul ‹_› ‹_›
  · exact mul_add_mul_le_mul_add_mul' ‹_› ‹_›

Square of Sum Inequality: $(a + b)^2 \leq 2(a^2 + b^2)$

Informal description

For any elements $a$ and $b$ in an ordered semiring $R$, the square of their sum satisfies the inequality: $$(a + b)^2 \leq 2(a^2 + b^2)$$

add_pow_le theorem

(ha : 0 ≤ a) (hb : 0 ≤ b) : ∀ n, (a + b) ^ n ≤ 2 ^ (n - 1) * (a ^ n + b ^ n)

Full source

lemma add_pow_le (ha : 0 ≤ a) (hb : 0 ≤ b) : ∀ n, (a + b) ^ n ≤ 2 ^ (n - 1) * (a ^ n + b ^ n)
  | 0 => by simp
  | 1 => by simp
  | n + 2 => by
    rw [pow_succ]
    calc
      _ ≤ 2 ^ n * (a ^ (n + 1) + b ^ (n + 1)) * (a + b) :=
          mul_le_mul_of_nonneg_right (add_pow_le ha hb (n + 1)) <| add_nonneg ha hb
      _ = 2 ^ n * (a ^ (n + 2) + b ^ (n + 2) + (a ^ (n + 1) * b + b ^ (n + 1) * a)) := by
          rw [mul_assoc, mul_add, add_mul, add_mul, ← pow_succ, ← pow_succ, add_comm _ (b ^ _),
            add_add_add_comm, add_comm (_ * a)]
      _ ≤ 2 ^ n * (a ^ (n + 2) + b ^ (n + 2) + (a ^ (n + 1) * a + b ^ (n + 1) * b)) :=
          mul_le_mul_of_nonneg_left (add_le_add_left ?_ _) <| pow_nonneg (zero_le_two (α := R)) _
      _ = _ := by simp only [← pow_succ, ← two_mul, ← mul_assoc]; rfl
    · obtain hab | hba := le_total a b
      · exact mul_add_mul_le_mul_add_mul (pow_le_pow_left₀ ha hab _) hab
      · exact mul_add_mul_le_mul_add_mul' (pow_le_pow_left₀ hb hba _) hba

Generalized Power Sum Inequality: $(a + b)^n \leq 2^{n-1}(a^n + b^n)$ for $a, b \geq 0$

Informal description

For any nonnegative elements $a$ and $b$ in an ordered semiring $R$ and for any natural number $n$, the following inequality holds: $$(a + b)^n \leq 2^{n-1} (a^n + b^n)$$

Even.add_pow_le theorem

(hn : Even n) : (a + b) ^ n ≤ 2 ^ (n - 1) * (a ^ n + b ^ n)

Full source

protected lemma Even.add_pow_le (hn : Even n) :
    (a + b) ^ n ≤ 2 ^ (n - 1) * (a ^ n + b ^ n) := by
  obtain ⟨n, rfl⟩ := hn
  rw [← two_mul, pow_mul]
  calc
    _ ≤ (2 * (a ^ 2 + b ^ 2)) ^ n := pow_le_pow_left₀ (sq_nonneg _) add_sq_le _
    _ = 2 ^ n * (a ^ 2 + b ^ 2) ^ n := by -- TODO: Should be `Nat.cast_commute`
        rw [Commute.mul_pow]; simp [Commute, SemiconjBy, two_mul, mul_two]
    _ ≤ 2 ^ n * (2 ^ (n - 1) * ((a ^ 2) ^ n + (b ^ 2) ^ n)) := mul_le_mul_of_nonneg_left
          (add_pow_le (sq_nonneg _) (sq_nonneg _) _) <| pow_nonneg (zero_le_two (α := R)) _
    _ = _ := by
      simp only [← mul_assoc, ← pow_add, ← pow_mul]
      cases n
      · rfl
      · simp [Nat.two_mul]

Generalized Power Sum Inequality for Even Exponents: $(a + b)^n \leq 2^{n-1}(a^n + b^n)$ when $n$ is even

Informal description

For any even natural number $n$ and any elements $a$ and $b$ in an ordered semiring $R$, the following inequality holds: $$(a + b)^n \leq 2^{n-1} (a^n + b^n)$$

Even.pow_nonneg theorem

(hn : Even n) (a : R) : 0 ≤ a ^ n

Full source

lemma Even.pow_nonneg (hn : Even n) (a : R) : 0 ≤ a ^ n := by
  obtain ⟨k, rfl⟩ := hn; rw [pow_add]; exact mul_self_nonneg _

Nonnegativity of Even Powers: $0 \leq a^n$ for even $n$

Informal description

For any element $a$ in an ordered ring $R$ and any even natural number $n$, the $n$-th power of $a$ is nonnegative, i.e., $0 \leq a^n$.

Even.pow_pos theorem

(hn : Even n) (ha : a ≠ 0) : 0 < a ^ n

Full source

lemma Even.pow_pos (hn : Even n) (ha : a ≠ 0) : 0 < a ^ n :=
  (hn.pow_nonneg _).lt_of_ne' (pow_ne_zero _ ha)

Positivity of Even Powers: $0 < a^n$ for even $n$ and $a \neq 0$

Informal description

For any element $a$ in an ordered ring $R$ and any even natural number $n$, if $a$ is nonzero, then the $n$-th power of $a$ is positive, i.e., $0 < a^n$.

Even.pow_pos_iff theorem

(hn : Even n) (h₀ : n ≠ 0) : 0 < a ^ n ↔ a ≠ 0

Full source

lemma Even.pow_pos_iff (hn : Even n) (h₀ : n ≠ 0) : 0 < a ^ n ↔ a ≠ 0 := by
  obtain ⟨k, rfl⟩ := hn; rw [pow_add, mul_self_pos, pow_ne_zero_iff (by simpa using h₀)]

Positivity of Even Powers: $0 < a^n \leftrightarrow a \neq 0$ for even $n \neq 0$

Informal description

Let $R$ be an ordered ring and let $n$ be an even natural number with $n \neq 0$. For any element $a \in R$, the power $a^n$ is positive if and only if $a$ is nonzero, i.e., $0 < a^n \leftrightarrow a \neq 0$.

Odd.pow_neg_iff theorem

(hn : Odd n) : a ^ n < 0 ↔ a < 0

Full source

lemma Odd.pow_neg_iff (hn : Odd n) : a ^ n < 0 ↔ a < 0 := by
  refine ⟨lt_imp_lt_of_le_imp_le (pow_nonneg · _), fun ha ↦ ?_⟩
  obtain ⟨k, rfl⟩ := hn
  rw [pow_succ]
  exact mul_neg_of_pos_of_neg ((even_two_mul _).pow_pos ha.ne) ha

Negativity of Odd Powers: $a^n < 0 \leftrightarrow a < 0$ for odd $n$

Informal description

For any element $a$ in an ordered ring $R$ and any odd natural number $n$, the $n$-th power of $a$ is negative if and only if $a$ is negative, i.e., $a^n < 0 \leftrightarrow a < 0$.

Odd.pow_nonneg_iff theorem

(hn : Odd n) : 0 ≤ a ^ n ↔ 0 ≤ a

Full source

lemma Odd.pow_nonneg_iff (hn : Odd n) : 0 ≤ a ^ n ↔ 0 ≤ a :=
  le_iff_le_iff_lt_iff_lt.2 hn.pow_neg_iff

Nonnegativity of Odd Powers: $0 \leq a^n \leftrightarrow 0 \leq a$ for odd $n$

Informal description

For any element $a$ in an ordered ring $R$ and any odd natural number $n$, the $n$-th power of $a$ is nonnegative if and only if $a$ is nonnegative, i.e., $0 \leq a^n \leftrightarrow 0 \leq a$.

Odd.pow_nonpos_iff theorem

(hn : Odd n) : a ^ n ≤ 0 ↔ a ≤ 0

Full source

lemma Odd.pow_nonpos_iff (hn : Odd n) : a ^ n ≤ 0 ↔ a ≤ 0 := by
  rw [le_iff_lt_or_eq, le_iff_lt_or_eq, hn.pow_neg_iff, pow_eq_zero_iff]
  rintro rfl; simp [Odd, eq_comm (a := 0)] at hn

Nonpositivity of Odd Powers: $a^n \leq 0 \leftrightarrow a \leq 0$ for odd $n$

Informal description

For any element $a$ in an ordered ring $R$ and any odd natural number $n$, the $n$-th power of $a$ is nonpositive if and only if $a$ is nonpositive, i.e., $a^n \leq 0 \leftrightarrow a \leq 0$.

Odd.pow_pos_iff theorem

(hn : Odd n) : 0 < a ^ n ↔ 0 < a

Full source

lemma Odd.pow_pos_iff (hn : Odd n) : 0 < a ^ n ↔ 0 < a := lt_iff_lt_of_le_iff_le hn.pow_nonpos_iff

Positivity of Odd Powers: $0 < a^n \leftrightarrow 0 < a$ for odd $n$

Informal description

For any element $a$ in an ordered ring $R$ and any odd natural number $n$, the $n$-th power of $a$ is positive if and only if $a$ is positive, i.e., $0 < a^n \leftrightarrow 0 < a$.

Odd.strictMono_pow theorem

(hn : Odd n) : StrictMono fun a : R => a ^ n

Full source

lemma Odd.strictMono_pow (hn : Odd n) : StrictMono fun a : R => a ^ n := by
  have hn₀ : n ≠ 0 := by rintro rfl; simp [Odd, eq_comm (a := 0)] at hn
  intro a b hab
  obtain ha | ha := le_total 0 a
  · exact pow_lt_pow_left₀ hab ha hn₀
  obtain hb | hb := lt_or_le 0 b
  · exact (hn.pow_nonpos ha).trans_lt (pow_pos hb _)
  obtain ⟨c, hac⟩ := exists_add_of_le ha
  obtain ⟨d, hbd⟩ := exists_add_of_le hb
  have hd := nonneg_of_le_add_right (hb.trans_eq hbd)
  refine lt_of_add_lt_add_right (a := c ^ n + d ^ n) ?_
  dsimp
  calc
    a ^ n + (c ^ n + d ^ n) = d ^ n := by
      rw [← add_assoc, hn.pow_add_pow_eq_zero hac.symm, zero_add]
    _ < c ^ n := pow_lt_pow_left₀ ?_ hd hn₀
    _ = b ^ n + (c ^ n + d ^ n) := by rw [add_left_comm, hn.pow_add_pow_eq_zero hbd.symm, add_zero]
  refine lt_of_add_lt_add_right (a := a + b) ?_
  rwa [add_rotate', ← hbd, add_zero, add_left_comm, ← add_assoc, ← hac, zero_add]

Strict Monotonicity of Odd Power Functions: $a \mapsto a^n$ for odd $n$

Informal description

For any odd natural number $n$, the function $f(a) = a^n$ is strictly increasing on an ordered ring $R$.

Odd.pow_injective theorem

{n : ℕ} (hn : Odd n) : Injective (· ^ n : R → R)

Full source

lemma Odd.pow_injective {n : ℕ} (hn : Odd n) : Injective (· ^ n : R → R) :=
  hn.strictMono_pow.injective

Injectivity of Odd Power Functions: $a \mapsto a^n$ for odd $n$

Informal description

For any odd natural number $n$, the power function $f(a) = a^n$ is injective on an ordered ring $R$.

Odd.pow_lt_pow theorem

{n : ℕ} (hn : Odd n) {a b : R} : a ^ n < b ^ n ↔ a < b

Full source

lemma Odd.pow_lt_pow {n : ℕ} (hn : Odd n) {a b : R} : a ^ n < b ^ n ↔ a < b :=
  hn.strictMono_pow.lt_iff_lt

Comparison of Odd Powers: $a^n < b^n \leftrightarrow a < b$ for odd $n$

Informal description

For any odd natural number $n$ and elements $a, b$ in an ordered ring $R$, the inequality $a^n < b^n$ holds if and only if $a < b$.

Odd.pow_le_pow theorem

{n : ℕ} (hn : Odd n) {a b : R} : a ^ n ≤ b ^ n ↔ a ≤ b

Full source

lemma Odd.pow_le_pow {n : ℕ} (hn : Odd n) {a b : R} : a ^ n ≤ b ^ n ↔ a ≤ b :=
  hn.strictMono_pow.le_iff_le

Odd Power Monotonicity: $a^n \leq b^n \leftrightarrow a \leq b$ for odd $n$

Informal description

For any odd natural number $n$ and elements $a, b$ in a linearly ordered ring $R$, the inequality $a^n \leq b^n$ holds if and only if $a \leq b$.

Odd.pow_inj theorem

{n : ℕ} (hn : Odd n) {a b : R} : a ^ n = b ^ n ↔ a = b

Full source

lemma Odd.pow_inj {n : ℕ} (hn : Odd n) {a b : R} : a ^ n = b ^ n ↔ a = b :=
  hn.pow_injective.eq_iff

Odd Power Injectivity: $a^n = b^n \leftrightarrow a = b$ for odd $n$

Informal description

For any odd natural number $n$ and elements $a, b$ in a linearly ordered ring $R$, the equality $a^n = b^n$ holds if and only if $a = b$.

sq_pos_iff theorem

{a : R} : 0 < a ^ 2 ↔ a ≠ 0

Full source

lemma sq_pos_iff {a : R} : 0 < a ^ 2 ↔ a ≠ 0 := even_two.pow_pos_iff two_ne_zero

Positivity of Squares: $0 < a^2 \leftrightarrow a \neq 0$

Informal description

For any element $a$ in a linearly ordered semiring or ring $R$, the square $a^2$ is positive if and only if $a$ is nonzero, i.e., $0 < a^2 \leftrightarrow a \neq 0$.

pow_four_le_pow_two_of_pow_two_le theorem

(h : a ^ 2 ≤ b) : a ^ 4 ≤ b ^ 2

Full source

lemma pow_four_le_pow_two_of_pow_two_le (h : a ^ 2 ≤ b) : a ^ 4 ≤ b ^ 2 :=
  (pow_mul a 2 2).symm ▸ pow_le_pow_left₀ (sq_nonneg a) h 2

Monotonicity of Even Powers: $a^4 \leq b^2$ from $a^2 \leq b$

Informal description

For any elements $a$ and $b$ in a linearly ordered semiring or ring $R$, if $a^2 \leq b$, then $a^4 \leq b^2$.