Theory Banach_Tarski_Theorem
theory Banach_Tarski_Theorem
imports Ball_Decomposition
begin
text ‹
Two copies of the ball, embedded in disjoint regions of ‹ℝ⇧3›.
›
definition shift3 :: "real^3" where
"shift3 = vector [3, 0, 0]"
definition ball3_copy_left :: "(real^3) set" where
"ball3_copy_left = ball3"
definition ball3_copy_right :: "(real^3) set" where
"ball3_copy_right = (+) shift3 ` ball3"
lemma norm_shift3 [simp]: "norm shift3 = 3"
unfolding shift3_def
by (simp add: norm_eq_sqrt_inner inner_vec_def sum_3)
lemma ball3_copies_disjoint:
"ball3_copy_left ∩ ball3_copy_right = {}"
proof
show "ball3_copy_left ∩ ball3_copy_right ⊆ {}"
proof
fix z
assume "z ∈ ball3_copy_left ∩ ball3_copy_right"
then obtain y where z_ball: "z ∈ ball3" and y_ball: "y ∈ ball3" and z_eq: "z = shift3 + y"
unfolding ball3_copy_left_def ball3_copy_right_def by auto
have z_norm: "norm z ≤ 1" and y_norm: "norm y ≤ 1"
using z_ball y_ball by (simp_all add: ball3_def)
have tri: "norm (z - y) ≤ norm z + norm y"
using norm_triangle_ineq4 by blast
have "3 = norm (z - y)"
using z_eq by simp
also have "… ≤ norm z + norm y"
by (rule tri)
also have "… ≤ 2"
using z_norm y_norm by simp
finally show "z ∈ {}"
by simp
qed
qed simp
text ‹
Isometries of ‹ℝ⇧3› are the motions used in the final assembly.
Rotations from ‹SO(3)›, translations, and their compositions are
isometries.
›
definition isometry :: "(real^3 ⇒ real^3) ⇒ bool" where
"isometry f ⟷ (∀x y. dist (f x) (f y) = dist x y)"
lemma id_isometry [simp]: "isometry id"
by (simp add: isometry_def)
lemma translation_isometry [simp]: "isometry ((+) a)"
by (simp add: isometry_def dist_norm)
lemma SO3_isometry:
assumes "g ∈ SO3"
shows "isometry g"
using assms
by (auto simp add: SO3_def rotation_def isometry_def orthogonal_transformation_isometry)
lemma isometry_compose:
assumes "isometry f" "isometry g"
shows "isometry (f ∘ g)"
using assms by (simp add: isometry_def)
lemma translation_compose_SO3_isometry [simp]:
assumes "g ∈ SO3"
shows "isometry ((+) a ∘ g)"
using assms by (intro isometry_compose translation_isometry SO3_isometry)
lemma offcenter_rotation_isometry:
assumes "R ∈ SO3"
shows "isometry (λx. c + R (x - c))"
proof -
have "(λx. c + R (x - c)) = (+) c ∘ R ∘ (+) (- c)"
by (rule ext) simp
thus ?thesis
using assms by (simp add: isometry_compose SO3_isometry)
qed
lemma offcenter_rotation_inverse_left:
fixes c :: "real^3"
assumes inv_left: "Rinv ∘ R = id"
defines "T ≡ λx. c + R (x - c)"
and "U ≡ λx. c + Rinv (x - c)"
shows "U (T x) = x"
using fun_cong[OF inv_left, of "x - c"]
by (simp add: T_def U_def)
lemma offcenter_rotation_inverse_right:
fixes c :: "real^3"
assumes inv_right: "R ∘ Rinv = id"
defines "T ≡ λx. c + R (x - c)"
and "U ≡ λx. c + Rinv (x - c)"
shows "T (U x) = x"
using fun_cong[OF inv_right, of "x - c"]
by (simp add: T_def U_def)
lemma offcenter_rotation_funpow_zero:
fixes c :: "real^3" and R :: "real^3 ⇒ real^3"
defines "T ≡ λx. c + R (x - c)"
shows "(T ^^ n) 0 = c + (R ^^ n) (- c)"
proof (induction n)
case 0
show ?case
by simp
next
case (Suc n)
have "(T ^^ Suc n) 0 = T ((T ^^ n) 0)"
by simp
also have "… = T (c + (R ^^ n) (- c))"
using Suc.IH by simp
also have "… = c + R ((R ^^ n) (- c))"
by (simp add: T_def)
also have "… = c + (R ^^ Suc n) (- c)"
by simp
finally show ?case .
qed
lemma sigma_replicate_b:
"sigma (replicate n (False, B)) = (Rz ^^ n)"
by (induction n) (simp_all add: letter_to_rot_def)
lemma canceled_replicate_b: "canceled (replicate n (False, B))"
unfolding canceled_def
proof
assume "Domainp cancels_to_1 (replicate n (False, B))"
then obtain w where "cancels_to_1 (replicate n (False, B)) w"
by auto
then obtain i where i: "Suc i < length (replicate n (False, B))"
and "canceling (replicate n (False, B) ! i) (replicate n (False, B) ! Suc i)"
by (auto simp: cancels_to_1_def cancels_to_1_at_def)
hence "canceling (False, B) (False, B)"
by simp
thus False
by (simp add: canceling_def)
qed
lemma replicate_b_in_F2: "replicate n (False, B) ∈ carrier F2"
by (intro canceled_in_F2 canceled_replicate_b)
theorem ball3_paradoxical_strong:
"∃P Q :: (real^3) set list. ∃gP gQ :: ((real^3) ⇒ (real^3)) list.
length P = length gP ∧ length Q = length gQ ∧
(∀g ∈ set gP. isometry g) ∧ (∀g ∈ set gQ. isometry g) ∧
pairwise_disjoint (P @ Q) ∧
pairwise_disjoint (map2 (λg A. g ` A) gP P) ∧
pairwise_disjoint (map2 (λg A. g ` A) gQ Q) ∧
(∀i < length P. P ! i ⊆ ball3) ∧
(∀i < length Q. Q ! i ⊆ ball3) ∧
ball3 = (⋃i<length P. P ! i) ∪ (⋃i<length Q. Q ! i) ∧
ball3 = (⋃i<length P. (gP ! i) ` (P ! i)) ∧
ball3 = (⋃i<length Q. (gQ ! i) ` (Q ! i))"
proof -
obtain a where a_sphere: "a ∈ sphere2" and a_not_D: "a ∉ bad_set_D"
using exists_antipodal_axis_avoiding_countable[OF bad_set_D_countable] by blast
let ?c = "- (1 / 2) *⇩R a"
define T where "T = (λx. ?c + Rz (x - ?c))"
define U where "U = (λx. ?c + Rz_inv (x - ?c))"
have T_iso: "isometry T"
unfolding T_def by (rule offcenter_rotation_isometry[OF Rz_in_SO3])
have U_iso: "isometry U"
unfolding U_def by (rule offcenter_rotation_isometry[OF Rz_inv_in_SO3])
have U_T: "⋀x. U (T x) = x"
unfolding T_def U_def
by (rule offcenter_rotation_inverse_left[OF Rz_inv_left])
have T_U: "⋀x. T (U x) = x"
unfolding T_def U_def
by (rule offcenter_rotation_inverse_right[OF Rz_inv_right])
have no_Rz_power_fix: "⋀n. n > 0 ⟹ (Rz ^^ n) a ≠ a"
proof
fix n :: nat
assume n_pos: "n > 0" and fixed: "(Rz ^^ n) a = a"
let ?w = "replicate n (False, B)"
have w_carrier: "?w ∈ carrier F2"
by (rule replicate_b_in_F2)
have w_ne: "?w ≠ []"
using n_pos by auto
have "sigma ?w a = a"
using fixed by (simp add: sigma_replicate_b)
hence "a ∈ fixed_point_set (sigma ?w)"
using a_sphere by (simp add: fixed_point_set_def)
hence "a ∈ bad_set_D"
unfolding bad_set_D_def using w_carrier w_ne by blast
with a_not_D show False
by contradiction
qed
have Rz_power_a_inj: "⋀n m. (Rz ^^ n) a = (Rz ^^ m) a ⟹ n = m"
proof -
fix n m :: nat
assume eq: "(Rz ^^ n) a = (Rz ^^ m) a"
show "n = m"
proof (cases n m rule: linorder_cases)
case less
let ?d = "m - n"
have d_pos: "?d > 0"
using less by simp
have m_eq: "m = n + ?d"
using less by simp
have "(Rz ^^ n) a = (Rz ^^ n) ((Rz ^^ ?d) a)"
using eq m_eq by (metis comp_apply funpow_add)
hence "a = (Rz ^^ ?d) a"
using SO3_inj[OF SO3_funpow[OF Rz_in_SO3, of n]] by (auto simp: inj_def)
with no_Rz_power_fix[OF d_pos] show ?thesis
by simp
next
case equal
then show ?thesis .
next
case greater
let ?d = "n - m"
have d_pos: "?d > 0"
using greater by simp
have n_eq: "n = m + ?d"
using greater by simp
have "(Rz ^^ m) a = (Rz ^^ m) ((Rz ^^ ?d) a)"
using eq n_eq by (metis comp_apply funpow_add)
hence "a = (Rz ^^ ?d) a"
using SO3_inj[OF SO3_funpow[OF Rz_in_SO3, of m]] by (auto simp: inj_def)
with no_Rz_power_fix[OF d_pos] show ?thesis
by simp
qed
qed
have T_pow_zero: "⋀n. (T ^^ n) 0 = ?c + (Rz ^^ n) (- ?c)"
unfolding T_def by (rule offcenter_rotation_funpow_zero)
have T_pow_zero_diff: "⋀n. (T ^^ n) 0 = (1 / 2) *⇩R ((Rz ^^ n) a - a)"
proof -
fix n
have lin: "linear (Rz ^^ n)"
by (rule SO3_linear[OF SO3_funpow[OF Rz_in_SO3]])
have "(T ^^ n) 0 = ?c + (Rz ^^ n) (- ?c)"
by (rule T_pow_zero)
also have "… = (- (1 / 2) *⇩R a) + (1 / 2) *⇩R ((Rz ^^ n) a)"
using linear_scale[OF lin, of "1 / 2" a] by simp
also have "… = (1 / 2) *⇩R ((Rz ^^ n) a - a)"
by (simp add: scaleR_right_diff_distrib)
finally show "(T ^^ n) 0 = (1 / 2) *⇩R ((Rz ^^ n) a - a)" .
qed
have T_orbit_inj: "⋀n m. (T ^^ n) 0 = (T ^^ m) 0 ⟹ n = m"
proof -
fix n m :: nat
assume eq: "(T ^^ n) 0 = (T ^^ m) 0"
have "(Rz ^^ n) a = (Rz ^^ m) a"
using eq T_pow_zero_diff by simp
thus "n = m"
by (rule Rz_power_a_inj)
qed
have orbit_disj:
"∀n m. n ≠ m ⟶ ((T^^n) ` {0}) ∩ ((T^^m) ` {0}) = {}"
using T_orbit_inj by auto
define E where "E = (⋃n. (T^^n) ` {0::real^3})"
have T_E: "T ` E = E - {0}"
unfolding E_def by (rule absorbing_rotation_shift[OF orbit_disj])
have zero_subset_E: "{0::real^3} ⊆ E"
proof
fix x :: "real^3"
assume "x ∈ {0}"
hence "x ∈ (T ^^ 0) ` {0}"
by simp
thus "x ∈ E"
unfolding E_def by blast
qed
have E_subset_ball3: "E ⊆ ball3"
proof
fix x
assume "x ∈ E"
then obtain n where x_eq: "x = (T ^^ n) 0"
unfolding E_def by blast
have Rza_sphere: "(Rz ^^ n) a ∈ sphere2"
using SO3_funpow_preserves_sphere2[OF Rz_in_SO3 a_sphere] .
have "norm x = norm ((1 / 2) *⇩R ((Rz ^^ n) a - a))"
using x_eq T_pow_zero_diff by simp
also have "… = (1 / 2) * norm ((Rz ^^ n) a - a)"
by simp
also have "… ≤ (1 / 2) * (norm ((Rz ^^ n) a) + norm a)"
by (intro mult_left_mono norm_triangle_ineq4) simp
also have "… = 1"
using Rza_sphere a_sphere by (simp add: sphere2_def)
finally show "x ∈ ball3"
by (simp add: ball3_def)
qed
let ?X = "ball3 - {0::real^3}"
let ?Y = "ball3"
let ?A = "[E, ball3 - E]"
let ?B = "[T ` E, ball3 - E]"
let ?e = "[T, id]"
let ?t = "[U, id]"
have A_cover: "?Y = (⋃k<length ?A. ?A ! k)"
using E_subset_ball3 by (auto simp: lessThan_Suc)
have A_disj: "pairwise_disjoint ?A"
unfolding pairwise_disjoint_def
proof (intro allI impI)
fix i j
assume i: "i < length ?A" and j: "j < length ?A" and ij: "i ≠ j"
have "(i = 0 ∧ j = 1) ∨ (i = 1 ∧ j = 0)"
using i j ij by auto
thus "?A ! i ∩ ?A ! j = {}"
by auto
qed
have B_cover: "?X = (⋃k<length ?B. ?B ! k)"
proof
show "?X ⊆ (⋃k<length ?B. ?B ! k)"
proof
fix x
assume x: "x ∈ ?X"
show "x ∈ (⋃k<length ?B. ?B ! k)"
proof (cases "x ∈ E")
case True
with x T_E show ?thesis
by force
next
case False
with x show ?thesis
by force
qed
qed
show "(⋃k<length ?B. ?B ! k) ⊆ ?X"
proof
fix x
assume x: "x ∈ (⋃k<length ?B. ?B ! k)"
then obtain k where k: "k < length ?B" and xk: "x ∈ ?B ! k"
by blast
have "k = 0 ∨ k = 1"
using k by auto
thus "x ∈ ?X"
proof
assume "k = 0"
with xk T_E E_subset_ball3 show ?thesis
by auto
next
assume "k = 1"
with xk zero_subset_E show ?thesis
by auto
qed
qed
qed
have B_disj: "pairwise_disjoint ?B"
unfolding pairwise_disjoint_def
proof (intro allI impI)
fix i j
assume i: "i < length ?B" and j: "j < length ?B" and ij: "i ≠ j"
have "(i = 0 ∧ j = 1) ∨ (i = 1 ∧ j = 0)"
using i j ij by auto
thus "?B ! i ∩ ?B ! j = {}"
using T_E by auto
qed
have e_left: "⋀k x. ⟦k < length ?A; x ∈ ?A ! k⟧
⟹ (?e ! k) x ∈ ?B ! k ∧ (?t ! k) ((?e ! k) x) = x"
proof -
fix k x
assume k: "k < length ?A" and x: "x ∈ ?A ! k"
have "k = 0 ∨ k = 1"
using k by auto
thus "(?e ! k) x ∈ ?B ! k ∧ (?t ! k) ((?e ! k) x) = x"
proof
assume "k = 0"
with x U_T show ?thesis
by auto
next
assume "k = 1"
with x show ?thesis
by auto
qed
qed
have t_left: "⋀k y. ⟦k < length ?B; y ∈ ?B ! k⟧
⟹ (?t ! k) y ∈ ?A ! k ∧ (?e ! k) ((?t ! k) y) = y"
proof -
fix k y
assume k: "k < length ?B" and y: "y ∈ ?B ! k"
have "k = 0 ∨ k = 1"
using k by auto
thus "(?t ! k) y ∈ ?A ! k ∧ (?e ! k) ((?t ! k) y) = y"
proof
assume "k = 0"
then obtain x where x: "x ∈ E" and y_eq: "y = T x"
using y by auto
hence "U y = x"
using U_T by simp
with x y_eq T_U ‹k = 0› show ?thesis
by simp
next
assume "k = 1"
with y show ?thesis
by auto
qed
qed
from ball3_minus_origin_paradoxical_strong obtain P Q :: "(real^3) set list"
and gP gQ :: "((real^3) ⇒ (real^3)) list"
where lenP: "length P = length gP"
and lenQ: "length Q = length gQ"
and gP_SO3: "set gP ⊆ SO3"
and gQ_SO3: "set gQ ⊆ SO3"
and source_disj: "pairwise_disjoint (P @ Q)"
and imageP_disj: "pairwise_disjoint (map2 (λg A. g ` A) gP P)"
and imageQ_disj: "pairwise_disjoint (map2 (λg A. g ` A) gQ Q)"
and P_sub: "∀i < length P. P ! i ⊆ ?X"
and Q_sub: "∀i < length Q. Q ! i ⊆ ?X"
and source_cover: "?X = (⋃i<length P. P ! i) ∪ (⋃i<length Q. Q ! i)"
and imageP_cover: "?X = (⋃i<length P. (gP ! i) ` (P ! i))"
and imageQ_cover: "?X = (⋃i<length Q. (gQ ! i) ` (Q ! i))"
by auto
have gP_inj: "⋀i. i < length P ⟹ inj (gP ! i)"
using SO3_inj gP_SO3 lenP nth_mem by auto
have gQ_inj: "⋀i. i < length Q ⟹ inj (gQ ! i)"
using SO3_inj gQ_SO3 lenQ nth_mem by auto
have mapsP: "⋀k i l. ⟦k < length ?A; i < length P; l < length ?B⟧
⟹ transfer_map ?t gP ?e k i l ∈ {f. isometry f}"
proof -
fix k i l
assume k: "k < length ?A" and i: "i < length P" and l: "l < length ?B"
have gi_SO3: "gP ! i ∈ SO3"
using gP_SO3 i lenP by auto
have gi_iso: "isometry (gP ! i)"
by (rule SO3_isometry[OF gi_SO3])
have ek_iso: "isometry (?e ! k)"
using T_iso k less_Suc_eq by fastforce
have tl_iso: "isometry (?t ! l)"
using U_iso l less_Suc_eq by fastforce
show "transfer_map ?t gP ?e k i l ∈ {f. isometry f}"
unfolding transfer_map_def
by (simp add: isometry_compose tl_iso gi_iso ek_iso)
qed
have mapsQ: "⋀k i l. ⟦k < length ?A; i < length Q; l < length ?B⟧
⟹ transfer_map ?t gQ ?e k i l ∈ {f. isometry f}"
proof -
fix k i l
assume k: "k < length ?A" and i: "i < length Q" and l: "l < length ?B"
have gi_SO3: "gQ ! i ∈ SO3"
using gQ_SO3 i lenQ by auto
have gi_iso: "isometry (gQ ! i)"
by (rule SO3_isometry[OF gi_SO3])
have ek_iso: "isometry (?e ! k)"
using T_iso k less_Suc_eq by fastforce
have tl_iso: "isometry (?t ! l)"
using U_iso l less_Suc_eq by fastforce
show "transfer_map ?t gQ ?e k i l ∈ {f. isometry f}"
unfolding transfer_map_def
by (simp add: isometry_compose tl_iso gi_iso ek_iso)
qed
have lenAB: "length ?A = length ?B"
by simp
from transfer_partitioned_paradox[
OF lenAB A_cover A_disj B_cover B_disj e_left t_left lenP lenQ source_disj
source_cover imageP_disj imageQ_disj imageP_cover imageQ_cover gP_inj gQ_inj
mapsP mapsQ]
obtain P' Q' :: "(real^3) set list" and hP hQ :: "((real^3) ⇒ (real^3)) list"
where lenP': "length P' = length hP"
and lenQ': "length Q' = length hQ"
and hP_iso: "set hP ⊆ {f. isometry f}"
and hQ_iso: "set hQ ⊆ {f. isometry f}"
and source_disj': "pairwise_disjoint (P' @ Q')"
and imageP_disj': "pairwise_disjoint (map2 (λg A. g ` A) hP P')"
and imageQ_disj': "pairwise_disjoint (map2 (λg A. g ` A) hQ Q')"
and source_cover': "?Y = (⋃i<length P'. P' ! i) ∪ (⋃i<length Q'. Q' ! i)"
and imageP_cover': "?Y = (⋃i<length P'. (hP ! i) ` (P' ! i))"
and imageQ_cover': "?Y = (⋃i<length Q'. (hQ ! i) ` (Q' ! i))"
by auto
have P'_sub: "∀i < length P'. P' ! i ⊆ ball3"
using source_cover' by blast
have Q'_sub: "∀i < length Q'. Q' ! i ⊆ ball3"
using source_cover' by blast
show ?thesis
proof (intro exI conjI)
show "length P' = length hP"
by (rule lenP')
show "length Q' = length hQ"
by (rule lenQ')
show "∀g∈set hP. isometry g"
using hP_iso by blast
show "∀g∈set hQ. isometry g"
using hQ_iso by blast
show "pairwise_disjoint (P' @ Q')"
by (rule source_disj')
show "pairwise_disjoint (map2 (λg A. g ` A) hP P')"
by (rule imageP_disj')
show "pairwise_disjoint (map2 (λg A. g ` A) hQ Q')"
by (rule imageQ_disj')
show "∀i<length P'. P' ! i ⊆ ball3"
by (rule P'_sub)
show "∀i<length Q'. Q' ! i ⊆ ball3"
by (rule Q'_sub)
show "ball3 = (⋃i<length P'. P' ! i) ∪ (⋃i<length Q'. Q' ! i)"
by (rule source_cover')
show "ball3 = (⋃i<length P'. (hP ! i) ` (P' ! i))"
by (rule imageP_cover')
show "ball3 = (⋃i<length Q'. (hQ ! i) ` (Q' ! i))"
by (rule imageQ_cover')
qed
qed
text ‹An auxiliary finite-cover theorem for the closed unit ball.›
theorem banach_tarski_finite_cover:
"∃P :: (real^3) set list. ∃gs :: ((real^3) ⇒ (real^3)) list.
length P = length gs ∧
(∀g ∈ set gs. isometry g) ∧
(∀i < length P. P ! i ⊆ ball3) ∧
ball3 = (⋃i<length P. P ! i) ∧
(ball3_copy_left ∪ ball3_copy_right) =
(⋃i<length P. (gs ! i) ` (P ! i)) ∧
ball3_copy_left ∩ ball3_copy_right = {}"
proof -
from ball3_paradoxical obtain P Q :: "(real^3) set list"
and gP gQ :: "((real^3 ⇒ real^3)) list"
where decomp:
"length P = length gP ∧ length Q = length gQ ∧
set gP ⊆ SO3 ∧ set gQ ⊆ SO3 ∧
(∀i < length P. P ! i ⊆ ball3) ∧
(∀i < length Q. Q ! i ⊆ ball3) ∧
ball3 = (⋃i<length P. P ! i) ∧
ball3 = (⋃i<length Q. Q ! i) ∧
ball3 = (⋃i<length P. (gP ! i) ` (P ! i)) ∧
ball3 = (⋃i<length Q. (gQ ! i) ` (Q ! i))"
by (elim exE)
from decomp have lenP: "length P = length gP"
by (elim conjE)
from decomp have lenQ: "length Q = length gQ"
by (elim conjE)
from decomp have gP_SO3: "set gP ⊆ SO3"
by (elim conjE)
from decomp have gQ_SO3: "set gQ ⊆ SO3"
by (elim conjE)
from decomp have P_sub: "∀i < length P. P ! i ⊆ ball3"
by (elim conjE)
from decomp have Q_sub: "∀i < length Q. Q ! i ⊆ ball3"
by (elim conjE)
from decomp have P_src: "ball3 = (⋃i<length P. P ! i)"
by (elim conjE)
from decomp have Q_src: "ball3 = (⋃i<length Q. Q ! i)"
by (elim conjE)
from decomp have P_cov: "ball3 = (⋃i<length P. (gP ! i) ` (P ! i))"
by (elim conjE)
from decomp have Q_cov: "ball3 = (⋃i<length Q. (gQ ! i) ` (Q ! i))"
by (elim conjE)
define pieces where "pieces = P @ Q"
define hQ where "hQ = map (λg. (+) shift3 ∘ g) gQ"
define gs where "gs = gP @ hQ"
have len_hQ: "length Q = length hQ"
by (simp add: hQ_def lenQ)
have len: "length pieces = length gs"
by (simp add: pieces_def gs_def lenP len_hQ)
have iso: "∀g ∈ set gs. isometry g"
using gP_SO3 gQ_SO3
by (auto simp add: gs_def hQ_def SO3_isometry)
have sub: "∀i < length pieces. pieces ! i ⊆ ball3"
using P_sub Q_sub by (auto simp add: pieces_def nth_append)
have src: "ball3 = (⋃i<length pieces. pieces ! i)"
proof -
have append_union:
"(⋃i<length (P @ Q). (P @ Q) ! i) =
(⋃i<length P. P ! i) ∪ (⋃i<length Q. Q ! i)"
using indexed_union_append[of P Q] .
have "(⋃i<length pieces. pieces ! i) =
(⋃i<length P. P ! i) ∪ (⋃i<length Q. Q ! i)"
unfolding pieces_def
using append_union .
also have "… = ball3"
using P_src Q_src by simp
finally show ?thesis by simp
qed
have right_cov:
"ball3_copy_right = (⋃i<length Q. (hQ ! i) ` (Q ! i))"
proof -
have right_union:
"(⋃i<length Q. (hQ ! i) ` (Q ! i)) =
(+) shift3 ` (⋃i<length Q. (gQ ! i) ` (Q ! i))"
proof (rule equalityI)
show "(⋃i<length Q. (hQ ! i) ` (Q ! i)) ⊆
(+) shift3 ` (⋃i<length Q. (gQ ! i) ` (Q ! i))"
proof
fix x assume "x ∈ (⋃i<length Q. (hQ ! i) ` (Q ! i))"
then obtain i y where i_lt: "i < length Q" and y_in: "y ∈ Q ! i"
and x_eq: "x = (hQ ! i) y"
by blast
have h_eq: "hQ ! i = (+) shift3 ∘ (gQ ! i)"
using i_lt lenQ by (simp add: hQ_def)
have "(gQ ! i) y ∈ (⋃i<length Q. (gQ ! i) ` (Q ! i))"
using i_lt y_in by blast
moreover have "x = shift3 + (gQ ! i) y"
using x_eq h_eq by simp
ultimately show "x ∈ (+) shift3 ` (⋃i<length Q. (gQ ! i) ` (Q ! i))"
by blast
qed
show "(+) shift3 ` (⋃i<length Q. (gQ ! i) ` (Q ! i)) ⊆
(⋃i<length Q. (hQ ! i) ` (Q ! i))"
proof
fix x assume "x ∈ (+) shift3 ` (⋃i<length Q. (gQ ! i) ` (Q ! i))"
then obtain z i y where x_eq: "x = shift3 + z"
and i_lt: "i < length Q" and y_in: "y ∈ Q ! i" and z_eq: "z = (gQ ! i) y"
by blast
have h_eq: "hQ ! i = (+) shift3 ∘ (gQ ! i)"
using i_lt lenQ by (simp add: hQ_def)
have "x = (hQ ! i) y"
using x_eq z_eq h_eq by simp
thus "x ∈ (⋃i<length Q. (hQ ! i) ` (Q ! i))"
using i_lt y_in by blast
qed
qed
show ?thesis
unfolding ball3_copy_right_def
using right_union Q_cov by simp
qed
have images:
"ball3_copy_left ∪ ball3_copy_right =
(⋃i<length pieces. (gs ! i) ` (pieces ! i))"
proof -
have append_images:
"(⋃i<length (P @ Q). (gP @ hQ) ! i ` ((P @ Q) ! i)) =
(⋃i<length P. (gP ! i) ` (P ! i)) ∪
(⋃i<length Q. (hQ ! i) ` (Q ! i))"
using indexed_image_union_append[OF lenP len_hQ] .
have "(⋃i<length pieces. (gs ! i) ` (pieces ! i)) =
(⋃i<length P. (gP ! i) ` (P ! i)) ∪
(⋃i<length Q. (hQ ! i) ` (Q ! i))"
unfolding pieces_def gs_def
using append_images .
also have "… = ball3_copy_left ∪ ball3_copy_right"
using P_cov right_cov by (simp add: ball3_copy_left_def)
finally show ?thesis by simp
qed
show ?thesis
apply (rule exI[of _ pieces])
apply (rule exI[of _ gs])
using len iso sub src images ball3_copies_disjoint
by simp
qed
text ‹The Banach--Tarski theorem for the closed unit ball, as a partition theorem.›
theorem banach_tarski:
"∃P :: (real^3) set list. ∃gs :: ((real^3) ⇒ (real^3)) list.
length P = length gs ∧
(∀g ∈ set gs. isometry g) ∧
pairwise_disjoint P ∧
pairwise_disjoint (map2 (λg A. g ` A) gs P) ∧
(∀i < length P. P ! i ⊆ ball3) ∧
ball3 = (⋃i<length P. P ! i) ∧
(ball3_copy_left ∪ ball3_copy_right) =
(⋃i<length P. (gs ! i) ` (P ! i)) ∧
ball3_copy_left ∩ ball3_copy_right = {}"
proof -
from ball3_paradoxical_strong obtain P Q :: "(real^3) set list"
and gP gQ :: "((real^3 ⇒ real^3)) list"
where lenP: "length P = length gP"
and lenQ: "length Q = length gQ"
and gP_iso: "∀g ∈ set gP. isometry g"
and gQ_iso: "∀g ∈ set gQ. isometry g"
and source_disj: "pairwise_disjoint (P @ Q)"
and imageP_disj: "pairwise_disjoint (map2 (λg A. g ` A) gP P)"
and imageQ_disj: "pairwise_disjoint (map2 (λg A. g ` A) gQ Q)"
and P_sub: "∀i < length P. P ! i ⊆ ball3"
and Q_sub: "∀i < length Q. Q ! i ⊆ ball3"
and source_cover: "ball3 = (⋃i<length P. P ! i) ∪ (⋃i<length Q. Q ! i)"
and P_cov: "ball3 = (⋃i<length P. (gP ! i) ` (P ! i))"
and Q_cov: "ball3 = (⋃i<length Q. (gQ ! i) ` (Q ! i))"
by auto
define pieces where "pieces = P @ Q"
define hQ where "hQ = map (λg. (+) shift3 ∘ g) gQ"
define gs where "gs = gP @ hQ"
have len_hQ: "length Q = length hQ"
by (simp add: hQ_def lenQ)
have len: "length pieces = length gs"
by (simp add: pieces_def gs_def lenP len_hQ)
have iso: "∀g ∈ set gs. isometry g"
using gP_iso gQ_iso
by (auto simp add: gs_def hQ_def isometry_compose)
have sub: "∀i < length pieces. pieces ! i ⊆ ball3"
using P_sub Q_sub by (auto simp add: pieces_def nth_append)
have src: "ball3 = (⋃i<length pieces. pieces ! i)"
by (metis indexed_union_append pieces_def source_cover)
have source_disj_pieces: "pairwise_disjoint pieces"
using source_disj by (simp add: pieces_def)
have right_cov:
"ball3_copy_right = (⋃i<length Q. (hQ ! i) ` (Q ! i))"
proof -
have right_union:
"(⋃i<length Q. (hQ ! i) ` (Q ! i)) =
(+) shift3 ` (⋃i<length Q. (gQ ! i) ` (Q ! i))"
proof (rule equalityI)
show "(⋃i<length Q. (hQ ! i) ` (Q ! i)) ⊆
(+) shift3 ` (⋃i<length Q. (gQ ! i) ` (Q ! i))"
proof
fix x assume "x ∈ (⋃i<length Q. (hQ ! i) ` (Q ! i))"
then obtain i y where i_lt: "i < length Q" and y_in: "y ∈ Q ! i"
and x_eq: "x = (hQ ! i) y"
by blast
have h_eq: "hQ ! i = (+) shift3 ∘ (gQ ! i)"
using i_lt lenQ by (simp add: hQ_def)
have "(gQ ! i) y ∈ (⋃i<length Q. (gQ ! i) ` (Q ! i))"
using i_lt y_in by blast
moreover have "x = shift3 + (gQ ! i) y"
using x_eq h_eq by simp
ultimately show "x ∈ (+) shift3 ` (⋃i<length Q. (gQ ! i) ` (Q ! i))"
by blast
qed
show "(+) shift3 ` (⋃i<length Q. (gQ ! i) ` (Q ! i)) ⊆
(⋃i<length Q. (hQ ! i) ` (Q ! i))"
proof
fix x assume "x ∈ (+) shift3 ` (⋃i<length Q. (gQ ! i) ` (Q ! i))"
then obtain z i y where x_eq: "x = shift3 + z"
and i_lt: "i < length Q" and y_in: "y ∈ Q ! i" and z_eq: "z = (gQ ! i) y"
by blast
have h_eq: "hQ ! i = (+) shift3 ∘ (gQ ! i)"
using i_lt lenQ by (simp add: hQ_def)
have "x = (hQ ! i) y"
using x_eq z_eq h_eq by simp
thus "x ∈ (⋃i<length Q. (hQ ! i) ` (Q ! i))"
using i_lt y_in by blast
qed
qed
show ?thesis
unfolding ball3_copy_right_def
using right_union Q_cov by simp
qed
have images:
"ball3_copy_left ∪ ball3_copy_right =
(⋃i<length pieces. (gs ! i) ` (pieces ! i))"
proof -
have "(⋃i<length pieces. (gs ! i) ` (pieces ! i)) =
(⋃i<length P. (gP ! i) ` (P ! i)) ∪
(⋃i<length Q. (hQ ! i) ` (Q ! i))"
unfolding pieces_def gs_def
by (rule indexed_image_union_append[OF lenP len_hQ])
also have "… = ball3_copy_left ∪ ball3_copy_right"
using P_cov right_cov by (simp add: ball3_copy_left_def)
finally show ?thesis by simp
qed
have shift_inj: "inj ((+) shift3)"
by (simp add: inj_def)
have right_image_disj: "pairwise_disjoint (map2 (λg A. g ` A) hQ Q)"
unfolding pairwise_disjoint_def
proof (intro allI impI)
fix i j
assume i: "i < length (map2 (λg A. g ` A) hQ Q)"
and j: "j < length (map2 (λg A. g ` A) hQ Q)"
and ij: "i ≠ j"
have iQ: "i < length Q" and jQ: "j < length Q"
using i j len_hQ by auto
have base_disj: "(gQ ! i ` (Q ! i)) ∩ (gQ ! j ` (Q ! j)) = {}"
using imageQ_disj lenQ iQ jQ ij by (simp add: pairwise_disjoint_def)
have hi: "hQ ! i = (+) shift3 ∘ (gQ ! i)"
using iQ lenQ by (simp add: hQ_def)
have hj: "hQ ! j = (+) shift3 ∘ (gQ ! j)"
using jQ lenQ by (simp add: hQ_def)
show "map2 (λg A. g ` A) hQ Q ! i ∩ map2 (λg A. g ` A) hQ Q ! j = {}"
using base_disj shift_inj iQ jQ len_hQ
by (auto simp: hi hj inj_def)
qed
have left_sets_sub: "⋀A. A ∈ set (map2 (λg A. g ` A) gP P) ⟹ A ⊆ ball3_copy_left"
proof -
fix A
assume A: "A ∈ set (map2 (λg A. g ` A) gP P)"
then obtain i where i: "i < length P" and A_eq: "A = (gP ! i) ` (P ! i)"
using lenP by (auto simp: in_set_conv_nth)
have "A ⊆ (⋃i<length P. (gP ! i) ` (P ! i))"
using i A_eq by blast
thus "A ⊆ ball3_copy_left"
using P_cov by (simp add: ball3_copy_left_def)
qed
have right_sets_sub: "⋀A. A ∈ set (map2 (λg A. g ` A) hQ Q) ⟹ A ⊆ ball3_copy_right"
proof -
fix A
assume A: "A ∈ set (map2 (λg A. g ` A) hQ Q)"
then obtain i where i: "i < length Q" and A_eq: "A = (hQ ! i) ` (Q ! i)"
using len_hQ by (auto simp: in_set_conv_nth)
have "A ⊆ (⋃i<length Q. (hQ ! i) ` (Q ! i))"
using i A_eq by blast
thus "A ⊆ ball3_copy_right"
using right_cov by simp
qed
have image_cross_disj:
"⋀A B. ⟦A ∈ set (map2 (λg A. g ` A) gP P);
B ∈ set (map2 (λg A. g ` A) hQ Q)⟧ ⟹ A ∩ B = {}"
proof -
fix A B
assume A: "A ∈ set (map2 (λg A. g ` A) gP P)"
and B: "B ∈ set (map2 (λg A. g ` A) hQ Q)"
have "A ∩ B ⊆ ball3_copy_left ∩ ball3_copy_right"
using left_sets_sub[OF A] right_sets_sub[OF B] by blast
thus "A ∩ B = {}"
using ball3_copies_disjoint by blast
qed
have image_disj: "pairwise_disjoint (map2 (λg A. g ` A) gs pieces)"
unfolding gs_def pieces_def
using pairwise_disjoint_appendI[OF imageP_disj right_image_disj image_cross_disj]
using lenP by fastforce
show ?thesis
proof (intro exI conjI)
show "length pieces = length gs"
by (rule len)
show "∀g∈set gs. isometry g"
by (rule iso)
show "pairwise_disjoint pieces"
by (rule source_disj_pieces)
show "pairwise_disjoint (map2 (λg A. g ` A) gs pieces)"
by (rule image_disj)
show "∀i<length pieces. pieces ! i ⊆ ball3"
by (rule sub)
show "ball3 = (⋃i<length pieces. pieces ! i)"
by (rule src)
show "ball3_copy_left ∪ ball3_copy_right =
(⋃i<length pieces. (gs ! i) ` (pieces ! i))"
by (rule images)
show "ball3_copy_left ∩ ball3_copy_right = {}"
by (rule ball3_copies_disjoint)
qed
qed
end