Theory Minkowskis_Theorem

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

  A proof of Blichfeldt's and Minkowski's theorem about the relation between
  subsets of the Euclidean space, the Lebesgue measure, and the integer lattice.
*)
section ‹Minkowski's theorem›
theory Minkowskis_Theorem
  imports "HOL-Analysis.Equivalence_Lebesgue_Henstock_Integration"
begin

(* Could be generalised to arbitrary euclidean spaces and full-dimensional lattices *)

subsection ‹Miscellaneous material›

lemma bij_betw_UN:
  assumes "bij_betw f A B"
  shows   "(⋃n∈A. g (f n)) = (⋃n∈B. g n)"
  using assms by (auto simp: bij_betw_def)

definition of_int_vec where
  "of_int_vec v = (χ i. of_int (v $ i))"

lemma of_int_vec_nth [simp]: "of_int_vec v $ n = of_int (v $ n)"
  by (simp add: of_int_vec_def)

lemma of_int_vec_eq_iff [simp]:
  "(of_int_vec a :: ('a :: ring_char_0) ^ 'n) = of_int_vec b ⟷ a = b"
  by (simp add: of_int_vec_def vec_eq_iff)

lemma inj_axis:
  assumes "c ≠ 0"
  shows   "inj (λk. axis k c :: ('a :: {zero}) ^ 'n)"
proof
  fix x y :: 'n
  assume *: "axis x c = axis y c"
  have "axis x c $ x = axis x c $ y"
    by (subst *) simp
  thus "x = y" using assms
    by (auto simp: axis_def split: if_splits)
qed

lemma compactD:
  assumes "compact (A :: 'a :: metric_space set)" "range f ⊆ A"
  shows   "∃h l. strict_mono (h::nat⇒nat) ∧ (f ∘ h) ⇢ l"
  using assms unfolding compact_def by blast

lemma closed_lattice:
  fixes A :: "(real ^ 'n) set"
  assumes "⋀v i. v ∈ A ⟹ v $ i ∈ ℤ"
  shows   "closed A"
proof (rule discrete_imp_closed[OF zero_less_one], safe, goal_cases)
  case (1 x y)
  have "x $ i = y $ i" for i
  proof -
    from 1 and assms have "x $ i - y $ i ∈ ℤ"
      by auto
    then obtain m where m: "of_int m = (x $ i - y $ i)"
      by (elim Ints_cases) auto
    hence "of_int (abs m) = abs ((x - y) $ i)"
      by simp
    also have "… ≤ norm (x - y)"
      by (rule component_le_norm_cart)
    also have "… < of_int 1"
      using 1 by (simp add: dist_norm norm_minus_commute)
    finally have "abs m < 1"
      by (subst (asm) of_int_less_iff)
    thus "x $ i = y $ i"
      using m by simp
  qed
  thus "y = x"
    by (simp add: vec_eq_iff)
qed


subsection ‹Auxiliary theorems about measure theory›

lemma emeasure_lborel_cbox_eq':
  "emeasure lborel (cbox a b) = ennreal (∏e∈Basis. max 0 ((b - a) ∙ e))"
proof (cases "∀ba∈Basis. a ∙ ba ≤ b ∙ ba")
  case True
  hence "emeasure lborel (cbox a b) = ennreal (prod ((∙) (b - a)) Basis)"
    unfolding emeasure_lborel_cbox_eq by auto
  also have "prod ((∙) (b - a)) Basis = (∏e∈Basis. max 0 ((b - a) ∙ e))"
    using True by (intro prod.cong refl) (auto simp: max_def inner_simps)
  finally show ?thesis .
next
  case False
  hence "emeasure lborel (cbox a b) = ennreal 0"
    by (auto simp: emeasure_lborel_cbox_eq)
  also from False have "0 = (∏e∈Basis. max 0 ((b - a) ∙ e))"
    by (auto simp: max_def inner_simps)
  finally show ?thesis .
qed

lemma emeasure_lborel_cbox_cart_eq:
  fixes a b :: "real ^ ('n :: finite)"
  shows "emeasure lborel (cbox a b) = ennreal (∏i ∈ UNIV. max 0 ((b - a) $ i))"
proof -
  have "emeasure lborel (cbox a b) = ennreal (∏e∈Basis. max 0 ((b - a) ∙ e))"
    unfolding emeasure_lborel_cbox_eq' ..
  also have "(Basis :: (real ^ 'n) set) = range (λk. axis k 1)"
    unfolding Basis_vec_def by auto
  also have "(∏e∈…. max 0 ((b - a) ∙ e)) = (∏ i ∈ UNIV . max 0 ((b - a) $ i))"
    by (subst prod.reindex) (auto intro!: inj_axis simp: algebra_simps inner_axis)
  finally show ?thesis .
qed

lemma sum_emeasure':
  assumes [simp]: "finite A"
  assumes [measurable]: "⋀x. x ∈ A ⟹ B x ∈ sets M"
  assumes "⋀x y. x ∈ A ⟹ y ∈ A ⟹ x ≠ y ⟹ emeasure M (B x ∩ B y) = 0"
  shows   "(∑x∈A. emeasure M (B x)) = emeasure M (⋃x∈A. B x)"
proof -
  define C where "C = (⋃x∈A. ⋃y∈(A-{x}). B x ∩ B y)"
  have C: "C ∈ null_sets M"
    unfolding C_def using assms
    by (intro null_sets.finite_UN) (auto simp: null_sets_def)
  hence [measurable]: "C ∈ sets M" and [simp]: "emeasure M C = 0"
    by (simp_all add: null_sets_def)
  have "(⋃x∈A. B x) = (⋃x∈A. B x - C) ∪ C"
    by (auto simp: C_def)
  also have "emeasure M … = emeasure M (⋃x∈A. B x - C)"
    by (subst emeasure_Un_null_set) (auto intro!: sets.Un sets.Diff)
  also from assms have "… = (∑x∈A. emeasure M (B x - C))"
    by (subst sum_emeasure)
       (auto simp: disjoint_family_on_def C_def intro!: sets.Diff sets.finite_UN)
  also have "… = (∑x∈A. emeasure M (B x))"
    by (intro sum.cong refl emeasure_Diff_null_set) auto
  finally show ?thesis ..
qed

lemma sums_emeasure':
  assumes [measurable]: "⋀x. B x ∈ sets M"
  assumes "⋀x y. x ≠ y ⟹ emeasure M (B x ∩ B y) = 0"
  shows   "(λx. emeasure M (B x)) sums emeasure M (⋃x. B x)"
proof -
  define C where "C = (⋃x. ⋃y∈-{x}. B x ∩ B y)"
  have C: "C ∈ null_sets M"
    unfolding C_def using assms
    by (intro null_sets_UN') (auto simp: null_sets_def)
  hence [measurable]: "C ∈ sets M" and [simp]: "emeasure M C = 0"
    by (simp_all add: null_sets_def)
  have "(⋃x. B x) = (⋃x. B x - C) ∪ C"
    by (auto simp: C_def)
  also have "emeasure M … = emeasure M (⋃x. B x - C)"
    by (subst emeasure_Un_null_set) (auto intro!: sets.Un sets.Diff)
  also from assms have "(λx. emeasure M (B x - C)) sums …  "
    by (intro sums_emeasure)
       (auto simp: disjoint_family_on_def C_def intro!: sets.Diff sets.finite_UN)
  also have "(λx. emeasure M (B x - C)) = (λx. emeasure M (B x))"
    by (intro ext emeasure_Diff_null_set) auto
  finally show ?thesis .
qed


subsection ‹Blichfeldt's theorem›

text ‹
  Blichfeldt's theorem states that, given a subset of $\mathbb{R}^n$ with $n > 0$ and a
  volume of more than 1, there exist two different points in that set whose difference
  vector has integer components.

  This will be the key ingredient in proving Minkowski's theorem.

  Note that in the HOL Light version, it is additionally required -- both for
  Blichfeldt's theorem and for Minkowski's theorem -- that the set is bounded,
  which we do not need.
›
proposition blichfeldt:
  fixes S :: "(real ^ 'n) set"
  assumes [measurable]: "S ∈ sets lebesgue"
  assumes "emeasure lebesgue S > 1"
  obtains x y where "x ≠ y" and "x ∈ S" and "y ∈ S" and "⋀i. (x - y) $ i ∈ ℤ"
proof -
  ― ‹We define for each lattice point in $\mathbb{Z}^n$ the corresponding cell in $\mathbb{R}^n$.›
  define R :: "int ^ 'n ⇒ (real ^ 'n) set"
    where "R = (λa. cbox (of_int_vec a) (of_int_vec (a + 1)))"

  ― ‹For each lattice point, we can intersect the cell it defines with our set @{term S}
      to obtain a partitioning of @{term S}.›
  define T :: "int ^ 'n ⇒ (real ^ 'n) set"
    where "T = (λa. S ∩ R a)"

  ― ‹We can then translate each such partition into the cell at the origin, i.\,e. the
      unit box @{term "R 0"}.›
  define T' :: "int ^ 'n ⇒ (real ^ 'n) set"
    where "T' = (λa. (λx. x - of_int_vec a) ` T a)"
  have T'_altdef: "T' a = (λx. x + of_int_vec a) -` T a" for a
    unfolding T'_def by force

  ― ‹We need to show measurability of all the defined sets.›
  have [measurable, simp]: "R a ∈ sets lebesgue" for a
    unfolding R_def by simp
  have [measurable, simp]: "T a ∈ sets lebesgue" for a
    unfolding T_def by auto
  have "(λx::real^'n. x + of_int_vec a) ∈ lebesgue →⇩M lebesgue" for a
    using lebesgue_affine_measurable[of "λ_. 1" "of_int_vec a"]
    by (auto simp: euclidean_representation add_ac)
  from measurable_sets[OF this, of "T a" a for a]
    have [measurable, simp]: "T' a ∈ sets lebesgue" for a
      unfolding T'_altdef by simp

  ― ‹Obviously, the original set @{term S} is the union of all the lattice
      point cell partitions.›
  have S_decompose: "S = (⋃a. T a)" unfolding T_def
  proof safe
    fix x assume x: "x ∈ S"
    define a where "a = (χ i. ⌊x $ i⌋)"
    have "x ∈ R a"
      unfolding R_def
      by (auto simp: cbox_interval less_eq_vec_def of_int_vec_def a_def)
    with x show "x ∈ (⋃a. S ∩ R a)" by auto
  qed

  ― ‹Translating the partitioned subsets does not change their volume.›
  have emeasure_T': "emeasure lebesgue (T' a) = emeasure lebesgue (T a)" for a
  proof -
    have "T' a = (λx. 1 *⇩R x + (- of_int_vec a)) ` T a"
      by (simp add: T'_def)
    also have "emeasure lebesgue … = emeasure lebesgue (T a)"
      by (subst emeasure_lebesgue_affine) auto
    finally show ?thesis
      by simp
  qed

  ― ‹Each translated partition of @{term S} is a subset of the unit cell at the origin.›
  have T'_subset: "T' a ⊆ cbox 0 1" for a
    unfolding T'_def T_def R_def
    by (auto simp: algebra_simps cbox_interval of_int_vec_def less_eq_vec_def)

  ― ‹It is clear that the intersection of two different lattice point cells is a null set.›
  have R_Int: "R a ∩ R b ∈ null_sets lebesgue" if "a ≠ b" for a b
  proof -
    from that obtain i where i: "a $ i ≠ b $ i"
      by (auto simp: vec_eq_iff)
    have "R a ∩ R b = cbox (χ i. max (a $ i) (b $ i)) (χ i. min (a $ i + 1) (b $ i + 1))"
      unfolding Int_interval_cart R_def interval_cbox
      by (simp add: of_int_vec_def max_def min_def if_distrib cong: if_cong)
    hence "emeasure lebesgue (R a ∩ R b) = emeasure lborel …"
      by simp
    also have "… = ennreal (∏i∈UNIV. max 0 (((χ x. real_of_int (min (a $ x + 1) (b $ x + 1))) -
                                  (χ x. real_of_int (max (a $ x) (b $ x)))) $ i))"
      (is "_ = ennreal ?P")
      unfolding emeasure_lborel_cbox_cart_eq by simp
    also have "?P = 0"
      using i by (auto simp: max_def intro!: exI[of _ i])
    finally show ?thesis
      by (auto simp: null_sets_def R_def)
  qed

  ― ‹Therefore, the intersection of two lattice point cell partitionings of @{term S} is
      also a null set.›
  have T_Int: "T a ∩ T b ∈ null_sets lebesgue" if "a ≠ b" for a b
  proof -
    have "T a ∩ T b = (R a ∩ R b) ∩ S"
      by (auto simp: T_def)
    also have "… ∈ null_sets lebesgue"
      by (rule null_set_Int2) (insert that, auto intro: R_Int assms)
    finally show ?thesis .
  qed
  have emeasure_T_Int: "emeasure lebesgue (T a ∩ T b) = 0" if "a ≠ b" for a b
    using T_Int[OF that] unfolding null_sets_def by blast

  ― ‹The set of lattice points $\mathbb{Z}^n$ is countably infinite, so there exists
      a bijection $f: \mathbb{N} \to \mathbb{Z}^n$. We need this for summing over all
      lattice points.›
  define f :: "nat ⇒ int ^ 'n" where "f = from_nat_into UNIV"
  have "countable (UNIV :: (int ^ 'n) set)" "infinite (UNIV :: (int ^ 'n) set)"
    using infinite_UNIV_char_0 by simp_all
  from bij_betw_from_nat_into [OF this] have f: "bij f"
    by (simp add: f_def)

  ― ‹Suppose all the translated cell partitions @{term T'} are disjoint.›
  {
    assume disjoint: "⋀a b. a ≠ b ⟹ T' a ∩ T' b = {}"
    ― ‹We know by assumption that the volume of @{term S} is greater than 1.›
    have "1 < emeasure lebesgue S" by fact
    also have "emeasure lebesgue S = emeasure lebesgue (⋃n. T' (f n))"
    proof -
      ― ‹The sum of the volumes of all the @{term T'} is precisely the volume
          of their union, which is @{term "S"}.›
      have "S = (⋃a. T a)" by (rule S_decompose)
      also have "… = (⋃n. T (f n))"
        by (rule bij_betw_UN [OF f, symmetric])
      also have "(λn. emeasure lebesgue (T (f n))) sums emeasure lebesgue …"
        by (intro sums_emeasure' emeasure_T_Int) (insert f, auto simp: bij_betw_def inj_on_def)
      also have "(λn. emeasure lebesgue (T (f n))) = (λn. emeasure lebesgue (T' (f n)))"
        by (simp add: emeasure_T')
      finally have "(λn. emeasure lebesgue (T' (f n))) sums emeasure lebesgue S" .
      moreover have "(λn. emeasure lebesgue (T' (f n))) sums emeasure lebesgue (⋃n. T' (f n))"
        using disjoint by (intro sums_emeasure)
                          (insert f, auto simp: disjoint_family_on_def bij_betw_def inj_on_def)
      ultimately show ?thesis
        by (auto simp: sums_iff)
    qed
    ― ‹On the other hand, all the translated partitions lie in the unit cell
        @{term "cbox (0 :: real ^ 'n) 1"}, so their combined volume cannot be
        greater than 1.›
    also have "emeasure lebesgue (⋃n. T' (f n)) ≤ emeasure lebesgue (cbox 0 (1 :: real ^ 'n))"
      using T'_subset by (intro emeasure_mono) auto
    also have "… = 1"
      by (simp add: emeasure_lborel_cbox_cart_eq)
    ― ‹This leads to a contradiction.›
    finally have False by simp
  }
  ― ‹Therefore, there exists a point that lies in two different translated partitions,
      which obviously corresponds two two points in the non-translated partitions
      whose difference is the difference between two lattice points and therefore
      has integer components.›
  then obtain a b x where "a ≠ b" "x ∈ T' a" "x ∈ T' b"
    by auto
  thus ?thesis
    by (intro that[of "x + of_int_vec a" "x + of_int_vec b"])
       (auto simp: T'_def T_def algebra_simps)
qed


subsection ‹Minkowski's theorem›

text ‹
  Minkowski's theorem now states that, given a convex subset of $\mathbb{R}^n$ that is
  symmetric around the origin and has a volume greater than $2^n$, that set must contain
  a non-zero point with integer coordinates.
›
theorem minkowski:
  fixes B :: "(real ^ 'n) set"
  assumes "convex B" and symmetric: "uminus ` B ⊆ B"
  assumes meas_B [measurable]: "B ∈ sets lebesgue"
  assumes measure_B: "emeasure lebesgue B > 2 ^ CARD('n)"
  obtains x where "x ∈ B" and "x ≠ 0" and "⋀i. x $ i ∈ ℤ"
proof -
  ― ‹We scale @{term B} with $\frac{1}{2}$.›
  define B' where "B' = (λx. 2 *⇩R x) -` B"
  have meas_B' [measurable]: "B' ∈ sets lebesgue"
    using measurable_sets[OF lebesgue_measurable_scaling[of 2] meas_B]
    by (simp add: B'_def)
  have B'_altdef: "B' = (λx. (1/2) *⇩R x) ` B"
    unfolding B'_def by force

  ― ‹The volume of the scaled set is $2^n$ times smaller than the original set, and
      therefore still has a volume greater than 1.›
  have "1 < ennreal ((1 / 2) ^ CARD('n)) * emeasure lebesgue B"
  proof (cases "emeasure lebesgue B")
    case (real x)
    have "ennreal (2 ^ CARD('n)) = 2 ^ CARD('n)"
      by (subst ennreal_power [symmetric]) auto
    also from measure_B and real have "… < ennreal x" by simp
    finally have "(2 ^ CARD('n)) < x"
      by (subst (asm) ennreal_less_iff) auto
    thus ?thesis
      using real by (simp add: ennreal_1 [symmetric] ennreal_mult' [symmetric]
                       ennreal_less_iff field_simps del: ennreal_1)
  qed (simp_all add: ennreal_mult_top)
  also have "… = emeasure lebesgue B'"
    unfolding B'_altdef using emeasure_lebesgue_affine[of "1/2" 0 B] by simp
  finally have *: "emeasure lebesgue B' > 1" .

  ― ‹We apply Blichfeldt's theorem to get two points whose difference vector has
      integer coefficients. It only remains to show that that difference vector is
      itself a point in the original set.›
  obtain x y
    where xy: "x ≠ y" "x ∈ B'" "y ∈ B'" "⋀i. (x - y) $ i ∈ ℤ"
    by (erule blichfeldt [OF meas_B' *])
  hence "2 *⇩R x ∈ B" "2 *⇩R y ∈ B" by (auto simp: B'_def)
  ― ‹Exploiting the symmetric of @{term B}, the reflection of @{term "2 *⇩R y"} is
      also in @{term B}.›
  moreover from this and symmetric have "-(2 *⇩R y) ∈ B" by blast
  ― ‹Since @{term B} is convex, the mid-point between @{term "2 *⇩R x"} and @{term "-2 *⇩R y"}
      is also in @{term B}, and that point is simply @{term "x - y"} as desired.›
  ultimately have "(1 / 2) *⇩R 2 *⇩R x + (1 / 2) *⇩R (- 2 *⇩R y) ∈ B"
    using ‹convex B› by (intro convexD) auto
  also have "(1 / 2) *⇩R 2 *⇩R x + (1 / 2) *⇩R (- 2 *⇩R y) = x - y"
    by simp
  finally show ?thesis using xy
    by (intro that[of "x - y"]) auto
qed

text ‹
  If the set in question is compact, the restriction to the volume can be weakened
  to ``at least 1'' from ``greater than 1''.
›
theorem minkowski_compact:
  fixes B :: "(real ^ 'n) set"
  assumes "convex B" and "compact B" and symmetric: "uminus ` B ⊆ B"
  assumes measure_B: "emeasure lebesgue B ≥ 2 ^ CARD('n)"
  obtains x where "x ∈ B" and "x ≠ 0" and "⋀i. x $ i ∈ ℤ"
proof (cases "emeasure lebesgue B = 2 ^ CARD('n)")
  ― ‹If the volume is greater than 1, we can just apply the theorem from before.›
  case False
  with measure_B have less: "emeasure lebesgue B > 2 ^ CARD('n)"
    by simp
  from ‹compact B› have meas: "B ∈ sets lebesgue"
    by (intro sets_completionI_sets lborelD borel_closed compact_imp_closed)
  from minkowski[OF assms(1) symmetric meas less] and that
    show ?thesis by blast
next
  case True
  ― ‹If the volume is precisely one, we look at what happens when @{term B} is
      scaled with a factor of $1 + \varepsilon$.›
  define B' where "B' = (λε. (*⇩R) (1 + ε) ` B)"
  from ‹compact B› have compact': "compact (B' ε)" for ε
    unfolding B'_def by (intro compact_scaling)
  have B'_altdef: "B' ε = (*⇩R) (inverse (1 + ε)) -` B" if ε: "ε > 0" for ε
    using ε unfolding B'_def by force

  ― ‹Since the scaled sets are convex, they are stable under scaling.›
  have B_scale: "a *⇩R x ∈ B" if "x ∈ B" "a ∈ {0..1}" for a x
  proof -
    have "((a + 1) / 2) *⇩R x + (1 - ((a + 1) / 2)) *⇩R (-x) ∈ B"
      using that and ‹convex B› and symmetric by (intro convexD) auto
    also have "((a + 1) / 2) *⇩R x + (1 - ((a + 1) / 2)) *⇩R (-x) =
                 (1 + a) *⇩R ((1/2) *⇩R (x + x)) - x"
      by (simp add: algebra_simps del: scaleR_half_double)
    also have "… = a *⇩R x"
      by (subst scaleR_half_double) (simp add: algebra_simps)
    finally show "… ∈ B" .
  qed

  ― ‹This means that @{term B'} is monotonic.›
  have B'_subset: "B' a ⊆ B' b" if "0 ≤ a" "a ≤ b" for a b
  proof
    fix x assume "x ∈ B' a"
    then obtain y where "x = (1 + a) *⇩R y" "y ∈ B"
      by (auto simp: B'_def)
    moreover then have "(inverse (1 + b) * (1 + a)) *⇩R y ∈ B"
      using that by (intro B_scale) (auto simp: field_simps)
    ultimately show "x ∈ B' b"
      using that by (force simp: B'_def)
  qed

  ― ‹We obtain some upper bound on the norm of @{term B}.›
  from ‹compact B› have "bounded B"
    by (rule compact_imp_bounded)
  then obtain C where C: "norm x ≤ C" if "x ∈ B" for x
    unfolding bounded_iff by blast

  ― ‹We can then bound the distance of any point in a scaled set to the original set.›
  have setdist_le: "setdist {x} B ≤ ε * C" if "x ∈ B' ε" and "ε ≥ 0" for x ε
  proof -
    from that obtain y where y: "y ∈ B" and [simp]: "x = (1 + ε) *⇩R y"
      by (auto simp: B'_def)
    from y have "setdist {x} B ≤ dist x y"
      by (intro setdist_le_dist) auto
    also from that have "dist x y = ε * norm y"
      by (simp add: dist_norm algebra_simps)
    also from y have "norm y ≤ C"
      by (rule C)
    finally show "setdist {x} B ≤ ε * C"
      using that by (simp add: mult_left_mono)
  qed

  ― ‹By applying the standard Minkowski theorem to the a scaled set, we can see that
      any scaled set contains a non-zero point with integer coordinates.›
  have "∃v. v ∈ B' ε - {0} ∧ (∀i. v $ i ∈ ℤ)" if ε: "ε > 0" for ε
  proof -
    from ‹convex B› have convex': "convex (B' ε)"
      unfolding B'_def by (rule convex_scaling)
    from ‹compact B› have meas: "B' ε ∈ sets lebesgue" unfolding B'_def
      by (intro sets_completionI_sets lborelD borel_closed compact_imp_closed compact_scaling)
    from symmetric have symmetric': "uminus ` B' ε ⊆ B' ε"
      by (auto simp: B'_altdef[OF ε])

    have "2 ^ CARD('n) = ennreal (2 ^ CARD('n))"
      by (subst ennreal_power [symmetric]) auto
    hence "1 * emeasure lebesgue B < ennreal ((1 + ε) ^ CARD('n)) * emeasure lebesgue B"
      using True and ε by (intro ennreal_mult_strict_right_mono) (auto)
    also have "… = emeasure lebesgue (B' ε)"
      using emeasure_lebesgue_affine[of "1+ε" 0 B] and ε by (simp add: B'_def)
    finally have measure_B': "emeasure lebesgue (B' ε) > 2 ^ CARD('n)"
      using True by simp
   
    obtain v where "v ∈ B' ε" "v ≠ 0" "⋀i. v $ i ∈ ℤ"
      by (erule minkowski[OF convex' symmetric' meas measure_B'])
    thus ?thesis
      by blast
  qed
  hence "∀n. ∃v. v ∈ B' (1/Suc n) - {0} ∧ (∀i. v $ i ∈ ℤ)"
    by auto
  ― ‹In particular, this means we can choose some sequence tending to zero
      -- say $\frac{1}{n+1}$ -- and always find a lattice point in the scaled set.›
  hence "∃v. ∀n. v n ∈ B' (1/Suc n) - {0} ∧ (∀i. v n $ i ∈ ℤ)"
    by (subst (asm) choice_iff)
  then obtain v where v: "v n ∈ B' (1/Suc n) - {0}" "v n $ i ∈ ℤ" for i n
    by blast

  ― ‹By the Bolzano--Weierstra{\ss} theorem, there exists a convergent subsequence of @{term v}.›
  have "∃h l. strict_mono (h::nat⇒nat) ∧ (v ∘ h) ⇢ l"
  proof (rule compactD)
    show "compact (B' 1)" by (rule compact')
    show "range v ⊆ B' 1"
      using B'_subset[of "1/Suc n" 1 for n] and v by auto
  qed
  then obtain h l where h: "strict_mono h" and l: "(v ∘ h) ⇢ l"
    by blast

  ― ‹Since the convergent subsequence tends to @{term l}, the distance of the
      sequence elements to @{term B} tends to the distance of @{term l} and @{term B}.
      Furthermore, the distance of the sequence elements is bounded by $(1+\varepsilon)C$,
      which tends to 0, so the distance of @{term l} to @{term B} must be 0.›
  have "setdist {l} B ≤ 0"
  proof (rule tendsto_le)
    show "((λx. setdist {x} B) ∘ (v ∘ h)) ⇢ setdist {l} B"
      by (intro continuous_imp_tendsto l continuous_at_setdist)
    show "(λn. inverse (Suc (h n)) * C) ⇢ 0"
      by (intro tendsto_mult_left_zero filterlim_compose[OF _ filterlim_subseq[OF h]]
                LIMSEQ_inverse_real_of_nat)
    show "∀⇩F x in sequentially. ((λx. setdist {x} B) ∘ (v ∘ h)) x
                                  ≤ inverse (real (Suc (h x))) * C"
      using setdist_le and v unfolding o_def
      by (intro always_eventually allI setdist_le) (auto simp: field_simps)
  qed auto
  hence "setdist {l} B = 0"
    by (intro antisym setdist_pos_le)
  with assms and ‹compact B› have "l ∈ B"
    by (subst (asm) setdist_eq_0_closed) (auto intro: compact_imp_closed)

  ― ‹It is also easy to see that, since the lattice is a closed set and all sequence
      elements lie on it, the limit @{term l} also lies on it.›
  moreover have "l ∈ {l. ∀i. l $ i ∈ ℤ} - {0}"
    using v by (intro closed_sequentially[OF closed_lattice _ l]) auto
  ultimately show ?thesis using that by blast
qed

end