## Stream: maths

### Topic: Some numerology

#### Patrick Massot (Sep 20 2019 at 21:44):

I have a little riddle for people who like numbers in Lean.

example (p : ℕ) (n : ℤ) (hp : 1 < p) (h : (p : ℚ) ^ -n < p) : (p : ℚ)^-n ≤ 1


#### Patrick Massot (Sep 20 2019 at 21:45):

Of course the question is not about the math proof, it's about convincing Lean

#### Floris van Doorn (Sep 20 2019 at 22:06):

import data.rat algebra.field_power

example (p : ℕ) (n : ℤ) (hp : 1 < p) (h : (p : ℚ) ^ -n < p) : (p : ℚ)^-n ≤ 1 :=
begin
have h2p : (1 : ℚ) ≤ p, { exact_mod_cast le_of_lt hp },
have h3p : (0 : ℚ) < p := lt_of_lt_of_le (by norm_num) h2p,
have : 0 ≤ n,
{ rw [← not_lt], intro h2,
have hn : 1 ≤ -n, { rw [le_neg], apply int.le_of_lt_add_one, exact h2 },
apply not_le.mpr h, convert fpow_le_of_le h2p hn, rw [fpow_one] },
rw [fpow_neg, div_le_iff (fpow_pos_of_pos h3p _), one_mul],
apply one_le_fpow_of_nonneg h2p this
end


#### Mario Carneiro (Sep 20 2019 at 22:09):

the -n seems unnecessary

#### Floris van Doorn (Sep 20 2019 at 22:15):

Using Mario's comment, I golfed it to

example (p : ℕ) (n : ℤ) (hp : 1 < p) (h : (p : ℚ) ^ n < p) : (p : ℚ)^n ≤ 1 :=
begin
have h2p : (1 : ℚ) ≤ p, { exact_mod_cast le_of_lt hp },
apply fpow_le_one_of_nonpos h2p, rw [← not_lt], intro h2, rw [← int.add_one_le_iff] at h2,
apply not_le.mpr h, convert fpow_le_of_le h2p h2, rw [zero_add, fpow_one]
end


#### Mario Carneiro (Sep 20 2019 at 22:19):

import data.rat algebra.field_power

example (p : ℕ) (n : ℤ) (hp : 1 ≤ p) (h : (p : ℚ) ^ n < p) : (p : ℚ)^n ≤ 1 :=
begin
have hp' : 1 ≤ (p : ℚ), {norm_cast, exact hp},
have : n ≤ 0,
{ refine le_of_not_lt (λ h', not_le_of_lt h _),
simpa using fpow_le_of_le hp' (int.add_one_le_iff.2 h') },
{ simpa using fpow_le_of_le hp' this }
end


#### Mario Carneiro (Sep 20 2019 at 22:23):

the golfy version is

example (p : ℕ) (n : ℤ) (hp : 1 ≤ p) (h : (p : ℚ) ^ n < p) : (p : ℚ)^n ≤ 1 :=
have hp' : 1 ≤ (p : ℚ), by exact_mod_cast hp,
by simpa using fpow_le_of_le hp' (le_of_not_lt $λ h' : 0 < n, not_le_of_lt h$
by simpa using fpow_le_of_le hp' (int.add_one_le_iff.2 h'))


#### Mario Carneiro (Sep 20 2019 at 22:25):

if I cheat by simplifying the statement some more:

example (p : ℚ) (n : ℤ) (hp : 1 ≤ p) (h : p ^ n < p) : p ^ n ≤ 1 :=
by simpa using fpow_le_of_le hp (le_of_not_lt $λ h' : 0 < n, not_le_of_lt h$
by simpa using fpow_le_of_le hp (int.add_one_le_iff.2 h'))


#### Patrick Massot (Sep 21 2019 at 08:15):

Thanks Floris and Mario!

#### Kevin Buzzard (Sep 21 2019 at 13:00):

Here's one I ran into the other day:

example (a b : ℤ) (hb : b > 0) : a < b → int.to_nat a < int.to_nat b := sorry


Should that be in mathlib? Is it there already?

#### Johan Commelin (Sep 21 2019 at 13:01):

int.to_nat is not maths right?

#### Kevin Buzzard (Sep 21 2019 at 13:04):

It sends negative things to 0, that's why this is true. This should be called to_nat_strict_mono or something.

#### Johan Commelin (Sep 21 2019 at 13:04):

It's far from strict

#### Kevin Buzzard (Sep 21 2019 at 13:04):

So yes, it's not maths.

#### Johan Commelin (Sep 21 2019 at 13:04):

I tend to prefer nat_abs

#### Kevin Buzzard (Sep 21 2019 at 13:04):

I thought strict meant "working with lt not le"

#### Johan Commelin (Sep 21 2019 at 13:04):

Also, we now have the lift tactic

#### Kevin Buzzard (Sep 21 2019 at 13:04):

nat_abs is the maths one, right?

#### Mario Carneiro (Sep 21 2019 at 18:31):

I assume it is int.to_nat_lt_to_nat

#### Kevin Buzzard (Sep 23 2019 at 07:42):

I can't find that in mathlib. Johan -- this all started with me trying to prove

def int.Ioo_fin_equiv (a b : ℤ) : set.Ioo a b ≃ fin (int.to_nat $b - a - 1) :=  The size of {a<x<b} really is to_nat. But I could prove something like example (a b : ℤ) (h : a < b) : set.Ioo a b ≃ fin (int.nat_abs$ b - a - 1) :=


#### Mario Carneiro (Sep 23 2019 at 07:45):

theorem le_to_nat (a : ℤ) : a ≤ to_nat a :=
by rw [to_nat_eq_max]; apply le_max_left

@[simp] theorem to_nat_le {a : ℤ} {n : ℕ} : to_nat a ≤ n ↔ a ≤ n :=
by rw [(coe_nat_le_coe_nat_iff _ _).symm, to_nat_eq_max, max_le_iff];
exact and_iff_left (coe_zero_le _)

@[simp] theorem lt_to_nat {n : ℕ} {a : ℤ} : n < to_nat a ↔ (n : ℤ) < a :=
le_iff_le_iff_lt_iff_lt.1 to_nat_le

theorem to_nat_le_to_nat {a b : ℤ} (h : a ≤ b) : to_nat a ≤ to_nat b :=
by rw to_nat_le; exact le_trans h (le_to_nat b)

theorem to_nat_lt_to_nat {a b : ℤ} (hb : 0 < b) (h : a < b) : to_nat a < to_nat b :=
by rw lt_to_nat; cases a; [exact h, exact hb]


#### Mario Carneiro (Sep 23 2019 at 07:45):

this goes in data.int.basic

#### Kevin Buzzard (Sep 23 2019 at 07:54):

I was unsure whether the idea was to develop the theory of to_nat any more, or whether one should use the "superior" nat_abs which is more mathematically appealing in some weird way

#### Kevin Buzzard (Sep 23 2019 at 07:55):

Is there some monotonicity tactic which needs to know about to_nat_lt_to_nat ? @Simon Hudon ?

#### Mario Carneiro (Sep 23 2019 at 08:15):

I don't know how well mono handles side conditions

#### Simon Hudon (Sep 23 2019 at 12:59):

I think mono could help here. What it does is that it tries assumption on the side condition while selecting a lemma. If it fails with assumption it just means that the lemma is more expensive to apply. The lemma with the fewest remaining side condition is selected. If there's only one candidate, you're just going to get a dump of all the side conditions that mono can't handle

def int.Ioo_fin_equiv (a b : ℤ) : set.Ioo a b ≃ fin (int.to_nat $b - a - 1) := { to_fun := λ s, ⟨int.to_nat (s.val - a - 1), begin cases s with s hs, show int.to_nat (s - a - 1) < int.to_nat (b - a - 1), cases hs with has hsb, have h1 : b - a - 1 > 0, linarith, apply int.to_nat_lt_to_nat _ _ h1, convert (sub_lt_sub_iff_right (a + 1)).2 hsb using 1; ring, end⟩, inv_fun := λ t, ⟨t.val + a + 1, begin split, apply int.lt_of_add_one_le, rw add_assoc, apply le_add_of_nonneg_left, simp, suffices : (t.val : ℤ) < b - a - 1, convert add_lt_add_left this (a + 1) using 1; ring, have t2 := t.2, convert int.coe_nat_lt_coe_nat_of_lt t2, rw int.to_nat_eq_max, rw max_eq_left, apply le_of_lt, have h : 0 < int.to_nat (b - a - 1), refine lt_of_le_of_lt (by simp) t2, rw lt_iff_not_ge', intro h2, apply lt_irrefl 0, convert h, replace h2 := (int.to_nat_le _ _).2 h2, symmetry, rwa nat.le_zero_iff at h2, end⟩, left_inv := begin rintro ⟨s, sa, sb⟩, suffices : ↑(int.to_nat (s - (a + 1))) + a + 1 = s, exact subtype.eq (by simpa using this), rw (int.to_nat_of_nonneg _), simp, linarith, end, right_inv := begin rintro ⟨s, hs⟩, dsimp, rw fin.ext_iff, dsimp, conv in (↑s + a + 1 + -a + -1 : ℤ) begin ring end, simp, end }  I really hope this can be seriously golfed. I just muddle through with stuff like this; there are a couple of non-terminal simps :-/ #### Chris Hughes (Sep 23 2019 at 20:15): import data.equiv.basic data.int.basic data.set.intervals def int.Ico_fin_equiv (a b : ℤ) : set.Ico a b ≃ fin (int.to_nat$ b - a) :=
calc set.Ico a b ≃ set.Ico 0 (b - a) :
λ _, by simp, λ _, by simp⟩
... ≃ fin (int.to_nat $b - a) : ⟨λ x, ⟨x.1.to_nat, int.coe_nat_lt.1$
by rw [int.to_nat_of_nonneg x.2.1, int.to_nat_of_nonneg (le_trans x.2.1 (le_of_lt x.2.2))];
exact x.2.2⟩,
λ x, ⟨x.1, int.coe_nat_nonneg _, begin
have := int.coe_nat_lt.2 x.2,
rwa [int.to_nat_of_nonneg] at this,
cases b - a;
simp only [int.to_nat, int.coe_nat_lt, nat.not_lt_zero, *] at *
end⟩,
λ x, by simp [int.to_nat_of_nonneg x.2.1],
λ x, by simp⟩

def int.Ioo_fin_equiv (a b : ℤ) : set.Ioo a b ≃ fin (int.to_nat $b - (a + 1)) := calc set.Ioo a b ≃ set.Ico (a + 1) b : equiv.set.of_eq (by simp [set.ext_iff, int.add_one_le_iff]) ... ≃ _ : int.Ico_fin_equiv _ _ def int.Ioc_fin_equiv (a b : ℤ) : set.Ioc a b ≃ fin (int.to_nat$ b - a) :=
calc set.Ioc a b ≃ set.Ioo a (b + 1) : equiv.set.of_eq (by simp [set.ext_iff, int.lt_add_one_iff])
... ≃ fin (int.to_nat $(b + 1) - (a + 1)) : int.Ioo_fin_equiv _ _ ... ≃ fin (int.to_nat$ b - a) : ⟨fin.cast (by simp), fin.cast (by simp),
λ _, fin.eq_of_veq rfl, λ _, fin.eq_of_veq rfl⟩

def int.Icc_fin_equiv (a b : ℤ) : set.Icc a b ≃ fin (int.to_nat $b + 1 - a) := calc set.Icc a b ≃ set.Ico a (b + 1) : equiv.set.of_eq (by simp [set.ext_iff, int.lt_add_one_iff]) ... ≃ fin (int.to_nat$ b + 1 - a) : int.Ico_fin_equiv _ _


#### Patrick Massot (Sep 23 2019 at 20:16):

Kevin, it is now your duty to PR this before it disappear from sight.

#### Kevin Buzzard (Sep 23 2019 at 20:31):

I'll have to remember how to PR stuff. I have to Skype interview someone in 30 minutes and I want to clean up the kitchen before that :-/ I'll get my act together after that.

#### Kevin Buzzard (Sep 23 2019 at 20:32):

That's very nice Chris. I just chose the equiv I needed, but if you prove the more convenient one first the rest can happen relatively simply.

#### Floris van Doorn (Sep 23 2019 at 20:38):

I feel like various steps in Chris's proof need to be separated out in their own lemmas when we PR this to mathlib.

#### Kevin Buzzard (Sep 23 2019 at 22:03):

sigh how do you do update-mathlib when you're editing mathlib, again?

#### Kevin Buzzard (Sep 23 2019 at 22:04):

I can't find it in the docs :-/

#### Kevin Buzzard (Sep 23 2019 at 22:06):

aah got it cache-olean

#### Kevin Buzzard (Sep 23 2019 at 22:18):

#1479 is the of_nat lemmas. I haven't done the equiv yet; I can see at least some of what can come off, my issue is simply that I don't know the import hierarchy so I just don't know where these lemmas go.

#### Kevin Buzzard (Sep 24 2019 at 01:35):

(3) Does this give anyone else an assertion violation?

import data.set.intervals

def set.Ico_equiv_add (a b n : ℤ) : set.Ico (a + n) (b + n) ≃ set.Ico a b :=
{ to_fun := λ s, ⟨s.1 - n, _⟩,
inv_fun := λ t, ⟨t.1 + n, _, _⟩,
left_inv := λ s, by simp,
right_inv := λ t, by simp }


[added 19th Oct 2019 -- I also seem to need to import data.equiv.basic now but I can still get the assertion violation]

#### Kevin Buzzard (Sep 24 2019 at 01:35):

(1) I thought I'd try it myself after I realised what I should be proving.

example (a b : ℤ) : set.Ico a b ≃ fin (int.to_nat $b - a) := { to_fun := λ s, ⟨int.to_nat (s.val - a), int.to_nat_lt_to_nat (sub_pos.2$ lt_of_le_of_lt s.2.1 s.2.2) $sub_lt_sub_right s.2.2 _⟩, inv_fun := λ t, ⟨(t.val : ℤ) + a, ⟨ le_add_of_nonneg_left$ int.of_nat_nonneg _, add_lt_of_lt_sub_right
$int.lt_to_nat.1 t.2⟩⟩, left_inv := λ ⟨s, has, hsb⟩, subtype.eq$
show ↑(int.to_nat (s - a)) + a = s,
begin rw int.to_nat_of_nonneg _, ring, linarith end,
right_inv := begin
rintro ⟨t, ht⟩,
suffices : int.to_nat (↑t + a - a) = t,
simp [this],
exact int.to_nat_coe_nat t,
end}


#### Kevin Buzzard (Sep 24 2019 at 01:35):

(4)

def set.Ico_equiv_add (a b n : ℤ) : set.Ico (a + n) (b + n) ≃ set.Ico a b :=
{ to_fun := λ s, ⟨s.1 - n, le_sub_right_of_add_le s.2.1, sub_lt_iff_lt_add.2 s.2.2⟩,
left_inv := λ _, by simp,
right_inv := λ _, by simp }


#### Kevin Buzzard (Sep 24 2019 at 01:35):

(2)

def set.Ico_equiv_sub (a b n : ℤ) : set.Ico a b ≃ set.Ico (a - n) (b - n) :=
{ to_fun := λ s, ⟨s.1 - n, sub_le_sub_right s.2.1 _, sub_lt_sub_right s.2.2 _⟩,
left_inv := λ s, by simp,
right_inv := λ t, by simp }

example (a b : ℤ) : set.Ico a b ≃ set.Ico 0 (b - a) := by convert set.Ico_equiv_sub a b a; simp


I was inspired to do the result Chris had; I should have used + not - for the sign of n. We're proving that the counting measure is invariant :-) (and hence must be the Haar measure).

#### Kevin Buzzard (Sep 24 2019 at 01:35):

(5) [meh, that'll teach me to post when offline; messages have appeared in random order]

#### Johan Commelin (Sep 24 2019 at 04:32):

Sorting is hard... every computer scientist knows that :stuck_out_tongue_wink:

Last updated: May 06 2021 at 19:30 UTC