Zulip Chat Archive

Stream: maths

Topic: Numbers in base p


view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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)) :=

view this post on Zulip 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,
  { by_contradiction H, cases 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

view this post on Zulip Reid Barton (May 18 2019 at 12:12):

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

view this post on Zulip Johan Commelin (May 18 2019 at 12:18):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Johan Commelin (May 23 2019 at 18:08):

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

view this post on Zulip 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.

view this post on Zulip Johan Commelin (May 23 2019 at 18:09):

Ok, that would also be nice (-;

view this post on Zulip Reid Barton (May 23 2019 at 18:11):

These facts ultimately rely on the calculation that pp divides n!n! exactly i1n/pi\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 (a+b)/pi(a/pi+b/pi)\lfloor (a+b)/p^i \rfloor - (\lfloor a/p^i \rfloor + \lfloor b/p^i \rfloor) is one (and not zero).

view this post on Zulip 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.

view this post on Zulip Reid Barton (May 23 2019 at 18:14):

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

view this post on Zulip Johan Commelin (May 23 2019 at 18:17):

Ok, sounds like a nice plan.

view this post on Zulip Johan Commelin (May 23 2019 at 18:21):

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

view this post on Zulip Johan Commelin (May 23 2019 at 18:21):

I'll start with reading the API on floors.

view this post on Zulip Mario Carneiro (May 23 2019 at 22:54):

I think I have that in metamath somewhere

view this post on Zulip Mario Carneiro (May 23 2019 at 22:55):

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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (May 23 2019 at 23:00):

it helps to know the sum actually stops at n

view this post on Zulip 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

view this post on Zulip Reid Barton (May 23 2019 at 23:00):

is there another reason the specific bound is important?

view this post on Zulip Mario Carneiro (May 23 2019 at 23:01):

it's short and a nat

view this post on Zulip Mario Carneiro (May 23 2019 at 23:01):

I think that's the main reason

view this post on Zulip 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

view this post on Zulip Reid Barton (May 23 2019 at 23:02):

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

view this post on Zulip Mario Carneiro (May 23 2019 at 23:02):

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

view this post on Zulip Mario Carneiro (May 23 2019 at 23:02):

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

view this post on Zulip Mario Carneiro (May 23 2019 at 23:03):

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

view this post on Zulip 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"

view this post on Zulip 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

view this post on Zulip Reid Barton (May 23 2019 at 23:06):

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

view this post on Zulip Mario Carneiro (May 23 2019 at 23:09):

pretty elaborate

view this post on Zulip 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

view this post on Zulip Mario Carneiro (May 23 2019 at 23:10):

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

view this post on Zulip Mario Carneiro (May 23 2019 at 23:12):

crap, wikipedia deleted it

view this post on Zulip Mario Carneiro (May 23 2019 at 23:13):

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

view this post on Zulip Mario Carneiro (May 23 2019 at 23:59):

apparently the section was too "technical"

view this post on Zulip 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