Kevin Wilson: Introduction (+ a question on small examples)

Stream: new members

[Kevin Wilson]

Hi there,

My name is Kevin Wilson. Currently I run the data science group at The Policy Lab at Brown University and generally think about organizing and utilizing administrative data nowadays, but in a former life I got a Ph.D. in number theory. A friend of mine and I were discussing his work in theorem provers the other day, and he mentioned how much the lean and mathlib communities had grown, so I figured I'd check it out!

First off, thank you for all the wonderful resources. Lean and mathlib installed exactly as advertised in the docs, and both the tutorial and the natural number game were excellent introductions.

So I thought I'd try to prove something on my own from my own branch of math: The number of squarefree integers less than X is ~ X/zeta(2). That seemed a good deal to bite off, so I figured I'd try an example:

The set of squarefree integers at most 9 is {1, 2, 3, 5, 6, 7}.

I quickly found myself lost in the thickets of the documentation of finset and so I wondered if I could prove the set of squarefree integers at most 1 has size 1. I got to here:

import algebra.squarefree
import tactic

noncomputable theory
open_locale classical

def set_squarefree_le_x (N : ℕ): finset ℕ := finset.filter squarefree (finset.range (N + 1))

lemma sq_1_eq_1 : finset.card (set_squarefree_le_x 1) = 1 :=
begin
  unfold set_squarefree_le_x,
  rw finset.card_eq_succ,
  use 1,
  use ∅,
  split,
  simp,
  split,
  rw finset.eq_singleton_iff_unique_mem,
  --- etc
end

At this point I got this in the interactive pane:

rewrite tactic failed, did not find instance of the pattern in the target expression
  ?m_2 = {?m_3}
state:
2 goals
⊢ {1} = finset.filter squarefree (finset.range (1 + 1))

⊢ ∅.card = 0

I stared at this for a long while (and eventually came up with a much longer proof to get around this), but I realized I must be approaching this the wrong way.

I was curious if there's some advice on approaching these sort of small, concrete examples, especially about subsets of the integers or subgroups of specific finite groups?

Thanks in advance for any help here, and thank you for the great work on this library!

Kevin

[Riccardo Brasca]

I would do this saying that finset.filter squarefree (finset.range (N + 1)) is a subset of finset.range (N + 1), so the cardinality is smaller.

[Riccardo Brasca]

The cardinality of finset.range is surely in mathlib, so you have that the cardinality is at most 2.

[Yaël Dillies]

Hey! Welcome. Small concrete calculations are usually the worst, so I'm not sure what to answer.

[Yaël Dillies]

We have docs#nat.squarefree.decidable_pred, so in such a small case the calculation can actually be done automatically.

[Johan Commelin]

@Kevin Wilson Welcome! There is something called decidable_pred. It basically means that there is an algorithm that you can run to find out the truth of a certain predicate/proposition. If you are lucky, someone has already shown that squarefree is a decidable predicate on the natural numbers. If so, your lemma should be provable in one line: dec_trivial.
But this proof method will probably become unbearably slow for N ≥ 10. Maybe even earlier.

[Riccardo Brasca]

But I agree with Yael, the rest is annoying, you have to prove that 0 is not in the filter, so it is actually a subset of erase and blah blah

[Yaël Dillies]

Johan Commelin said:

But this proof method will probably become unbearably slow for N ≥ 10. Maybe even earlier.

Erhm...

[Yaël Dillies]

import algebra.squarefree

#eval (list.range 50000).filter squarefree

[Yaël Dillies]

list.length of that yields 30401.

[Kevin Wilson]

(Sorry, not used to Zulip so sent this before I saw the later messages! Please give me a moment while I read them!)

@Riccardo Brasca I did think about that, but eventually you have to show that it's ≤ 1, so you'll eventually need to enumerate finset.range (1 + 1) and check each element. Hence I figured I'd just show in this case, it was equal to {1}. :-)

@Yaël Dillies Sadness. If there are examples, though, I'd be happy to take a look, even if they're the worst!

[Yaël Dillies]

In that case, your pain also came from using docs#finset.range rather than docs#list.range. Finsets are unordered, so they lack an easy induction treatment, as opposed to lists. For small calculations, lists are usually better.

[Yaël Dillies]

If you're interested, here's a PR that does precisely this: small calculations in a smart way using lists. #10645

[Kevin Wilson]

@Johan Commelin Yeah I was confused by the decideable_pred because it was clearly already in the algebra.squarefree packages as @Yaël Dillies points out. It was unclear if I needed to hint that somehow to the rewriter and even how to do such things.

@Yaël Dillies this makes sense. I was drawn to docs#finset.range because, well, it seemed like what I was going for. I'll take a look at this small Roth number computation and see if I can make this work! Thanks!

[Johan Commelin]

@Yaël Dillies This doesn't work, do you know why?

lemma sq_1_eq_1 : finset.card (set_squarefree_le_x 1) = 1 :=
begin
  delta set_squarefree_le_x,
  dec_trivial,
end

[Yaël Dillies]

Because it's a finset, Johan. Replace that with a list and it will work out.

[Johan Commelin]

Why the heck is that a problem? Lean should be able to compute with finset.range 2.

[Yaël Dillies]

Hmm, maybe I said bullshit. This doesn't work either

import algebra.squarefree

example : ((list.range 2).filter squarefree).length = 1 := rfl

[Yaël Dillies]

Is it that #eval can do stuff that rfl or dec_trivial can't?

[Rob Lewis]

Hi @Kevin Wilson ! I'm also at Brown, new this year to the CS department, and taught a course using Lean this fall. Nice to see someone else nearby getting into it!

[Yaël Dillies]

But it's a problem with squarefree, because example : ((list.range 2).filter ⊤).length = 2 := rfl works

[Yaël Dillies]

Ahah! Is it some reducibility setting maybe?

[Kevin Wilson]

Nice to meet you, @Rob Lewis ! I'll definitely take a look at this course. I might bug you for a coffee at some point as well!

[Eric Rodriguez]

how do you trace dec_trivial calls? this is something I've wanted to know for a while and never found an answer sadly

[Eric Rodriguez]

something is very weird in that example...

[Yakov Pechersky]

Finsets have an induction on them, what do you mean Yael that they don't have an easy one?

[Yaël Dillies]

I think I got confused by the error.

[Heather Macbeth]

Hi @Kevin Wilson, nice to see you here!

[Kevin Wilson]

Hi @Heather Macbeth ! Long time no see!!

[Heather Macbeth]

Indeed! Well, if we get you addicted here, it may be short time much see!

[Kyle Miller]

Yaël Dillies said:

Ahah! Is it some reducibility setting maybe?

This is a sort of error I asked about a couple weeks ago, and Mario was saying it's something to do with which axioms appear in the definition, and some of them make it get "stuck."

Some examples to show some behavior (but not explaining what's wrong with squarefree):

import algebra.squarefree

example : ¬ squarefree 0 := dec_trivial -- ok
example : ¬ squarefree 1 := dec_trivial -- fails
example : squarefree 2 := dec_trivial -- fails

instance : decidable (squarefree 2) :=
is_true begin
  rw nat.squarefree_iff_nodup_factors (dec_trivial : 2 ≠ 0),
  norm_num
end

example : squarefree 2 := dec_trivial -- ok

[Kyle Miller]

I suspect the problem is that n.factors.nodup gets stuck on n.factors, which involves division, so well-founded recursion. (But I don't really know.)

[Kyle Miller]

New guess: it's that factors itself depends on well-founded recursion. Those don't seem to work with dec_trivial...

def factors : ℕ → list ℕ
| 0 := []
| 1 := []
| n@(k+2) :=
  let m := min_fac n in have n / m < n := factors_lemma,
  m :: factors (n / m)

[Kyle Miller]

It looks like it's possible to get it to work with an auxiliary algorithm for squarefree. I wrote a terrible one that does trial division with a naive upper bound:

def squarefree'_aux (n : ℕ) : ℕ → bool
| 0 := tt
| 1 := tt
| t'@(t+1) := if n % (t'*t') = 0 then ff else squarefree'_aux t

def squarefree' : ℕ → bool
| 0 := ff
| 1 := ff
| n := squarefree'_aux n n

lemma squarefree_iff_squarefree' (n : ℕ) :
  squarefree n ↔ squarefree' n := sorry

instance foo {n : ℕ} : decidable (squarefree n) :=
begin
  refine if hs : squarefree' n then _ else _,
  apply is_true, rw squarefree_iff_squarefree', assumption,
  apply is_false, rw squarefree_iff_squarefree', assumption,
end

example : ¬ squarefree 1 := dec_trivial -- works
example : squarefree 37 := dec_trivial -- works

[Yaël Dillies]

Can't you use docs#decidable_of_iff' to shorten foo?

[Kyle Miller]

I thought when I'd tried that the examples got stuck, but I guess that works too. (I wrote it in a way where I could be sure it definitely wouldn't get stuck, since this isn't so fun to debug :smile:). Replaced in code block

[Yaël Dillies]

I think decidable_of_iff and decidable_of_iff' were explicitly designed not to get stuck.

[Kyle Miller]

I wonder how you can write factors to be similarly efficient but still not get stuck. Maybe you can have an auxiliary function that you give "gas" (i.e., the number of recursive steps it will ever apply), and you can estimate how much gas you'll ever need? For example, factors won't ever give more factors than n, so that can serve as the gas to power the recursion. (And of course nat.min_fac uses well-founded recursion, too...)

[Kevin Wilson]

I'd be curious if there is, because by attempts at proving this squarefree number asymptotic seems to keep getting stymied at dec_trivials that seemingly get stuck on things like squarefree and factors and divisors.

[Alex J. Best]

If you are trying to prove an asymptotic dec_trivial likely won't be too helpful anyway, its just a way of forcing lean to evaluate closed expressions. So its useful to do small calculations when a problem is inherently finite, but will not be able to really prove much more than that. Where are you stuck exactly?

[Kevin Wilson]

There's a lot of induction lying around in proving some rearrangement equals some other rearrangement. So the base cases end up looking like needing to prove f 1 = 1. I can type #eval f 1 and it shows me 1. Writing it out by hand is, well, quite nightmarish!

[Yaël Dillies]

Also I must tell you that you probably didn't pick the easiest problem to start with!

[Kevin Wilson]

Gotta challenge yourself! :-)

[Yaël Dillies]

(we don't even have the Zeta function)

[Kevin Wilson]

But I'm definitely realizing that!

[Kevin Wilson]

Conveniently, the standard proof doesn't directly use the zeta function. But it does involve proving things like $\sum_{d^2 \mid n} \mu(d) = 1$ if and only if $n$ is squarefree.

[Kevin Wilson]

And that proof essentially goes: a) prove that function is multiplicative; b) prove it for prime powers. I saw there were arithmetic_functions, moebius, and even the notion of a multiplicative arithmetic function, so I figured at least the foundation is there!

[Alex J. Best]

Ok dec_trivial could be helpful but maybe another good way when the definitions are a bit more complicated is to coax tactic#norm_num into unfolding the right things and evaluating them (normally this involves passing it extra function names / lemmas, like for simp, so that it rewrites the right things until it gets to a point it can actually do the calculation)

[Kyle Miller]

@Kevin Wilson Did you finish the proof in your first post? I took a stab at it and got through mostly with simp, ext, norm_num, and interval_cases.

import algebra.squarefree
import tactic

noncomputable theory
open_locale classical

def set_squarefree_le_x (N : ℕ): finset ℕ := finset.filter squarefree (finset.range (N + 1))

lemma sq_1_eq_1 : finset.card (set_squarefree_le_x 1) = 1 :=
begin
  unfold set_squarefree_le_x,
  rw finset.card_eq_succ,
  use 1,
  use ∅,
  split,
  simp,
  simp,
  ext,
  simp,
  split,
  rintro rfl,
  simp,
  rintro ⟨ha, hsf⟩,
  norm_num at ha,
  interval_cases a,
  simpa using hsf,
end

[Kyle Miller]

With a somewhat cleaned-up proof (I squeeze_simped to fix non-terminal simps, and I added braces for goals):

lemma sq_1_eq_1 : finset.card (set_squarefree_le_x 1) = 1 :=
begin
  unfold set_squarefree_le_x,
  rw finset.card_eq_succ,
  use [1, ∅],
  simp only [true_and, finset.not_mem_empty, insert_emptyc_eq, finset.card_empty, and_true,
    eq_self_iff_true, not_false_iff],
  ext a,
  simp only [finset.mem_singleton, finset.mem_filter, finset.mem_range],
  split,
  { rintro rfl,
    simp, },
  { rintro ⟨ha, hsf⟩,
    norm_num at ha,
    interval_cases a,
    simpa using hsf, },
end

[Johan Commelin]

(Aside @Kevin Wilson: on zulip you can write latex/math using double dollars: $$a^2 + b^2 \in \mathbb R$$ yields $a^2 + b^2 \in \mathbb R$.)

[Johan Commelin]

Alex J. Best said:

Ok dec_trivial could be helpful but maybe another good way when the definitions are a bit more complicated is to coax tactic#norm_num into unfolding the right things and evaluating them (normally this involves passing it extra function names / lemmas, like for simp, so that it rewrites the right things until it gets to a point it can actually do the calculation)

I guess norm_num doesn't know what to do with square_free as of today, right?

[Kevin Wilson]

That is correct :-)

[Kevin Wilson]

@Kyle Miller I did finish a proof, but it was quite a bit longer. I hadn't come across the ext tactic, which does make this a lot easier! I ended up with several auxiliary lemmas whose purpose was essentially to get me ext

[Alex J. Best]

Here's a slightly different version, but still annoyingly long to be honest

lemma sq_1_eq_1 : finset.card (set_squarefree_le_x 1) = 1 :=
begin
  unfold set_squarefree_le_x,
  have : finset.filter squarefree (finset.range (1 + 1)) = {1},
  { ext a,
    norm_num,
    split,
    { rintros ⟨h, hh⟩,
      interval_cases a, -- reorders goals?
      simpa using hh, },
    { simp {contextual := tt}, } },
  rw this,
  apply finset.card_singleton,
end

[Alex J. Best]

And for a bit of fun I wrote a different decidable instance for squarefree, its also trial division I suppose, I just approach the setup a bit differently

import algebra.squarefree

instance nat.decidable_is_unit : decidable_pred (@is_unit ℕ _) :=
begin
  intro x,
  exact decidable_of_iff _ nat.is_unit_iff.symm,
end

instance nat_sq : decidable_pred (λ x : ℕ, squarefree x) :=
begin
  intro n,
  by_cases hz : n = 0,
  { simp only [hz, not_squarefree_zero],
    exact decidable.false, },
  have : squarefree n ↔ (∀ x, x ≤ n → x * x ∣ n → is_unit x),
  { rw squarefree,
    apply forall_congr,
    intro x,
    split; intros hx,
    { intro h,
      exact hx, },
    intro h,
    apply hx _ h,
    have hl : x * x ≤ n,
    exact nat.le_of_dvd (zero_lt_iff.mpr hz) h,
    have : 1 ≤ x,
    { by_contra hn,
      simp only [not_le, nat.lt_one_iff] at hn,
      apply hz,
      simpa [hn] using h, },
    have h' : x * 1 ≤ x * x,
    refine mul_le_mul' (le_refl x) this,
    rw [mul_one] at h',
    exact h'.trans hl, },
  exact decidable_of_iff _ this.symm,
end

example : squarefree 130 := dec_trivial

[Mario Carneiro]

Johan Commelin said:

I guess norm_num doesn't know what to do with square_free as of today, right?

Already on the case

[Kevin Wilson]

This is very cool! Thank you for the intro to all the internals as well!

[Mario Carneiro]

#11666

[Mario Carneiro]

And here's an application to use norm_num to sum up all the squarefrees up to a bound:

import algebra.squarefree

example : ((list.range 50).map squarefree).count true = 31 :=
by norm_num [list.range, list.range_core]

I had to write it in a slightly funny way because this is just relying on simp to simplify the list stuff, there isn't any custom evaluation code for it. It also doesn't seem be be able to handle very large numbers; there are much better algorithms for calculating the sum of squarefrees up to a bound than just expanding out the list and simplifying.

[Mario Carneiro]

The actual underlying algorithm seems to be able to handle pretty large numbers so I guess it is the surrounding simp stuff that is expensive

example : squarefree 99302206 := by norm_num

[Kevin Wilson]

So I finished my goal: the "usual" proof on the asymptotics of squarefree numbers. https://github.com/khwilson/squarefree_asymptotics

It turned out to be quite long, but I'd love to record my experiences somewhere at least as a tutorial for others. And I'd love any comments on how this could have been done better. Indeed, I think my biggest conundrum was that it was hard to find good examples of "how to approach an integral problem" or "how to prove that two functions differ on a set of measure 0."

Thanks again for all the early help!

[Yaël Dillies]

Wow, that's amazing!

[Yaël Dillies]

cc @Bhavik Mehta

[Yaël Dillies]

(we were originally a bit sorry for you that you had chosen such a hard item)

[Kevin Wilson]

Never underestimate the power of "doing things while watching Downton Abbey [or your preferred mindless television show]" :-)

[Riccardo Brasca]

Congratulations!! A good way to get feedback is to try to PR what you proved.

You can start with some preliminary lemmas (try to open several short PRs rather than a big one).

[Sebastien Gouezel]

I was having a look at the readme on your page, and I see there that you are asking if there is a good way of formalising the notion of "for sufficiently large parameters, ...". The answer is that we are already using this a lot, and this is called filters. You can grep the library for ∀ᶠ.*in at_top to see how it is used.

[Kevin Wilson]

@Riccardo Brasca great idea! Do you have a recommendation for a PR that was good in your opinion? Especially for PRs that depend on each other? (Always a problem in software!)

@Sebastien Gouezel Yeah with the filters, I spent a lot of time in the code and in the docs trying to find good examples and I couldn’t quite figure out how to put it altogether, at least in an elegant way. Hence the notes at the bottom that I couldn’t quite grok them or how to prove that two sets differ on a set of measure 0 😅

If you have a favorite example, I’d love a pointer!

Thanks again!

[Riccardo Brasca]

You can just open one or two PR with the basic material (mentioning what the final goal is), and once they are accepted you can remove the result from your repository. There is no need to PR everything at the same time, especially if this means a lot of dependent PR.

[Kyle Miller]

I briefly looked at general.lean to see if there were a lemma or two that could be a small PR, but I got sidetracked with one_le_of_ne_zero, since it seemed like it just had to be in mathlib already in some form. If you do

lemma one_le_of_ne_zero {m : ℕ} : 1 ≤ m ↔ m ≠ 0 := by library_search

it gives nat.one_le_iff_ne_zero. Similarly, the lemma two_le_prime is nat.prime.two_le. I couldn't find prime_squarefree immediately by the same tactic, but searching for "prime squarefree" in the online docs turned up docs#prime.squarefree

These seem to be new:

lemma sqrt_one_eq_one : 1 = sqrt 1 := by { rw eq_sqrt, simp, linarith, }

lemma one_le_sqrt {n : ℕ} (hn : 1 ≤ n) : 1 ≤ sqrt n :=
begin
  rw sqrt_one_eq_one,
  exact sqrt_le_sqrt hn,
end

[Damiano Testa]

Btw, lemma sqrt_one_eq_one is probably more mathlib-like formulated with the equality in the opposite way:

lemma sqrt_one_eq_one : sqrt 1 = 1

The guiding principle being that the RHS should be "simpler" than the LHS.

[Damiano Testa]

Also, convert nat.sqrt_eq 1 might simplify the proof, leaving only a mul_one (untested).
docs#nat.sqrt_eq

[Yaël Dillies]

I swear sqrt 1 = 1 has to be rfl (if we're talking about docs#nat.sqrt)

[Kevin Buzzard]

well you would be wrong

[Kevin Wilson]

Thank you for the comments. I'll take a stab at migrating some of those!

One thing that was confusing to me throughout was when the naming convention called for "object notation" (e.g., prime.two_le) versus [not sure what it should be called but the opposite] notation, (e.g., two_le_prime). Never quite figured out the patter!

[Riccardo Brasca]

You can look on zulip for "not dot notation", there are quite a lot of threads, but the idea is that we like it and we try to use it.

Take for example docs#polynomial.monic.pow: it says that the power of a monic polynomial is monic, so it has as an assumption hp : p.monic. The idea of dot notation is that we can use it writing hp.pow n instead of monic.pow hp n.

[Riccardo Brasca]

But at beginning don't worry too much about this, it will be part of the review process

[Kevin Buzzard]

"not notation"

dot notation :-)

[Kevin Wilson]

Made @Kyle Miller 's changes (love small change requests that reduce code!) https://github.com/khwilson/squarefree_asymptotics/pull/1

[Kevin Wilson]

Also, I think I found prime.squarfree but everything fails to unify if you use that. I think because N isn't a monoid according to Lean? (I hit this sort of thing several times.)

[Kevin Wilson]

lemma prime_squarfree {p : ℕ} (hp : nat.prime p) : squarefree p :=
begin
  exact prime.squarefree hp,
end

[Kevin Wilson]

Leads to

[Kevin Buzzard]

Surely N is a monoid?

[Kevin Wilson]

type mismatch at application
  prime.squarefree hp
term
  hp
has type
  prime p
but is expected to have type
  @prime ℕ (@cancel_comm_monoid_with_zero.to_comm_monoid_with_zero ℕ nat.cancel_comm_monoid_with_zero) p
state:
p : ℕ,
hp : prime p
⊢ squarefree p

[Kevin Buzzard]

The issue there I suspect is that there is more than one notion of prime in play.

[Alex J. Best]

We have a bit of description of how nice dot notation can be at the end of the section https://leanprover-community.github.io/tips_and_tricks.html#avoiding-many-nested-parentheses-with- of the tips and tricks page

[Kevin Wilson]

Also, I definitely agree the dot notation is nice! I just couldn't quite grok when to use dot notation instead of the _of_ notation (and especially when to search with the dot notation instead of the _of_ notation :-) )

[Riccardo Brasca]

Yes, docs#nat.prime is not the same as docs#prime

[Riccardo Brasca]

But we surely know somewhere that they are equivalent

[Kevin Buzzard]

Can you post fully working code? I can't reproduce your error.

import data.nat.prime
import algebra.squarefree

lemma prime_squarfree {p : ℕ} (hp : nat.prime p) : squarefree p :=
begin
  exact prime.squarefree hp,
end

gives the problem I'm flagging -- nat.prime isn't the same as prime (but my error is much more sensible than yours)

[Kevin Wilson]

And @Kevin Buzzard yes, you're correct. Reading that error it definitely seems that N is a monoid! But perhaps there's some Lean magic to get it to work

[Riccardo Brasca]

docs#nat.prime_iff

[Kevin Wilson]

import algebra.squarefree

noncomputable theory
open nat
open_locale classical

lemma prime_squarfree {p : ℕ} (hp : nat.prime p) : squarefree p :=
begin
  exact prime.squarefree hp,
end

[Kevin Wilson]

@Kevin Buzzard ^^^

[Kevin Buzzard]

Oh you have open nat, yeah that makes the same error look a lot more exotic :-)

[Kevin Wilson]

Hah still not exactly sure what counts as "minimum" and how to debug :-)

[Kevin Buzzard]

lemma prime_squarfree {p : ℕ} (hp : nat.prime p) : squarefree p :=
begin
  rw nat.prime_iff at hp,
  exact prime.squarefree hp,
end

as Riccardo said. There are two primes here, and with open nat they're both called prime.

[Kevin Wilson]

Ah well that would explain that. I'm guessing nat.prime has special features that prime doesn't have?

[Kevin Buzzard]

By the way I would recommend you avoid open_locale classical, it was a "hammer" approach to decidability problems popular a few years ago; we now have far more precise tools to deal with these issues.

[Kevin Buzzard]

nat.prime and prime are simply two different things.

[Kevin Wilson]

Oh I just meant that why don't you just define nat.prime via nat.prime_iff ?

[Kevin Buzzard]

nat.prime is about naturals, prime is a far more general algebraic concept which works for commutative rings and has a different definition. This is why you need nat.prime_iff to glue the two concepts together.

[Kevin Buzzard]

It's not for me to say why definitions are as they are. Perhaps historical? nat.prime was defined by the computer scientists before we mathematicians came along telling them that there was a far more general concept of primality?

[Kevin Wilson]

Hah! "Path dependence" is almost always the answer

[Kevin Buzzard]

Yeah, it might also be that :-)

[Eric Rodriguez]

yeah, that's what happened

[Riccardo Brasca]

We changed the definition recently, didn't we? Using irreducible.

[Riccardo Brasca]

But I may be wrong

[Kevin Buzzard]

Indeed it seems that nat.prime was refactored 3 months ago in #11031

[Ruben Van de Velde]

Yeah, but it takes > 500 lines to prove that irreducible implies prime for nat

[Kevin Buzzard]

...by Ruben :-)

[Ruben Van de Velde]

We could probably turn it around, but that was more work than I wanted to take on at that point

[Eric Rodriguez]

https://github.com/leanprover-community/mathlib/blob/81a31ca4a8c0287bf0b0ce40f1a0df16543b7abe/src/data/nat/prime.lean this is the old version, which also isn't prime

[Eric Rodriguez]

there's like a zillion things in the library that are specialised for nat just so we can get the rest of the theory going, which is annoying but I guess how it has to be

[Kevin Wilson]

Gotta start somewhere :-)

[Kevin Wilson]

It would be "neat" (and very probably terrible) if there was some sort of shim overtop "CS nat" that obviated this for folks like me, but I guess if mathlib is C in this analogy, this would be asking for Python [or your even higher level language of choice]

[Kevin Wilson]

Anyway, @Kevin Buzzard removed the open_locale classical's. They showed up early due to an auxiliary function.

[Kevin Wilson]

https://github.com/khwilson/squarefree_asymptotics/pull/2

[Kevin Wilson]

Before disappearing to the day job, the contributing notice for mathlib notes that I'm supposed to "ask for write access to non-master branches of the mathlib repository." Where do I ask this question? (If it is here, I'm khwilson on github. :-) )

[Riccardo Brasca]

Let me see if I am able to do it with my phone

[Riccardo Brasca]

You should have an invitation

[Kevin Wilson]

Invitation received! Thank you!

[Kevin Buzzard]

Kevin Wilson said:

Anyway, Kevin Buzzard removed the open_locale classical's. They showed up early due to an auxiliary function.

If you need classical assumptions (e.g. decidability) in the statement of a theorem or definition, put them in explicltly; if you just need them in a proof, use the classical tactic beforehand. That's the (simplified version of the) modern mantra.

[Kevin Wilson]

Makes a lot of sense. As you can see from the start of this thread, decidability was a lot to grok early on! ("Why is this red squiggly appearing just because I wrote ite ?!?! )

[Ruben Van de Velde]

It seems like redefining nat.prime := prime might be workable after all - I'll see if I have time to work it out thus week

[Mauricio Collares]

I'd argue that nat.prime and prime are different definitions in mathematics too, as reflected in almost any number theory book (e.g., Apostol). That is, if you say "the definition of nat.prime is is really the definition for irreducible in a more general context", I think this will ring a bell for most mathematicians.

[Riccardo Brasca]

It's unfortunate that what we call a prime number in primary school is actually an irreducible element in N. But that's life I guess

[Eric Rodriguez]

Mauricio Collares said:

I'd argue that nat.prime and prime are different definitions in mathematics too, as reflected in almost any number theory book (e.g., Apostol). That is, if you say "the definition of nat.prime is is really the definition for irreducible in a more general context", I think this will ring a bell for most mathematicians.

sure, but they're equivalent, and considering we have prime.irreducible things work out pretty nicely in the general case

[Mario Carneiro]

@Kevin Buzzard said:

nat.prime is about naturals, prime is a far more general algebraic concept which works for commutative rings and has a different definition. This is why you need nat.prime_iff to glue the two concepts together.

It's not for me to say why definitions are as they are. Perhaps historical? nat.prime was defined by the computer scientists before we mathematicians came along telling them that there was a far more general concept of primality?

I very much doubt "computer science" motivations are at play here. Most likely this is something like Jeremy Avigad wanting simple proofs about primality like exists_infinite_primes to actually be comprehensible as an introductory example to first-year students. This tends not to last long before being refactored away in current mathlib, though.

[Kevin Wilson]

OK, I have started migrating various lemmas over to mathlib with some success (two PRs in!). But in the process I figured I'd try to generalize and simplify various things. Then I hit a weird issue I'm not sure how to debug. Specifically, I need the following lemma:

import order.filter
import topology.basic
import data.real.basic
import topology.instances.real
import order

noncomputable theory
open filter
open_locale topological_space

lemma real_tendsto_implies_nat_tendsto
{a : ℝ} {f : ℝ → ℝ}
(hf : filter.tendsto f at_top (𝓝 a)) :
filter.tendsto (λ (n : ℕ), f ↑n) filter.at_top (𝓝 a) :=
begin
  rw filter.tendsto_at_top',
  intros s hs,
  rw filter.tendsto_at_top' at hf,
  specialize hf s hs,
  cases hf with a ha,
  use ⌈a⌉₊,
  intros b,
  specialize ha ↑b,
  intros hb,
  have : ⌈a⌉₊ ≤ b, exact hb,
  have : a ≤ ↑b,
    calc a ≤ ↑⌈a⌉₊ : nat.le_ceil a
      ... ≤ ↑b : nat.cast_le.mpr this,
  exact ha this,
end

Of course, this should be true for basically anything where all the elements are defined, so I attempted to do the following:

import order.filter
import topology.basic
import data.real.basic
import topology.instances.real
import order

noncomputable theory
open filter
open_locale topological_space

lemma real_tendsto_implies_nat_tendsto'
  {α β : Type*}
  [nonempty α] [semilattice_sup α] [linear_ordered_semiring α]
  [topological_space β] [preorder β] [order_closed_topology β]
  {a : β} {f : α → β} (hf : tendsto f at_top (𝓝 a)) :
  tendsto (λ (n : ℕ), f ↑n) filter.at_top (𝓝 a) :=
begin
  rw filter.tendsto_at_top',
  intros s hs,
  -- Fails
  rw filter.tendsto_at_top' at hf,
  sorry,
end

This seemed odd, so I did some experimentation and it seems to be failing with a bit of a strange (to me!) error:

import order.filter
import topology.basic
import data.real.basic
import topology.instances.real
import order

noncomputable theory
open filter
open_locale topological_space

lemma real_tendsto_implies_nat_tendsto''
  {α β : Type*}
  [aa : nonempty α] [bb : semilattice_sup α] [linear_ordered_semiring α]
  [topological_space β] [preorder β] [order_closed_topology β]
  {a : β} {f : α → β} (hf : tendsto f at_top (𝓝 a)) :
  tendsto (λ (n : ℕ), f ↑n) filter.at_top (𝓝 a) :=
begin
  rw filter.tendsto_at_top',
  intros s hs,
  -- Fails with detailed error
  -- type mismatch at application
  --   tendsto_at_top'.mp hf
  -- term
  --   hf
  -- has type
  --   @tendsto α β f
  --     (@at_top α
  --       (@partial_order.to_preorder α
  --           (@ordered_cancel_add_comm_monoid.to_partial_order α
  --             (@ordered_semiring.to_ordered_cancel_add_comm_monoid α
  --                 (@linear_ordered_semiring.to_ordered_semiring α _inst_1)))))
  --     (𝓝 a)
  -- but is expected to have type
  --   @tendsto α β f (@at_top α (@partial_order.to_preorder α (@semilattice_sup.to_partial_order α bb))) (𝓝 a)
  let foo := (@filter.tendsto_at_top' α β aa bb f (𝓝 a)).mp hf,
  sorry,
end

Which I interpret as an issue that the preorder can arise either from the explicit semilattice_sup or the implicit linear_ordercoming from a linear_ordered_ring. This works fine for α = ℝ because ℝ's semilattice_sup structure explicitly comes from its linear_order structure https://leanprover-community.github.io/mathlib_docs/data/real/basic.html#real.semilattice_sup

So my question is: what's the right way to specify, "I mean things where the semilattice_sup structure comes from the linear_order structure?"

Thanks again!

[Heather Macbeth]

@Kevin Wilson To jump immediately to your original motivation:

lemma real_tendsto_implies_nat_tendsto
  {a : ℝ} {f : ℝ → ℝ}
  (hf : filter.tendsto f at_top (𝓝 a)) :
  filter.tendsto (λ (n : ℕ), f ↑n) filter.at_top (𝓝 a) :=
hf.comp tendsto_coe_nat_at_top_at_top

[Heather Macbeth]

And to answer the question you asked: linear_order implies semilattice_sup, so you can assume just the former and the latter will be silently inferred where needed.

example {α : Type*} [linear_order α] : semilattice_sup α := by apply_instance

[Kevin Wilson]

example is the keyword! Very cool :-)

As for the spoiler proof, that's amazing. Half the battle is searching for the right lemma :-)

Though, notably, the lemma I wrote supposes a linear_ordered_semiring, whereas archimedean (an assumption of tendsto_coe_nat_at_top_at_top) implies floor_ring(https://leanprover-community.github.io/mathlib_docs/algebra/order/archimedean.html#archimedean.floor_ring).

[Heather Macbeth]

@Kevin Wilson I think it's the other way, right? floor_ring implies archimedean. And the lemma tendsto_coe_nat_at_top_at_top is stated for archimedean, the weaker one, so it applies for (eg) the nonnegative reals, too.

import data.real.nnreal
import order.filter.archimedean

open_locale nnreal
open filter

example : tendsto (λ n : ℕ, (n:ℝ≥0)) at_top at_top := tendsto_coe_nat_at_top_at_top

[Yaël Dillies]

No, Heather. archimedean also noncomputably imply floor_ring.

[Kevin Buzzard]

I suspect that you can make $\mathbb{R}[X]$ into a linear ordered ring by demanding that $0<|X|$ but that $|X|<\epsilon$ for all positive $\epsilon$, and then following your nose (I didn't check this but I think I've checked it in the past). This might well be a floor_ring which is not archimedean -- something for the counterexamples folder? (there might be simpler examples)

[Kevin Buzzard]

Ridiculously, the reason I was thinking about this a few years ago was working with @Calle Sönne on decimal expansions! He started off wanting to define them for the reals, but I pointed out that it should work for the rationals, and then we started wondering exactly which rings decimal expansions should work for, and we thought that floor_rings were an excellent choice! And then realised that perhaps the decimal expansion of a number might not sum back up to the number again because of examples like this :-)

[Adam Topaz]

Kevin Buzzard said:

I suspect that you can make $\mathbb{R}[X]$ into a linear ordered ring by demanding that $0<|X|$ but that $|X|<\epsilon$ for all positive $\epsilon$, and then following your nose (I didn't check this but I think I've checked it in the past). This might well be a floor_ring which is not archimedean -- something for the counterexamples folder? (there might be simpler examples)

This would be a fun counterexample to try to construct using what we have in mathlib for model theory! Take an ultrapower of $\mathbb{R}$ w.r.t. a nonprincipal ultrafilter on $\mathbb{N}$, and let $\epsilon = (1/n)_n$ be an infinitesimal element in this ultrapower. Now prove that $\epsilon$ is transcendental over $\mathbb{R}$, etc.

[Reid Barton]

Wait I'm confused now--I think there are multiple notions of archimedean here (I mean besides the p-adic related one).

[Adam Topaz]

docs#archimedean

[Reid Barton]

I would argue this isn't the definition that most people would guess

[Yaël Dillies]

Yes, have a look at the WIkipedia page.

[Reid Barton]

but it doesn't matter for fields

[Kevin Wilson]

To @Kevin Buzzard , I think that is correct. All sorts of weird orderings on polynomial rings that Groebner bases make use of! See theorem 2.5 here and then take the floor to be the floor of the constant coefficient.

[Kevin Wilson]

Speaking of, @Heather Macbeth everything in the file with tendsto_coe_nat_at_top_at_top seems to be implied by the lemma exists_nat_ge. Now this lemma is _also_ true in a floor_semiring (just take the ceil of an element and use the Galois connection).

I don't actually use this lemma at this level of generality, but I'm happy while I'm here to swap out the lemmas in the file to use this (slightly) more general lemma. However, as @Yaël Dillies pointed out, archimedean rings are only _noncomputably_ floor_rings. I honestly do not know the implications of this for the library, so I'm also happy _not_ to do this and just use Heather's trick for my purposes!

[Junyan Xu]

Kevin Buzzard said:

I suspect that you can make $\mathbb{R}[X]$ into a linear ordered ring by demanding that $0<|X|$ but that $|X|<\epsilon$ for all positive $\epsilon$, and then following your nose

This is just the lexicographic order on R^(order_dual N) (restricted to finsupp), right?

[Heather Macbeth]

@Kevin Wilson Please go ahead! I (I'll even say "we") don't care about noncomputability at all.

[Kevin Wilson]

Hi again! I've now gotten several PRs merged, including the fact that sqrt 1 = 1 and Moebius function is multiplicative! Always amazing to be a first time contributor to a project :-)

A quick question as I continue slowly merging in these 3kloc: I still have a lot of lemmas that I couldn't find a good representation of in mathlib but which are very useful for analytic number theory. For instance, these two:

theorem integral_tendsto_of_has_deriv_at {a b : ℝ} {f f' : ℝ → ℝ}
  (hderiv : ∀ x ∈ Ici a, has_deriv_at f (f' x) x)
  (hvanish : tendsto f at_top (𝓝 b))
  (hint : ∀ (b : ℝ), b ∈ Ici a → interval_integrable f' volume a b) :
  tendsto (λ (b : ℝ), ∫ y in a..b, f' y) at_top (𝓝 (b - f a)) := ...

and its consequence:

lemma integral_rpow_tendsto_at_top (a r : ℝ) (ha : 0 < a) (hr : r < -1):
tendsto (λ (y : ℝ), ∫ (x : ℝ) in a..y, x ^ r) at_top (𝓝 (-a ^ (r + 1) / (r + 1))) := ...

My general question: What is the etiquette for figuring out _where_ a lemma should go? E.g., should I just continue posting on this now very long thread, or should I post in something like "Is there code for X?"

And a follow up: If this is the appropriate forum, where's the best place to put those above lemmas? :-)

Thanks again!

[Yaël Dillies]

A great way to figure this out is to look up the lemmas you used in the proof and see whether you can stick yours in their file.

[Kevin Wilson]

Thanks! That's been my strategy so far, but this one had me a little stumped b/c OTOH, it's basically identical to a lemma in the docs#interval_integral and OTOH, there's an entire file docs#measure_theory.ae_cover which is sort of meant to handle these things.

Is it better to "take a guess" and post a PR and discuss there, or would you all prefer a discussion on Zulip?

[Yaël Dillies]

Asking doesn't hurt :smile:

[Kevin Wilson]

:-)

[Kevin Wilson]

(Also, sorry about the docs links, was trying to figure out how exactly they worked!)

In the spirit of asking, do y'all have a preference before I make a PR for those two lemmas?

[Yaël Dillies]

Personally, no. The measure theory library is quite alien to me! Yury G. Kudryashov will have opinions, however.

[Kevin Wilson]

Excellent. I'll wait for a ruling before barging ahead on those!