Rearranging and regrouping sums

Stream: new members

[Gareth Ma]

Hi. I am trying to prove the following result: Screenshot-2023-02-06-at-22.38.37.png. In short and generalising, if an arithmetic function f satisfies f(p^k) = f(p), then summing f over all prime powers is the same as summing over primes and multiplying by floor(log_p(n)). On paper it sounds simple, and it really really should be, but I swear I can't figure out how to prove it in Lean. I have spent multiple hours on this one statement :tear: Can someone help?
Here is the statement:

import data.nat.basic
import data.real.basic
import number_theory.von_mangoldt
import tactic

open real finset
open_locale nat big_operators

example {n : ℕ} : ∑ (x : ℕ) in filter nat.prime (Icc 1 n), nat.log x n • real.log ↑x
                = ∑ (a : ℕ) in filter is_prime_pow (Icc 1 n), real.log ↑(a.min_fac) :=
begin
  sorry,
end

[Eric Wieser]

Can you rearrange to an equality of logs with the sum on the inside?

[Gareth Ma]

I had an idea to partition Icc into union of disjoint sets, as then I can write sum(x in S) = sum(x in S1) +sum(x in S2) + ... And in this case, if we write filter is_prime_pow (Icc 1 n) = union of {p ^ k}, then it should work intuitively. But I cannot express this nor prove it in Lean.

[Gareth Ma]

What do you mean for that?

[Gareth Ma]

The summand on the left depends on p

[Eric Wieser]

Use the lemmas docs#real.log_prod, and docs#real.log_pow to move the real.log to the outside of both sides

[Gareth Ma]

image.png I will still have to prove this, what I think is similar in nature

[Eric Wieser]

Sure, but now all the real.logs are gone so your problem is simpler

[Eric Wieser]

You should be able to rearrange $p^k ≤N$ into $k ≤ log_p N$ somehow

[Ruben Van de Velde]

Is this the kind of $p^k \le N$ that sums over p's and k's?

[Gareth Ma]

Yes!

[Gareth Ma]

@Eric Wieser Right, let me try that, so I should write

$$p^{\lfloor \log_p N\rfloor}$$

as

$$\prod_{1 \leq i \leq \lfloor \log_p N\rfloor} p$$

And write the right hand side as you said, then they should be equal

[Ruben Van de Velde]

Once you have a product over the primes \le N on both sides, you can use... docs#finset.prod_congr

[Eric Wieser]

(deleted)

[Gareth Ma]

Thank you, I needed that :P I tried \( \), $ $ and finally ```maths :D

[Gareth Ma]

I am not sure if I made it better or worse, but I have this:

∏ (a : ℕ) in Icc 1 n, ite (is_prime_pow a) ↑(a.min_fac) 1 = ∏ (x : ℕ) in filter nat.prime (Icc 1 n), ∏ (i : ℕ) in Icc 1 (nat.log x n), ↑x

And I can't manipulate the left hand side at all. Things like simp_rw [is_prime_pow_iff_min_fac_pow_factorization_eq _] doesn't work.

[Eric Wieser]

I think you need

    have :
      (Icc 1 n).filter is_prime_pow =
        ((Icc 1 n).filter nat.prime).bUnion (λ p, (Icc 1 (nat.log p n)).image (λ k, p ^ k))

although I almost certainly made an off-by-one error

[Gareth Ma]

Oh, let me try that. It should be easy by ext and rewriting using the mem_ lemmas right

[Eric Wieser]

Here's an overall outline:

import data.nat.basic
import data.real.basic
import number_theory.von_mangoldt
import tactic

open real finset
open_locale nat big_operators

example {n : ℕ} : ∑ (x : ℕ) in filter nat.prime (Icc 1 n), nat.log x n • real.log ↑x
                = ∑ (a : ℕ) in filter is_prime_pow (Icc 1 n), real.log ↑(a.min_fac) :=
begin
  simp_rw [nsmul_eq_mul, ←real.log_pow, ←nat.cast_pow],
  rw [←real.log_prod _ _ (λ i hi, _), ←real.log_prod _ _ (λ i hi, _)],
  { congr' 1,
    simp_rw [←nat.cast_prod, nat.cast_inj],
    have :
      (Icc 1 n).filter is_prime_pow =
        ((Icc 1 n).filter nat.prime).bUnion (λ p, (Icc 1 (nat.log p n)).image (λ k, p ^ k)),
    { sorry },
    rw this,
    rw prod_bUnion,
    { congr' 1 with x,
      rw prod_image,
      { -- clean up under the sum
        sorry },
      { -- prove the image is injective
        sorry } },
    { intros i hi j hj hij,
      simp_rw [mem_coe, mem_filter] at hi hj,
      rw [function.on_fun, disjoint_left],
      -- prove the families are disjoint
      sorry } },
  { norm_cast,
    exact (nat.min_fac_pos _).ne' },
  { norm_cast,
    -- easy :)
    sorry },
end

[Gareth Ma]

Thank you so much, I will try this! I didn't know about the bUnion part and was writing your lemma as some finsupp.sum, and of course it didn't work.

[Eric Wieser]

Right, your choices here are either docs#finset.bUnion, or if you want to prove the disjointness up front, docs#finset.disj_Union

[Eric Wieser]

(similarly you can prove the injectivity up front with docs#finset.map instead of docs#finset.image)

[Gareth Ma]

I got it!! Here it is: https://github.com/grhkm21/lean/commit/4e644cf032a5a1f4063f1607a6bbb05aba582960 Around 80 lines of code for what humans would consider trivial :P I feel like I will encounter this a lot while doing number theory or combinatorics.