feat(analysis/special_functions/pow): Equivalent conditions for zero …

…powers (#9897)

Lemmas for 0^x in the reals and complex numbers.

src/analysis/special_functions/pow.lean

@@ -58,6 +58,22 @@ by { simp only [cpow_def], split_ifs; simp [*, exp_ne_zero] }
 @[simp] lemma zero_cpow {x : ℂ} (h : x ≠ 0) : (0 : ℂ) ^ x = 0 :=
 by simp [cpow_def, *]
 
+lemma zero_cpow_eq_iff {x : ℂ} {a : ℂ} : 0 ^ x = a ↔ (x ≠ 0 ∧ a = 0) ∨ (x = 0 ∧ a = 1) :=
+begin
+  split,
+  { intros hyp,
+    simp [cpow_def] at hyp,
+    by_cases x = 0,
+    { subst h, simp only [if_true, eq_self_iff_true] at hyp, right, exact ⟨rfl, hyp.symm⟩},
+    { rw if_neg h at hyp, left, exact ⟨h, hyp.symm⟩, }, },
+  { rintro (⟨h, rfl⟩|⟨rfl,rfl⟩),
+    { exact zero_cpow h, },
+    { exact cpow_zero _, }, },
+end
+
+lemma eq_zero_cpow_iff {x : ℂ} {a : ℂ} : a = 0 ^ x ↔ (x ≠ 0 ∧ a = 0) ∨ (x = 0 ∧ a = 1) :=
+by rw [←zero_cpow_eq_iff, eq_comm]
+
 @[simp] lemma cpow_one (x : ℂ) : x ^ (1 : ℂ) = x :=
 if hx : x = 0 then by simp [hx, cpow_def]
 else by rw [cpow_def, if_neg (one_ne_zero : (1 : ℂ) ≠ 0), if_neg hx, mul_one, exp_log hx]
@@ -405,6 +421,25 @@ by rw rpow_def_of_pos hx; apply exp_pos
 @[simp] lemma zero_rpow {x : ℝ} (h : x ≠ 0) : (0 : ℝ) ^ x = 0 :=
 by simp [rpow_def, *]
 
+lemma zero_rpow_eq_iff {x : ℝ} {a : ℝ} : 0 ^ x = a ↔ (x ≠ 0 ∧ a = 0) ∨ (x = 0 ∧ a = 1) :=
+begin
+  split,
+  { intros hyp,
+    simp [rpow_def] at hyp,
+    by_cases x = 0,
+    { subst h,
+      simp only [complex.one_re, complex.of_real_zero, complex.cpow_zero] at hyp,
+      exact or.inr ⟨rfl, hyp.symm⟩},
+    { rw complex.zero_cpow (complex.of_real_ne_zero.mpr h) at hyp,
+      exact or.inl ⟨h, hyp.symm⟩, }, },
+  { rintro (⟨h,rfl⟩|⟨rfl,rfl⟩),
+    { exact zero_rpow h, },
+    { exact rpow_zero _, }, },
+end
+
+lemma eq_zero_rpow_iff {x : ℝ} {a : ℝ} : a = 0 ^ x ↔ (x ≠ 0 ∧ a = 0) ∨ (x = 0 ∧ a = 1) :=
+by rw [←zero_rpow_eq_iff, eq_comm]
+
 @[simp] lemma rpow_one (x : ℝ) : x ^ (1 : ℝ) = x := by simp [rpow_def]
 
 @[simp] lemma one_rpow (x : ℝ) : (1 : ℝ) ^ x = 1 := by simp [rpow_def]