Zulip Chat Archive

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: Dec 20 2023 at 11:08 UTC