## Stream: maths

### Topic: Numbers in base p

#### Johan Commelin (May 18 2019 at 07:02):

I thought we had a little bit about numbers written in base p. But I can't find it. Do we have this?

#### Kevin Buzzard (May 18 2019 at 09:30):

This rings a bell. Some Imperial undergraduates were working on this stuff, and also on convergence of base p expansions, perhaps for some arbitrary floor ring. But then exams hit and nothing got PR'ed. @Calle Sönne was one of the key players, I know that.

#### Kevin Buzzard (May 18 2019 at 09:31):

https://github.com/leanprover-community/mathlib/tree/digits is something; there was definitely more than that though.

#### Calle Sönne (May 18 2019 at 11:24):

I have some more stuff, but I only locally. It contains some basic definitions of "digits" in base b in a linearly ordered floor ring and some very elementary theorems.

#### Calle Sönne (May 18 2019 at 11:25):

The only harder theorem I have proved so far is:

definition digit (b : ℕ) (r : α) (n : ℕ) := floor(r * b ^ (n+1)) - floor(r * b ^ n)*b

theorem approx {b : ℕ} (hb : 0 < b) (r : α) (n : ℕ) :
⌊(fract r * b ^ n)⌋ = finset.sum (finset.range n) (λ i, digit b r i * b ^ (n-1-i)) :=


#### Johan Commelin (May 18 2019 at 11:55):

I was wondering if we can formalise (something math-equivalent to):

import ring_theory.multiplicity

local attribute [class] nat.prime
variables (p : ℕ) [nat.prime p]

section
open multiplicity nat

lemma finite_nat_prime_iff (i : ℕ) :
finite p i ↔ i > 0 :=
begin
rw finite_nat_iff, split; intro h,
{ exact h.2 },
{ exact ⟨ne_of_gt (prime.gt_one ‹_›), h⟩ }
end

lemma finite_nat_choose_iff' (k i : ℕ) :
finite p (choose (p^k) i) ↔ (i ≤ p^k) :=
begin
rw finite_nat_iff, split; intro h,
simp only [not_le, choose_eq_zero_of_lt, not_lt_zero, *] at * },
{ split,
{ exact ne_of_gt (prime.gt_one ‹_›) },
{ exact choose_pos h } }
end

lemma multiplicity_choose_prime_pow (k i : ℕ) (ipos : i > 0) (ile : i ≤ p^k) :
(multiplicity p (choose (p^k) i)).get ((finite_nat_choose_iff' p k i).mpr ile) =
k - (multiplicity p i).get ((finite_nat_prime_iff p i).mpr ipos) :=
begin
sorry
end

end


#### Reid Barton (May 18 2019 at 12:12):

The underlying fact here is that ${a \choose b}$ is exactly divisible by $p^r$ where $r$ is the number of borrows when calculating $a - b$ in base $p$. That might be a bit tricky to formalize.
Another useful consequence of this is that $\gcd\{{n \choose 1}, {n \choose 2}, \ldots, {n \choose n-1}\}$ is $p$ if $n$ is a prime power $n = p^k$ and 1 otherwise.

#### Johan Commelin (May 18 2019 at 12:18):

Right, so we need to formalise the number of borrows...

#### Reid Barton (May 18 2019 at 20:51):

Maybe the easiest way is not to talk about digits at all but just the floor of a over p^n

#### Reid Barton (May 18 2019 at 20:51):

Because that is what appears in the formula for the number of times p divides n! anyways

#### Reid Barton (May 18 2019 at 20:52):

And defining "borrowing" sounds more complicated than is really necessary for the things we want to prove

#### Johan Commelin (May 23 2019 at 18:08):

@Reid Barton Did you by any chance try anything in this direction?

#### Reid Barton (May 23 2019 at 18:09):

Haven't tried anything like this yet but I was on phone at the time and I could explain what I had in mind in more detail.

#### Johan Commelin (May 23 2019 at 18:09):

Ok, that would also be nice (-;

#### Reid Barton (May 23 2019 at 18:11):

These facts ultimately rely on the calculation that $p$ divides $n!$ exactly $\sum_{i \ge 1} \lfloor n/p^i \rfloor$ times. The borrowing/carrying formulation amounts to the observation that the sum a+b has a carry into the ith place exactly when $\lfloor (a+b)/p^i \rfloor - (\lfloor a/p^i \rfloor + \lfloor b/p^i \rfloor)$ is one (and not zero).

#### Reid Barton (May 23 2019 at 18:12):

I think we already have a decent API for dealing with floors and divisibility so it's probably easier for formalization to avoid the language of carries/borrows and just work with these floor formulas directly.

#### Reid Barton (May 23 2019 at 18:14):

For example to find the power of $p$ that divides ${p^i \choose k}$ we need to know how many of these floor differences are 1 and for that we can just write $k = p^r a$ and argue directly about which ones are 1 and which are 0.

#### Johan Commelin (May 23 2019 at 18:17):

Ok, sounds like a nice plan.

#### Johan Commelin (May 23 2019 at 18:21):

Still, the proof of $v_p(n!) = \sum_{i \ge 1} \lfloor n/p^i \rfloor$ seems quite nontrivial to formalise.

#### Mario Carneiro (May 23 2019 at 22:54):

I think I have that in metamath somewhere

#### Mario Carneiro (May 23 2019 at 22:55):

http://us2.metamath.org/mpeuni/pcfac.html

#### Reid Barton (May 23 2019 at 22:58):

Interesting to see how you wrote the infinite sum. When I was thinking about this earlier I wondered if it would be sensible to introduce a "for all sufficiently large M" quantifier. This is similar, but with an explicit bound

#### Mario Carneiro (May 23 2019 at 23:00):

it helps to know the sum actually stops at n

#### Reid Barton (May 23 2019 at 23:00):

I guess you would want to know at a use site that the absent terms are all zero

#### Reid Barton (May 23 2019 at 23:00):

is there another reason the specific bound is important?

#### Mario Carneiro (May 23 2019 at 23:01):

it's short and a nat

#### Mario Carneiro (May 23 2019 at 23:01):

I think that's the main reason

#### Reid Barton (May 23 2019 at 23:01):

You could also define this function by well-founded recursion but I don't know if that's better for any purpose

#### Reid Barton (May 23 2019 at 23:02):

v n = n/p + v (n/p)

#### Mario Carneiro (May 23 2019 at 23:02):

I don't think I ever need details about the higher terms later

#### Mario Carneiro (May 23 2019 at 23:02):

(This came up as part of bertrand's postulate btw)

#### Mario Carneiro (May 23 2019 at 23:03):

The fact that this adds up to the full v_p(n!) is enough

#### Reid Barton (May 23 2019 at 23:03):

I was just working that out by following the "used by" links... "central binomial coefficients? oh I know where this is going"

#### Reid Barton (May 23 2019 at 23:04):

By the way, @Johan Commelin if you don't need this urgently, it could also make a good wishlist project

#### Reid Barton (May 23 2019 at 23:06):

I forget, how hard is the rest of the proof of Bertrand's postulate?

pretty elaborate

#### Mario Carneiro (May 23 2019 at 23:09):

There is a nice proof on wikipedia that I put there when I was working on it

#### Mario Carneiro (May 23 2019 at 23:10):

(in maths it's only half a page but there is a lot of set up)

#### Mario Carneiro (May 23 2019 at 23:12):

crap, wikipedia deleted it

#### Mario Carneiro (May 23 2019 at 23:13):

well it's still pretty good https://en.wikipedia.org/wiki/Proof_of_Bertrand's_postulate

#### Mario Carneiro (May 23 2019 at 23:59):

apparently the section was too "technical"

#### Mario Carneiro (May 24 2019 at 00:00):

this is why being a formalizer in a room of mathematicians is hard

Last updated: May 10 2021 at 06:13 UTC