feat(Positivity): add positivity extensions for NNReal.rpow and ENNReal.rpow (#29463)

Author: HugLycan

Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean

@@ -44,6 +44,8 @@ theorem coe_rpow (x : ℝ≥0) (y : ℝ) : ((x ^ y : ℝ≥0) : ℝ) = (x : ℝ)
 theorem rpow_zero (x : ℝ≥0) : x ^ (0 : ℝ) = 1 :=
   NNReal.eq <| Real.rpow_zero _
 
+theorem rpow_zero_pos (x : ℝ≥0) : 0 < x ^ (0 : ℝ) := by rw [rpow_zero]; exact one_pos
+
 @[simp]
 theorem rpow_eq_zero_iff {x : ℝ≥0} {y : ℝ} : x ^ y = 0 ↔ x = 0 ∧ y ≠ 0 := by
   rw [← NNReal.coe_inj, coe_rpow, ← NNReal.coe_eq_zero]
@@ -456,6 +458,8 @@ theorem rpow_zero {x : ℝ≥0∞} : x ^ (0 : ℝ) = 1 := by
     · dsimp only [(· ^ ·), Pow.pow, rpow]
       simp
 
+theorem rpow_zero_pos (x : ℝ≥0∞) : 0 < x ^ (0 : ℝ) := by rw [rpow_zero]; exact one_pos
+
 theorem top_rpow_def (y : ℝ) : (⊤ : ℝ≥0∞) ^ y = if 0 < y then ⊤ else if y = 0 then 1 else 0 :=
   rfl
 
@@ -1062,3 +1066,62 @@ end ENNReal
 -- end Tactic
 
 -- end Tactics
+
+/-! ### Positivity extension -/
+
+namespace Mathlib.Meta.Positivity
+open Lean Meta Qq
+
+/-- Extension for the `positivity` tactic: exponentiation by a real number is nonnegative when
+the base is nonnegative and positive when the base is positive.
+This is the `NNReal` analogue of `evalRpow` for `Real`. -/
+@[positivity (_ : ℝ≥0) ^ (_ : ℝ)]
+def evalNNRealRpow : PositivityExt where eval {u α} _ _ e := do
+  match u, α, e with
+  | 0, ~q(ℝ≥0), ~q($a ^ (0 : ℝ)) =>
+    assertInstancesCommute
+    pure (.positive q(NNReal.rpow_zero_pos $a))
+  | 0, ~q(ℝ≥0), ~q($a ^ ($b : ℝ)) =>
+    let ra ← core q(inferInstance) q(inferInstance) a
+    assertInstancesCommute
+    match ra with
+    | .positive pa =>
+        pure (.positive q(NNReal.rpow_pos $pa))
+    | _ => pure (.nonnegative q(zero_le $e))
+  | _, _, _ => throwError "not NNReal.rpow"
+
+private def isFiniteM? (x : Q(ℝ≥0∞)) : MetaM (Option Q($x ≠ (⊤ : ℝ≥0∞))) := do
+  let mvar ← mkFreshExprMVar q($x ≠ (⊤ : ℝ≥0∞))
+  let save ← saveState
+  let (goals, _) ← Elab.runTactic mvar.mvarId! <|← `(tactic| finiteness)
+  if goals.isEmpty then
+    pure <| some <|← instantiateMVars mvar
+  else
+    restoreState save
+    pure none
+
+/-- Extension for the `positivity` tactic: exponentiation by a real number is nonnegative when
+the base is nonnegative and positive when the base is positive.
+This is the `ENNReal` analogue of `evalRpow` for `Real`. -/
+@[positivity (_ : ℝ≥0∞) ^ (_ : ℝ)]
+def evalENNRealRpow : PositivityExt where eval {u α} _ _ e := do
+  match u, α, e with
+  | 0, ~q(ℝ≥0∞), ~q($a ^ (0 : ℝ)) =>
+    assertInstancesCommute
+    pure (.positive q(ENNReal.rpow_zero_pos $a))
+  | 0, ~q(ℝ≥0∞), ~q($a ^ ($b : ℝ)) =>
+    let ra ← core q(inferInstance) q(inferInstance) a
+    let rb ← catchNone <| core q(inferInstance) q(inferInstance) b
+    assertInstancesCommute
+    match ra, rb with
+    | .positive pa, .positive pb =>
+        pure (.positive q(ENNReal.rpow_pos_of_nonneg $pa <| le_of_lt $pb))
+    | .positive pa, .nonnegative pb =>
+        pure (.positive q(ENNReal.rpow_pos_of_nonneg $pa $pb))
+    | .positive pa, _ =>
+        let some ha ← isFiniteM? a | pure <| .nonnegative q(zero_le $e)
+        pure <| .positive q(ENNReal.rpow_pos $pa $ha)
+    | _, _ => pure <| .nonnegative q(zero_le $e)
+  | _, _, _ => throwError "not ENNReal.rpow"
+
+end Mathlib.Meta.Positivity

MathlibTest/positivity.lean

@@ -325,9 +325,13 @@ example [Semifield α] [LinearOrder α] [IsStrictOrderedRing α]
 
 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 : ℝ≥0} {b : ℝ} : 0 ≤ a ^ b := by positivity
+example {a : ℝ≥0} {b : ℝ} (ha : 0 < a) : 0 < a ^ b := by positivity
+example {a : ℝ≥0∞} {b : ℝ} : 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 : ℝ≥0∞} : 0 < a ^ 0 := by positivity
+example {a : ℝ≥0∞} {b : ℝ} (ha : 0 < a) (hat : a ≠ ⊤) : 0 < a ^ b := by positivity
 example {a : ℝ} : 0 < a ^ 0 := by positivity
 
 example {a : ℤ} (ha : 3 < a) : 0 ≤ a ^ 2 + a := by positivity