Theory Prime_Distribution_Elementary.Lcm_Nat_Upto

(*
  File:    Lcm_Nat_Upto.thy
  Author:  Manuel Eberl, TU München

  The LCM of {1..n}, including the relationship Lcm {1..n} = exp (ψ n).
*)

section ‹The LCM of the first $n$ natural numbers›
theory Lcm_Nat_Upto
  imports Prime_Number_Theorem.Prime_Counting_Functions
begin

text ‹
  In this section, we examine @{term "Lcm {1..(n::nat)}"}. In particular,
  we will show that it is equal to $e^{\psi(n)}$ and thus (by the PNT) $e^{n + o(n)}$.
›
lemma multiplicity_Lcm:
  fixes A :: "'a :: {semiring_Gcd, factorial_semiring_gcd} set"
  assumes "finite A" "A  {}" "prime p" "0  A"
  shows   "multiplicity p (Lcm A) = Max (multiplicity p ` A)"
  using assms
proof (induction A rule: finite_ne_induct)
  case (insert x A)
  have "Lcm (insert x A) = lcm x (Lcm A)" by simp
  also have "multiplicity p  = Max (multiplicity p ` insert x A)"
    using insert by (subst multiplicity_lcm) (auto simp: Lcm_0_iff)
  finally show ?case by simp
qed auto

text ‹
  The multiplicity of any prime p› in @{term "Lcm {1..(n::nat)}"} differs from
  that in @{term "Lcm {1..(n - 1 :: nat)}"} iff n› is a power of p›, in which case
  it is greater by 1.
›
lemma multiplicity_Lcm_atLeast1AtMost_Suc:
  fixes p n :: nat
  assumes p: "prime p" and n: "n > 0"
  shows "multiplicity p (Lcm {1..Suc n}) =
           (if k. Suc n = p ^ k then 1 else 0) + multiplicity p (Lcm {1..n})"
proof -
  define k where "k = Max (multiplicity p ` {1..n})"
  define l where "l = multiplicity p (Suc n)"
  have eq: "{1..Suc n} = insert (Suc n) {1..n}" by auto
  from prime p have "p > 1" by (auto dest: prime_gt_1_nat)

  have "multiplicity p (Lcm {1..Suc n}) = Max (multiplicity p ` {1..Suc n})"
    using assms by (subst multiplicity_Lcm) auto
  also have "multiplicity p ` {1..Suc n} =
               insert (multiplicity p (Suc n)) (multiplicity p ` {1..n})"
    by (simp only: eq image_insert)
  also have "Max  = max l k"
    unfolding l_def k_def using assms by (subst Max.insert) auto
  also have " = (if k. Suc n = p ^ k then 1 else 0) + k"
  proof (cases "k. Suc n = p ^ k")
    case False
    have "p ^ l dvd Suc n"
      unfolding l_def by (intro multiplicity_dvd)
    hence "p ^ l  Suc n"
      unfolding l_def by (intro dvd_imp_le multiplicity_dvd) auto
    moreover have "Suc n  p ^ l" using False by blast
    ultimately have "p ^ l < Suc n" by linarith
    moreover have "p ^ l > 0" using p > 1 by (intro zero_less_power) auto
    ultimately have "l = multiplicity p (p ^ l)" and "p ^ l  {1..n}"
      using prime p by auto
    hence "l  k" unfolding k_def by (intro Max.coboundedI) auto
    with False show ?thesis by (simp add: l_def k_def)
  next
    case True
    then obtain x where x: "Suc n = p ^ x" by blast
    from x and n > 0 have "x > 0" by (intro Nat.gr0I) auto
    from x have [simp]: "l = x" using prime p by (simp add: l_def)
    have "x = k + 1"
    proof (intro antisym)
      have "p ^ (x - 1) < Suc n"
        using x > 0 p > 1 unfolding x by (intro power_strict_increasing) auto
      moreover have "p ^ (x - 1) > 0"
        using p > 1 by (intro zero_less_power) auto
      ultimately have "multiplicity p (p ^ (x - 1)) = x - 1" and "p ^ (x - 1)  {1..n}"
        using prime p by auto
      hence "x - 1  k"
        unfolding k_def by (intro Max.coboundedI) force+
      thus "x  k + 1" by linarith
    next
      have "multiplicity p y < x" if "y  {1..n}" for y
      proof -
        have "p ^ multiplicity p y  y"
          using that by (intro dvd_imp_le multiplicity_dvd) auto
        also have " < Suc n" using that by simp
        also have " = p ^ x" by (fact x)
        finally show "multiplicity p y < x"
          using p > 1 by (subst (asm) power_strict_increasing_iff)
      qed
      hence "k < x"
        using n > 0 unfolding k_def by (subst Max_less_iff) auto
      thus "k + 1  x" by simp
    qed
    thus ?thesis using True by simp
  qed
  also have "k = multiplicity p (Lcm {1..n})"
    unfolding k_def using n > 0 and prime p by (subst multiplicity_Lcm) auto
  finally show ?thesis .
qed

text ‹
  Consequently, termLcm {1..(n::nat)} differs from termLcm {1..(n-1::nat)}
  iff n› is of the form $p^k$ for some prime $p$, in which case it is greater by a factor
  of p›.
›
lemma Lcm_atLeast1AtMost_Suc:
  "Lcm {1..Suc n} = Lcm {1..n} * (if primepow (Suc n) then aprimedivisor (Suc n) else 1)"
proof (cases "n > 0")
  case True
  show ?thesis
  proof (rule multiplicity_eq_nat)
    fix p :: nat assume "prime p"
    define x where "x = (if primepow (Suc n) then aprimedivisor (Suc n) else 1)"
    have "x > 0"
      using n > 0 by (auto simp: x_def intro!: aprimedivisor_pos_nat)
  
    have "multiplicity p (Lcm {1..n} * x) = multiplicity p (Lcm {1..n}) + multiplicity p x"
      using prime p x > 0 by (subst prime_elem_multiplicity_mult_distrib) auto
    also consider "k. Suc n = p ^ k" | "primepow (Suc n)" "¬(k. Suc n = p ^ k)" 
                | "¬primepow (Suc n)" by blast
    hence "multiplicity p x = (if k. Suc n = p ^ k then 1 else 0)"
    proof cases
      assume "k. Suc n = p ^ k"
      thus ?thesis using prime p n > 0
        by (auto simp: x_def aprimedivisor_prime_power intro!: Nat.gr0I)
    next
      assume *: "primepow (Suc n)" "k. Suc n = p ^ k"
      then obtain q k where qk: "prime q" "Suc n = q ^ k" "k > 0" "q  p"
        by (auto simp: primepow_def)
      thus ?thesis using prime p
        by (subst *) (auto simp: x_def aprimedivisor_prime_power prime_multiplicity_other)
    next
      assume *: "¬primepow (Suc n)"
      hence **: "k. Suc n = p ^ k" using prime p n > 0 by auto
      from * show ?thesis unfolding x_def
        by (subst **) auto
    qed
    also have "multiplicity p (Lcm {1..n}) +  = multiplicity p (Lcm {1..Suc n})"
      using prime p n > 0 by (subst multiplicity_Lcm_atLeast1AtMost_Suc) (auto simp: x_def)
    finally show "multiplicity p (Lcm {1..Suc n}) = multiplicity p (Lcm {1..n} * x)" ..
  qed (use n > 0 in auto intro!: Nat.gr0I dest: aprimedivisor_pos_nat) 
qed auto

text ‹
  It follows by induction that $\text{Lcm}\ \{1..n\} = e^{\psi(n)}$.
›
lemma Lcm_atLeast1AtMost_conv_ψ:
  includes prime_counting_notation
  shows "real (Lcm {1..n}) = exp (ψ (real n))"
proof (induction n)
  case (Suc n)
  have "real (Lcm {1..Suc n}) =
          real (Lcm {1..n}) * (if primepow (Suc n) then aprimedivisor (Suc n) else 1)"
    by (subst Lcm_atLeast1AtMost_Suc) auto
  also {
    assume "primepow (Suc n)"
    hence "Suc n > Suc 0" by (rule primepow_gt_Suc_0)
    hence "aprimedivisor (Suc n) > 0" by (intro aprimedivisor_pos_nat) auto
  }
  hence "(if primepow (Suc n) then aprimedivisor (Suc n) else 1) = exp (mangoldt (Suc n))"
    by (simp add: mangoldt_def)
  also have "Lcm {1..n} *  = exp (ψ (real n + 1))"
    using Suc.IH by (simp add: primes_psi_def sum_upto_plus1 exp_add)
  finally show ?case by (simp add: add_ac)
qed simp_all

lemma Lcm_upto_real_conv_ψ:
  includes prime_counting_notation
  shows "real (Lcm {1..nat x}) = exp (ψ x)"
  by (subst Lcm_atLeast1AtMost_conv_ψ) (simp add: primes_psi_def sum_upto_altdef)

end