Rearranging sums

Stream: mathlib4

[Gareth Ma]

Hi, I am trying to do some proofs that require rearranging sums, but I have no idea how to start. Can someone please demonstrate how to prove this for example?

import Mathlib.Data.Nat.Interval
import Mathlib.NumberTheory.ArithmeticFunction

open Nat Finset ArithmeticFunction BigOperators

example (f : ℕ → ℕ) : ∑ n in Icc 1 x, ∑ d in n.divisors, f d = ∑ d in Icc 1 x, f d * (x / d) := by
  sorry

The mathematical idea is that $\sum_{n = 1}^x \sum_{d \mid n} f(d) = \sum_{d = 1}^x \sum_{n = 1, d \mid n}^x f(d) \stackrel{n = dn'}{=} \sum_{d = 1}^x \sum_{n' = 1}^{\lfloor x / d \rfloor} f(d) = \sum_{d = 1}^x f(d) \lfloor \frac{x}{d} \rfloor$

[Gareth Ma]

I found sum_partition which intuitively seems to be what I want, since rearranging sums = repartitioning the sets of $\{(n_i, d_i)\}$ we are considering, but I can't figure out how to use it

[Gareth Ma]

Another one I need help with is

example (f : ℕ → ℕ → ℕ) : ∑ i in Icc 1 x, ∑ j in Icc 1 i, f i j = ∑ j in Icc 1 x, ∑ i in Icc j x, f i j := by
  sorry

[Gareth Ma]

Thanks in advance

[Gareth Ma]

Ahh the second one can be done like this:

example (f : ℕ → ℕ → ℕ) : ∑ i in Icc 1 x, ∑ j in Icc 1 i, f i j = ∑ j in Icc 1 x, ∑ i in Icc j x, f i j := by
  refine sum_comm' ?_
  /- The rest is proving ⊢ a ∈ Icc 1 x ∧ b ∈ Icc 1 a ↔ a ∈ Icc b x ∧ b ∈ Icc 1 x -/
  intro a b
  constructor
  all_goals
    intro ⟨h1, h3⟩
    let ⟨h1, h2⟩ := mem_Icc.mp h1
    let ⟨h3, h4⟩ := mem_Icc.mp h3
    constructor
  all_goals
    rw [mem_Icc]
    constructor
  all_goals
    linarith

[Gareth Ma]

Ahh I proved the first one too.

example (f : ℕ → ℕ) : ∑ n in Icc 1 x, ∑ d in n.divisors, f d = ∑ d in Icc 1 x, f d * (x / d) := by
  have : ∀ n d, n ∈ Icc 1 x ∧ d ∈ n.divisors ↔ n ∈ (Icc 1 x).filter (fun a ↦ d ∣ a) ∧ d ∈ Icc 1 x := by
    intro n d
    constructor <;> intro ⟨h₁, h₂⟩
    · rw [mem_divisors] at h₂
      constructor
      · exact mem_filter.mpr ⟨h₁, h₂.left⟩
      · rw [mem_Icc] ; constructor
        · exact one_le_iff_ne_zero.mpr $ ne_zero_of_dvd_ne_zero h₂.right h₂.left
        · rw [mem_Icc] at h₁
          exact le_trans (le_of_dvd h₁.left h₂.left) h₁.right
    · rw [mem_filter] at h₁
      exact ⟨h₁.left, mem_divisors.mpr ⟨h₁.right, one_le_iff_ne_zero.mp (mem_Icc.mp h₁.left).left⟩⟩
  rw [sum_comm' this, Icc_succ_left]
  /- congr ext is not required, but it needs simp_rw which is slow? -/
  congr 1
  ext d
  rw [sum_const, Ioc_filter_dvd_card_eq_div, smul_eq_mul, mul_comm]

[Gareth Ma]

Hope this helps future people who search for "rearranging sums" on zulip :)

[Gareth Ma]

A more useful version:

lemma l3 (N : ℕ) (hN : N ≠ 0) :
    ∑ n in Icc 1 x, ∑ d in (n.gcd N).divisors, μ d = ∑ d in N.divisors, μ d * (x / d) := by
  have : ∀ n d, n ∈ Icc 1 x ∧ d ∈ (n.gcd N).divisors
      ↔ n ∈ (Icc 1 x).filter (fun a ↦ d ∣ a) ∧ d ∈ N.divisors := by
    intro n d
    constructor <;> intro ⟨h₁, h₂⟩
    · rw [mem_divisors] at h₂
      constructor
      · exact mem_filter.mpr ⟨h₁, (Nat.dvd_gcd_iff.mp h₂.left).left⟩
      · exact mem_divisors.mpr ⟨(Nat.dvd_gcd_iff.mp h₂.left).right, hN⟩
    · rw [mem_filter] at h₁
      constructor
      · exact h₁.left
      · apply mem_divisors.mpr
        constructor
        · exact Nat.dvd_gcd_iff.mpr ⟨h₁.right, (mem_divisors.mp h₂).left⟩
        · exact Nat.gcd_eq_zero_iff.not.mpr $ fun h ↦ hN h.right
  rw [sum_comm' this, Icc_succ_left]
  /- congr ext is not required, but it needs simp_rw which is slow? -/
  congr 1
  ext d
  rw [sum_const, Ioc_filter_dvd_card_eq_div, mul_comm]
  rfl