Hints/Suggestions

Stream: new members

[Newell Jensen]

I have been trying to prove the simple fact that a prime p less than n is less than n#, which is product of all primes less than or equal to n. Should be super straight forward one would think (and maybe it is but I haven't seen the light) and could use some guidance. I would think that I would need to use the proof that {p} is actually prime at this point somehow. Is there a more straightforward way to do this?

import Mathlib.Data.Nat.Basic
import Mathlib.Data.Nat.Prime
import Mathlib.NumberTheory.Primorial

local notation x "#" => primorial x

-- Need p ∣ n# first
--example (n : Nat) (h : 0 < n#) : p ∣ n# → p ≤ n# := Nat.le_of_dvd h

-- def primorial (n : ℕ) : ℕ :=
--   ∏ p in filter Nat.Prime (range (n + 1)), p

example (n p : Nat) (pp : Nat.Prime p) (hp : p < n) : p ∣ n# := by
  use (∏ i in Finset.filter Nat.Prime (Finset.range (n + 1)) \ {p}, i)
  unfold primorial
  sorry

[Ruben Van de Velde]

Maybe docs#finset.dvd_prod_of_mem could help

[Newell Jensen]

I actually was trying to use that earlier but didn't figure it out. Will give it another go.

[Ruben Van de Velde]

(the lean 4 version, of course. I wasn't paying enough attention)

[Kevin Buzzard]

Why not just prove n<=n#? Then you don't need anything about p at all.

[Kevin Buzzard]

Did we ever get that there's always a prime between n and 2n? There was a PR about that for ages. Then n<=n# should be easy by strong induction

[Mario Carneiro]

docs#nat.bertrand

[Kevin Buzzard]

I guess this isn't really the super straightforward approach though. You can prove that 2*2^t<=(2^t)# by induction on t>=3 or whatever using Bertrand and then n<=n# follows. But for this question the elementary approach above will work fine and probably my suggestion, whilst perhaps useful for the library, is just a distraction.

[Kevin Buzzard]

Elementary approach: I would instead prove that if p>2 is prime then 2p divides p#, then prove that if a<=b then a# divides b#. Those lemmas should see you on your way

[Kevin Buzzard]

Then if 2<p<n we have 2p divides n# so p<n#, and for 2 you just need that 6 divides 3# so 6<=n#

[Kevin Buzzard]

(0 < n# is the other thing you need)

[Kevin Buzzard]

The reason the argument is not completely trivial is that if we replace the set of prime numbers with some random infinite set X and define Xorials the same way then the result is not true, eg if X={2,5,7,...} then 3#=2 is not strictly greater than 2

[Kevin Buzzard]

Aka you say this is a simple fact but where is your rigorous paper proof? Or do you just have a proof of the form "for n large this is obvious and for n small check by hand"?

[Newell Jensen]

n# grows really fast compared to n, hence the remark.

[Newell Jensen]

I don't have much experience with Finset and so that is what was causing me some pain. Right now I am just trying to figure out how to actually show something divides the primorial. As mentioned there is dvd_prod_of_mem but that needs a proof that p is in the filtered Finset and I think I need to have an instance of that membership somehow? Now sure...still trying to figure it out.

[Mario Carneiro]

You definitely need something about there being enough primes, since if you replace the set of primes with a random other set of natural numbers it's not necessarily true

[Kevin Buzzard]

Yeah that's exactly the kind of "this is obvious so let's not write down the details" proof that you can't formalise, because formalisation involves writing down the details. My sketch above should hopefully turn into a rigorous proof which isn't hard to formalise but note that with my X example above it's also true that n# grows really fast with n. Another bad example would be X is all the primes up to 1000 and then skip all the primes up to N=10^10^10^10 and then start again with the remaining primes, then n<=n# is false for n=N-1 and you say "well obviously the primes don't look like that" and I say "yeah but that's the prime number theorem"

[Mario Carneiro]

actually the PNT doesn't even help here since it's an asymptotic statement - it is consistent with your hypothetical

[Mario Carneiro]

A number which divides a primorial is necessarily squarefree, but I don't think there is much else you can say about such numbers

[Mario Carneiro]

Your original statement sounds very simple though: p < n implies p | n# because p is one of the factors involved in the definition of n#

[Yaël Dillies]

import number_theory.primorial

open finset

example (n p : ℕ) (hp : p.prime) (hpn : p ≤ n) : p ∣ primorial n :=
dvd_prod_of_mem _ $ mem_filter.2 ⟨mem_range.2 $ nat.lt_succ_iff.2 hpn, hp⟩

[Newell Jensen]

I hope one day I can figure this stuff out as fast. Thanks, will try and digest what you did here.

[Notification Bot]

Newell Jensen has marked this topic as resolved.

[Ruben Van de Velde]

But note that p dvd n# only implies p<=n#, not immediately p<n#, which you were talking about earlier

[Newell Jensen]

Yeah I am aware of that. I was just trying to get past this hurdle at this point. Appreciate everyone's comments, thanks again.

[Mario Carneiro]

it's not hard to prove that 2 < p <= n implies 2 * p | n# by something similar to Yael's proof though

[Mario Carneiro]

and for p = 2 the claim p < n# is false

[Newell Jensen]

@Yaël Dillies the dollar sign in the middle of the angles brackets is throwing me off. My understanding is that $ is for not having to have parenthesis when you are nesting them to the right. When I do a simple substitution of "(" for the dollar signs and ")" at the very end (same amount to balance them), it isn't working.

[Notification Bot]

Newell Jensen has marked this topic as unresolved.

[Yaël Dillies]

Here's the equivalent dollar-less proof.

import number_theory.primorial

open finset

example (n p : ℕ) (hp : p.prime) (hpn : p ≤ n) : p ∣ primorial n :=
dvd_prod_of_mem _ (mem_filter.2 ⟨mem_range.2 (nat.lt_succ_iff.2 hpn), hp⟩)

Probably you tried doing dvd_prod_of_mem _ (mem_filter.2 ⟨mem_range.2 (nat.lt_succ_iff.2 hpn, hp⟩)) instead?

[Newell Jensen]

I tried that and some other variations :)

[Newell Jensen]

So how did you know dollar sign in the middle would do that? Is it because it closed off a function with an argument? Seems to be the case.

[Newell Jensen]

Seems that is how the $ works in general if that is the case. I had previously assumed it put all the end parenthesis at the very end.

[Ruben Van de Velde]

Yeah, the dollar sign is basically "function call, but wrap the rest of the expression in parentheses". Impossible to search for, sadly

[Kevin Buzzard]

Mario Carneiro said:

and for p = 2 the claim p < n# is false

The original claim is true because p < n so n>=3 so n# is a multiple of 6. But it's this sort of technical detail ("edge cases") which mathematicians are very keen to brush off as "needing no proof" and for which theorem provers demand the details. This is why I tried to come up with a more conceptual argument.

[Kevin Buzzard]

@Newell Jensen here's Yael's proof unpicked into Lean 4 tactic mode:

import Mathlib.Data.Nat.Basic
import Mathlib.Data.Nat.Prime
import Mathlib.NumberTheory.Primorial

local notation x "#" => primorial x

open Finset

example (n p : Nat) (pp : Nat.Prime p) (hp : p < n) : p ∣ n# := by
  apply dvd_prod_of_mem
  rw [mem_filter]
  refine ⟨?_, pp⟩
  rw [mem_range]
  rw [Nat.lt_succ_iff]
  exact hp.le -- dot notation trick

When I was learning I found it far easier to write the tactic mode proof first and then, if I wanted the extra exercise, I'd trasnslate it into term mode. After you get better and get the hang of the _ tricks you find that you can write the term mode proof directly.

[Newell Jensen]

@Kevin Buzzard Yes, one step at a time. I think another thing limiting me is just me not knowing mathlib as well either. Takes time. Gotta put in the work, no other way around it.

[Newell Jensen]

And yes, fully agree with you about the details. It is this very reason that I am trying to learn Lean.

[Kevin Buzzard]

You don't have to know mathlib. You just have to know the underlying philosophy of mathlib. This is a really important lesson. Got a goal of the form p ∈ range (n + 1)? Rewrite with a lemma called mem_range or mem_range_iff. It will be there. Got a goal of the form p ∈ filter Nat.Prime (range (n + 1))? Rewrite with a lemma called mem_filter. You have to trust that the lemmas you want are there, and because this is what we're striving for, they often are.