feat(analysis/special_functions/pow, set_theory/*): positivity exte…

…nsion for powers (#16462)

Add the following `positivity` extensions to handle powers:
* `positivity_rpow` for real powers
* `positivity_opow` for ordinal powers
* `positivity_cardinal_pow` for cardinal powers

src/analysis/special_functions/pow.lean

@@ -2103,3 +2103,59 @@ prove_rpow' ``ennrpow_pos ``ennrpow_neg ``ennreal.rpow_zero `(ℝ≥0∞) `(ℝ)
 | _ := tactic.failed
 
 end norm_num
+
+namespace tactic
+namespace positivity
+
+/-- Auxiliary definition for the `positivity` tactic to handle real powers of reals. -/
+meta def prove_rpow (a b : expr) : tactic strictness :=
+do
+  strictness_a ← core a,
+  match strictness_a with
+  | nonnegative p := nonnegative <$> mk_app ``real.rpow_nonneg_of_nonneg [p, b]
+  | positive p := positive <$> mk_app ``real.rpow_pos_of_pos [p, b]
+  end
+
+private lemma nnrpow_pos {a : ℝ≥0} (ha : 0 < a) (b : ℝ) : 0 < a ^ b := nnreal.rpow_pos ha
+
+/-- Auxiliary definition for the `positivity` tactic to handle real powers of nonnegative reals. -/
+meta def prove_nnrpow (a b : expr) : tactic strictness :=
+do
+  strictness_a ← core a,
+  match strictness_a with
+  | positive p := positive <$> mk_app ``nnrpow_pos [p, b]
+  | _ := failed -- We already know `0 ≤ x` for all `x : ℝ≥0`
+  end
+
+private lemma ennrpow_pos {a : ℝ≥0∞} {b : ℝ} (ha : 0 < a) (hb : 0 < b) : 0 < a ^ b :=
+ennreal.rpow_pos_of_nonneg ha hb.le
+
+/-- Auxiliary definition for the `positivity` tactic to handle real powers of extended nonnegative
+reals. -/
+meta def prove_ennrpow (a b : expr) : tactic strictness :=
+do
+  strictness_a ← core a,
+  strictness_b ← core b,
+  match strictness_a, strictness_b with
+  | positive pa, positive pb := positive <$> mk_app ``ennrpow_pos [pa, pb]
+  | positive pa, nonnegative pb := positive <$> mk_app ``ennreal.rpow_pos_of_nonneg [pa, pb]
+  | _, _ := failed -- We already know `0 ≤ x` for all `x : ℝ≥0∞`
+  end
+
+end positivity
+
+open positivity
+
+/-- Extension for the `positivity` tactic: exponentiation by a real number is nonnegative when the
+base is nonnegative and positive when the base is positive. -/
+@[positivity]
+meta def positivity_rpow : expr → tactic strictness
+| `(@has_pow.pow _ _ real.has_pow %%a %%b) := prove_rpow a b
+| `(real.rpow %%a %%b) := prove_rpow a b
+| `(@has_pow.pow _ _ nnreal.real.has_pow %%a %%b) := prove_nnrpow a b
+| `(nnreal.rpow %%a %%b) := prove_nnrpow a b
+| `(@has_pow.pow _ _ ennreal.real.has_pow %%a %%b) := prove_ennrpow a b
+| `(ennreal.rpow %%a %%b) := prove_ennrpow a b
+| _ := failed
+
+end tactic

src/set_theory/cardinal/basic.lean

@@ -11,6 +11,7 @@ import logic.small
 import order.conditionally_complete_lattice
 import order.succ_pred.basic
 import set_theory.cardinal.schroeder_bernstein
+import tactic.positivity
 
 /-!
 # Cardinal Numbers
@@ -518,6 +519,8 @@ end
 theorem power_le_power_right {a b c : cardinal} : a ≤ b → a ^ c ≤ b ^ c :=
 induction_on₃ a b c $ λ α β γ ⟨e⟩, ⟨embedding.arrow_congr_right e⟩
 
+theorem power_pos {a : cardinal} (b) (ha : 0 < a) : 0 < a ^ b := (power_ne_zero _ ha.ne').bot_lt
+
 end order_properties
 
 protected theorem lt_wf : @well_founded cardinal.{u} (<) :=
@@ -1580,3 +1583,19 @@ begin
 end
 
 end cardinal
+
+namespace tactic
+open cardinal positivity
+
+/-- Extension for the `positivity` tactic: The cardinal power of a positive cardinal is positive. -/
+@[positivity]
+meta def positivity_cardinal_pow : expr → tactic strictness
+| `(@has_pow.pow _ _ %%inst %%a %%b) := do
+  strictness_a ← core a,
+  match strictness_a with
+  | positive p := positive <$> mk_app ``power_pos [b, p]
+  | _ := failed -- We already know that `0 ≤ x` for all `x : cardinal`
+  end
+| _ := failed
+
+end tactic

src/set_theory/ordinal/arithmetic.lean

@@ -2363,3 +2363,20 @@ begin
 end
 
 end ordinal
+
+namespace tactic
+open ordinal positivity
+
+/-- Extension for the `positivity` tactic: `ordinal.opow` takes positive values on positive inputs.
+-/
+@[positivity]
+meta def positivity_opow : expr → tactic strictness
+| `(@has_pow.pow _ _ %%inst %%a %%b) := do
+  strictness_a ← core a,
+  match strictness_a with
+  | positive p := positive <$> mk_app ``opow_pos [b, p]
+  | _ := failed -- We already know that `0 ≤ x` for all `x : ordinal`
+  end
+| _ := failed
+
+end tactic

src/tactic/positivity.lean

@@ -358,29 +358,48 @@ meta def positivity_inv : expr → tactic strictness
 private lemma pow_zero_pos [ordered_semiring R] [nontrivial R] (a : R) : 0 < a ^ 0 :=
 zero_lt_one.trans_le (pow_zero a).ge
 
-/-- Extension for the `positivity` tactic: raising a number `a` to a natural number power `n` is
-known to be positive if `n = 0` (since `a ^ 0 = 1`) or if `0 < a`, and is known to be nonnegative if
-`n = 2` (squares are nonnegative) or if `0 ≤ a`. -/
+private lemma zpow_zero_pos [linear_ordered_semifield R] (a : R) : 0 < a ^ (0 : ℤ) :=
+zero_lt_one.trans_le (zpow_zero a).ge
+
+/-- Extension for the `positivity` tactic: raising a number `a` to a natural/integer power `n` is
+positive if `n = 0` (since `a ^ 0 = 1`) or if `0 < a`, and is nonnegative if `n` is even (squares
+are nonnegative) or if `0 ≤ a`. -/
 @[positivity]
 meta def positivity_pow : expr → tactic strictness
 | `(%%a ^ %%n) := do
-  n_typ ← infer_type n,
-  match n_typ with
-  | `(ℕ) := do
+  typ ← infer_type n,
+  (do
+    unify typ `(ℕ),
     if n = `(0) then
       positive <$> mk_app ``pow_zero_pos [a]
-    else tactic.positivity.orelse'
-      -- squares are nonnegative (TODO: similar for any `bit0` exponent?)
-      (nonnegative <$> mk_app ``sq_nonneg [a])
-      -- moreover `a ^ n` is positive if `a` is and nonnegative if `a` is
-      (do
+    else positivity.orelse'
+      (do -- even powers are nonnegative
+        match n with -- TODO: Decision procedure for parity
+        | `(bit0 %% n) := nonnegative <$> mk_app ``pow_bit0_nonneg [a, n]
+        | _ := failed
+        end) $
+      do -- `a ^ n` is positive if `a` is, and nonnegative if `a` is
         strictness_a ← core a,
         match strictness_a with
-        | (positive pa) := positive <$> mk_app ``pow_pos [pa, n]
-        | (nonnegative pa) := nonnegative <$> mk_app ``pow_nonneg [pa, n]
-        end)
-  | _ := failed -- TODO handle integer powers, maybe even real powers
-  end
+        | positive p := positive <$> mk_app ``pow_pos [p, n]
+        | nonnegative p := nonnegative <$> mk_app `pow_nonneg [p, n]
+        end) <|>
+    (do
+      unify typ `(ℤ),
+      if n = `(0 : ℤ) then
+        positive <$> mk_app ``zpow_zero_pos [a]
+      else positivity.orelse'
+        (do -- even powers are nonnegative
+          match n with -- TODO: Decision procedure for parity
+          | `(bit0 %% n) := nonnegative <$> mk_app ``zpow_bit0_nonneg [a, n]
+          | _ := failed
+          end) $
+        do -- `a ^ n` is positive if `a` is, and nonnegative if `a` is
+          strictness_a ← core a,
+          match strictness_a with
+          | positive p := positive <$> mk_app ``zpow_pos_of_pos [p, n]
+          | nonnegative p := nonnegative <$> mk_app ``zpow_nonneg [p, n]
+          end)
 | _ := failed
 
 /-- Extension for the `positivity` tactic: an absolute value is nonnegative, and is strictly

test/positivity.lean

@@ -1,5 +1,6 @@
 import algebra.order.smul
 import analysis.normed.group.basic
+import analysis.special_functions.pow
 import data.complex.exponential
 import data.rat.nnrat
 import data.real.ereal
@@ -12,7 +13,10 @@ import tactic.positivity
 This tactic proves goals of the form `0 ≤ a` and `0 < a`.
 -/
 
-open_locale ennreal nnrat nnreal
+open_locale ennreal nnreal
+
+universe u
+variables {α β : Type*}
 
 /- ## Numeric goals -/
 
@@ -56,7 +60,26 @@ example {a b : ℤ} (ha : 3 < a) (hb : 4 ≤ b) : 0 < 3 + a * b / 7 + b + 7 + 14
 
 example {a : ℤ} (ha : 0 < a) : 0 < a / a := by positivity
 
-example {a : ℕ} : 0 < a ^ 0 := by positivity
+/-! ### Exponentiation -/
+
+example [ordered_semiring α] [nontrivial α] (a : α) : 0 < a ^ 0 := by positivity
+example [linear_ordered_ring α] (a : α) (n : ℕ) : 0 ≤ a ^ (bit0 n) := by positivity
+example [ordered_semiring α] {a : α} {n : ℕ} (ha : 0 ≤ a) : 0 ≤ a ^ n := by positivity
+example [ordered_semiring α] {a : α} {n : ℕ} (ha : 0 < a) : 0 < a ^ n := by positivity
+
+example [linear_ordered_semifield α] (a : α) : 0 < a ^ (0 : ℤ) := by positivity
+example [linear_ordered_field α] (a : α) (n : ℤ) : 0 ≤ a ^ (bit0 n) := by positivity
+example [linear_ordered_semifield α] {a : α} {n : ℤ} (ha : 0 ≤ a) : 0 ≤ a ^ n := by positivity
+example [linear_ordered_semifield α] {a : α} {n : ℤ} (ha : 0 < a) : 0 < a ^ n := by positivity
+
+example {a b : cardinal.{u}} (ha : 0 < a) : 0 < a ^ b := by positivity
+example {a b : ordinal.{u}} (ha : 0 < a) : 0 < a ^ b := by positivity
+
+example {a b : ℝ} (ha : 0 ≤ a) : 0 ≤ a ^ b := by positivity
+example {a b : ℝ} (ha : 0 < a) : 0 < a ^ b := by positivity
+example {a : ℝ≥0} {b : ℝ} (ha : 0 < a) : 0 < a ^ b := by positivity
+example {a : ℝ≥0∞} {b : ℝ} (ha : 0 < a) (hb : 0 ≤ b) : 0 < a ^ b := by positivity
+example {a : ℝ≥0∞} {b : ℝ} (ha : 0 < a) (hb : 0 < b) : 0 < a ^ b := by positivity
 
 example {a : ℤ} (ha : 3 < a) : 0 ≤ a ^ 2 + a := by positivity
 
@@ -99,7 +122,7 @@ example : 0 ≤ max (0:ℤ) (-3) := by positivity
 
 example : 0 ≤ max (-3 : ℤ) 5 := by positivity
 
-example {α β : Type*} [ordered_semiring α] [ordered_add_comm_monoid β] [smul_with_zero α β]
+example [ordered_semiring α] [ordered_add_comm_monoid β] [smul_with_zero α β]
   [ordered_smul α β] {a : α} (ha : 0 < a) {b : β} (hb : 0 < b) : 0 ≤ a • b := by positivity
 
 example {r : ℝ} : 0 < real.exp r := by positivity