Theory Squarefree_Nat

(*
  File:   Squarefree_Nat.thy
  Author: Manuel Eberl <manuel@pruvisto.org>

  The unique decomposition of a natural number into a squarefree part and a square.
*)

section ‹Squarefree decomposition of natural numbers›
theory Squarefree_Nat
imports
  Main
  "HOL-Number_Theory.Number_Theory"
  Prime_Harmonic_Misc
begin

text ‹
  The squarefree part of a natural number is the set of all prime factors that appear 
  with odd multiplicity. The square part, correspondingly, is what remains after dividing
  by the squarefree part.
›
definition squarefree_part :: "nat ⇒ nat set" where
  "squarefree_part n = {p∈prime_factors n. odd (multiplicity p n)}"

definition square_part :: "nat ⇒ nat" where
  "square_part n = (if n = 0 then 0 else (∏p∈prime_factors n. p ^ (multiplicity p n div 2)))"

lemma squarefree_part_0 [simp]: "squarefree_part 0 = {}"
  by (simp add: squarefree_part_def)

lemma square_part_0 [simp]: "square_part 0 = 0"
  by (simp add: square_part_def)

lemma squarefree_decompose: "∏(squarefree_part n) * square_part n ^ 2 = n"
proof (cases "n = 0")
  case False
  define A s where "A = squarefree_part n" and "s = square_part n"
  have "(∏A) = (∏p∈A. p ^ (multiplicity p n mod 2))"
    by (intro prod.cong) (auto simp: A_def squarefree_part_def elim!: oddE)
  also have "… = (∏p∈prime_factors n. p ^ (multiplicity p n mod 2))"
    by (intro prod.mono_neutral_left) (auto simp: A_def  squarefree_part_def)
  also from False have "… * s^2 = n"
    by (simp add: s_def square_part_def prod.distrib [symmetric] power_add [symmetric] 
                  power_mult [symmetric] prime_factorization_nat [symmetric] algebra_simps
                  prod_power_distrib)
  finally show "∏A * s^2 = n" .
qed simp

lemma squarefree_part_pos [simp]: "∏(squarefree_part n) > 0"
  using prime_gt_0_nat unfolding squarefree_part_def by auto
    
lemma squarefree_part_ge_Suc_0 [simp]: "∏(squarefree_part n) ≥ Suc 0"
  using squarefree_part_pos[of n] by presburger

lemma squarefree_part_subset [intro]: "squarefree_part n ⊆ prime_factors n"
  unfolding squarefree_part_def by auto

lemma squarefree_part_finite [simp]: "finite (squarefree_part n)"
  by (rule finite_subset[OF squarefree_part_subset]) simp

lemma squarefree_part_dvd [simp]: "∏(squarefree_part n) dvd n"
  by (subst (2) squarefree_decompose [of n, symmetric]) simp

lemma squarefree_part_dvd' [simp]: "p ∈ squarefree_part n ⟹ p dvd n"
  by (rule dvd_prodD[OF _ squarefree_part_dvd]) simp_all

lemma square_part_dvd [simp]: "square_part n ^ 2 dvd n"
  by (subst (2) squarefree_decompose [of n, symmetric]) simp

lemma square_part_dvd' [simp]: "square_part n dvd n"
  by (subst (2) squarefree_decompose [of n, symmetric]) simp

lemma squarefree_part_le: "p ∈ squarefree_part n ⟹ p ≤ n"
  by (cases "n = 0") (simp_all add: dvd_imp_le)

lemma square_part_le: "square_part n ≤ n"
  by (cases "n = 0") (simp_all add: dvd_imp_le)

lemma square_part_le_sqrt: "square_part n ≤ nat ⌊sqrt (real n)⌋"
proof -
  have "1 * square_part n ^ 2 ≤ ∏(squarefree_part n) * square_part n ^ 2"
    by (intro mult_right_mono) simp_all
  also have "… = n" by (rule squarefree_decompose)
  finally have "real (square_part n ^ 2) ≤ real n" by (subst of_nat_le_iff) simp
  hence "sqrt (real (square_part n ^ 2)) ≤ sqrt (real n)" 
    by (subst real_sqrt_le_iff) simp_all
  also have "sqrt (real (square_part n ^ 2)) = real (square_part n)" by simp
  finally show ?thesis by linarith
qed    

lemma square_part_pos [simp]: "n > 0 ⟹ square_part n > 0"
  unfolding square_part_def using prime_gt_0_nat by auto
    
lemma square_part_ge_Suc_0 [simp]: "n > 0 ⟹ square_part n ≥ Suc 0"
  using square_part_pos[of n] by presburger

lemma zero_not_in_squarefree_part [simp]: "0 ∉ squarefree_part n"
  unfolding squarefree_part_def by auto

lemma multiplicity_squarefree_part:
  "prime p ⟹ multiplicity p (∏(squarefree_part n)) = (if p ∈ squarefree_part n then 1 else 0)"
  using squarefree_part_subset[of n]
  by (intro multiplicity_prod_prime_powers_nat') auto

text ‹
  The squarefree part really is square, its only square divisor is 1.
›
lemma square_dvd_squarefree_part_iff:
  "x^2 dvd ∏(squarefree_part n) ⟷ x = 1"
proof (rule iffI, rule multiplicity_eq_nat)
  assume dvd: "x^2 dvd ∏(squarefree_part n)"
  hence "x ≠ 0" using squarefree_part_subset[of n] prime_gt_0_nat by (intro notI) auto
  thus x: "x > 0" by simp
  
  fix p :: nat assume p: "prime p"
  from p x have "2 * multiplicity p x = multiplicity p (x^2)" 
    by (simp add: multiplicity_power_nat)
  also from dvd have "… ≤ multiplicity p (∏(squarefree_part n))"
    by (intro dvd_imp_multiplicity_le) simp_all
  also have "… ≤ 1" using multiplicity_squarefree_part[of p n] p by simp
  finally show "multiplicity p x = multiplicity p 1" by simp
qed simp_all


lemma squarefree_decomposition_unique1:
  assumes "squarefree_part m = squarefree_part n"
  assumes "square_part m = square_part n"
  shows   "m = n"
  by (subst (1 2) squarefree_decompose [symmetric]) (simp add: assms)

lemma squarefree_decomposition_unique2:
  assumes n: "n > 0"
  assumes decomp: "n = (∏A2 * s2^2)"
  assumes prime: "⋀x. x ∈ A2 ⟹ prime x"
  assumes fin: "finite A2"
  assumes s2_nonneg: "s2 ≥ 0"
  shows "A2 = squarefree_part n" and "s2 = square_part n"
proof -
  define A1 s1 where "A1 = squarefree_part n" and "s1 = square_part n"
  have "finite A1" unfolding A1_def by simp
  note fin = ‹finite A1› ‹finite A2›

  have "A1 ⊆ prime_factors n" unfolding A1_def using squarefree_part_subset .
  note subset = this prime

  have "∏A1 > 0" "∏A2 > 0" using subset(1)  prime_gt_0_nat 
    by (auto intro!: prod_pos dest: prime)
  from n have "s1 > 0" unfolding s1_def by simp
  from assms have "s2 ≠ 0" by (intro notI) simp
  hence "s2 > 0" by simp
  note pos = ‹∏A1 > 0› ‹∏A2 > 0› ‹s1 > 0› ‹s2 > 0›

  have eq': "multiplicity p s1 = multiplicity p s2" 
            "multiplicity p (∏A1) = multiplicity p (∏A2)" 
    if   p: "prime p" for p
  proof -
    define m where "m = multiplicity p"
    from decomp have "m (∏A1 * s1^2) = m (∏A2 * s2^2)" unfolding A1_def s1_def
      by (simp add: A1_def s1_def squarefree_decompose)
    with p pos have eq: "m (∏A1) + 2 * m s1 = m (∏A2) + 2 * m s2"
      by (simp add: m_def prime_elem_multiplicity_mult_distrib multiplicity_power_nat)
    moreover from fin subset p have "m (∏A1) ≤ 1" "m (∏A2) ≤ 1" unfolding m_def
      by ((subst multiplicity_prod_prime_powers_nat', auto)[])+
    ultimately show "m s1 = m s2" by linarith
    with eq show "m (∏A1) = m (∏A2)" by simp
  qed
  
  show "s2 = square_part n"
    by (rule multiplicity_eq_nat) (insert pos eq'(1), auto simp: s1_def)
  have "∏A2 = ∏(squarefree_part n)"
    by (rule multiplicity_eq_nat) (insert pos eq'(2), auto simp: A1_def)
  with fin subset show "A2 = squarefree_part n" unfolding A1_def
    by (intro prod_prime_eq) auto
qed

lemma squarefree_decomposition_unique2':
  assumes decomp: "(∏A1 * s1^2) = (∏A2 * s2^2 :: nat)"
  assumes fin: "finite A1" "finite A2"
  assumes subset: "⋀x. x ∈ A1 ⟹ prime x" "⋀x. x ∈ A2 ⟹ prime x"
  assumes pos: "s1 > 0" "s2 > 0"
  defines "n ≡ ∏A1 * s1^2"
  shows "A1 = A2" "s1 = s2"
proof -
  from pos have n: "n > 0" using prime_gt_0_nat 
    by (auto simp: n_def intro!: prod_pos dest: subset)
  have "A1 = squarefree_part n" "s1 = square_part n" 
    by ((rule squarefree_decomposition_unique2[of n A1 s1], insert assms n, simp_all)[])+
  moreover have "A2 = squarefree_part n" "s2 = square_part n" 
    by ((rule squarefree_decomposition_unique2[of n A2 s2], insert assms n, simp_all)[])+
  ultimately show "A1 = A2" "s1 = s2" by simp_all
qed

text ‹
  The following is a nice and simple lower bound on the number of prime numbers less than 
  a given number due to Erd\H{o}s. In particular, it implies that there are infinitely many primes.
›
lemma primes_lower_bound:
  fixes n :: nat
  assumes "n > 0"
  defines "π ≡ λn. card {p. prime p ∧ p ≤ n}"
  shows   "real (π n) ≥ ln (real n) / ln 4"
proof -
  have "real n = real (card {1..n})" by simp
  also have "{1..n} = (λ(A, b). ∏A * b^2) ` (λn. (squarefree_part n, square_part n)) ` {1..n}"
    unfolding image_comp o_def squarefree_decompose case_prod_unfold fst_conv snd_conv by simp
  also have "card … ≤ card ((λn. (squarefree_part n, square_part n)) ` {1..n})"
    by (rule card_image_le) simp_all
  also have "… ≤ card (squarefree_part ` {1..n} × square_part ` {1..n})"
    by (rule card_mono) auto
  also have "real … = real (card (squarefree_part ` {1..n})) * real (card (square_part ` {1..n}))"
    by simp
  also have "… ≤ 2 ^ π n * sqrt (real n)"
  proof (rule mult_mono)
    have "card (squarefree_part ` {1..n}) ≤ card (Pow {p. prime p ∧ p ≤ n})"
      using squarefree_part_subset squarefree_part_le by (intro card_mono) force+
    also have "real … = 2 ^ π n" by (simp add: π_def card_Pow)
    finally show "real (card (squarefree_part ` {1..n})) ≤ 2 ^ π n" by - simp_all
  next
    have "square_part k ≤ nat ⌊sqrt n⌋" if "k ≤ n" for k
      by (rule order.trans[OF square_part_le_sqrt])
         (insert that, auto intro!: nat_mono floor_mono)
    hence "card (square_part ` {1..n}) ≤ card {1..nat ⌊sqrt n⌋}"
      by (intro card_mono) (auto intro: order.trans[OF square_part_le_sqrt])
    also have "… = nat ⌊sqrt n⌋" by simp
    also have "real … ≤ sqrt n" by simp
    finally show "real (card (square_part ` {1..n})) ≤ sqrt (real n)" by - simp_all
  qed simp_all
  finally have "real n ≤ 2 ^ π n * sqrt (real n)" by - simp_all
  with ‹n > 0› have "ln (real n) ≤ ln (2 ^ π n * sqrt (real n))"
    by (subst ln_le_cancel_iff) simp_all
  moreover have "ln (4 :: real) = real 2 * ln 2" by (subst ln_realpow [symmetric]) simp_all
  ultimately show ?thesis using ‹n > 0›
    by (simp add: ln_mult ln_realpow[of _ "π n"] ln_sqrt field_simps)
qed

end