Moebius Inversion on a subset of ℕ

Stream: Is there code for X?

[Arend Mellendijk]

I have two functions f g : ℕ → ℝ and a natural number S and I know that (f*ζ) n = g n for all n ∣ S, where * denotes Dirichlet convolution. I want to be able to conclude that f n = (g*μ) n for all n ∣ S, but the standard Moebius inversion results (e.g. docs#Nat.ArithmeticFunction.sum_eq_iff_sum_smul_moebius_eq) require the equalities hold for all positive n. Ideally there would be something like

theorem sum_eq_iff_sum_smul_moebius_eq' [AddCommGroup R] {f g : ℕ → R}
  (P : ℕ → Prop) (hP : ∀ m n, m ∣ n → P n → P m) :
    (∀ n : ℕ, 0 < n → P n → (∑ i in n.divisors, f i) = g n) ↔
     ∀ n : ℕ, 0 < n → P n → (∑ x : ℕ × ℕ in n.divisorsAntidiagonal, μ x.fst • g x.snd) = f n

so the condition n ∣ S could be replaced by say Squarefree n.

I do have a workaround for my application but it's a bit of a painful change of variables. Is there a better way to do this?

[Kevin Buzzard]

I can believe it's not there :-( One way to prove this would be to define new functions F and G which equal f and g on the naturals satisfying P and are 0 outside, and then applying standard Moebius inversion to F and G and then working back to f and g.

[Arend Mellendijk]

Right - what I ran into when I tried that in an ad-hoc way was that you could have (F*ζ)(2*S) ≠ 0 = G (2*S), so the result I linked doesn't directly apply. You'd need to work directly with the fact that ζ*μ=1, at which point you also have to make F and G an ArithmeticFunctionand you're just repeating the proof of docs#Nat.ArithmeticFunction.sum_eq_iff_sum_smul_moebius_eq in a slightly more general context.

[Arend Mellendijk]

Thinking about it some more, what you'd actually have to do is define F as equal to f on P and 0 outside, and define G=F*ζ. Then the standard result applies and on P we get f=F and g=G.

[Arend Mellendijk]

It works! Sadly you do have to swap the definitions of F and G going the other way, so I've had to prove both directions separately.

The code

import Mathlib.NumberTheory.ArithmeticFunction

open Finset
open scoped BigOperators Nat.ArithmeticFunction Classical

theorem sum_eq_iff_sum_smul_moebius_eq_of_prop [AddCommGroup R] {f g : ℕ → R}
  (P : ℕ → Prop) (hP : ∀ m n, m ∣ n → P n → P m) :
    (∀ n : ℕ, 0 < n → P n → (∑ i in n.divisors, f i) = g n) ↔
     ∀ n : ℕ, 0 < n → P n → (∑ x : ℕ × ℕ in n.divisorsAntidiagonal, μ x.fst • g x.snd) = f n := by
  constructor
  · intro h
    let F := fun (n:ℕ) => if P n then f n else 0
    let G := fun (n:ℕ) => (∑ i in n.divisors, F i)
    have hF : ∀n, P n → F n = f n := by
      intro n hnP; dsimp only []; rw [if_pos hnP]
    have hG : ∀n, 0<n → P n → G n = g n := by
      intro n hn hnP; dsimp only []; rw [←h n hn hnP, sum_congr rfl]
      intro d hd; rw [if_pos $ hP _ _ (Nat.dvd_of_mem_divisors hd) hnP]
    intro n hn hnP
    suffices ∑ d in n.divisors, μ (n/d) • G d = F n from by
      rw [Nat.sum_divisorsAntidiagonal' (f:= fun x y => μ x • g y), ←hF n hnP, ←this, sum_congr rfl]
      intro d hd
      rw [←hG d (Nat.pos_of_mem_divisors hd)]
      exact hP _ _ (Nat.mem_divisors.mp hd).1 hnP
    rw [←Nat.sum_divisorsAntidiagonal' (f:= fun x y => μ x • G y)]
    apply Nat.ArithmeticFunction.sum_eq_iff_sum_smul_moebius_eq.mp _ n hn
    intro _ _; rfl
  · intro h
    conv at h =>
      ext n
      rw [Nat.sum_divisorsAntidiagonal' (f:= fun x y => μ x • g y)]
    let G := fun (n:ℕ) => if P n then g n else 0
    let F := fun (n:ℕ) => ∑ d in n.divisors, μ (n/d) • G d
    have hF : ∀n, 0<n → P n → F n = f n := by
      intro n hn hnP; dsimp only []; rw [←h n hn hnP, sum_congr rfl]
      intro d hd; rw [if_pos $ hP d n (Nat.dvd_of_mem_divisors hd) hnP]
    have hG : ∀n, P n → G n = g n := by
      intro n hnP; dsimp only []; rw [if_pos hnP]
    intro n hn hnP
    suffices ∑ d in n.divisors, F d = G n from by
      rw [←hG n hnP, ←this, sum_congr rfl]
      intro d hd
      rw [←hF d (Nat.pos_of_mem_divisors hd)]
      exact hP d n (Nat.dvd_of_mem_divisors hd) hnP
    apply Nat.ArithmeticFunction.sum_eq_iff_sum_smul_moebius_eq.mpr _ n hn
    intro _ _
    rw [Nat.sum_divisorsAntidiagonal' (f:= fun x y => μ x • G y)]

[Kevin Buzzard]

Oh nice! Could I ask you to PR it to mathlib4? It's the most efficient way to get someone to review your code :-)

[Arend Mellendijk]

If someone could give me write access, sure :) My username is FLDutchmann

[Kevin Buzzard]

@maintainers

[Anne Baanen]

Invite sent!

[Arend Mellendijk]

Got it! Thank you.

[Arend Mellendijk]

Opened #5445