Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

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

Closed
wants to merge 29 commits into from
Closed
Changes from 1 commit
Commits
Show all changes
29 commits
Select commit Hold shift + click to select a range
4f85f91
feat(data/padics): use has_norm typeclasses for padics
robertylewis Sep 6, 2018
d9f1be1
style(data/padic/padic_integers): remove comment, long line
robertylewis Sep 6, 2018
ba27d2f
feat(data/padics): more scattered lemmas, integers are complete
robertylewis Sep 6, 2018
29f723f
feat(algebra): various helper lemmas, mostly about powers
robertylewis Sep 11, 2018
7587fe2
feat(data/real,analysis/limits): some properties about limits of sequ…
robertylewis Sep 11, 2018
73a0f0d
feat(data/finsupp,data/polynomial): facts about polynomials
robertylewis Sep 11, 2018
237c23f
feat(data/nat): helper lemmas
robertylewis Sep 11, 2018
1b8a2d9
feat(analysis/normed_space,analysis/topology/topological_structures):…
robertylewis Sep 11, 2018
cfad546
feat(data/padics): prove Hensel's lemma
robertylewis Sep 11, 2018
89fa0b7
fix(analysis/normed_space,data/padics): fix mistake in merge; remove …
robertylewis Sep 11, 2018
8e7399d
fix(data/padics/hensel,data/real/cau_seq_filter): missing docstrings
robertylewis Sep 11, 2018
124120f
feat(docs/theories): document padics development
robertylewis Sep 12, 2018
8184c0e
style(data/padics/hensel): polynomials and prime numbers have differe…
robertylewis Sep 12, 2018
a47b547
feat(data/padics): address review comments
robertylewis Sep 17, 2018
82084f6
style(data/polynomial): variable name and comment
robertylewis Sep 17, 2018
713f3c6
feat(data/padics): style, minor refactor
robertylewis Sep 24, 2018
625f76e
feat(data/padics/padic_norm): add division lemma
robertylewis Sep 24, 2018
c199015
feat(data/padics/padic_norm): extra lemmas about padic val and norm
robertylewis Sep 27, 2018
b72cc01
feat(data/real/cau_seq): relate cauchy sequence completeness and filt…
robertylewis Sep 28, 2018
336b6c4
style(analysis/limits,data/real/cau_seq_filter): cleanup
robertylewis Sep 29, 2018
db2c395
remove tactic.find
johoelzl Oct 1, 2018
f37821c
Merge branch 'master' into padic
johoelzl Oct 1, 2018
4719d34
feat(data/padics): use prime typeclass
robertylewis Oct 1, 2018
54cbd88
feat(data/real,data/padics): cauchy_complete typeclass
robertylewis Oct 1, 2018
020924c
fix(data/real,data/padics): remove dead code
robertylewis Oct 1, 2018
7bf76f2
style(data/padics): anonymous instances
robertylewis Oct 2, 2018
01f18f6
fix(data/real,data/padics): fix merge
robertylewis Oct 2, 2018
7a1398e
refactor(data/polynomial): remove analysis import
robertylewis Oct 2, 2018
9c168db
style(analysis/polynomial): unnecessary dsimp
robertylewis Oct 2, 2018
File filter...
Filter file types
Jump to…
Jump to file or symbol
Failed to load files and symbols.
+37 −1
Diff settings

Always

Just for now

feat(data/finsupp,data/polynomial): facts about polynomials

  • Loading branch information...
robertylewis committed Sep 11, 2018
commit 73a0f0d2016d67611497fd75028b163533c2a3e8
Copy path View file
@@ -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) =
@@ -412,6 +417,11 @@ begin
end,
ext $ assume a, by simp [single_apply, this]

lemma sum_single' [add_comm_monoid γ] [has_zero β] {a b} (g : α β γ) (hg : g a 0 = 0) :

This comment has been minimized.

Copy link
@johoelzl

johoelzl Sep 17, 2018

Collaborator

this is sum_single_index

(finsupp.single a b).sum g = g a b :=
if h : b = 0 then by simp [finsupp.sum, h, hg]
else by simp [finsupp.sum, finsupp.support_single_ne_zero h]

@[to_additive finsupp.sum_add_index]
lemma prod_add_index [add_comm_monoid β] [comm_monoid γ] {f g : α ₀ β}
{h : α β γ} (h_zero : a, h a 0 = 1) (h_add : a b₁ b₂, h a (b₁ + b₂) = h a b₁ * h a b₂) :
Copy path View file
@@ -5,7 +5,7 @@ Authors: Chris Hughes, Johannes Hölzl, Jens Wagemaker
Theory of univariate polynomials, represented as `ℕ →₀ α`, where α is a commutative semiring.
-/
import data.finsupp algebra.euclidean_domain
import data.finsupp algebra.euclidean_domain analysis.topology.topological_structures

/-- `polynomial α` is the type of univariate polynomials over `α`.
@@ -212,6 +212,29 @@ lemma root_mul_right_of_is_root {p : polynomial α} (q : polynomial α) :
is_root p a is_root (p * q) a :=
by simp [is_root.def, eval_mul] {contextual := tt}

lemma eval_sum (p : polynomial α) (f : ℕ α polynomial α) (x : α) :
(p.sum f).eval x = p.sum (λ n a, (f n a).eval x) :=
finsupp.sum_sum_index (by simp) (by intros; simp [right_distrib])

lemma continuous_eval [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,
dsimp [polynomial.eval, polynomial.eval₂],
have : x, finsupp.sum (finsupp.single a b) (λ (e : ℕ) (a : α), a * x ^ e) = b * x ^a,
from λ x, finsupp.sum_single' _ (by simp),
convert continuous_mul _ _,
{ ext, apply this },
{ apply_instance },
{ apply continuous_const },
{ apply continuous_pow }}
end

end eval

section map
@@ -1201,6 +1224,9 @@ calc derivative (f * g) = f.sum (λn a, g.sum (λm b, C ((a * b) * (n + m : ℕ)
simp [finsupp.sum, mul_assoc, mul_comm, mul_left_comm]
end

lemma derivative_eval (p : polynomial α) (x : α) : p.derivative.eval x = p.sum (λ n a, (a * n)*x^(n-1)) :=
by simp [derivative, eval_sum, eval_pow]

end derivative

section domain
ProTip! Use n and p to navigate between commits in a pull request.
You can’t perform that action at this time.