Generalisation of "even part" and "odd part"?

Stream: maths

[Stuart Presnell]

If we have n = 2^k * n' where n' is odd, we might call 2^k and n' the "even part" and "odd part" of n respectively. Is there standard terminology for the generalisation of this to arbitrary prime p (when we have n = p^k * n' for n' not divisible by p)?

[Andrew Yang]

The k is called the p-adic valuation of n.

[Stuart Presnell]

For context, I'm interested in proving generalisations of the lemmas at the beginning of @Bolton Bailey and @Sean Golinski's #12254

[Eric Rodriguez]

in some ways this is just docs#nat.pow_factorization_dvd

[Stuart Presnell]

Indeed, the idea would be to re-phrase lemmas like docs#nat.pow_factorization_dvd, docs#nat.prime.pow_dvd_iff_dvd_pow_factorization and docs#nat.not_dvd_div_pow_factorization, and also to prove general versions of mul_two_power_part and mul_odd_part from #12254. So it would be nice to have some more concise notation for p ^ n.factorization p and n / p ^ n.factorization p.

[Andrew Yang]

I would use nat.pow_vp or nat.inv_vp_norm (nat.inv_val_norm?) for $p^{v_p(n)}$, but I am not aware if there is a standard name for this object.

[Stuart Presnell]

I'm having a basic difficulty in getting this to work as I'd like. A simplified #mwe:

import data.nat.factorization.basic

open nat

@[reducible]
def even_part (n : ℕ) := 2 ^ n.factorization 2

lemma pow_factorization_dvd (n : ℕ) : even_part n ∣ n :=
begin
  rw [even_part],  -- if this is commented out, the next line fails
  rw [←factors_count_eq],
  sorry,
end

I'd like to be able to write lemmas in terms of even_part (or, in reality, in terms of the generalisation to arbitrary p), but in a way that makes this name transparent to Lean. I thought making the definition reducible would do this, but the above #mwe shows that it doesn't: when the goal is even_part n ∣ n , docs#nat.factors_count_eq can't find a match for n.factorization p.

I've also tried changing the @[reducible] def to abbreviation, but that also doesn't work. Is there any way to get what I want?

[Stuart Presnell]

Specifically, what I want is to be able to write even_part n in theorem statements etc. and for Lean to treat this as if I'd written 2 ^ n.factorization 2. But I don't want to have to explicitly unfold or rewrite even_part, or make a simp lemma that automatically rewrites it away, since that voids the purpose of having the notation.

[Sebastien Gouezel]

Can you use notation?

[Stuart Presnell]

Ah, yes, notation `even_part` n := 2 ^ (nat.factorization n 2) works! Thanks!

[Stuart Presnell]

Oh, except that it immediately gets rewritten to 2 ^ (nat.factorization n 2) in the goal of the lemma, which I was hoping to avoid.

[Sebastien Gouezel]

That's strange, normally notation is also used in the goal view.

[Stuart Presnell]

import data.nat.factorization.basic

open nat

notation `even_part` n := 2 ^ (nat.factorization n 2)

lemma pow_factorization_dvd' (n : ℕ) : (even_part n) ∣ n :=
begin
  -- At this point the goal is ` 2 ^ (n.factorization) 2 ∣ n`
  rw [←factors_count_eq],  -- and hence this rewrite works
  sorry,
end

[Kyle Miller]

docs#nat.factorization gives a docs#finsupp, so there's a has_coe_to_fun coercion in there. I've found that pretty printing notation that involves a coercion like that tends to be unreliable.

[Ruben Van de Velde]

Not sure if it's relevant to what you're doing, but I did some work with the even and odd parts of factorisation over here: https://github.com/Ruben-VandeVelde/flt/blob/1c4d172fa4ab02ff70da13e384b11b019ad4b58a/src/odd_prime_or_four.lean

[Stuart Presnell]

Ok, perhaps I might have to accept that any notation I define for this will be unfolded in the goal view. But I guess it would still be useful to have it to simplify lemma statements.

[Stuart Presnell]

So how do I generalise from even_part to a function of two arguments? If I write the following, I get a λ in the goal state which blocks the rw.

import data.nat.factorization.basic
open nat

notation `padic_part` := λ n p, p ^ (nat.factorization n p)

lemma pow_factorization_dvd (n p : ℕ) (hp : p.prime) : (padic_part n p) ∣ n :=
begin
  -- The goal state here is `(λ (n p : ℕ), p ^ (n.factorization) p) n p ∣ n`
  rw [←factors_count_eq],  -- and so this rewrite fails
  sorry,
end

[Stuart Presnell]

(Sorry, I'm aware that these are very elementary questions, but I can't find answers in the various documentation I've searched through.)

[Kyle Miller]

The p-adic valuation is also known as "ord":

import data.nat.factorization
open nat

notation `ord[` p `]` n:max := p ^ (nat.factorization n p)

lemma pow_factorization_dvd (n p : ℕ) (hp : p.prime) : ord[p] n ∣ n :=
begin
  -- The goal state here is `(λ (n p : ℕ), p ^ (n.factorization) p) n p ∣ n`
  rw [←factors_count_eq],  -- rewrite succeeds
  sorry,
end

[Kyle Miller]

The max precedence makes it so ord[p] is as if it were function application. One weakness of this notation is that it must be applied otherwise it's a parse error. But you can still write λ n, ord[2] n.

[Kyle Miller]

Stuart Presnell said:

Ok, perhaps I might have to accept that any notation I define for this will be unfolded in the goal view.

I hope it'll be fixed someday, so maybe it's fine if we pretend for now that it does work?

[Stuart Presnell]

Fantastic, thanks, that works nicely

[Stuart Presnell]

One odd detail is that when I put the cursor over ord in the document, the popup is:

has_pow.pow : Π {α β : Type} [self : has_pow α β], α → β → α
-------
n.factorization is the finitely supported function ℕ →₀ ℕ mapping each prime factor of n to its multiplicity in n.

Is this a bug?

[Stuart Presnell]

Also, can anyone suggest a suitable name for n / ord[p] n, the generalisation of "odd part"? I've provisionally called it coord[p] n, but that's not a good name because of the clash with coordinates.

[Stuart Presnell]

(I'm open to the answer that this should just be spelled n / ord[p] n and not given its own notation. But it might still be good to have a name for it for use in lemma names.)

[Kyle Miller]

@Stuart Presnell Sorry, I'm not sure what I was thinking, but ord[p] n should be nat.factorization n p. Maybe ord_proj[p] n for the projection onto the p part and ord_compl[p] n for the projection onto the "orthogonal complement"?

[Stuart Presnell]

Yes, I was wondering about that when I came back to look at it again this morning. Thanks for the suggestions!

[Stuart Presnell]

#15589
Thanks to everyone for your help

[David Ang]

Just curious: is it not possible to reuse the code in src/number_theory/padics/padic_val.lean ?

[Kyle Miller]

I see the p-adic valuation in there (which I think should be the same as nat.factorization, though the definition is different), but I'm not sure there's the p-part of a number

[Stuart Presnell]

docs#nat.factorization is defined as padic_val_nat p n for p.prime (and zero otherwise), in the form of a finsupp ℕ →₀ ℕ to use the extensive finsupp API.