Source indexedtheorem · leanprover/lean4:v4.32.0

Aux.conv_lambda_sq_larger_sum

PrimeNumberTheoremAnd.Mathlib.NumberTheory.Sieve.AuxResults · PrimeNumberTheoremAnd/Mathlib/NumberTheory/Sieve/AuxResults.lean:42 to 59

Mathematical statement

Exact Lean statement

theorem conv_lambda_sq_larger_sum (f : ℕ → ℕ → ℕ → ℝ) (n : ℕ) :
    (∑ d ∈ n.divisors,
        ∑ d1 ∈ d.divisors,
          ∑ d2 ∈ d.divisors, if d = Nat.lcm d1 d2 then f d1 d2 d else 0) =
      ∑ d ∈ n.divisors,
        ∑ d1 ∈ n.divisors,
          ∑ d2 ∈ n.divisors, if d = Nat.lcm d1 d2 then f d1 d2 d else 0

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

theorem conv_lambda_sq_larger_sum (f : ℕ → ℕ → ℕ → ℝ) (n : ℕ) :    (∑ d ∈ n.divisors,        ∑ d1 ∈ d.divisors,          ∑ d2 ∈ d.divisors, if d = Nat.lcm d1 d2 then f d1 d2 d else 0) =      ∑ d ∈ n.divisors,        ∑ d1 ∈ n.divisors,          ∑ d2 ∈ n.divisors, if d = Nat.lcm d1 d2 then f d1 d2 d else 0 := by  apply sum_congr rfl; intro d hd  rw [mem_divisors] at hd  simp_rw [←Nat.divisors_filter_dvd_of_dvd hd.2 hd.1, sum_filter, ←ite_and, ite_sum_zero,    ←ite_and]  congr with d1  congr with d2  congr  rw [eq_iff_iff]  refine ⟨fun ⟨_, _, h⟩ ↦ h, ?_⟩  rintro rfl  exact ⟨Nat.dvd_lcm_left d1 d2, Nat.dvd_lcm_right d1 d2, rfl⟩