feat(ENNReal): x⁻¹ ^ n = (x ^ n)⁻¹ (#28090)

FormulaRabbit81 · YaelDillies · FormulaRabbit81 · commit 2fb870934f7e · 2025-08-14T17:15:31.000Z
Co-authored-by: FormulaRabbit81 &lt;122625239+FormulaRabbit81@users.noreply.github.com&gt;
Co-authored-by: Yaël Dillies &lt;yael.dillies@gmail.com&gt;
diff --git a/Mathlib/Data/ENNReal/Inv.lean b/Mathlib/Data/ENNReal/Inv.lean
@@ -643,6 +643,12 @@ theorem coe_zpow (hr : r ≠ 0) (n : ℤ) : (↑(r ^ n) : ℝ≥0∞) = (r : ℝ
   · have : r ^ n.succ ≠ 0 := pow_ne_zero (n + 1) hr
     simp only [zpow_negSucc, coe_inv this, coe_pow]
 
+lemma zero_zpow_def (n : ℤ) : (0 : ℝ≥0∞) ^ n = if n = 0 then 1 else if 0 < n then 0 else ⊤ := by
+  obtain ((_ | n) | n) := n <;> simp [-Nat.cast_add, -Int.natCast_add]
+
+lemma top_zpow_def (n : ℤ) : (⊤ : ℝ≥0∞) ^ n = if n = 0 then 1 else if 0 < n then ⊤ else 0 := by
+  obtain ((_ | n) | n) := n <;> simp [-Nat.cast_add, -Int.natCast_add]
+
 theorem zpow_pos (ha : a ≠ 0) (h'a : a ≠ ∞) (n : ℤ) : 0 < a ^ n := by
   cases n
   · simpa using ENNReal.pow_pos ha.bot_lt _
@@ -718,13 +724,30 @@ protected theorem zpow_add {x : ℝ≥0∞} (hx : x ≠ 0) (h'x : x ≠ ∞) (m
   replace hx : x ≠ 0 := by simpa only [Ne, coe_eq_zero] using hx
   simp only [← coe_zpow hx, zpow_add₀ hx, coe_mul]
 
-protected theorem zpow_neg {x : ℝ≥0∞} (x_ne_zero : x ≠ 0) (x_ne_top : x ≠ ⊤) (m : ℤ) :
-    x ^ (-m) = (x ^ m)⁻¹ :=
-  ENNReal.eq_inv_of_mul_eq_one_left (by simp [← ENNReal.zpow_add x_ne_zero x_ne_top])
+protected theorem zpow_neg (x : ℝ≥0∞) (m : ℤ) : x ^ (-m) = (x ^ m)⁻¹ := by
+  obtain hx₀ | hx₀ := eq_or_ne x 0
+  · obtain hm | hm | hm := lt_trichotomy m 0 <;>
+      simp_all [zero_zpow_def, ne_of_lt, ne_of_gt, lt_asymm]
+  obtain hx | hx := eq_or_ne x ⊤
+  · obtain hm | hm | hm := lt_trichotomy m 0 <;>
+      simp_all [top_zpow_def, ne_of_lt, ne_of_gt, lt_asymm]
+  exact ENNReal.eq_inv_of_mul_eq_one_left (by simp [← ENNReal.zpow_add hx₀ hx])
 
 protected theorem zpow_sub {x : ℝ≥0∞} (x_ne_zero : x ≠ 0) (x_ne_top : x ≠ ⊤) (m n : ℤ) :
     x ^ (m - n) = (x ^ m) * (x ^ n)⁻¹ := by
-  rw [sub_eq_add_neg, ENNReal.zpow_add x_ne_zero x_ne_top, ENNReal.zpow_neg x_ne_zero x_ne_top n]
+  rw [sub_eq_add_neg, ENNReal.zpow_add x_ne_zero x_ne_top, ENNReal.zpow_neg]
+
+protected lemma inv_zpow (x : ℝ≥0∞) (n : ℤ) : x⁻¹ ^ n = (x ^ n)⁻¹ := by
+  cases n <;> simp [ENNReal.inv_pow]
+
+protected lemma inv_zpow' (x : ℝ≥0∞) (n : ℤ) : x⁻¹ ^ n = x ^ (-n) := by
+  rw [ENNReal.zpow_neg, ENNReal.inv_zpow]
+
+lemma zpow_le_one_of_nonpos {n : ℤ} (hn : n ≤ 0) {x : ℝ≥0∞} (hx : 1 ≤ x) : x ^ n ≤ 1 := by
+  obtain ⟨m, rfl⟩ := neg_surjective n
+  lift m to ℕ using by simpa using hn
+  rw [← ENNReal.inv_zpow', ENNReal.inv_zpow, ENNReal.inv_le_one]
+  exact mod_cast one_le_pow₀ hx
 
 lemma isUnit_iff : IsUnit a ↔ a ≠ 0 ∧ a ≠ ∞ := by
   refine ⟨fun ha ↦ ⟨ha.ne_zero, ?_⟩,
