Theory Sigma

section‹Sum of divisors function›

theory Sigma
imports PerfectBasics "HOL-Library.Infinite_Set"
begin

definition divisors :: "nat ⇒ nat set" where
    "divisors m ≡ {n . n dvd m}"

abbreviation sigma :: "nat ⇒ nat" where
    "sigma m ≡ ∑ (divisors(m))"

lemma divisors_eq_dvd[iff]: "(a ∈ divisors(n)) ⟷ (a dvd n)"
  by(simp add: divisors_def)

lemma finite_divisors [simp]:
   assumes "n>0" shows "finite (divisors n)"
  by (simp add: assms divisors_def)

lemma divs_of_zero_UNIV[simp]: "divisors(0) = UNIV"
  by(auto simp add: divisors_def)

lemma sigma0[simp]: "sigma(0) = 0"
  by simp

lemma sigma1[simp]: "sigma(Suc 0) = 1"
  by (simp add: sum_eq_Suc0_iff)

lemma prime_divisors: "prime p ⟷ divisors p = {1,p} ∧ p>1"
  by (auto simp add: divisors_def prime_nat_iff)

lemma prime_imp_sigma: "prime (p::nat) ⟹ sigma(p) = p+1"
proof -
  assume "prime (p::nat)"
  hence "p>1 ∧ divisors(p) = {1,p}" by (simp add: prime_divisors)
  hence "p>1 ∧ sigma(p) = ∑ {1,p}" by (auto simp only: divisors_def)
  thus "sigma(p) = p+1" by simp
qed

lemma sigma_third_divisor:
  assumes "1 < a" "a < n" "a dvd n"
  shows "1+a+n ≤ sigma(n)"
proof -
  from assms have "{1,a,n} ≤ divisors n" 
    by auto
  hence "∑ {1,a,n} ≤ sigma n"
    by (meson ‹a < n› finite_divisors order.strict_trans1 sum_mono2 zero_le)
  with assms show ?thesis by auto
qed

proposition prime_iff_sigma: "prime n ⟷ sigma(n) = Suc n"
proof
  assume L: "sigma(n) = Suc n"
  then have "n > 1"
    using less_linear sigma1 by fastforce
  moreover
  have "m = Suc 0" if "m dvd n" "m ≠ n" for m
  proof -
    have "0 < m"
      using that by auto
    then have "¬ 1 + m + n ≤ 1 + n"
      by linarith
    then show ?thesis
      using sigma_third_divisor [of m]
      by (metis L One_nat_def Suc_lessD Suc_lessI ‹n > 1› dvd_imp_le ‹0 < m› less_le plus_1_eq_Suc that)
  qed
  then have "divisors n = {n,1}" 
    by (auto simp: divisors_def)
  ultimately show "prime n"
    by (simp add: insert_commute prime_divisors)
qed (use prime_divisors in auto)

lemma dvd_prime_power_iff:
  fixes p::nat
  assumes prime: "prime p"
  shows "{d. d dvd p^n} = (λk. p^k) ` {0..n}"
  using divides_primepow_nat prime by (auto simp add: le_imp_power_dvd)

lemma rewrite_sum_of_powers:
  assumes p: "(p::nat)>1"
  shows "∑ ((^) p ` {0..n}) = (∑ i = 0 .. n . p^i)" (is "?l = ?r")
  by (metis inj_on_def p power_inject_exp sum.reindex_cong)

lemma sum_of_powers_int: "(x - 1::int) * (∑i=0..n . x^i) = x ^ Suc n - 1"
  by (metis atLeast0AtMost lessThan_Suc_atMost power_diff_1_eq) 

lemma sum_of_powers_nat: "(x - 1::nat) * (∑i=0..n . x^i) = x ^ Suc n - 1"
   (is "?l = ?r")
proof (cases "x = 0")
  case False
  then have "int ((x - 1) * sum ((^) x) {0..n}) = int (x ^ Suc n - 1)"
    using sum_of_powers_int [of "int x" n] by (simp add: of_nat_diff)
  then show ?thesis
    using of_nat_eq_iff by blast
qed auto


theorem sigma_primepower:
  assumes "prime p"
  shows "(p - 1) * sigma(p^e) = p^(e+1) - 1"
proof -
  have "sigma(p^e) = (∑i=0..e . p^i)"
    using assms divisors_def dvd_prime_power_iff prime_nat_iff rewrite_sum_of_powers by auto
  thus "(p - 1)*sigma(p^e) = p^(e+1) - 1"
    using sum_of_powers_nat by auto
qed

proposition sigma_prime_power_two: "sigma(2^n) = 2^(n+1) - 1"
proof -
  have "(2 - 1) * sigma(2^n) = 2^(n+1) - 1"
    by (auto simp only: sigma_primepower two_is_prime_nat)
  thus ?thesis by simp
qed

lemma prodsums_eq_sumprods:
  fixes p :: nat and m :: nat
  assumes "coprime p m"
  shows "∑((λk. p^k) ` {0..n}) * sigma m = ∑{p^k * b |k b. k ≤ n ∧ b dvd m}"
    (is "?lhs = ?rhs")
proof -
  have "coprime p x" if "x dvd m" for x
    using assms by (rule coprime_imp_coprime) (auto intro: dvd_trans that)
  then have "coprime (p ^ f) x" if "x dvd m" for x f
    using that by simp
  then have "?lhs = ∑{a * b |a b. (∃f. a = p ^ f ∧ f ≤ n) ∧ b dvd m}"
    apply (subst sum_mult_sum_if_inj [OF mult_inj_if_coprime_nat]) 
       apply (force intro!: sum.cong)+
    done
  also have "... = ?rhs"
    by (blast intro: sum.cong)
  finally show ?thesis .
qed

lemma div_decomp_comp:
  fixes a::nat
  shows "coprime m n ⟹ a dvd m*n ⟷ (∃b c. a = b * c ∧ b dvd m ∧ c dvd n)"
by (auto simp only: division_decomp mult_dvd_mono)

theorem sigma_semimultiplicative:
  assumes p: "prime p" and cop: "coprime p m"
  shows "sigma (p^n) * sigma m = sigma (p^n * m)" (is "?lhs = ?rhs")
proof -
  from cop have cop2: "coprime (p^n) m"
    by simp
  from p have "?lhs = ∑((λf. p^f) ` {0..n}) * sigma m"
    using divisors_def dvd_prime_power_iff by auto
  also from cop have "... = (∑ {p^f*b| f b . f≤n ∧ b dvd m})"
    by (auto simp add: prodsums_eq_sumprods prime_nat_iff)
  also have "... = (∑ {a*b| a b . a dvd (p^n) ∧ b dvd m})"
    by (metis (no_types, opaque_lifting) le_imp_power_dvd divides_primepow_nat p)
  also have "… = ∑{c. c dvd (p^n*m)}"
    using cop2 div_decomp_comp by auto
  finally show ?thesis
    by (simp add: divisors_def)
qed

end