Cleanup nnreal.pow_enat

src/examples/char_p.lean

@@ -13,119 +13,17 @@ open function
 
 local postfix `ᵒ` : 66 := power_bounded_subring
 
-section
-
-def nnreal_of_enat (b : nnreal) (n : enat) : nnreal :=
-if h : n.dom then (b^n.get h) else 0
-
-@[simp] lemma nnreal_of_enat_top (b : nnreal) :
-  nnreal_of_enat b ⊤ = 0 :=
-begin
-  rw [nnreal_of_enat, dif_neg], exact not_false
-end
-
-@[simp] lemma nnreal_of_enat_zero (b : nnreal) :
-  nnreal_of_enat b 0 = 1 :=
-begin
-  rw [nnreal_of_enat, dif_pos, enat.get_zero, pow_zero],
-  exact trivial,
-end
-
-@[simp] lemma nnreal_of_enat_one (b : nnreal) :
-  nnreal_of_enat b 1 = b :=
-begin
-  rw [nnreal_of_enat, dif_pos, enat.get_one, pow_one],
-  exact trivial,
-end
-
-@[simp] lemma nnreal_of_enat_add (b : nnreal) (m n : enat) :
-  nnreal_of_enat b (m + n) = nnreal_of_enat b m * nnreal_of_enat b n :=
-begin
-  delta nnreal_of_enat,
-  by_cases hm : m.dom,
-  { by_cases hn : n.dom,
-    { have hmn : (m + n).dom := ⟨hm, hn⟩,
-      rw [dif_pos hm, dif_pos hn, dif_pos,
-          subtype.coe_ext, nnreal.coe_mul, ← nnreal.coe_mul, ← pow_add, enat.get_add, add_comm],
-      exact hmn, },
-    { rw [dif_pos hm, dif_neg hn, dif_neg, mul_zero],
-      contrapose! hn with H, exact H.2 } },
-  { rw [dif_neg hm, dif_neg, zero_mul],
-    contrapose! hm with H, exact H.1 },
-end
-
-@[simp] lemma nnreal_of_enat_le (b : nnreal) (h₁ : b ≠ 0) (h₂ : b ≤ 1) (m n : enat) (h : m ≤ n) :
-  nnreal_of_enat b n ≤ nnreal_of_enat b m :=
-begin
-  delta nnreal_of_enat,
-  by_cases hn : n.dom,
-  { rw ← enat.coe_get hn at h,
-    have hm : m.dom := enat.dom_of_le_some h,
-    rw [← enat.coe_get hm, enat.coe_le_coe] at h,
-    rw [dif_pos hm, dif_pos hn],
-    rw [← linear_ordered_structure.inv_le_inv _ h₁, inv_one'] at h₂,
-    have := pow_le_pow h₂ h,
-    -- We need lots of norm_cast lemmas
-    rwa [nnreal.coe_le, nnreal.coe_pow, nnreal.coe_pow, nnreal.coe_inv, ← pow_inv, ← pow_inv,
-      ← nnreal.coe_pow, ← nnreal.coe_pow, ← nnreal.coe_inv, ← nnreal.coe_inv, ← nnreal.coe_le,
-      linear_ordered_structure.inv_le_inv] at this,
-    any_goals { exact one_ne_zero },
-    all_goals { contrapose! h₁ },
-    any_goals { exact subtype.val_injective h₁ },
-    any_goals { apply group_with_zero.pow_eq_zero, assumption } },
-  { rw dif_neg hn, exact zero_le _ }
-end
-
-@[simp] lemma nnreal_of_enat_lt (b : nnreal) (h₁ : b ≠ 0) (h₂ : b < 1) (m n : enat) (h : m < n) :
-  nnreal_of_enat b n < nnreal_of_enat b m :=
-begin
-  delta nnreal_of_enat,
-  by_cases hn : n.dom,
-  { rw ← enat.coe_get hn at h,
-    have hm : m.dom := enat.dom_of_le_some (le_of_lt h),
-    rw [← enat.coe_get hm, enat.coe_lt_coe] at h,
-    rw [dif_pos hm, dif_pos hn],
-    rw [← linear_ordered_structure.inv_lt_inv _ h₁, inv_one'] at h₂,
-    have := pow_lt_pow h₂ h,
-    -- We need lots of norm_cast lemmas
-    rwa [nnreal.coe_lt, nnreal.coe_pow, nnreal.coe_pow, nnreal.coe_inv, ← pow_inv, ← pow_inv,
-      ← nnreal.coe_pow, ← nnreal.coe_pow, ← nnreal.coe_inv, ← nnreal.coe_inv, ← nnreal.coe_lt,
-      linear_ordered_structure.inv_lt_inv] at this,
-    any_goals { exact one_ne_zero },
-    all_goals { contrapose! h₁ },
-    any_goals { exact subtype.val_injective h₁ },
-    all_goals { apply group_with_zero.pow_eq_zero, assumption } },
-  { rw dif_neg hn,
-    have : n = ⊤ := roption.eq_none_iff'.mpr hn, subst this,
-    replace h := ne_of_lt h,
-    rw enat.ne_top_iff at h, rcases h with ⟨m, rfl⟩,
-    rw dif_pos, swap, {trivial},
-    apply pow_pos,
-    exact lt_of_le_of_ne b.2 h₁.symm }
-end
-
-@[simp] lemma nnreal_of_enat_inj (b : nnreal) (h₁ : b ≠ 0) (h₂ : b < 1) :
-  injective (nnreal_of_enat b) :=
-begin
-  intros m n h,
-  wlog H : m ≤ n,
-  rcases lt_or_eq_of_le H with H|rfl,
-  { have := nnreal_of_enat_lt b h₁ h₂ m n H,
-    exfalso, exact ne_of_lt this h.symm, },
-  { refl },
-end
-
-end
+local attribute [instance] nnreal.pow_enat
 
 namespace power_series
 variables (p : nat.primes)
 variables (K : Type*) [discrete_field K] [char_p K p]
 
 def valuation : valuation (power_series K) nnreal :=
-{ to_fun := λ φ, nnreal_of_enat (p⁻¹) φ.order,
-  map_zero' := by rw [order_zero, nnreal_of_enat_top],
-  map_one' := by rw [order_one, nnreal_of_enat_zero],
-  map_mul' := λ x y, by rw [order_mul, nnreal_of_enat_add],
+{ to_fun := λ φ, (p⁻¹) ^ φ.order,
+  map_zero' := by rw [order_zero, nnreal.pow_enat_top],
+  map_one' := by rw [order_one, nnreal.pow_enat_zero],
+  map_mul' := λ x y, by rw [order_mul, nnreal.pow_enat_add],
   map_add' := λ x y,
   begin
     have : _ ≤ _ := order_add_ge x y,
@@ -137,7 +35,7 @@ def valuation : valuation (power_series K) nnreal :=
       rw [show (p : nnreal) = (p : ℕ), by rw coe_coe] at H, exact_mod_cast H, },
     cases this with h h; [left, right],
     all_goals
-    { apply nnreal_of_enat_le _ inv_p_ne_zero _ _ _ h,
+    { apply nnreal.pow_enat_le _ inv_p_ne_zero _ _ _ h,
       rw [← linear_ordered_structure.inv_le_inv _ inv_p_ne_zero, inv_inv'', inv_one'],
       { apply le_of_lt,
         rw [show (p : nnreal) = (p : ℕ), by rw coe_coe],
@@ -169,13 +67,13 @@ valuation.localization (power_series.valuation p K) $ λ φ h,
 begin
   rw localization.fraction_ring.mem_non_zero_divisors_iff_ne_zero at h,
   contrapose! h,
-  change nnreal_of_enat _ _ = 0 at h,
+  change (_ : nnreal) ^ φ.order = 0 at h,
   have inv_p_ne_zero : (p : nnreal)⁻¹ ≠ 0,
   { assume H, rw [← inv_inj'', inv_inv'', inv_zero'] at H,
     apply p.ne_zero,
     rw [show (p : nnreal) = (p : ℕ), by rw coe_coe] at H,
     exact_mod_cast H },
-  rwa [← nnreal_of_enat_top, (nnreal_of_enat_inj _ inv_p_ne_zero _).eq_iff,
+  rwa [← nnreal.pow_enat_top, (nnreal.pow_enat_inj _ inv_p_ne_zero _).eq_iff,
       power_series.order_eq_top] at h,
   rw [← linear_ordered_structure.inv_lt_inv _ inv_p_ne_zero, inv_inv'', inv_one'],
   { rw [show (p : nnreal) = (p : ℕ), by rw coe_coe],
@@ -186,12 +84,12 @@ end
 lemma non_trivial : ¬ (valuation p K).is_trivial :=
 begin
   assume H, cases H (localization.of (power_series.X)) with h h;
-  erw valuation.localization_apply at h; change nnreal_of_enat _ _ = _ at h,
+  erw valuation.localization_apply at h; change _ ^ _ = _ at h,
   { apply p.ne_zero,
     rw [show (p : nnreal) = (p : ℕ), by rw coe_coe] at h,
-    simpa only [nnreal.inv_eq_zero, nnreal_of_enat_one,
+    simpa only [nnreal.inv_eq_zero, nnreal.pow_enat_one,
       nat.cast_eq_zero, power_series.order_X] using h, },
-  { simp only [nnreal_of_enat_one, power_series.order_X] at h,
+  { simp only [nnreal.pow_enat_one, power_series.order_X] at h,
     rw [← inv_inj'', inv_inv'', inv_one'] at h,
     apply p.ne_one,
     rw [show (p : nnreal) = (p : ℕ), by rw coe_coe] at h,

src/for_mathlib/nnreal.lean

@@ -47,4 +47,119 @@ noncomputable instance : linear_ordered_comm_group_with_zero nnreal :=
   .. (infer_instance : linear_order nnreal),
   .. (infer_instance : comm_semiring nnreal) }
 
+section pow_enat
+noncomputable theory
+open_locale classical
+open function
+
+/--If r is a nonnegative real number and n an enat,
+than b^n is defined as expected if n is natural, and b^infty = 0.
+Hence, this should only be applied to b < 1.-/
+def pow_enat : has_pow nnreal enat :=
+⟨λ r n, if h : n.dom then (r^n.get h) else 0⟩
+
+local attribute [instance] pow_enat
+
+lemma pow_enat_def {b : nnreal} {n : enat} :
+  b^n = if h : n.dom then (b^n.get h) else 0 := rfl
+
+@[simp] lemma pow_enat_top (b : nnreal) :
+  b ^ (⊤ : enat) = 0 :=
+begin
+  rw [pow_enat_def, dif_neg], exact not_false
+end
+
+@[simp] lemma pow_enat_zero (b : nnreal) :
+  b ^ (0 : enat) = 1 :=
+begin
+  rw [pow_enat_def, dif_pos, enat.get_zero, pow_zero],
+  exact trivial,
+end
+
+@[simp] lemma pow_enat_one (b : nnreal) :
+  b ^ (1 : enat) = b :=
+begin
+  rw [pow_enat_def, dif_pos, enat.get_one, pow_one],
+  exact trivial,
+end
+
+@[simp] lemma pow_enat_add (b : nnreal) (m n : enat) :
+  b ^ (m + n) = b ^ m * b ^ n :=
+begin
+  iterate 3 {rw pow_enat_def},
+  by_cases hm : m.dom,
+  { by_cases hn : n.dom,
+    { have hmn : (m + n).dom := ⟨hm, hn⟩,
+      rw [dif_pos hm, dif_pos hn, dif_pos,
+          subtype.coe_ext, nnreal.coe_mul, ← nnreal.coe_mul, ← pow_add, enat.get_add, add_comm],
+      exact hmn, },
+    { rw [dif_pos hm, dif_neg hn, dif_neg, mul_zero],
+      contrapose! hn with H, exact H.2 } },
+  { rw [dif_neg hm, dif_neg, zero_mul],
+    contrapose! hm with H, exact H.1 },
+end
+
+@[simp] lemma pow_enat_le (b : nnreal) (h₁ : b ≠ 0) (h₂ : b ≤ 1) (m n : enat) (h : m ≤ n) :
+  b ^ n ≤ b ^ m :=
+begin
+  iterate 2 {rw pow_enat_def},
+  by_cases hn : n.dom,
+  { rw ← enat.coe_get hn at h,
+    have hm : m.dom := enat.dom_of_le_some h,
+    rw [← enat.coe_get hm, enat.coe_le_coe] at h,
+    rw [dif_pos hm, dif_pos hn],
+    rw [← linear_ordered_structure.inv_le_inv _ h₁, inv_one'] at h₂,
+    have := pow_le_pow h₂ h,
+    -- We need lots of norm_cast lemmas
+    rwa [nnreal.coe_le, nnreal.coe_pow, nnreal.coe_pow, nnreal.coe_inv, ← pow_inv, ← pow_inv,
+      ← nnreal.coe_pow, ← nnreal.coe_pow, ← nnreal.coe_inv, ← nnreal.coe_inv, ← nnreal.coe_le,
+      linear_ordered_structure.inv_le_inv] at this,
+    any_goals { exact one_ne_zero },
+    all_goals { contrapose! h₁ },
+    any_goals { exact subtype.val_injective h₁ },
+    any_goals { apply group_with_zero.pow_eq_zero, assumption } },
+  { rw dif_neg hn, exact zero_le _ }
+end
+
+@[simp] lemma pow_enat_lt (b : nnreal) (h₁ : b ≠ 0) (h₂ : b < 1) (m n : enat) (h : m < n) :
+  b ^ n < b ^ m :=
+begin
+  iterate 2 {rw pow_enat_def},
+  by_cases hn : n.dom,
+  { rw ← enat.coe_get hn at h,
+    have hm : m.dom := enat.dom_of_le_some (le_of_lt h),
+    rw [← enat.coe_get hm, enat.coe_lt_coe] at h,
+    rw [dif_pos hm, dif_pos hn],
+    rw [← linear_ordered_structure.inv_lt_inv _ h₁, inv_one'] at h₂,
+    have := pow_lt_pow h₂ h,
+    -- We need lots of norm_cast lemmas
+    rwa [nnreal.coe_lt, nnreal.coe_pow, nnreal.coe_pow, nnreal.coe_inv, ← pow_inv, ← pow_inv,
+      ← nnreal.coe_pow, ← nnreal.coe_pow, ← nnreal.coe_inv, ← nnreal.coe_inv, ← nnreal.coe_lt,
+      linear_ordered_structure.inv_lt_inv] at this,
+    any_goals { exact one_ne_zero },
+    all_goals { contrapose! h₁ },
+    any_goals { exact subtype.val_injective h₁ },
+    all_goals { apply group_with_zero.pow_eq_zero, assumption } },
+  { rw dif_neg hn,
+    have : n = ⊤ := roption.eq_none_iff'.mpr hn, subst this,
+    replace h := ne_of_lt h,
+    rw enat.ne_top_iff at h, rcases h with ⟨m, rfl⟩,
+    rw dif_pos, swap, {trivial},
+    apply pow_pos,
+    exact lt_of_le_of_ne b.2 h₁.symm }
+end
+
+@[simp] lemma pow_enat_inj (b : nnreal) (h₁ : b ≠ 0) (h₂ : b < 1) :
+  injective ((^) b : enat → nnreal) :=
+begin
+  intros m n h,
+  wlog H : m ≤ n,
+  rcases lt_or_eq_of_le H with H|rfl,
+  { have := pow_enat_lt b h₁ h₂ m n H,
+    exfalso, exact ne_of_lt this h.symm, },
+  { refl },
+end
+
+end pow_enat
+
 end nnreal