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

p-adic numbers #262

Merged
merged 12 commits into from Aug 16, 2018

Conversation

Projects
None yet
3 participants
@robertylewis
Copy link
Collaborator

commented Aug 15, 2018

This pull request defines the p-adic numbers as the Cauchy completion of with respect to the p-adic norm. As a side effect, I've generalized the construction of , since it shares some steps with this one. This isn't strictly necessary -- I can drop the third commit if you'd rather leave real.lean as it was. I've also added field_power.lean, since gpow doesn't extend to . There's more that could be filled out here, what I have is just sufficient for this project.

I've added various lemmas in various places along the way, in the first commit. I tried to find sensible names and places for most of them. Tell me if you think they should be moved, renamed, or just used locally.

Lifting the norm from to ℚ_p involves some explicit calculations with indices. @johoelzl suggested approaching this with the at_top filter. To be honest, I'm not immediately sure how that construction would go, and I'm a little skeptical that it would save much work in the end. (I suspect it might be prettier though!)

TO CONTRIBUTORS:

Make sure you have:

  • reviewed and applied the coding style: coding, naming
  • for tactics:
  • make sure definitions and lemmas are put in the right files
  • make sure definitions and lemmas are not redundant

For reviewers: code review check list

@digama0
Copy link
Member

left a comment

Looks like there's quite a lot of stuff here! If you like, I can also do some of these changes after merging.

@@ -98,6 +98,18 @@ eq.trans (by rw [int.cast_neg]; refl) (ceil_add_int _ _)
theorem ceil_lt_add_one (x : α) : (⌈x⌉ : α) < x + 1 :=
by rw [← lt_ceil, ← int.cast_one, ceil_add_int]; apply lt_add_one

lemma ceil_pos {a : α} : 0 < ceil a 0 < a :=

This comment has been minimized.

Copy link
@digama0

digama0 Aug 15, 2018

Member

can these two use the ceil notation?


section field_power
open int nat
variables {α : Type u} [field α]

This comment has been minimized.

Copy link
@digama0

digama0 Aug 15, 2018

Member

this should be definable over a division ring, although you can keep the name fpow if you like

| (of_nat n) := a ^ n
| -[1+n] := 1/(a ^ (n+1))

@[simp] lemma unit_pow {a : α} (ha : a 0) : n : ℕ, a ^ n = ↑((units.mk0 a ha)^n)

This comment has been minimized.

Copy link
@digama0

digama0 Aug 15, 2018

Member

This seems like a bad simp lemma. It's just going to write all your powers in terms of units pow. Is that what you want? I would have expected the simp lemma to point the other way.

This comment has been minimized.

Copy link
@robertylewis

robertylewis Aug 15, 2018

Author Collaborator

Er, yeah, I don't remember tagging this as a simp lemma. That's definitely wrong.

by simp [fpow, h1]

lemma fpow_add {a : α} (ha : a 0) (z1 z2 : ℤ) : fpow a (z1 + z2) = fpow a z1 * fpow a z2 :=
begin simp only [fpow_eq_gpow ha], rw ←units.mul_coe, congr, apply gpow_add end

This comment has been minimized.

Copy link
@digama0

digama0 Aug 15, 2018

Member

this doesn't look like it needs discrete_field

This comment has been minimized.

Copy link
@robertylewis

robertylewis Aug 15, 2018

Author Collaborator

No, looks like not. I should have cleaned up the type classes in this file.

if ha' : 1 < a then le_of_lt $ inv_lt_one ha'
else
have 1 = a, from le_antisymm ha (le_of_not_lt ha'),
by simp [this.symm]

This comment has been minimized.

Copy link
@digama0

digama0 Aug 15, 2018

Member

This should be in ordered_field.lean

have bound - m < minv, from (nat.sub_lt_left_iff_lt_add hmb').2 this,
begin rw nat.sub_sub_self at minv', exact minv' this, exact hmb' end

protected def nat.find_greatest : ℕ := nat.find_greatest_x hall hex

This comment has been minimized.

Copy link
@digama0

digama0 Aug 15, 2018

Member

Unlike nat.find, this doesn't require any fancy arguments for termination, so I think it should be defined as a total function given P and bound (I guess it can return an option in the core version, since it can determine itself if there is a witness).

let hle := le_of_dvd (int.nat_abs_pos_of_ne_zero hn) hdvd' in
not_le_of_gt this hle

def padic_val {p : ℕ} (hp : p > 1) (n : ℤ) : ℕ :=

This comment has been minimized.

Copy link
@digama0

digama0 Aug 15, 2018

Member

this should not be a partial function

by rw [padic_val_rat.defn, padic_val_rat.defn]; simpa
... = min (padic_val_rat (prime.gt_one p_prime) q)
(padic_val_rat (prime.gt_one p_prime) r) :
by rw [←rat.num_denom q, ←rat.num_denom r]

This comment has been minimized.

Copy link
@digama0

digama0 Aug 15, 2018

Member

warning: I will probably rewrite this

This comment has been minimized.

Copy link
@robertylewis

robertylewis Aug 15, 2018

Author Collaborator

Please. I thought about rewriting this today as I was cleaning things up, but got scared.

def stationary_point {f : padic_seq hp} (hf : ¬ f ≈ 0) : ℕ :=
classical.some $ stationary hf

def stationary_point_spec {f : padic_seq hp} (hf : ¬ f ≈ 0) :

This comment has been minimized.

Copy link
@digama0

digama0 Aug 15, 2018

Member

this is a theorem

refine (int.nat_abs_dvd.1 $ int.dvd_nat_abs.1 $ int.coe_nat_dvd.2 $
c.dvd_of_dvd_mul_right _),
have := congr_arg int.nat_abs e,
simp [int.nat_abs_mul, int.nat_abs_of_nat] at this, simp [this]

This comment has been minimized.

Copy link
@digama0

digama0 Aug 15, 2018

Member

What's going on here? It looks like you just commented out and recopied the same theorem

This comment has been minimized.

Copy link
@robertylewis

robertylewis Aug 15, 2018

Author Collaborator

Well, I forgot the comment that explained what was going on here (also why I left the old proof there for now). It's not the same theorem: check the type of b in the old one. The b0 argument forces b to be a nat, then it gets cast to an int in the type. I'm guessing that's not what you intended, and changing it doesn't break anything, but I meant to ask.

This comment has been minimized.

Copy link
@digama0

digama0 Aug 15, 2018

Member

oh, I see, it's that stupid nat default thing because of the 0 numeral in b0. Yeah, that was not intended. Is there a reason you changed num_dvd to rat.num_dvd though? Surely we are already in the rat namespace, so that would cause double namespacing.

This comment has been minimized.

Copy link
@robertylewis

robertylewis Aug 15, 2018

Author Collaborator

Nope, that's another c/p mistake.

@robertylewis

This comment has been minimized.

Copy link
Collaborator Author

commented Aug 15, 2018

Looks like there's quite a lot of stuff here! If you like, I can also do some of these changes after merging.

Yeah, sorry for the big PR. Unless you're in a hurry to merge it, I can clean things up when I'm in the office tomorrow. Making padic_val total is the only real non-cosmetic change.

@digama0

This comment has been minimized.

Copy link
Member

commented Aug 15, 2018

I'd prefer that all the functions are total, in fact. The only problem you could run into is once you start inferring typeclasses like is_absolute_value (padic_norm hp). If hp isn't in the type, it will need to be inferred. Chris had a similar problem with zmod, since he wanted to infer that zmod p is a field when p is prime. I think that the case for prime being a typeclass is strengthening. (This doesn't mean we have to use it with square brackets everywhere, but it will help in places where we want to fix a prime without doing complicated things with it.)

@robertylewis

This comment has been minimized.

Copy link
Collaborator Author

commented Aug 15, 2018

Yeah, I thought about this briefly as I was starting, and I think if you go that direction you really need a prime typeclass. Would you like me to add that and totalize padic_norm ? If you'd rather do it yourself, I'll just change the functions that aren't typeclass instances.

@digama0

This comment has been minimized.

Copy link
Member

commented Aug 15, 2018

I think I should probably do it myself, since it affects several other places beyond this PR.

@robertylewis

This comment has been minimized.

Copy link
Collaborator Author

commented Aug 16, 2018

I believe I've made all the requested changes. I'm sure there are other interfaces/implementations for nat.find_greatest; I'm not committed to this one, anything will work for me. padic_val and padic_val_rat are now total.

have q = q.num /. q.denom, from num_denom _,
by simpa [hq]

lemma num_ne_zero_of_ne_zero {q : ℚ} (h : q 0) : q.num 0 :=

This comment has been minimized.

Copy link
@digama0

digama0 Aug 16, 2018

Member

I hesitate to bring this up because we've disagreed on this in the past, but you appear to have added a lot of contrapositive theorems like this one. I would prefer not to have duplicate theorems if you can access them with a combination of .1, .2 and mt on a base theorem (biconditional if possible). I would demonstrate that whatever use you have for these theorems can be written shorter without them, but I suspect these theorems have received little to no use yet so it would not be a particularly effective demonstration. What are your thoughts on this?

As a concrete example, here's a short proof of this theorem:

lemma num_ne_zero_of_ne_zero {q : ℚ} : q  0  q.num  0 := mt zero_of_num_zero

The proof is literally shorter than the theorem name.

This comment has been minimized.

Copy link
@robertylewis

robertylewis Aug 16, 2018

Author Collaborator

Every time I use a biconditional, I have to remember (1) which direction does the name go, (2) do I need .1 or .2, (3) are there arguments that force me to put it in parentheses? It takes me about as long to run through this list as it does to state the contrapositive theorem, and then applying it is mechanical. That said, your style guidelines rule here. If you prefer the concision over my mental energy, that's fine!

This comment has been minimized.

Copy link
@digama0

digama0 Aug 16, 2018

Member

Hm, I usually just try all the combinations and let lean tell me what's what. I think I will merge this now, but expect these theorems to be replaced in the future.

This comment has been minimized.

Copy link
@spl

spl Aug 17, 2018

Collaborator

Just to add my own 2¢, I initially had issues looking for contrapositive theorems, but once @digama0 taught me the mt “trick” (at least twice, I think), it has become habitual to look, if I need it, for the theorem that fits the pattern to which I apply mt. Also, I prefer .mp and .mpr over .1 and .2 for their more descriptive nature.

@digama0

This comment has been minimized.

Copy link
Member

commented Aug 16, 2018

It's looking good, I'll merge it shortly. I'll put this on the back burner for larger revisions but this can (and should) go in now so that we don't get any fragmentation. Plus, p-adics are a big step forward. How far are we from C_p?

@robertylewis

This comment has been minimized.

Copy link
Collaborator Author

commented Aug 16, 2018

Cool. I'm happy to update things if/when there's a prime typeclass. My plan was to stick with Q_p and Z_p for the short term (e.g. Hensel's lemma), but C_p is a reasonable direction to go in as well.

@digama0 digama0 merged commit 93817f1 into leanprover-community:master Aug 16, 2018

1 check was pending

continuous-integration/travis-ci/pr The Travis CI build is in progress
Details
@robertylewis

This comment has been minimized.

Copy link
Collaborator Author

commented Aug 16, 2018

Oops, just noticed I added a tactic.find import in padic_norm.lean with the edits. Could you erase that?

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.