English
For every real r, the intersection of unitLattice(K) with the closed ball of radius r is finite.
Русский
Для каждого $r$ пересечение единичного латИСа c шаром радиуса $r$ конечно.
LaTeX
$$$((\mathrm{unitLattice}(K) : Set (\logSpace K)) \cap \mathrm{Metric.closedBall} 0\; r).Finite$$$
Lean4
theorem unitLattice_inter_ball_finite (r : ℝ) : ((unitLattice K : Set (logSpace K)) ∩ Metric.closedBall 0 r).Finite :=
by
obtain hr | hr := lt_or_ge r 0
· convert Set.finite_empty
rw [Metric.closedBall_eq_empty.mpr hr]
exact Set.inter_empty _
· suffices
{x : (𝓞 K)ˣ |
IsIntegral ℤ (x : K) ∧ ∀ (φ : K →+* ℂ), ‖φ x‖ ≤ Real.exp ((Fintype.card (InfinitePlace K)) * r)}.Finite
by
refine (Set.Finite.image (logEmbedding K) this).subset ?_
rintro _ ⟨⟨x, ⟨_, rfl⟩⟩, hx⟩
refine ⟨x, ⟨x.val.prop, (le_iff_le _ _).mp (fun w ↦ (Real.log_le_iff_le_exp ?_).mp ?_)⟩, rfl⟩
· exact pos_iff.mpr (coe_ne_zero x)
· rw [mem_closedBall_zero_iff] at hx
exact (le_abs_self _).trans (log_le_of_logEmbedding_le hr hx w)
refine Set.Finite.of_finite_image ?_ (coe_injective K).injOn
refine (Embeddings.finite_of_norm_le K ℂ (Real.exp ((Fintype.card (InfinitePlace K)) * r))).subset ?_
rintro _ ⟨x, ⟨⟨h_int, h_le⟩, rfl⟩⟩
exact ⟨h_int, h_le⟩
