Theory Gaussian_Integers_Sums_Of_Two_Squares
subsection ‹Sums of two squares›
theory Gaussian_Integers_Sums_Of_Two_Squares
imports Gaussian_Integers
begin
text ‹
As an application, we can now easily prove that a positive natural number is the
sum of two squares if and only if all prime factors congruent 3 modulo 4 have even
multiplicity.
›
inductive sum_of_2_squares_nat :: "nat ⇒ bool" where
"sum_of_2_squares_nat (a ^ 2 + b ^ 2)"
lemma sum_of_2_squares_nat_altdef: "sum_of_2_squares_nat n ⟷ n ∈ range gauss_int_norm"
proof (safe elim!: sum_of_2_squares_nat.cases)
fix a b :: nat
have "a ^ 2 + b ^ 2 = gauss_int_norm (of_nat a + 𝗂⇩ℤ * of_nat b)"
by (auto simp: gauss_int_norm_def nat_add_distrib nat_power_eq)
thus "a ^ 2 + b ^ 2 ∈ range gauss_int_norm" by blast
next
fix z :: gauss_int
have "gauss_int_norm z = nat ¦ReZ z¦ ^ 2 + nat ¦ImZ z¦ ^ 2"
by (auto simp: gauss_int_norm_def nat_add_distrib simp flip: nat_power_eq)
thus "sum_of_2_squares_nat (gauss_int_norm z)"
by (auto intro: sum_of_2_squares_nat.intros)
qed
lemma sum_of_2_squares_nat_gauss_int_norm [intro]: "sum_of_2_squares_nat (gauss_int_norm z)"
by (auto simp: sum_of_2_squares_nat_altdef)
lemma sum_of_2_squares_nat_0 [simp, intro]: "sum_of_2_squares_nat 0"
and sum_of_2_squares_nat_1 [simp, intro]: "sum_of_2_squares_nat 1"
and sum_of_2_squares_nat_Suc_0 [simp, intro]: "sum_of_2_squares_nat (Suc 0)"
and sum_of_2_squares_nat_2 [simp, intro]: "sum_of_2_squares_nat 2"
using sum_of_2_squares_nat.intros[of 0 0] sum_of_2_squares_nat.intros[of 0 1]
sum_of_2_squares_nat.intros[of 1 1] by (simp_all add: numeral_2_eq_2)
lemma sum_of_2_squares_nat_mult [intro]:
assumes "sum_of_2_squares_nat x" "sum_of_2_squares_nat y"
shows "sum_of_2_squares_nat (x * y)"
proof -
from assms obtain z1 z2 where "x = gauss_int_norm z1" "y = gauss_int_norm z2"
by (auto simp: sum_of_2_squares_nat_altdef)
hence "x * y = gauss_int_norm (z1 * z2)"
by (simp add: gauss_int_norm_mult)
thus ?thesis by auto
qed
lemma sum_of_2_squares_nat_power [intro]:
assumes "sum_of_2_squares_nat m"
shows "sum_of_2_squares_nat (m ^ n)"
using assms by (induction n) auto
lemma sum_of_2_squares_nat_prod [intro]:
assumes "⋀x. x ∈ A ⟹ sum_of_2_squares_nat (f x)"
shows "sum_of_2_squares_nat (∏x∈A. f x)"
using assms by (induction A rule: infinite_finite_induct) auto
lemma sum_of_2_squares_nat_prod_mset [intro]:
assumes "⋀x. x ∈# A ⟹ sum_of_2_squares_nat x"
shows "sum_of_2_squares_nat (prod_mset A)"
using assms by (induction A) auto
lemma sum_of_2_squares_nat_necessary:
assumes "sum_of_2_squares_nat n" "n > 0"
assumes "prime p" "[p = 3] (mod 4)"
shows "even (multiplicity p n)"
proof -
define k where "k = multiplicity p n"
from assms obtain z where z: "gauss_int_norm z = n"
by (auto simp: sum_of_2_squares_nat_altdef)
from assms and z have [simp]: "z ≠ 0"
by auto
have prime': "prime (of_nat p :: gauss_int)"
using assms prime_gauss_int_of_nat by blast
have [simp]: "multiplicity (of_nat p) (gauss_cnj z) = multiplicity (of_nat p) z"
using multiplicity_gauss_cnj[of "of_nat p" z] by simp
have "multiplicity (of_nat p) (of_nat n :: gauss_int) =
multiplicity (of_nat p) (z * gauss_cnj z)"
using z by (simp add: self_mult_gauss_cnj)
also have "… = 2 * multiplicity (of_nat p) z"
using prime' by (subst prime_elem_multiplicity_mult_distrib) auto
finally have "multiplicity p n = 2 * multiplicity (of_nat p) z"
by (subst (asm) multiplicity_gauss_int_of_nat)
thus ?thesis by auto
qed
lemma sum_of_2_squares_nat_sufficient:
fixes n :: nat
assumes "n > 0"
assumes "⋀p. p ∈ prime_factors n ⟹ [p = 3] (mod 4) ⟹ even (multiplicity p n)"
shows "sum_of_2_squares_nat n"
proof -
define P2 where "P2 = {p∈prime_factors n. [p = 1] (mod 4)}"
define P3 where "P3 = {p∈prime_factors n. [p = 3] (mod 4)}"
from ‹n > 0› have "n = (∏p∈prime_factors n. p ^ multiplicity p n)"
by (subst prime_factorization_nat) auto
also have "… = (∏p∈{2}∪P2∪P3. p ^ multiplicity p n)"
using prime_mod_4_cases
by (intro prod.mono_neutral_left)
(auto simp: P2_def P3_def in_prime_factors_iff not_dvd_imp_multiplicity_0)
also have "… = (∏p∈{2}∪P2. p ^ multiplicity p n) * (∏p∈P3. p ^ multiplicity p n)"
by (intro prod.union_disjoint) (auto simp: P2_def P3_def cong_def)
also have "(∏p∈{2}∪P2. p ^ multiplicity p n) =
2 ^ multiplicity 2 n * (∏p∈P2. p ^ multiplicity p n)"
by (subst prod.union_disjoint) (auto simp: P2_def cong_def)
also have "(∏p∈P3. p ^ multiplicity p n) = (∏p∈P3. (p ^ 2) ^ (multiplicity p n div 2))"
proof (intro prod.cong refl)
fix p :: nat assume p: "p ∈ P3"
have "(p ^ 2) ^ (multiplicity p n div 2) = p ^ (2 * (multiplicity p n div 2))"
by (simp add: power_mult)
also have "even (multiplicity p n)"
using assms p by (auto simp: P3_def)
hence "2 * (multiplicity p n div 2) = multiplicity p n"
by simp
finally show "p ^ multiplicity p n = (p ^ 2) ^ (multiplicity p n div 2)"
by simp
qed
finally have "n = 2 ^ multiplicity 2 n * (∏p∈P2. p ^ multiplicity p n) *
(∏p∈P3. p⇧2 ^ (multiplicity p n div 2))" .
also have "sum_of_2_squares_nat …"
proof (intro sum_of_2_squares_nat_mult sum_of_2_squares_nat_prod; rule sum_of_2_squares_nat_power)
fix p :: nat assume p: "p ∈ P2"
with prime_cong_1_mod_4_gauss_int_norm_exists[of p] show "sum_of_2_squares_nat p"
by (auto simp: P2_def)
next
fix p :: nat assume p: "p ∈ P3"
have "sum_of_2_squares_nat (gauss_int_norm (of_nat p))" ..
also have "gauss_int_norm (of_nat p) = p ^ 2"
by simp
finally show "sum_of_2_squares_nat (p ^ 2)" .
qed auto
finally show ?thesis .
qed
theorem sum_of_2_squares_nat_iff:
"sum_of_2_squares_nat n ⟷
n = 0 ∨ (∀p∈prime_factors n. [p = 3] (mod 4) ⟶ even (multiplicity p n))"
using sum_of_2_squares_nat_necessary[of n] sum_of_2_squares_nat_sufficient[of n] by auto
end