## Stream: maths

### Topic: Correct phrasing of a function

#### Patrick Stevens (May 19 2020 at 20:22):

I'm following the proof of Bertrand's postulate at page 40 of https://tartarus.org/gareth/maths/notes/ii/Number_Theory_2011.pdf, and it involves the following three lemmas.

import data.nat.prime
import data.nat.choose
import ring_theory.multiplicity
import tactic

open_locale big_operators

-- The multiplicity of p in 2n choose n
def α (n : nat) (pos : 0 < n) (p : nat) (is_prime : nat.prime p) : nat :=
let not_one : p ≠ 1 := nat.prime.ne_one is_prime in
let pos : 0 < nat.choose (2 * n) n := nat.choose_pos (by linarith) in
let fin : multiplicity.finite p (nat.choose (2 * n) n) :=
(@multiplicity.finite_nat_iff p (nat.choose (2 * n) n)).2 ⟨not_one, pos⟩ in
(multiplicity p (nat.choose (2 * n) n)).get (multiplicity.finite_iff_dom.1 fin)

lemma claim_1
(p : nat)
(is_prime : nat.prime p)
(n : nat)
(n_big : 3 < n)
: pow p (α n (by linarith) p is_prime) ≤ 2 * n
:= by sorry

lemma claim_2
(p : nat)
(is_prime : nat.prime p)
(n : nat)
(n_big : 3 < n)
(smallish : (2 * n) < p ^ 2)
: (α n (by linarith) p is_prime) ∈ ({0, 1} : finset ℕ)
:= by sorry

lemma claim_3
(p : nat)
(is_prime : nat.prime p)
(n : nat)
(n_big : 3 < n)
(biggish : 2 * n < 3 * p)
: α n (by linarith) p is_prime = 1
:= by sorry


My question is: have I chosen a formulation of α that will make this job at all possible? I have a horrible feeling that by hiding away the use of multiplicity, I'll stop being able to deduce things about the behaviour of α; but I do want to make sure I don't have to keep re-proving that the multiplicity is noninfinite, because that's just a bit painful. What's likely to be the smoothest path to victory?

#### Kevin Buzzard (May 19 2020 at 20:23):

What does "the multiplicity of p in 2n choose n" mean?

#### Kevin Buzzard (May 19 2020 at 20:23):

Do you mean what I would call the $p$-adic valuation of $\binom{2n}{n}$?

#### Patrick Stevens (May 19 2020 at 20:24):

Sorry, multiplicity is in mathlib's sense - yes

#### Patrick Stevens (May 19 2020 at 20:24):

The highest power of p dividing the binomial coefficient

#### Kevin Buzzard (May 19 2020 at 20:24):

Oh great -- I was just going to point out that mathlib already had $p$-adic valuations, but I realise that this is what you are using.

#### Reid Barton (May 19 2020 at 20:25):

It's a bit hard to understand the definition because it seems to end with an unbalanced (.

#### Patrick Stevens (May 19 2020 at 20:26):

Sorry, I seem to have dropped the parenthesis - fixed, am just checking that it's still the same text I copied out

#### Reid Barton (May 19 2020 at 20:26):

However, I would start with something like (multiplicity p (nat.choose (2 * n) n)).get \$ begin ... end and then stuff all the proofs in that Prop, where it's safe.

#### Patrick Stevens (May 19 2020 at 20:26):

What do you mean by "safe" here?

#### Kevin Buzzard (May 19 2020 at 20:27):

They're not clogging anything up

#### Reid Barton (May 19 2020 at 20:27):

I just mean you can put random garbage in a proof, and never have to worry about what it is later.

#### Kevin Buzzard (May 19 2020 at 20:27):

they are forgotten the moment they are processed, unlike the lets

#### Patrick Stevens (May 19 2020 at 20:27):

Ah, that makes sense

#### Reid Barton (May 19 2020 at 20:27):

Whereas in your current definition you have to dig through a lot of clutter to even get to the main term

#### Reid Barton (May 19 2020 at 20:27):

In practice, I think let is also not a big problem to deal with

#### Reid Barton (May 19 2020 at 20:28):

However, stuffing those in the proof is more obviously fine

Last updated: May 19 2021 at 02:10 UTC