Theory Dirichlet_Misc
section ‹Miscellaneous auxiliary facts›
theory Dirichlet_Misc
imports
"HOL-Number_Theory.Number_Theory"
begin
lemma
fixes a k :: nat
assumes "a > 1" "k > 0"
shows geometric_sum_nat_aux: "(a - 1) * (∑i<k. a ^ i) = a ^ k - 1"
and geometric_sum_nat_dvd: "a - 1 dvd a ^ k - 1"
and geometric_sum_nat: "(∑i<k. a ^ i) = (a ^ k - 1) div (a - 1)"
proof -
have "(real a - 1) * (∑i<k. real a ^ i) = real a ^ k - 1"
using assms by (subst geometric_sum) auto
also have "(real a - 1) * (∑i<k. real a ^ i) = real ((a - 1) * (∑i<k. a ^ i))"
using assms by (simp add: of_nat_diff)
also have "real a ^ k - 1 = real (a ^ k - 1)" using assms by (subst of_nat_diff) auto
finally show *: "(a - 1) * (∑i<k. a ^ i) = a ^ k - 1" by (subst (asm) of_nat_eq_iff)
show "a - 1 dvd a ^ k - 1" by (subst * [symmetric]) simp
from assms show "(∑i<k. a ^ i) = (a ^ k - 1) div (a - 1)"
by (subst * [symmetric]) simp
qed
lemma dvd_div_gt0: "d dvd n ⟹ n > 0 ⟹ n div d > (0::nat)"
by auto
lemma Set_filter_insert:
"Set.filter P (insert x A) = (if P x then insert x (Set.filter P A) else Set.filter P A)"
by auto
lemma Set_filter_union: "Set.filter P (A ∪ B) = Set.filter P A ∪ Set.filter P B"
by auto
lemma Set_filter_empty [simp]: "Set.filter P {} = {}"
by auto
lemma Set_filter_image: "Set.filter P (f ` A) = f ` Set.filter (P ∘ f) A"
by auto
lemma Set_filter_cong [cong]:
"(⋀x. x ∈ A ⟹ P x ⟷ Q x) ⟹ A = B ⟹ Set.filter P A = Set.filter Q B"
by auto
lemma inj_on_insert': "(⋀B. B ∈ A ⟹ x ∉ B) ⟹ inj_on (insert x) A"
by (auto simp: inj_on_def insert_eq_iff)
lemma
assumes "finite A" "A ≠ {}"
shows card_even_subset_aux: "card {B. B ⊆ A ∧ even (card B)} = 2 ^ (card A - 1)"
and card_odd_subset_aux: "card {B. B ⊆ A ∧ odd (card B)} = 2 ^ (card A - 1)"
and card_even_odd_subset: "card {B. B ⊆ A ∧ even (card B)} = card {B. B ⊆ A ∧ odd (card B)}"
proof -
from assms have *: "2 * card (Set.filter (even ∘ card) (Pow A)) = 2 ^ card A"
proof (induction A rule: finite_ne_induct)
case (singleton x)
hence "Pow {x} = {{}, {x}}" by auto
thus ?case by (simp add: Set_filter_insert)
next
case (insert x A)
note fin = finite_subset[OF _ ‹finite A›]
have "Pow (insert x A) = Pow A ∪ insert x ` Pow A" by (rule Pow_insert)
have "Set.filter (even ∘ card) (Pow (insert x A)) =
Set.filter (even ∘ card) (Pow A) ∪
insert x ` Set.filter (even ∘ card ∘ insert x) (Pow A)"
unfolding Pow_insert Set_filter_union Set_filter_image by blast
also have "Set.filter (even ∘ card ∘ insert x) (Pow A) = Set.filter (odd ∘ card) (Pow A)"
unfolding o_def
by (intro Set_filter_cong refl, subst card_insert_disjoint)
(insert insert.hyps, auto dest: finite_subset)
also have "card (Set.filter (even ∘ card) (Pow A) ∪ insert x ` …) =
card (Set.filter (even ∘ card) (Pow A)) + card (insert x ` …)"
(is "card (?A ∪ ?B) = _")
by (intro card_Un_disjoint finite_filter finite_imageI) (auto simp: insert.hyps)
also have "card ?B = card (Set.filter (odd ∘ card) (Pow A))"
using insert.hyps by (intro card_image inj_on_insert') auto
also have "Set.filter (odd ∘ card) (Pow A) = Pow A - Set.filter (even ∘ card) (Pow A)"
by auto
also have "card … = card (Pow A) - card (Set.filter (even ∘ card) (Pow A))"
using insert.hyps by (subst card_Diff_subset) (auto simp: finite_filter)
also have "card (Set.filter (even ∘ card) (Pow A)) + … = card (Pow A)"
by (intro add_diff_inverse_nat, subst not_less, rule card_mono) (insert insert.hyps, auto)
also have "2 * … = 2 ^ card (insert x A)"
using insert.hyps by (simp add: card_Pow)
finally show ?case .
qed
from * show A: "card {B. B ⊆ A ∧ even (card B)} = 2 ^ (card A - 1)"
by (cases "card A") (simp_all add: Set.filter_def)
have "Set.filter (odd ∘ card) (Pow A) = Pow A - Set.filter (even ∘ card) (Pow A)" by auto
also have "2 * card … = 2 * 2 ^ card A - 2 * card (Set.filter (even ∘ card) (Pow A))"
using assms by (subst card_Diff_subset) (auto intro!: finite_filter simp: card_Pow)
also note *
also have "2 * 2 ^ card A - 2 ^ card A = (2 ^ card A :: nat)" by simp
finally show B: "card {B. B ⊆ A ∧ odd (card B)} = 2 ^ (card A - 1)"
by (cases "card A") (simp_all add: Set.filter_def)
from A and B show "card {B. B ⊆ A ∧ even (card B)} = card {B. B ⊆ A ∧ odd (card B)}" by simp
qed
lemma bij_betw_prod_divisors_coprime:
assumes "coprime a (b :: nat)"
shows "bij_betw (λx. fst x * snd x) ({d. d dvd a} × {d. d dvd b}) {k. k dvd a * b}"
unfolding bij_betw_def
proof
from assms show "inj_on (λx. fst x * snd x) ({d. d dvd a} × {d. d dvd b})"
by (auto simp: inj_on_def coprime_crossproduct_nat coprime_divisors)
show "(λx. fst x * snd x) ` ({d. d dvd a} × {d. d dvd b}) = {k. k dvd a * b}"
proof safe
fix x assume "x dvd a * b"
then obtain b' c' where "x = b' * c'" "b' dvd a" "c' dvd b"
using division_decomp by blast
thus "x ∈ (λx. fst x * snd x) ` ({d. d dvd a} × {d. d dvd b})" by force
qed (insert assms, auto intro: mult_dvd_mono)
qed
lemma bij_betw_prime_power_divisors:
assumes "prime (p :: nat)"
shows "bij_betw ((^) p) {..k} {d. d dvd p ^ k}"
unfolding bij_betw_def
proof
from assms have *: "p > 1" by (simp add: prime_gt_Suc_0_nat)
show "inj_on ((^) p) {..k}" using assms
by (auto simp: inj_on_def prime_gt_Suc_0_nat power_inject_exp[OF *])
show "(^) p ` {..k} = {d. d dvd p ^ k}"
using assms by (auto simp: le_imp_power_dvd divides_primepow_nat)
qed
lemma sum_divisors_coprime_mult:
assumes "coprime a (b :: nat)"
shows "(∑d | d dvd a * b. f d) = (∑r | r dvd a. ∑s | s dvd b. f (r * s))"
proof -
have "(∑r | r dvd a. ∑s | s dvd b. f (r * s)) =
(∑z∈{r. r dvd a} × {s. s dvd b}. f (fst z * snd z))"
by (subst sum.cartesian_product) (simp add: case_prod_unfold)
also have "… = (∑d | d dvd a * b. f d)"
by (intro sum.reindex_bij_betw bij_betw_prod_divisors_coprime assms)
finally show ?thesis ..
qed
end