# Zulip Chat Archive

## 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

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

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) : ⟨λ x, ⟨x.1 - a, sub_nonneg.2 x.2.1, add_lt_add_right x.2.2 _⟩, λ x, ⟨x.1 + a, le_add_of_nonneg_left x.2.1, lt_sub_iff_add_lt.1 x.2.2⟩, λ _, 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], rw add_sub_cancel, 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⟩, inv_fun := λ t, ⟨t.1 + n, add_le_add_right t.2.1 _, add_lt_add_right t.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 _⟩, inv_fun := λ t, ⟨t.1 + n, le_add_of_sub_right_le t.2.1, add_lt_of_lt_sub_right t.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