Mathlib.Algebra.Order.Field.Power

Even.zpow_nonneg theorem

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

Full source

protected theorem Even.zpow_nonneg (hn : Even n) (a : α) : 0 ≤ a ^ n := by
  obtain ⟨k, rfl⟩ := hn; rw [zpow_add' (by simp [em'])]; exact mul_self_nonneg _

Nonnegativity of Even Powers in Ordered Fields

Informal description

For any element $a$ in a linearly ordered field $\alpha$ and any even integer $n$, the $n$-th power of $a$ is nonnegative, i.e., $0 \leq a^n$.

zpow_two_nonneg theorem

(a : α) : 0 ≤ a ^ (2 : ℤ)

Full source

lemma zpow_two_nonneg (a : α) : 0 ≤ a ^ (2 : ℤ) := even_two.zpow_nonneg _

Nonnegativity of Squares in Ordered Fields

Informal description

For any element $a$ in a linearly ordered field $\alpha$, the square of $a$ (i.e., $a^2$) is nonnegative, i.e., $0 \leq a^2$.

zpow_neg_two_nonneg theorem

(a : α) : 0 ≤ a ^ (-2 : ℤ)

Full source

lemma zpow_neg_two_nonneg (a : α) : 0 ≤ a ^ (-2 : ℤ) := even_neg_two.zpow_nonneg _

Nonnegativity of Negative Even Powers in Ordered Fields: $0 \leq a^{-2}$

Informal description

For any element $a$ in a linearly ordered field $\alpha$, the $-2$-th power of $a$ is nonnegative, i.e., $0 \leq a^{-2}$.

Even.zpow_pos theorem

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

Full source

protected lemma Even.zpow_pos (hn : Even n) (ha : a ≠ 0) : 0 < a ^ n :=
  (hn.zpow_nonneg _).lt_of_ne' (zpow_ne_zero _ ha)

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

Informal description

For any element $a$ in a linearly ordered field $\alpha$ and any even integer $n$, if $a$ is nonzero, then the $n$-th power of $a$ is strictly positive, i.e., $0 < a^n$.

zpow_two_pos_of_ne_zero theorem

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

Full source

lemma zpow_two_pos_of_ne_zero (ha : a ≠ 0) : 0 < a ^ (2 : ℤ) := even_two.zpow_pos ha

Positivity of Squares for Nonzero Elements: $0 < a^2$ when $a \neq 0$

Informal description

For any nonzero element $a$ in a linearly ordered field, the square of $a$ is strictly positive, i.e., $0 < a^2$.

Even.zpow_pos_iff theorem

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

Full source

theorem Even.zpow_pos_iff (hn : Even n) (h : n ≠ 0) : 0 < a ^ n ↔ a ≠ 0 := by
  obtain ⟨k, rfl⟩ := hn
  rw [zpow_add' (by simp [em']), mul_self_pos, zpow_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

For any even integer $n \neq 0$ and any element $a$ in a strict ordered semiring, the $n$-th power $a^n$ is positive if and only if $a$ is nonzero, i.e., $0 < a^n \leftrightarrow a \neq 0$.

Odd.zpow_neg_iff theorem

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

Full source

theorem Odd.zpow_neg_iff (hn : Odd n) : a ^ n < 0 ↔ a < 0 := by
  refine ⟨lt_imp_lt_of_le_imp_le (zpow_nonneg · _), fun ha ↦ ?_⟩
  obtain ⟨k, rfl⟩ := hn
  rw [zpow_add_one₀ ha.ne]
  exact mul_neg_of_pos_of_neg (Even.zpow_pos (even_two_mul _) ha.ne) ha

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

Informal description

For any odd integer $n$ and any element $a$ in a linearly ordered field, the $n$-th power of $a$ is negative if and only if $a$ is negative, i.e., $a^n < 0 \leftrightarrow a < 0$.

Odd.zpow_nonneg_iff theorem

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

Full source

protected lemma Odd.zpow_nonneg_iff (hn : Odd n) : 0 ≤ a ^ n ↔ 0 ≤ a :=
  le_iff_le_iff_lt_iff_lt.2 hn.zpow_neg_iff

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

Informal description

For any odd integer $n$ and any element $a$ in a linearly ordered field, 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.zpow_nonpos_iff theorem

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

Full source

theorem Odd.zpow_nonpos_iff (hn : Odd n) : a ^ n ≤ 0 ↔ a ≤ 0 := by
  rw [le_iff_lt_or_eq, le_iff_lt_or_eq, hn.zpow_neg_iff, zpow_eq_zero_iff]
  rintro rfl
  exact Int.not_even_iff_odd.2 hn .zero

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

Informal description

For any odd integer $n$ and any element $a$ in a linearly ordered field, 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.zpow_pos_iff theorem

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

Full source

lemma Odd.zpow_pos_iff (hn : Odd n) : 0 < a ^ n ↔ 0 < a := lt_iff_lt_of_le_iff_le hn.zpow_nonpos_iff

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

Informal description

For any odd integer $n$ and any element $a$ in a linearly ordered field, the $n$-th power of $a$ is positive if and only if $a$ is positive, i.e., $0 < a^n \leftrightarrow 0 < a$.

Even.zpow_abs theorem

{p : ℤ} (hp : Even p) (a : α) : |a| ^ p = a ^ p

Full source

theorem Even.zpow_abs {p : ℤ} (hp : Even p) (a : α) : |a| ^ p = a ^ p := by
  rcases abs_choice a with h | h <;> simp only [h, hp.neg_zpow _]

Absolute Value and Even Powers: $|a|^p = a^p$ for Even $p$

Informal description

For any integer $p$ such that $p$ is even, and for any element $a$ in a linearly ordered field $\alpha$, the absolute value of $a$ raised to the power $p$ is equal to $a$ raised to the power $p$, i.e., $|a|^p = a^p$.

zpow_eq_zpow_iff_of_ne_zero₀ theorem

(hn : n ≠ 0) : a ^ n = b ^ n ↔ a = b ∨ a = -b ∧ Even n

Full source

lemma zpow_eq_zpow_iff_of_ne_zero₀ (hn : n ≠ 0) : a ^ n = b ^ n ↔ a = b ∨ a = -b ∧ Even n :=
  match n with
  | Int.ofNat m => by
    simp only [Int.ofNat_eq_coe, ne_eq, Nat.cast_eq_zero, zpow_natCast, Int.even_coe_nat] at *
    exact pow_eq_pow_iff_of_ne_zero hn
  | Int.negSucc m => by
    simp only [← neg_ofNat_succ, ne_eq, neg_eq_zero, Nat.cast_eq_zero, zpow_neg, zpow_natCast,
      inv_inj, even_neg, Int.even_coe_nat] at *
    exact pow_eq_pow_iff_of_ne_zero hn

Equality of Integer Powers in Ordered Fields: $a^n = b^n \leftrightarrow a = b \lor (a = -b \land \text{even } n)$ for $n \neq 0$

Informal description

For any elements $a$ and $b$ in a linearly ordered field and any nonzero integer $n$, the equality $a^n = b^n$ holds if and only if either $a = b$ or $a = -b$ and $n$ is even.

zpow_eq_zpow_iff_cases₀ theorem

: a ^ n = b ^ n ↔ n = 0 ∨ a = b ∨ a = -b ∧ Even n

Full source

lemma zpow_eq_zpow_iff_cases₀ : a ^ n = b ^ n ↔ n = 0 ∨ a = b ∨ a = -b ∧ Even n := by
  rcases eq_or_ne n 0 with rfl | hn <;> simp [zpow_eq_zpow_iff_of_ne_zero₀, *]

Integer Power Equality Cases: $a^n = b^n$ iff $n=0$, $a=b$, or $a=-b$ and $n$ is even

Informal description

For any elements $a$ and $b$ in a division-inversion monoid and any integer $n$, the equality $a^n = b^n$ holds if and only if either $n = 0$, or $a = b$, or $a = -b$ and $n$ is even.

zpow_eq_one_iff_of_ne_zero₀ theorem

(hn : n ≠ 0) : a ^ n = 1 ↔ a = 1 ∨ a = -1 ∧ Even n

Full source

lemma zpow_eq_one_iff_of_ne_zero₀ (hn : n ≠ 0) : a ^ n = 1 ↔ a = 1 ∨ a = -1 ∧ Even n := by
  simp [← zpow_eq_zpow_iff_of_ne_zero₀ hn]

Integer Power Equals One: $a^n = 1$ iff $a=1$ or ($a=-1$ and $n$ even) for $n \neq 0$

Informal description

For any nonzero integer $n$ and any element $a$ in a linearly ordered field, the equation $a^n = 1$ holds if and only if either $a = 1$ or $a = -1$ and $n$ is even.

zpow_eq_one_iff_cases₀ theorem

: a ^ n = 1 ↔ n = 0 ∨ a = 1 ∨ a = -1 ∧ Even n

Full source

lemma zpow_eq_one_iff_cases₀ : a ^ n = 1 ↔ n = 0 ∨ a = 1 ∨ a = -1 ∧ Even n := by
  simp [← zpow_eq_zpow_iff_cases₀]

Integer Power Equals One Cases: $a^n = 1$ iff $n=0$, $a=1$, or $a=-1$ and $n$ even

Informal description

For any element $a$ in a division-inversion monoid and any integer $n$, the equality $a^n = 1$ holds if and only if either $n = 0$, or $a = 1$, or $a = -1$ and $n$ is even.

zpow_eq_neg_zpow_iff₀ theorem

(hb : b ≠ 0) : a ^ n = -b ^ n ↔ a = -b ∧ Odd n

Full source

lemma zpow_eq_neg_zpow_iff₀ (hb : b ≠ 0) : a ^ n = -b ^ n ↔ a = -b ∧ Odd n :=
  match n with
  | Int.ofNat m => by
    simp [pow_eq_neg_pow_iff, hb]
  | Int.negSucc m => by
    simp only [← neg_ofNat_succ, zpow_neg, inv_pow, ← inv_neg, pow_eq_neg_pow_iff hb, inv_inj,
      zpow_natCast]
    simp [parity_simps]

Integer Power Negation Equivalence: $a^n = -b^n \leftrightarrow (a = -b \land \text{$n$ odd})$ for $b \neq 0$

Informal description

For any nonzero element $b$ in a division-inversion monoid, the equation $a^n = -b^n$ holds if and only if $a = -b$ and $n$ is an odd integer.

zpow_eq_neg_one_iff₀ theorem

: a ^ n = -1 ↔ a = -1 ∧ Odd n

Full source

lemma zpow_eq_neg_one_iff₀ : a ^ n = -1 ↔ a = -1 ∧ Odd n := by
  simpa using zpow_eq_neg_zpow_iff₀ (α := α) one_ne_zero

Integer Power Equals Negative One: $a^n = -1 \leftrightarrow (a = -1 \land \text{$n$ odd})$

Informal description

For any element $a$ in a division-inversion monoid and any integer $n$, the equality $a^n = -1$ holds if and only if $a = -1$ and $n$ is odd.

Nat.cast_le_pow_sub_div_sub theorem

(H : 1 < a) (n : ℕ) : (n : α) ≤ (a ^ n - 1) / (a - 1)

Full source

/-- Bernoulli's inequality reformulated to estimate `(n : α)`. -/
theorem Nat.cast_le_pow_sub_div_sub (H : 1 < a) (n : ℕ) : (n : α) ≤ (a ^ n - 1) / (a - 1) :=
  (le_div_iff₀ (sub_pos.2 H)).2 <|
    le_sub_left_of_add_le <| one_add_mul_sub_le_pow ((neg_le_self zero_le_one).trans H.le) _

Inequality for Natural Number Cast and Power: $n \leq \frac{a^n - 1}{a - 1}$ when $1 < a$

Informal description

For any element $a$ in a linear ordered field with $1 < a$ and any natural number $n$, the following inequality holds: \[ n \leq \frac{a^n - 1}{a - 1}. \]

Nat.cast_le_pow_div_sub theorem

(H : 1 < a) (n : ℕ) : (n : α) ≤ a ^ n / (a - 1)

Full source

/-- For any `a > 1` and a natural `n` we have `n ≤ a ^ n / (a - 1)`. See also
`Nat.cast_le_pow_sub_div_sub` for a stronger inequality with `a ^ n - 1` in the numerator. -/
theorem Nat.cast_le_pow_div_sub (H : 1 < a) (n : ℕ) : (n : α) ≤ a ^ n / (a - 1) :=
  (n.cast_le_pow_sub_div_sub H).trans <|
    div_le_div_of_nonneg_right (sub_le_self _ zero_le_one) (sub_nonneg.2 H.le)

Bernoulli's Inequality Variant: $n \leq \frac{a^n}{a - 1}$ for $a > 1$

Informal description

For any element $a > 1$ in a linearly ordered field and any natural number $n$, the following inequality holds: \[ n \leq \frac{a^n}{a - 1}. \]

Mathlib.Meta.Positivity.evalZPow definition

: PositivityExt

Full source

/-- The `positivity` extension which identifies expressions of the form `a ^ (b : ℤ)`,
such that `positivity` successfully recognises both `a` and `b`. -/
@[positivity _ ^ (_ : ℤ), Pow.pow _ (_ : ℤ)]
def evalZPow : PositivityExt where eval {u α} zα pα e := do
  let .app (.app _ (a : Q($α))) (b : Q(ℤ)) ← withReducible (whnf e) | throwError "not ^"
  let result ← catchNone do
    let _a ← synthInstanceQ q(Field $α)
    let _a ← synthInstanceQ q(LinearOrder $α)
    let _a ← synthInstanceQ q(IsStrictOrderedRing $α)
    assumeInstancesCommute
    match ← whnfR b with
    | .app (.app (.app (.const `OfNat.ofNat _) _) (.lit (Literal.natVal n))) _ =>
      guard (n % 2 = 0)
      have m : Q(ℕ) := mkRawNatLit (n / 2)
      haveI' : $b =Q $m + $m := ⟨⟩
      haveI' : $e =Q $a ^ $b := ⟨⟩
      pure (.nonnegative q(Even.zpow_nonneg (Even.add_self _) $a))
    | .app (.app (.app (.const `Neg.neg _) _) _) b' =>
      let b' ← whnfR b'
      let .true := b'.isAppOfArity ``OfNat.ofNat 3 | throwError "not a ^ -n where n is a literal"
      let some n := (b'.getRevArg! 1).rawNatLit? | throwError "not a ^ -n where n is a literal"
      guard (n % 2 = 0)
      have m : Q(ℕ) := mkRawNatLit (n / 2)
      haveI' : $b =Q (-$m) + (-$m) := ⟨⟩
      haveI' : $e =Q $a ^ $b := ⟨⟩
      pure (.nonnegative q(Even.zpow_nonneg (Even.add_self _) $a))
    | _ => throwError "not a ^ n where n is a literal or a negated literal"
  orElse result do
    let ra ← core zα pα a
    let ofNonneg (pa : Q(0 ≤ $a))
        (_oα : Q(Semifield $α)) (_oα : Q(LinearOrder $α)) (_oα : Q(IsStrictOrderedRing $α)) :
        MetaM (Strictness zα pα e) := do
      haveI' : $e =Q $a ^ $b := ⟨⟩
      assumeInstancesCommute
      pure (.nonnegative q(zpow_nonneg $pa $b))
    let ofNonzero (pa : Q($a ≠ 0)) (_oα : Q(GroupWithZero $α)) : MetaM (Strictness zα pα e) := do
      haveI' : $e =Q $a ^ $b := ⟨⟩
      let _a ← synthInstanceQ q(GroupWithZero $α)
      assumeInstancesCommute
      pure (.nonzero q(zpow_ne_zero $b $pa))
    match ra with
    | .positive pa =>
      try
        let _a ← synthInstanceQ q(Semifield $α)
        let _a ← synthInstanceQ q(LinearOrder $α)
        let _a ← synthInstanceQ q(IsStrictOrderedRing $α)
        haveI' : $e =Q $a ^ $b := ⟨⟩
        assumeInstancesCommute
        pure (.positive q(zpow_pos $pa $b))
      catch e : Exception =>
        trace[Tactic.positivity.failure] "{e.toMessageData}"
        let sα ← synthInstanceQ q(Semifield $α)
        let oα ← synthInstanceQ q(LinearOrder $α)
        let iα ← synthInstanceQ q(IsStrictOrderedRing $α)
        orElse (← catchNone (ofNonneg q(le_of_lt $pa) sα oα iα))
          (ofNonzero q(ne_of_gt $pa) q(inferInstance))
    | .nonnegative pa =>
      ofNonneg pa (← synthInstanceQ (_ : Q(Type u)))
                  (← synthInstanceQ (_ : Q(Type u))) (← synthInstanceQ (_ : Q(Prop)))
    | .nonzero pa => ofNonzero pa (← synthInstanceQ (_ : Q(Type u)))
    | .none => pure .none

Positivity extension for integer powers

Informal description

The `evalZPow` positivity extension identifies expressions of the form $ a^b $ where $ b $ is an integer, and determines their positivity properties. Specifically, it checks whether the base $ a $ is positive, non-negative, or non-zero, and combines this with the exponent $ b $ to determine the strictness of the resulting expression. The extension handles cases where $ b $ is an even natural number or its negation, ensuring the result is non-negative in these cases.