# Hensel's lemma over the p-adic integers #337

Closed
wants to merge 29 commits into from
Closed

# Hensel's lemma over the p-adic integers#337

Commits
Show all changes
29 commits
Select commit Hold shift + click to select a range
Filter file types
Failed to load files and symbols.
+2,334 −713

#### Just for now

 @@ -104,7 +104,9 @@ lemma ceil_pos {a : α} : 0 < ⌈a⌉ ↔ 0 < a := λ h, have -a < 0, from neg_neg_of_pos h, neg_pos_of_neg \$ lt_of_not_ge \$ (not_iff_not_of_iff floor_nonneg).2 \$ not_le_of_gt this ⟩ lemma ceil_nonneg {q : ℚ} (hq : q ≥ 0) : ⌈q⌉ ≥ 0 := @[simp] theorem ceil_zero : ⌈(0 : α)⌉ = 0 := by simp [ceil] lemma ceil_nonneg [decidable_rel ((<) : α → α → Prop)] {q : α} (hq : q ≥ 0) : ⌈q⌉ ≥ 0 := if h : q > 0 then le_of_lt \$ ceil_pos.2 h else have h' : q = 0, from le_antisymm (le_of_not_lt h) hq, @@ -233,6 +235,18 @@ begin ← div_lt_iff' (sub_pos.2 h), one_div_eq_inv] end theorem exists_nat_one_div_lt {ε : α} (hε : ε > 0) : ∃ n : ℕ, 1 / (n + 1: α) < ε := begin cases archimedean_iff_nat_lt.1 (by apply_instance) (1/ε) with n hn, existsi n, apply div_lt_of_mul_lt_of_pos, { simp, apply add_pos_of_pos_of_nonneg zero_lt_one, apply nat.cast_nonneg }, { apply (div_lt_iff' hε).1, transitivity, { exact hn }, { simp [zero_lt_one] }} end include α @[simp] theorem rat.cast_floor (x : ℚ) : by haveI := archimedean.floor_ring α; exact ⌊(x:α)⌋ = ⌊x⌋ :=
 @@ -37,7 +37,6 @@ lemma fpow_ne_zero_of_ne_zero {a : α} (ha : a ≠ 0) : ∀ (z : ℤ), fpow a z | (of_nat n) := pow_ne_zero _ ha | -[1+n] := one_div_ne_zero \$ pow_ne_zero _ ha @[simp] lemma fpow_zero {a : α} : fpow a 0 = 1 := pow_zero _ @@ -58,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 @@ -69,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 @@ -102,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))
 @@ -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]
 @@ -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 α] :
 @@ -134,6 +134,22 @@ 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 tendsto_inverse_at_top_nhds_0_nat : tendsto (λ n : ℕ, (n : ℝ)⁻¹) at_top (nhds 0) := tendsto.comp (tendsto_coe_iff.2 tendsto_id) tendsto_inverse_at_top_nhds_0 lemma tendsto_one_div_at_top_nhds_0_nat : tendsto (λ n : ℕ, 1/(n : ℝ)) at_top (nhds 0) := by simpa only [inv_eq_one_div] using tendsto_inverse_at_top_nhds_0_nat 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]
@@ -84,6 +84,9 @@ abs_le.2 \$ and.intro
lemma dist_norm_norm_le (g h : α) : dist ∥g∥ ∥h∥ ∥g - h∥ :=
abs_norm_sub_norm_le g h

lemma norm_sub_rev (g h : α) : ∥g - h∥ = ∥h - g∥ :=
by rw ←norm_neg; simp

section nnnorm

def nnnorm (a : α) : nnreal := ⟨norm a, norm_nonneg a⟩
@@ -179,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
@@ -192,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 \$
This conversation was marked as resolved by johoelzl
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 },
{ 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 α :=
@@ -201,6 +248,31 @@ 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 :=
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
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

@[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,
dist_eq := assume x y, rfl,
 @@ -0,0 +1,27 @@ /- Copyright (c) 2018 Robert Y. Lewis. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Author: Robert Y. Lewis Analytic facts about polynomials. -/ import analysis.topology.topological_structures data.polynomial lemma polynomial.continuous_eval {α} [comm_semiring α] [decidable_eq α] [topological_space α] [topological_semiring α] (p : polynomial α) : continuous (λ x, p.eval x) := begin apply p.induction, { convert continuous_const, ext, show polynomial.eval x 0 = 0, from rfl }, { intros a b f haf hb hcts, simp only [polynomial.eval_add], refine continuous_add _ hcts, have : ∀ x, finsupp.sum (finsupp.single a b) (λ (e : ℕ) (a : α), a * x ^ e) = b * x ^a, from λ x, finsupp.sum_single_index (by simp), convert continuous_mul _ _, { ext, apply this }, { apply_instance }, { apply continuous_const }, { apply continuous_pow }} end
 @@ -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)
 @@ -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) =
 @@ -582,22 +582,25 @@ lemma dvd_nat_abs_of_of_nat_dvd {a : ℕ} : ∀ {z : ℤ} (haz : ↑a ∣ z), a have haz' : (↑a:ℤ) ∣ (↑(k+1):ℤ), from dvd_of_dvd_neg haz, int.coe_nat_dvd.1 haz' lemma pow_div_of_le_of_pow_div_int {p m n : ℕ} {k : ℤ} (hmn : m ≤ n) (hdiv : ↑(p ^ n) ∣ k) : lemma pow_dvd_of_le_of_pow_dvd {p m n : ℕ} {k : ℤ} (hmn : m ≤ n) (hdiv : ↑(p ^ n) ∣ k) : ↑(p ^ m) ∣ k := begin induction k, { apply int.coe_nat_dvd.2, apply pow_div_of_le_of_pow_div hmn, apply pow_dvd_of_le_of_pow_dvd hmn, apply int.coe_nat_dvd.1 hdiv }, { change -[1+k] with -(↑(k+1) : ℤ), apply dvd_neg_of_dvd, apply int.coe_nat_dvd.2, apply pow_div_of_le_of_pow_div hmn, apply pow_dvd_of_le_of_pow_dvd hmn, apply int.coe_nat_dvd.1, apply dvd_of_dvd_neg, exact hdiv } end 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 /- / and ordering -/ protected theorem div_mul_le (a : ℤ) {b : ℤ} (H : b ≠ 0) : a / b * b ≤ a :=
ProTip! Use n and p to navigate between commits in a pull request.
You can’t perform that action at this time.