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
Copy path View file
@@ -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?

λ h, have-a⌋ < 0, from neg_of_neg_pos h,
pos_of_neg_neg $ lt_of_not_ge $ (not_iff_not_of_iff floor_nonneg).1 $ not_le_of_gt this,
λ 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) : ceil 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,
by simp [h']

end

class archimedean (α) [ordered_comm_monoid α] : Prop :=
Copy path View file
@@ -0,0 +1,113 @@
/-
Copyright (c) 2018 Robert Y. Lewis. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Robert Y. Lewis
Integer power operation on fields.
-/

import algebra.group_power tactic.wlog

universe u

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


@[simp] lemma zero_gpow : z : ℕ, z 0 (0 : α)^z = 0
| 0 h := absurd rfl h
| (k+1) h := zero_mul _

def fpow (a : α) : ℤ α
| (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.

| 0 := by simp; refl
| (k+1) := by simp [_root_.pow_add]; congr; apply unit_pow

lemma fpow_eq_gpow {a : α} (h : a 0) : (z : ℤ), fpow a z = ↑(gpow (units.mk0 a h) z)
| (of_nat k) := by simp only [fpow, gpow]; apply unit_pow
| -[1+k] := by simp [fpow, gpow]; congr; apply unit_pow

lemma fpow_inv (a : α) : fpow a (-1) = a⁻¹ :=
begin change fpow a -[1+0] = a⁻¹, simp [fpow] end

lemma fpow_ne_zero_of_ne_zero {a : α} (ha : a 0) : (z : ℤ), fpow a z 0
| (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 _

end field_power

section discrete_field_power
open int nat
variables {α : Type u} [discrete_field α]

lemma zero_fpow : z : ℤ, z 0 fpow (0 : α) z = 0
| (of_nat n) h :=
have h2 : n 0, from assume : n = 0, by simpa [this] using h,
by simp [h, h2, fpow]
| -[1+n] h :=
have h1 : (0 : α) ^ (n+1) = 0, from zero_mul _,
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.


end discrete_field_power

section ordered_field_power
open int

variables {α : Type u} [discrete_linear_ordered_field α]

lemma inv_le_one {a : α} (ha : 1 a) : a⁻¹ 1 :=
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


lemma fpow_nonneg_of_nonneg {a : α} (ha : a 0) : (z : ℤ), fpow a z 0
| (of_nat n) := pow_nonneg ha _
| -[1+n] := div_nonneg' zero_le_one $ pow_nonneg ha _


lemma fpow_le_of_le {x : α} (hx : 1 x) {a b : ℤ} (h : a b) : fpow x a fpow x b :=
begin
induction a with a a; induction b with b b,
{ simp only [fpow],
apply pow_le_pow hx,
apply le_of_coe_nat_le_coe_nat h },
{ apply absurd h,
apply not_le_of_gt,
exact lt_of_lt_of_le (neg_succ_lt_zero _) (of_nat_nonneg _) },
{ simp only [fpow, one_div_eq_inv],
apply le_trans,
apply inv_le_one,
repeat { apply one_le_pow_of_one_le hx } },
{ simp only [fpow],
apply (one_div_le_one_div _ _).2,
{ apply pow_le_pow hx,
have : -(↑(a+1) : ℤ) -(↑(b+1) : ℤ), from h,
have h' := le_of_neg_le_neg this,
apply le_of_coe_nat_le_coe_nat h' },
repeat { apply pow_pos (lt_of_lt_of_le zero_lt_one hx) } }

This comment has been minimized.

Copy link
@digama0

digama0 Aug 15, 2018

Member

style: there is an extra indent from L82 onward, and another extra indent after L94. To indicate that L93 has two subgoals, you can put L98 in an additional bracket pair, like this:

apply (one_div_le_one_div _ _).2,
{ apply pow_le_pow hx,
  have : -(↑(a+1) : ℤ) ≤ -(↑(b+1) : ℤ), from h,
  have h' := le_of_neg_le_neg this,
  apply le_of_coe_nat_le_coe_nat h' },
{ repeat { apply pow_pos (lt_of_lt_of_le zero_lt_one hx) } } }

This comment has been minimized.

Copy link
@robertylewis

robertylewis Aug 16, 2018

Author Collaborator

Huh, I never realized that this indentation style didn't match the mathlib conventions, it's what I always use. Guess I'll change that everywhere. Not following you about line 93. There are three subgoals there -- one gets killed by 94-97, the other two by the repeat. Bracketing the repeat means one is left.

This comment has been minimized.

Copy link
@digama0

digama0 Aug 16, 2018

Member

Oh, I see. In that case it just needs to be unindented, although I might recommend using exact instead of apply in the repeat to make it clear that the first repeat doesn't interfere with the second.

end

lemma pow_le_max_of_min_le {x : α} (hx : x 1) {a b c : ℤ} (h : min a b c) :
fpow x (-c) max (fpow x (-a)) (fpow x (-b)) :=
begin
wlog hle := le_total a b using a b,

This comment has been minimized.

Copy link
@digama0

digama0 Aug 15, 2018

Member

You should be able to just say wlog hle : a ≤ b here, since there is special support for le_total in wlog

This comment has been minimized.

Copy link
@robertylewis

robertylewis Aug 15, 2018

Author Collaborator

I've only used wlog on le_total proofs in this file. There were one or two instances where the nicer syntax failed with inscrutable error messages. (Or crashed Lean, as I mentioned on Zulip -- I managed to reproduce that without specifying the match pattern too.) But you're right, this one should be fine with the nicer syntax.

This comment has been minimized.

Copy link
@digama0

digama0 Aug 15, 2018

Member

the bug in wlog should be fixed btw

have hnle : -b -a, from neg_le_neg hle,
have hfle : fpow x (-b) fpow x (-a), from fpow_le_of_le hx hnle,
have : fpow x (-c) fpow x (-a),
{ apply fpow_le_of_le hx,
simpa [hle, min_eq_left] using h },
simpa [hfle, max_eq_left] using this
end

end ordered_field_power
Copy path View file
@@ -3,7 +3,7 @@ Copyright (c) 2017 Mario Carneiro. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Mario Carneiro
-/
import algebra.ordered_group order.lattice
import algebra.ordered_group order.lattice tactic.wlog

This comment has been minimized.

Copy link
@digama0

digama0 Aug 15, 2018

Member

Can we avoid wlog here? I hate to ask for this but wlog has data.list.perm as a requirement, so this is going to make the dependency structure all tangled up.

This comment has been minimized.

Copy link
@robertylewis

robertylewis Aug 15, 2018

Author Collaborator

I thought you might ask for that. Yeah, it can be avoided without too much work.


open lattice

@@ -77,6 +77,20 @@ by by_cases h : a ≤ b; simp [min, h]
theorem max_choice (a b : α) : max a b = a max a b = b :=
by by_cases h : a b; simp [max, h]

lemma le_of_max_le_left {a b c : α} (h : max a b c) : a c :=
le_trans (le_max_left _ _) h

lemma le_of_max_le_right {a b c : α} (h : max a b c) : b c :=
le_trans (le_max_right _ _) h

lemma min_add_eq_min_add_min {α : Type u} [decidable_linear_ordered_comm_group α] (a b c : α) :
min a b - c = min (a-c) (b-c) :=

This comment has been minimized.

Copy link
@digama0

digama0 Aug 15, 2018

Member

this theorem has nothing to do with adding. Is this a copy paste error?

Also, it looks like it would be defeq to an instance of the analogous theorem with addition, so you should prove that instead and have this as a corollary.

This comment has been minimized.

Copy link
@robertylewis

robertylewis Aug 15, 2018

Author Collaborator

Huh. Yeah, I'll blame c/p, not sure what happened there.

begin
wlog hle : a b,
have : a - c b - c, from sub_le_sub hle (le_refl _),
simp [*, min_eq_left] at *
end

end

section decidable_linear_ordered_comm_group
@@ -125,6 +139,24 @@ abs_le_of_le_of_neg_le
(by simp [le_max_iff, le_trans hbc (le_abs_self c)])
(by simp [le_max_iff, le_trans (neg_le_neg hab) (neg_le_abs_self a)])

lemma min_le_add_of_nonneg_right {a b : α} (hb : b 0) : min a b a + b :=
calc
min a b a : by apply min_le_left
... a + b : le_add_of_nonneg_right hb

lemma min_le_add_of_nonneg_left {a b : α} (ha : a 0) : min a b a + b :=
calc
min a b b : by apply min_le_right
... a + b : le_add_of_nonneg_left ha

lemma max_le_add_of_nonneg {a b : α} (ha : a 0) (hb : b 0) : max a b a + b :=
begin
wlog hle : a b,
rw max_eq_right hle,
apply le_add_of_nonneg_left',
assumption
end

end decidable_linear_ordered_comm_group

section decidable_linear_ordered_comm_ring
Copy path View file
@@ -109,6 +109,10 @@ le_iff_le_iff_lt_iff_lt.1 (mul_le_mul_right_of_neg h)
lemma sub_one_lt (a : α) : a - 1 < a :=
sub_lt_iff_lt_add.2 (lt_add_one a)

lemma mul_le_one {α : Type*} [linear_ordered_semiring α] {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

end linear_ordered_ring

set_option old_structure_cmd true
Copy path View file
@@ -527,6 +527,38 @@ eq_one_of_dvd_one H ⟨b, H'.symm⟩
theorem eq_one_of_mul_eq_one_left {a b : ℤ} (H : b 0) (H' : a * b = 1) : b = 1 :=
eq_one_of_mul_eq_one_right H (by rw [mul_comm, H'])

lemma of_nat_dvd_of_dvd_nat_abs {a : ℕ} : {z : ℤ} (haz : a ∣ z.nat_abs), ↑a ∣ z
| (int.of_nat _) haz := int.coe_nat_dvd.2 haz
| -[1+k] haz :=
begin
change ↑a ∣ -(k+1 : ℤ),
apply dvd_neg_of_dvd,
apply int.coe_nat_dvd.2,
exact haz
end

lemma dvd_nat_abs_of_of_nat_dvd {a : ℕ} : {z : ℤ} (haz : ↑a ∣ z), a ∣ z.nat_abs
| (int.of_nat _) haz := int.coe_nat_dvd.1 (int.dvd_nat_abs.2 haz)
| -[1+k] haz :=
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) :
↑(p ^ m) ∣ k :=
begin
induction k,
{ apply int.coe_nat_dvd.2,
apply pow_div_of_le_of_pow_div 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 int.coe_nat_dvd.1,
apply dvd_of_dvd_neg,
exact hdiv }
end

/- / and ordering -/

protected theorem div_mul_le (a : ℤ) {b : ℤ} (H : b 0) : a / b * b a :=
@@ -582,6 +614,16 @@ int.div_eq_of_eq_mul_right H3 $
by rw [← int.mul_div_assoc _ H2]; exact
(int.div_eq_of_eq_mul_left H4 H5.symm).symm

theorem eq_mul_div_of_mul_eq_mul_of_dvd_left {a b c d : ℤ} (hb : b 0) (hd : d 0) (hbc : b ∣ c)
(h : b * a = c * d) : a = c / b * d :=
begin
cases hbc with k hk,
subst hk,
rw int.mul_div_cancel_left, rw mul_assoc at h,
apply _root_.eq_of_mul_eq_mul_left _ h,
repeat {assumption}
end

theorem of_nat_add_neg_succ_of_nat_of_lt {m n : ℕ}
(h : m < n.succ) : of_nat m + -[1+n] = -[1+ n - m] :=
begin
@@ -631,6 +673,9 @@ by cases a; cases b; simp [(*), int.mul, nat_abs_neg_of_nat]
theorem neg_succ_of_nat_eq' (m : ℕ) : -[1+ m] = -m - 1 :=
by simp [neg_succ_of_nat_eq]

lemma nat_abs_ne_zero_of_ne_zero {z : ℤ} (hz : z 0) : z.nat_abs 0 :=
λ h, hz $ int.eq_zero_of_nat_abs_eq_zero h

/- to_nat -/

theorem to_nat_eq_max : (a : ℤ), (to_nat a : ℤ) = max a 0
Oops, something went wrong.
ProTip! Use n and p to navigate between commits in a pull request.
You can’t perform that action at this time.