feat(data/padics): prove Hensel's lemma

algebra/field_power.lean

@@ -6,7 +6,7 @@ Authors: Robert Y. Lewis
 Integer power operation on fields.
 -/
 
-import algebra.group_power tactic.wlog 
+import algebra.group_power tactic.wlog tactic.find
 
 universe u
 
@@ -57,6 +57,14 @@ lemma zero_fpow : ∀ z : ℤ, z ≠ 0 → fpow (0 : α) z = 0
   have h1 : (0 : α) ^ (n+1) = 0, from zero_mul _,
   by simp [fpow, h1]
 
+lemma fpow_neg (a : α) : ∀ n, fpow a (-n) = 1 / fpow a n
+| (of_nat 0) := by simp [of_nat_zero]
+| (of_nat (n+1)) := rfl
+| -[1+n] := show fpow a (n+1) = 1 / (1 / fpow a (n+1)), by rw one_div_one_div
+
+lemma fpow_sub {a : α} (ha : a ≠ 0) (z1 z2 : ℤ) : fpow a (z1 - z2) = fpow a z1 / fpow a z2 :=
+by rw [sub_eq_add_neg, fpow_add ha, fpow_neg, ←div_eq_mul_one_div]
+
 end discrete_field_power
 
 section ordered_field_power
@@ -68,6 +76,9 @@ lemma fpow_nonneg_of_nonneg {a : α} (ha : a ≥ 0) : ∀ (z : ℤ), fpow a z 
 | (of_nat n) := pow_nonneg ha _
 | -[1+n] := div_nonneg' zero_le_one $ pow_nonneg ha _
 
+lemma fpow_pos_of_pos {a : α} (ha : a > 0) : ∀ (z : ℤ), fpow a z > 0
+| (of_nat n) := pow_pos ha _
+| -[1+n] := div_pos zero_lt_one $ pow_pos ha _
 
 lemma fpow_le_of_le {x : α} (hx : 1 ≤ x) {a b : ℤ} (h : a ≤ b) : fpow x a ≤ fpow x b :=
 begin
@@ -101,4 +112,28 @@ begin
   simpa [hfle] using this
 end
 
-end ordered_field_power
+lemma fpow_le_one_of_nonpos {p : α} (hp : p ≥ 1) {z : ℤ} (hz : z ≤ 0) : fpow p z ≤ 1 :=
+calc fpow p z ≤ fpow p 0 : fpow_le_of_le hp hz
+          ... = 1        : by simp
+
+lemma fpow_ge_one_of_nonneg {p : α} (hp : p ≥ 1) {z : ℤ} (hz : z ≥ 0) : fpow p z ≥ 1 :=
+calc fpow p z ≥ fpow p 0 : fpow_le_of_le hp hz
+          ... = 1        : by simp
+
+end ordered_field_power
+
+lemma one_lt_pow {α} [linear_ordered_semiring α] {p : α} (hp : p > 1) : ∀ {n : ℕ}, 1 ≤ n → 1 < p ^ n
+| 1 h := by simp; assumption
+| (k+2) h :=
+  begin
+    rw ←one_mul (1 : α),
+    apply mul_lt_mul,
+    { assumption },
+    { apply le_of_lt, simpa using one_lt_pow (nat.le_add_left 1 k)},
+    { apply zero_lt_one },
+    { apply le_of_lt (lt_trans zero_lt_one hp) }
+  end
+
+lemma one_lt_fpow {α}  [discrete_linear_ordered_field α] {p : α} (hp : p > 1) :
+  ∀ z : ℤ, z > 0 → 1 < fpow p z
+| (int.of_nat n) h := one_lt_pow hp (nat.succ_le_of_lt (int.lt_of_coe_nat_lt_coe_nat h))

algebra/group_power.lean

@@ -440,6 +440,38 @@ calc a ^ n = a ^ n * 1 : by simp
     (pow_nonneg (le_trans zero_le_one ha) _)
   ... = a ^ m : by rw [←hk, pow_add]
 
+lemma pow_le_pow_of_le_left  {a b : α} (ha : 0 ≤ a) (hab : a ≤ b) : ∀ i : ℕ, a^i ≤ b^i
+| 0 := by simp
+| (k+1) := mul_le_mul hab (pow_le_pow_of_le_left _) (pow_nonneg ha _) (le_trans ha hab)
+
+private lemma pow_lt_pow_of_lt_one_aux {a : α} (h : 0 < a) (ha : a < 1) (i : ℕ) :
+  ∀ k : ℕ, a ^ (i + k + 1) < a ^ i
+| 0 := begin simp, rw ←one_mul (a^i), exact mul_lt_mul ha (le_refl _) (pow_pos h _) zero_le_one end
+| (k+1) :=
+  begin
+    rw ←one_mul (a^i),
+    apply mul_lt_mul ha _ _ zero_le_one,
+    { apply le_of_lt, apply pow_lt_pow_of_lt_one_aux },
+    { show 0 < a ^ (i + (k + 1) + 0), apply pow_pos h }
+  end
+
+private lemma pow_le_pow_of_le_one_aux {a : α}  (h : 0 ≤ a) (ha : a ≤ 1) (i : ℕ) :
+  ∀ k : ℕ, a ^ (i + k) ≤ a ^ i
+| 0 := by simp
+| (k+1) := by rw [←add_assoc, ←one_mul (a^i)];
+              exact mul_le_mul ha (pow_le_pow_of_le_one_aux _) (pow_nonneg h _) zero_le_one
+
+lemma pow_lt_pow_of_lt_one  {a : α} (h : 0 < a) (ha : a < 1)
+  {i j : ℕ} (hij : i < j) : a ^ j < a ^ i :=
+let ⟨k, hk⟩ := nat.exists_eq_add_of_lt hij in
+by rw hk; exact pow_lt_pow_of_lt_one_aux h ha _ _
+
+lemma pow_le_pow_of_le_one  {a : α} (h : 0 ≤ a) (ha : a ≤ 1)
+  {i j : ℕ} (hij : i ≤ j) : a ^ j ≤ a ^ i :=
+let ⟨k, hk⟩ := nat.exists_eq_add_of_le hij in
+by rw hk; exact pow_le_pow_of_le_one_aux h ha _ _
+
+
 end linear_ordered_semiring
 
 theorem pow_two_nonneg [linear_ordered_ring α] (a : α) : 0 ≤ a ^ 2 :=
@@ -457,4 +489,10 @@ lemma units_pow_two (u : units ℤ) : u ^ 2 = 1 :=
 lemma units_pow_eq_pow_mod_two (u : units ℤ) (n : ℕ) : u ^ n = u ^ (n % 2) :=
 by conv {to_lhs, rw ← nat.mod_add_div n 2}; simp [pow_add, pow_mul, units_pow_two]
 
-end int
+end int
+
+@[simp] lemma neg_square {α} [ring α] (z : α) : (-z)^2 = z^2 :=
+by simp [pow, monoid.pow]
+
+lemma div_sq_cancel {α} [field α] {a : α} (ha : a ≠ 0) (b : α) : a^2 * b / a = a * b :=
+by rw [pow_two, mul_assoc, mul_div_cancel_left _ ha]

algebra/ordered_ring.lean

@@ -81,6 +81,22 @@ lemma one_lt_mul {a b : α} (ha : 1 ≤ a) (hb : 1 < b) : 1 < a * b :=
 lemma mul_le_one {a b : α} (ha : a ≤ 1) (hb' : 0 ≤ b) (hb : b ≤ 1) : a * b ≤ 1 :=
 begin rw ← one_mul (1 : α), apply mul_le_mul; {assumption <|> apply zero_le_one} end
 
+lemma mul_le_iff_le_one_left {a b : α} (hb : b > 0) : a * b ≤ b ↔ a ≤ 1 :=
+⟨ λ h, le_of_not_lt (mt (lt_mul_iff_one_lt_left hb).2 (not_lt_of_ge h)),
+  λ h, le_of_not_lt (mt (lt_mul_iff_one_lt_left hb).1 (not_lt_of_ge h)) ⟩
+
+lemma mul_lt_iff_lt_one_left {a b : α} (hb : b > 0) : a * b < b ↔ a < 1 :=
+⟨ λ h, lt_of_not_ge (mt (le_mul_iff_one_le_left hb).2 (not_le_of_gt h)),
+  λ h, lt_of_not_ge (mt (le_mul_iff_one_le_left hb).1 (not_le_of_gt h)) ⟩
+
+lemma mul_le_iff_le_one_right {a b : α} (hb : b > 0) : b * a ≤ b ↔ a ≤ 1 :=
+⟨ λ h, le_of_not_lt (mt (lt_mul_iff_one_lt_right hb).2 (not_lt_of_ge h)),
+  λ h, le_of_not_lt (mt (lt_mul_iff_one_lt_right hb).1 (not_lt_of_ge h)) ⟩
+
+lemma mul_lt_iff_lt_one_right {a b : α} (hb : b > 0) : b * a < b ↔ a < 1 :=
+⟨ λ h, lt_of_not_ge (mt (le_mul_iff_one_le_right hb).2 (not_le_of_gt h)),
+  λ h, lt_of_not_ge (mt (le_mul_iff_one_le_right hb).1 (not_le_of_gt h)) ⟩
+
 end linear_ordered_semiring
 
 instance linear_ordered_semiring.to_no_top_order {α : Type*} [linear_ordered_semiring α] :

analysis/limits.lean

@@ -134,6 +134,17 @@ by_cases
         tendsto_inverse_at_top_nhds_0,
     tendsto_cong this $ univ_mem_sets' $ by simp *)
 
+lemma tendsto_coe_iff {f : ℕ → ℕ} : tendsto (λ n, (f n : ℝ)) at_top at_top ↔ tendsto f at_top at_top :=
+⟨ λ h, tendsto_infi.2 $ λ i, tendsto_principal.2
+    (have _, from tendsto_infi.1 h i, by simpa using tendsto_principal.1 this),
+  λ h, tendsto.comp h tendsto_of_nat_at_top_at_top ⟩
+
+lemma tendsto_pow_at_top_at_top_of_gt_1_nat {k : ℕ} (h : k > 1) : tendsto (λn:ℕ, k ^ n) at_top at_top :=
+tendsto_coe_iff.1 $
+  have hr : (k : ℝ) > 1, from show (k : ℝ) > (1 : ℕ), from nat.cast_lt.2 h,
+  by simpa using tendsto_pow_at_top_at_top_of_gt_1 hr
+
+
 lemma sum_geometric' {r : ℝ} (h : r ≠ 0) :
   ∀{n}, (finset.range n).sum (λi, (r + 1) ^ i) = ((r + 1) ^ n - 1) / r
 | 0     := by simp [zero_div]

analysis/normed_space.lean

@@ -182,6 +182,13 @@ instance normed_ring.to_normed_group [β : normed_ring α] : normed_group α :=
 lemma norm_mul {α : Type*} [normed_ring α] (a b : α) : (∥a*b∥) ≤ (∥a∥) * (∥b∥) :=
 normed_ring.norm_mul _ _
 
+lemma norm_pow {α : Type*} [normed_ring α] (a : α) : ∀ {n : ℕ}, n > 0 → ∥a^n∥ ≤ ∥a∥^n
+| 1 h := by simp
+| (n+2) h :=
+  le_trans (norm_mul a (a^(n+1)))
+           (mul_le_mul (le_refl _)
+                       (norm_pow (nat.succ_pos _)) (norm_nonneg _) (norm_nonneg _))
+
 instance prod.normed_ring [normed_ring α] [normed_ring β] : normed_ring (α × β) :=
 { norm_mul := assume x y,
   calc
@@ -195,6 +202,43 @@ instance prod.normed_ring [normed_ring α] [normed_ring β] : normed_ring (α ×
   ..prod.normed_group }
 end normed_ring
 
+instance normed_ring_top_monoid [normed_ring α] : topological_monoid α :=
+⟨ continuous_iff_tendsto.2 $ λ x, tendsto_iff_norm_tendsto_zero.2 $
+    have ∀ e : α × α, e.fst * e.snd - x.fst * x.snd =
+      e.fst * e.snd - e.fst * x.snd + (e.fst * x.snd - x.fst * x.snd), by intro; rw sub_add_sub_cancel,
+    begin
+      apply squeeze_zero,
+      { intro, apply norm_nonneg },
+      { simp only [this], intro, apply norm_triangle },
+      { rw ←zero_add (0 : ℝ), apply tendsto_add,
+        { apply squeeze_zero,
+          { intro, apply norm_nonneg },
+          { intro t, show ∥t.fst * t.snd - t.fst * x.snd∥ ≤ ∥t.fst∥ * ∥t.snd - x.snd∥,
+            rw ←mul_sub, apply norm_mul },
+          { rw ←mul_zero (∥x.fst∥), apply tendsto_mul,
+            { apply continuous_iff_tendsto.1,
+              apply continuous.comp,
+              { apply continuous_fst },
+              { apply continuous_norm }},
+            { apply tendsto_iff_norm_tendsto_zero.1,
+              apply continuous_iff_tendsto.1,
+              apply continuous_snd }}},
+        { apply squeeze_zero,
+          { intro, apply norm_nonneg },
+          { intro t, show ∥t.fst * x.snd - x.fst * x.snd∥ ≤ ∥t.fst - x.fst∥ * ∥x.snd∥,
+            rw ←sub_mul, apply norm_mul },
+          { rw ←zero_mul (∥x.snd∥), apply tendsto_mul,
+            { apply tendsto_iff_norm_tendsto_zero.1,
+              apply continuous_iff_tendsto.1,
+              apply continuous_fst },
+            { apply tendsto_const_nhds }}}}
+    end ⟩
+
+instance normed_top_ring [normed_ring α] : topological_ring α :=
+⟨ continuous_iff_tendsto.2 $ λ x, tendsto_iff_norm_tendsto_zero.2 $
+    have ∀ e : α, -e - -x = -(e - x), by intro; simp,
+    by simp only [this, norm_neg]; apply lim_norm ⟩
+
 section normed_field
 
 class normed_field (α : Type*) extends has_norm α, discrete_field α, metric_space α :=
@@ -204,22 +248,30 @@ class normed_field (α : Type*) extends has_norm α, discrete_field α, metric_s
 instance normed_field.to_normed_ring [i : normed_field α] : normed_ring α :=
 { norm_mul := by finish [i.norm_mul], ..i }
 
-@[simp] lemma norm_one {α : Type*} [normed_field α] : ∥(1 : α)∥ = 1 := 
+@[simp] lemma norm_one {α : Type*} [normed_field α] : ∥(1 : α)∥ = 1 :=
 have  ∥(1 : α)∥ * ∥(1 : α)∥ = ∥(1 : α)∥ * 1, by calc
  ∥(1 : α)∥ * ∥(1 : α)∥ = ∥(1 : α) * (1 : α)∥ : by rw normed_field.norm_mul
                   ... = ∥(1 : α)∥ * 1 : by simp,
 eq_of_mul_eq_mul_left (ne_of_gt ((norm_pos_iff _).2 (by simp))) this
 
-@[simp] lemma norm_div {α : Type*} [normed_field α] (a b : α) : ∥a/b∥ = ∥a∥/∥b∥ := 
-if hb : b = 0 then by simp [hb] else 
-begin 
+@[simp] lemma norm_div {α : Type*} [normed_field α] (a b : α) : ∥a/b∥ = ∥a∥/∥b∥ :=
+if hb : b = 0 then by simp [hb] else
+begin
   apply eq_div_of_mul_eq,
   { apply ne_of_gt, apply (norm_pos_iff _).mpr hb },
   { rw [←normed_field.norm_mul, div_mul_cancel _ hb] }
-end 
+end
+
+@[simp] lemma norm_inv {α : Type*} [normed_field α] (a : α) : ∥a⁻¹∥ = ∥a∥⁻¹ :=
+by simp only [inv_eq_one_div, norm_div, norm_one]
 
-@[simp] lemma norm_inv {α : Type*} [normed_field α] (a : α) : ∥a⁻¹∥ = ∥a∥⁻¹ := 
-by simp only [inv_eq_one_div, norm_div, norm_one] 
+@[simp] lemma normed_field.norm_pow {α : Type*} [normed_field α] (a : α) :
+  ∀ n : ℕ, ∥a^n∥ = ∥a∥^n
+| 0 := by simp
+| (k+1) := calc
+  ∥a ^ (k + 1)∥ = ∥a*(a^k)∥ : rfl
+           ... = ∥a∥*∥a^k∥ : by rw normed_field.norm_mul
+           ... = ∥a∥ ^ (k + 1) : by rw normed_field.norm_pow; simp [pow, monoid.pow]
 
 instance : normed_field ℝ :=
 { norm := λ x, abs x,

analysis/topology/topological_structures.lean

@@ -42,6 +42,10 @@ lemma continuous_mul [topological_space β] {f : β → α} {g : β → α}
   continuous (λx, f x * g x) :=
 (hf.prod_mk hg).comp continuous_mul'
 
+lemma continuous_pow : ∀ n : ℕ, continuous (λ a : α, a ^ n)
+| 0 := by simpa using continuous_const
+| (k+1) := show continuous (λ (a : α), a * a ^ k), from continuous_mul continuous_id (continuous_pow _)
+
 lemma tendsto_mul' {a b : α} : tendsto (λp:α×α, p.fst * p.snd) (nhds (a, b)) (nhds (a * b)) :=
 continuous_iff_tendsto.mp (topological_monoid.continuous_mul α) (a, b)
 

data/finsupp.lean

@@ -391,6 +391,11 @@ finset.sum_add_distrib
   {h : α → β → γ} : f.sum (λa b, - h a b) = - f.sum h :=
 finset.sum_hom (@has_neg.neg γ _) neg_zero (assume a b, neg_add _ _)
 
+@[simp] lemma sum_sub [add_comm_monoid β] [add_comm_group γ] {f : α →₀ β}
+  {h₁ h₂ : α → β → γ} :
+  f.sum (λa b, h₁ a b - h₂ a b) = f.sum h₁ - f.sum h₂ :=
+by rw [sub_eq_add_neg, ←sum_neg, ←sum_add]; refl
+
 @[simp] lemma sum_single [add_comm_monoid β] {f : α →₀ β} :
   f.sum single = f :=
 have ∀a:α, f.sum (λa' b, ite (a' = a) b 0) =

data/int/modeq.lean

@@ -98,6 +98,29 @@ lemma gcd_a_modeq (a b : ℕ) : (a : ℤ) * nat.gcd_a a b ≡ nat.gcd a b [ZMOD
 by rw [← add_zero ((a : ℤ) * _), nat.gcd_eq_gcd_ab];
   exact int.modeq.modeq_add rfl (int.modeq.modeq_zero_iff.2 (dvd_mul_right _ _)).symm
 
+theorem modeq_add_fac {a b n : ℤ} (c : ℤ) (ha : a ≡ b [ZMOD n]) : a + n*c ≡ b [ZMOD n] :=
+calc a + n*c ≡ b + n*c [ZMOD n] : int.modeq.modeq_add ha (int.modeq.refl _)
+         ... ≡ b + 0 [ZMOD n] : int.modeq.modeq_add (int.modeq.refl _) (int.modeq.modeq_zero_iff.2 (dvd_mul_right _ _))
+         ... ≡ b [ZMOD n] : by simp
+
+open nat
+lemma mod_coprime {a b : ℕ} (hab : coprime a b) : ∃ y : ℤ, a * y ≡ 1 [ZMOD b] :=
+⟨ gcd_a a b,
+  have hgcd : nat.gcd a b = 1, from coprime.gcd_eq_one hab,
+  calc
+   ↑a * gcd_a a b ≡ ↑a*gcd_a a b + ↑b*gcd_b a b [ZMOD ↑b] : int.modeq.symm $ modeq_add_fac _ $ int.modeq.refl _
+              ... ≡ 1 [ZMOD ↑b] : by rw [←gcd_eq_gcd_ab, hgcd]; reflexivity ⟩
+
+lemma exists_unique_equiv (a : ℤ) {b : ℤ} (hb : b > 0) : ∃ z : ℤ, 0 ≤ z ∧ z < b ∧ z ≡ a [ZMOD b] :=
+⟨ a % b, int.mod_nonneg _ (ne_of_gt hb),
+  have a % b < abs b, from int.mod_lt _ (ne_of_gt hb),
+  by rwa abs_of_pos hb at this,
+  by simp [int.modeq] ⟩
+
+lemma exists_unique_equiv_nat (a : ℤ) {b : ℤ} (hb : b > 0) : ∃ z : ℕ, ↑z < b ∧ ↑z ≡ a [ZMOD b] :=
+let ⟨z, hz1, hz2, hz3⟩ := exists_unique_equiv a hb in
+⟨z.nat_abs, by split; rw [←int.of_nat_eq_coe, int.of_nat_nat_abs_eq_of_nonneg hz1]; assumption⟩
+
 end modeq
 
 @[simp] lemma mod_mul_right_mod (a b c : ℤ) : a % (b * c) % b = a % b :=

data/nat/basic.lean

@@ -729,9 +729,20 @@ lemma pow_dvd_of_le_of_pow_dvd {p m n k : ℕ} (hmn : m ≤ n) (hdiv : p ^ n ∣
 have p ^ m ∣ p ^ n, from pow_dvd_pow _ hmn,
 dvd_trans this hdiv
 
-lemma dvd_of_pow_dvd {p k m : ℕ} (hk : 1 ≤ k) (hpk : p^k ∣ m) : p ∣ m := 
+lemma dvd_of_pow_dvd {p k m : ℕ} (hk : 1 ≤ k) (hpk : p^k ∣ m) : p ∣ m :=
 by rw ←nat.pow_one p; exact pow_dvd_of_le_of_pow_dvd hk hpk
 
 end div
 
+lemma exists_eq_add_of_le : ∀ {m n : ℕ}, m ≤ n → ∃ k : ℕ, n = m + k
+| 0 0 h := ⟨0, by simp⟩
+| 0 (n+1) h := ⟨n+1, by simp⟩
+| (m+1) (n+1) h := let ⟨k, hk⟩ := exists_eq_add_of_le (nat.le_of_succ_le_succ h) in ⟨k, by simp [hk]⟩
+
+lemma exists_eq_add_of_lt : ∀ {m n : ℕ}, m < n → ∃ k : ℕ, n = m + k + 1
+| 0 0 h := false.elim $ lt_irrefl _ h
+| 0 (n+1) h := ⟨n, by simp⟩
+| (m+1) (n+1) h := let ⟨k, hk⟩ := exists_eq_add_of_le (nat.le_of_succ_le_succ h) in ⟨k, by simp [hk]⟩
+
+
 end nat

data/padics/default.lean

@@ -0,0 +1 @@
+import data.padics.padic_integers