Theory Dirichlet_Series.Euler_Products

(*
    File:      Euler_Products.thy
    Author:    Manuel Eberl, TU München
*)
section ‹Euler product expansions›
theory Euler_Products
imports 
  "HOL-Analysis.Analysis"
  Multiplicative_Function
begin

text ‹Conflicting notation from theoryHOL-Analysis.Infinite_Sum
no_notation Infinite_Sum.abs_summable_on (infixr "abs'_summable'_on" 46)

lemma prime_factors_power_subset:
  "prime_factors (x ^ n)  prime_factors x"
  by (cases "n = 0") (auto simp: prime_factors_power)

lemma prime_power_product_in_Pi:
  "(λg. p{p. p  (n::nat)  prime p}. p ^ g p)
     ({p. p  n  prime p} E UNIV) 
       {m. 0 < m  prime_factors m  {..n}}"
proof (safe, goal_cases)
  case (2 f p)
  have "prime_factors (p{p. p  n  prime p}. p ^ f p) = 
          (p{p. p  n  prime p}. prime_factors (p ^ f p))"
    by (subst prime_factors_prod) auto
  also have "  (p{p. p  n  prime p}. prime_factors p)"
    using prime_factors_power_subset by blast
  also have "  (p{p. p  n  prime p}. {p})"
    by (auto simp: prime_factors_dvd prime_gt_0_nat dest!: dvd_imp_le)
  also have "  {..n}" by auto
  finally show ?case using 2 by auto
qed (auto simp: prime_gt_0_nat)

lemma inj_prime_power: "inj_on (λx. fst x ^ snd x :: nat) ({a. prime a} × {0<..})"
proof (intro inj_onI, clarify, goal_cases)
  case (1 p m q n)
  with prime_power_eq_imp_eq[of p q m n] and 1 
    have "p = q" by auto
  moreover from this have "m = n"
    using prime_gt_1_nat 1 by auto
  ultimately show ?case by simp
qed

lemma bij_betw_prime_powers:
  "bij_betw (λg. p{p. p  n  prime p}. p ^ g p) ({p. p  n  prime p} E UNIV)
     {m. 0 < m  prime_factors m  {..(n::nat)}}"
proof (rule bij_betwI[of _ _ _ "(λm p. if p  n  prime p then multiplicity p m else undefined)"], 
         goal_cases)
  case 1
  show ?case by (rule prime_power_product_in_Pi)
next
  case 2
  show ?case
    by (auto split: if_splits)
next
  case (3 f)
  show ?case
  proof (rule ext, goal_cases)
    case (1 q)
    show ?case
    proof (cases "q  n  prime q")
      case True
      hence "multiplicity q (p{p. p  n  prime p}. p ^ f p) = 
               (x{p. p  n  prime p}. multiplicity q (x ^ f x))"
        by (subst prime_elem_multiplicity_prod_distrib) auto
      also have " = (x{p. p  n  prime p}. if x = q then f q else 0)"
        using True by (intro sum.cong refl) (auto simp: multiplicity_distinct_prime_power)
      also have " = f q" using True by auto
      finally show ?thesis using True by simp
    qed (insert 3, force+)
  qed
next
  case (4 m)
  have "(p | p  n  prime p. p ^ (if p  n  prime p then multiplicity p m else undefined)) =
          (pprime_factors m. p ^ multiplicity p m)"
  proof (rule prod.mono_neutral_cong)
    show "finite (prime_factors m)" by simp
  qed (insert 4, auto simp: prime_factors_multiplicity)
  also from 4 have " = m"
    by (intro prime_factorization_nat [symmetric]) auto
  finally show ?case .
qed
      
lemma
  fixes f :: "nat  'a :: {real_normed_field,banach,second_countable_topology}"
  assumes summable: "summable (λn. norm (f n))"
  assumes "multiplicative_function f"
  shows   abs_convergent_euler_product:
            "abs_convergent_prod (λp. if prime p then n. f (p ^ n) else 1)"
    and   euler_product_LIMSEQ:
            "(λn. (pn. if prime p then n. f (p ^ n) else 1))  (n. f n)"
proof -
  interpret f: multiplicative_function f by fact
  define N where "N = (n. norm (f n))"

  have summable': "f abs_summable_on A" for A
    by (rule abs_summable_on_subset[of _ UNIV])
       (insert summable, auto simp: abs_summable_on_nat_iff')

  have summable'': "(λx. f (p ^ x)) abs_summable_on A" if "prime p" for A p
  proof (subst abs_summable_on_reindex_iff[of _ _ f])
    from prime p have "p > 1" 
      by (rule prime_gt_1_nat)
    thus "inj_on (λi. p ^ i) A"
      by (auto simp: inj_on_def)
  qed (intro summable')

  have "(λn. norm ((m. f m) - (p{p. p  n  prime p}. i. f (p ^ i))))  0"
          (is "filterlim ?h _ _")
  proof (rule tendsto_sandwich)
    show "eventually (λn. ?h n  N - (mn. norm (f m))) at_top"
    proof (intro always_eventually allI)
      fix n :: nat
      interpret product_sigma_finite "λ_::nat. count_space (UNIV :: nat set)"
        by (intro product_sigma_finite.intro sigma_finite_measure_count_space)

      have "(p | p  n  prime p. i. f (p ^ i)) =
              (p | p  n  prime p. a iUNIV. f (p ^ i))"
        by (intro prod.cong refl infsetsum_nat' [symmetric] summable'') auto
      also have " = (ag{p. p  n  prime p} E UNIV.
                         x{p. p  n  prime p}. f (x ^ g x))"
        by (subst infsetsum_prod_PiE [symmetric])
           (auto simp: prime_gt_Suc_0_nat summable'')
      also have " = (ag{p. p  n  prime p} E UNIV.
                         f (x{p. p  n  prime p}. x ^ g x))"
        by (subst f.prod_coprime) (auto simp add: primes_coprime)
      also have " = (am | m > 0  prime_factors m  {..n}. f m)"
        by (intro infsetsum_reindex_bij_betw bij_betw_prime_powers)
      also have "(amUNIV. f m) -  = (amUNIV - {m. m > 0  prime_factors m  {..n}}. f m)"
        by (intro infsetsum_Diff [symmetric] summable') auto
      also have "(amUNIV. f m) = (m. f m)"
        by (intro infsetsum_nat' summable')
      also have "UNIV - {m. m > 0  prime_factors m  {..n}} = 
                   insert 0 {m. ¬prime_factors m  {..n}}"
        by auto
      also have "(am. f m) = (am | ¬prime_factors m  {..n}. f m)"
        by (intro infsetsum_cong_neutral) auto
      also have "norm   (am | ¬prime_factors m  {..n}. norm (f m))"
        by (rule norm_infsetsum_bound)
      also have "  (am{n<..}. norm (f m))" 
      proof (intro infsetsum_mono_neutral_left summable' abs_summable_on_normI)
        show "{m. ¬ prime_factors m  {..n}}  {n<..}"
        proof safe
          fix m k assume "¬m > n" and "k  prime_factors m"
          thus "k  n" by (cases "m = 0") (auto simp: prime_factors_dvd dest: dvd_imp_le)
        qed
      qed auto
      also have "{n<..} = UNIV - {..n}" 
        by auto
      also have "(am. norm (f m)) = (amUNIV. norm (f m)) - (am{..n}. norm (f m))"
        using summable by (intro infsetsum_Diff) (auto simp: abs_summable_on_nat_iff')
      also have "(amUNIV. norm (f m)) = N"
        unfolding N_def using summable 
        by (intro infsetsum_nat') (auto simp: abs_summable_on_nat_iff')
      also have "(am{..n}. norm (f m)) = (mn. norm (f m))"
        by (simp add: suminf_finite)
      finally show "?h n  N - (mn. norm (f m))" .
   qed
  next
    show "eventually (λn. ?h n  0) at_top" by simp
  next
    show "(λn. N - (mn. norm (f m)))  0" unfolding N_def
      by (rule tendsto_eq_intros refl summable_LIMSEQ' summable)+ simp_all
  qed simp_all
  hence "(λn. (m. f m) - (p{p. p  n  prime p}. i. f (p ^ i)))  0"
    by (simp add: tendsto_norm_zero_iff)
  from tendsto_diff[OF tendsto_const[of "m. f m"] this]
    have "(λn. p | p  n  prime p. i. f (p ^ i))  (m. f m)" by simp
  also have "(λn. p | p  n  prime p. i. f (p ^ i)) = 
                 (λn. pn. if prime p then (i. f (p ^ i)) else 1)"
    by (intro ext prod.mono_neutral_cong_left) auto
  finally show "  (m. f m)" .

  show "abs_convergent_prod (λp. if prime p then (i. f (p ^ i)) else 1)"
  proof (rule summable_imp_abs_convergent_prod)
    have "(λ(p,i). f (p ^ i)) abs_summable_on {p. prime p} × {0<..}"
      unfolding case_prod_unfold 
      by (subst abs_summable_on_reindex_iff[OF inj_prime_power]) fact
    hence "(λp. ai{0<..}. f (p ^ i)) abs_summable_on {p. prime p}"
      by (rule abs_summable_on_Sigma_project1') simp_all
    also have "?this  (λp. (i. f (p ^ i)) - 1) abs_summable_on {p. prime p}"
    proof (intro abs_summable_on_cong refl)
      fix p :: nat assume p: "p  {p. prime p}"
      have "{0<..} = UNIV - {0::nat}" by auto
      also have "(ai. f (p ^ i)) = (i. f (p ^ i)) - 1"
        using p by (subst infsetsum_Diff) (simp_all add: infsetsum_nat' summable'')
      finally show "(ai{0<..}. f (p ^ i)) = (i. f (p ^ i)) - 1" .
    qed
    finally have "summable (λp. if prime p then norm ((i. f (p ^ i)) - 1) else 0)"
      (is "summable ?T") by (simp add: abs_summable_on_nat_iff)
    also have "?T = (λp. norm ((if prime p then i. f (p ^ i) else 1) - 1))"
      by (rule ext) (simp add: if_splits)
    finally show "summable " .
  qed
qed

lemma
  fixes f :: "nat  'a :: {real_normed_field,banach,second_countable_topology}"
  assumes summable: "summable (λn. norm (f n))"
  assumes "completely_multiplicative_function f"
  shows   abs_convergent_euler_product':
            "abs_convergent_prod (λp. if prime p then inverse (1 - f p) else 1)"
    and   completely_multiplicative_summable_norm: 
            "p. prime p  norm (f p) < 1"
    and   euler_product_LIMSEQ':
            "(λn. (pn. if prime p then inverse (1 - f p) else 1))  (n. f n)"
proof -
  interpret f: completely_multiplicative_function f by fact
  {
    fix p :: nat assume "prime p"
    hence "inj (λi. p ^ i)" 
      by (auto simp: inj_on_def dest: prime_gt_1_nat)
    from summable_reindex[OF summable this] 
      have *: "summable (λi. norm (f (p ^ i)))" by (auto simp: o_def)
    also have "(λi. norm (f (p ^ i))) = (λi. norm (f p) ^ i)"
      by (simp add: f.power norm_power)
    finally show "norm (f p) < 1"
      by (subst (asm) summable_geometric_iff) simp_all
    note * and this
  } note summable' = this

  have eq: "(λp. if prime p then (i. f (p ^ i)) else 1) = 
              (λp. if prime p then inverse (1 - f p) else 1)"
  proof (rule ext, goal_cases)
    case (1 p)
    show ?case
    proof (cases "prime p")
      case True
      hence "norm (f p) < 1" by (rule summable')
      from suminf_geometric[OF this] and True show ?thesis
        by (simp add: field_simps f.power)
    qed simp_all
  qed
  hence eq': "(λn. pn. if prime p then n. f (p ^ n) else 1) =
                (λn. pn. if prime p then inverse (1 - f p) else 1)"
    by (auto simp: fun_eq_iff)

  have f: "multiplicative_function f" ..
  from abs_convergent_euler_product[OF assms(1) f] and euler_product_LIMSEQ[OF assms(1) f]
    show "abs_convergent_prod (λp. if prime p then inverse (1 - f p) else 1)"
       and "(λn. pn. if prime p then inverse (1 - f p) else 1)  (n. f n)"
      by (simp_all only: eq eq')
qed

end