Theory Dirichlet_Series.Liouville_Lambda

(*
    File:      Liouville_Lambda.thy
    Author:    Manuel Eberl, TU München
*)
section ‹The Liouville $\lambda$ function›
theory Liouville_Lambda
  imports 
    "HOL-Computational_Algebra.Computational_Algebra"
    "HOL-Number_Theory.Number_Theory"
    Dirichlet_Series
    Multiplicative_Function 
    Moebius_Mu
begin

definition liouville_lambda :: "nat  'a :: comm_ring_1" where
  "liouville_lambda n = (if n = 0 then 0 else (-1) ^ size (prime_factorization n))"

interpretation liouville_lambda: completely_multiplicative_function' liouville_lambda "λ_. -1"
proof
  fix a b :: nat assume "a > 1" "b > 1"
  thus "liouville_lambda (a * b) = liouville_lambda a * liouville_lambda b"
    by (simp add: liouville_lambda_def prime_factorization_mult power_add)
qed (simp_all add: liouville_lambda_def prime_factorization_prime One_nat_def [symmetric] 
              del: One_nat_def)

lemma liouville_lambda_prime [simp]: "prime p  liouville_lambda p = -1"
  by (simp add: liouville_lambda_def prime_factorization_prime)

lemma liouville_lambda_prime_power [simp]: "prime p  liouville_lambda (p ^ k) = (-1) ^ k"
  by (simp add: liouville_lambda_def prime_factorization_prime_power)

lemma liouville_lambda_squarefree: "squarefree n  liouville_lambda n = moebius_mu n"
  by (auto simp: liouville_lambda_def moebius_mu_squarefree_eq' intro!: Nat.gr0I)

lemma power_neg_one_If: "(-1) ^ n = (if even n then 1 else -1 :: 'a :: ring_1)"
  by (induction n) (simp_all split: if_splits)

lemma liouville_lambda_power_even: 
  "n > 0  even m  liouville_lambda (n ^ m) = 1"
  by (subst liouville_lambda.power) (auto elim!: evenE simp: liouville_lambda_def power_neg_one_If)

lemma liouville_lambda_power_odd: 
  "odd m  liouville_lambda (n ^ m) = liouville_lambda n"
  by (subst liouville_lambda.power) (auto elim!: oddE simp: liouville_lambda_def power_neg_one_If)
    
lemma liouville_lambda_power:
  "liouville_lambda (n ^ m) = 
     (if n = 0  m > 0 then 0 else if even m then 1 else liouville_lambda n)"
  by (auto simp: liouville_lambda_power_even liouville_lambda_power_odd power_0_left)
                                      
interpretation squarefree: multiplicative_function' 
  "ind squarefree" "λp k. if k > 1 then 0 else 1" "λ_. 1"
proof
  fix p k :: nat assume "prime p" "k > 0"
  thus "ind squarefree (p ^ k) = (if 1 < k then 0 else 1 :: 'a)"
    by (cases "k = 1") (auto simp: squarefree_power_iff squarefree_prime ind_def)
qed (auto simp: squarefree_mult_coprime squarefree_power_iff ind_def dest: squarefree_multD 
          simp del: One_nat_def)
        

interpretation is_nth_power: multiplicative_function "ind (is_nth_power n)"
  by standard (auto simp: is_nth_power_mult_coprime_nat_iff)

interpretation is_nth_power: multiplicative_function' 
  "ind (is_nth_power n)" "λp k. if n dvd k then 1 else 0" "λ_. if n = 1 then 1 else 0"
  by standard (simp_all add: is_nth_power_prime_power_nat_iff ind_def)

interpretation is_square: multiplicative_function "ind is_square"
  by standard (auto simp: is_nth_power_mult_coprime_nat_iff)

interpretation is_square: multiplicative_function' 
  "ind is_square" "λp k. if even k then 1 else 0" "λ_. 0"
  by standard (simp_all add: is_nth_power_prime_power_nat_iff ind_def)


lemma liouville_lambda_divisors_sum:
  "(d | d dvd n. liouville_lambda d) = ind is_square n"
proof (rule multiplicative_function_eqI)
  show "multiplicative_function (λn. (d | d dvd n. liouville_lambda d))"
    by (rule liouville_lambda.multiplicative_sum_divisors)
  show "multiplicative_function (ind is_square)"
    by (rule is_nth_power.multiplicative_function_axioms)
next
  fix p k :: nat assume pk: "prime p" "k > 0"
  hence p_gt_1: "p > 1" by (simp add: prime_gt_Suc_0_nat)
  have "(d | d dvd p ^ k. liouville_lambda d) = (d(λi. p ^ i) ` {..k}. liouville_lambda d)"
    using pk by (intro sum.cong refl) (auto intro: le_imp_power_dvd simp: divides_primepow_nat)
  also from pk and p_gt_1 have " = (ik. liouville_lambda (p ^ i))"
    by (subst sum.reindex) (auto simp: inj_on_def prime_gt_1_nat)
  also from pk have " = (ik. (-1) ^ i)" by (intro sum.cong refl) simp
  also have " = (if even k then 1 else 0)" by (induction k) auto
  also from pk have " = ind is_square (p ^ k)" by (simp add: is_square.prime_power)
  finally show "(d | d dvd p ^ k. liouville_lambda d) = ind is_square (p ^ k)" .
qed

lemma fds_liouville_lambda_times_zeta: "fds liouville_lambda * fds_zeta = fds_ind is_square"
  by (rule fds_eqI) (simp add: liouville_lambda_divisors_sum fds_nth_mult dirichlet_prod_def)

lemma fds_liouville_lambda: "fds liouville_lambda = fds_ind is_square * fds moebius_mu"
proof -
  have "fds liouville_lambda * fds_zeta * fds moebius_mu = fds_ind is_square * fds moebius_mu"
    by (simp add: fds_liouville_lambda_times_zeta)
  also have "fds liouville_lambda * fds_zeta * fds moebius_mu = fds liouville_lambda"
    by (simp only: mult.assoc fds_zeta_times_moebius_mu mult_1_right)
  finally show ?thesis .
qed

lemma liouville_lambda_altdef:
  "liouville_lambda n = (d | d ^ 2 dvd n. moebius_mu (n div d ^ 2))"
proof (cases "n = 0")
  case False
  have "liouville_lambda n = fds_nth (fds liouville_lambda) n" by (simp add: fds_nth_fds)
  also have "fds liouville_lambda = fds_ind is_square * (fds moebius_mu :: 'a fds)" 
    by (rule fds_liouville_lambda)
  also have "fds_nth  n = (d | d dvd n. ind is_square d * moebius_mu (n div d))"
    by (simp add: fds_nth_mult dirichlet_prod_def)
  also have " = (d  (λd. d^2) ` {d. d ^ 2 dvd n}. moebius_mu (n div d))" using False
    by (intro sum.mono_neutral_cong_right) (auto simp: ind_def is_nth_power_def)
  also have " = (d | d ^ 2 dvd n. moebius_mu (n div d ^ 2))"
    by (subst sum.reindex) (auto simp: inj_on_def dest: power2_eq_imp_eq)
  finally show ?thesis .
qed auto

lemma abs_moebius_mu: "abs (moebius_mu n :: 'a :: linordered_idom) = ind squarefree n"
  by (auto simp: ind_def moebius_mu_def)

end