Zulip Chat Archive

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,
  { 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

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.

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

I'll start with reading the API on floors.

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