From 96c6d9b99c5d32539c519019fdf39cf2924408ff Mon Sep 17 00:00:00 2001 From: Chris Birkbeck Date: Mon, 22 Jun 2026 07:57:37 +0100 Subject: [PATCH 1/2] feat(ForMathlib): index-image finiteness for bounded sets (1/4) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Adds `CebotarevDensity/ForMathlib/IndexImageCount.lean` with `setFinite_index_image_of_isBounded`: the `index n`-image of a bounded set is finite. Stated with `[Finite ι]` (Fintype recovered in the proof). The diameter/chart/frontier counts and their helpers follow in the stacked PRs 2/4-4/4. Wired into the umbrella import. Co-Authored-By: Claude Opus 4.8 (1M context) --- CebotarevDensity.lean | 1 + .../ForMathlib/IndexImageCount.lean | 64 +++++++++++++++++++ 2 files changed, 65 insertions(+) create mode 100644 CebotarevDensity/ForMathlib/IndexImageCount.lean diff --git a/CebotarevDensity.lean b/CebotarevDensity.lean index 94dee4c..40af2e5 100644 --- a/CebotarevDensity.lean +++ b/CebotarevDensity.lean @@ -1,3 +1,4 @@ import CebotarevDensity.Density +import CebotarevDensity.ForMathlib.IndexImageCount import CebotarevDensity.ForMathlib.LogOneDivSubOne import CebotarevDensity.Main diff --git a/CebotarevDensity/ForMathlib/IndexImageCount.lean b/CebotarevDensity/ForMathlib/IndexImageCount.lean new file mode 100644 index 0000000..06b2454 --- /dev/null +++ b/CebotarevDensity/ForMathlib/IndexImageCount.lean @@ -0,0 +1,64 @@ +module + +public import Mathlib.Analysis.BoxIntegral.UnitPartition +public import Mathlib.Data.Pi.Interval +public import Mathlib.Data.Set.Card.Arithmetic +public import Mathlib.Topology.MetricSpace.Lipschitz + +/-! +# Index-image counting bounds for the scaled integer lattice + +Counting bounds for the image `index n '' T ⊆ ι → ℤ` of a set under the unit-partition `index` +map. Finiteness for bounded `T` (`setFinite_index_image_of_isBounded`), a diameter bound +(`ncard_index_image_le_of_diam_le`), and the resulting `O(nᵈ⁻¹)` boundary-cell bounds for a single +Lipschitz chart (`ncard_index_image_chart_le`) and for a Lipschitz-covered frontier +(`ncard_index_image_frontier_le`). These are the boundary-cell inputs to the effective +lattice-point count in `LatticePointCount.lean`. + +## References + +* Serge Lang, *Algebraic Number Theory*, 2nd ed., GTM 110, Springer 1994, Ch. VI §3 (p. 129). +* S. Gun, O. Ramaré, J. Sivaraman, *Counting ideals in ray classes*, J. Number Theory 243 (2023) + §3.3, after K. Debaene. +-/ + +open Submodule Pointwise MeasureTheory Set BoxIntegral BoxIntegral.unitPartition + +open scoped NNReal + +namespace Chebotarev + +@[expose] public section + +section Sublemmas + +variable {ι : Type*} [Fintype ι] + +omit [Fintype ι] in +/-- The `index n`-image of a bounded set is finite: only finitely many cells of the `n⁻¹ℤ^ι` +grid meet a bounded set. -/ +theorem setFinite_index_image_of_isBounded [Finite ι] (n : ℕ) {T : Set (ι → ℝ)} + (hbdd : Bornology.IsBounded T) : (index n '' T).Finite := by + classical + haveI : Fintype ι := Fintype.ofFinite ι + obtain ⟨R, hR⟩ := hbdd.subset_closedBall (0 : ι → ℝ) + set F : Finset (ι → ℤ) := + Fintype.piFinset fun _ : ι ↦ Finset.Icc (⌈-((n : ℝ) * R)⌉ - 1) (⌈(n : ℝ) * R⌉ - 1) with hF + refine Set.Finite.subset (Finset.finite_toSet F) ?_ + rintro _ ⟨x, hx, rfl⟩ + simp only [hF, Finset.mem_coe, Fintype.mem_piFinset, Finset.mem_Icc, index_apply] + intro i + have hxi : |x i| ≤ R := by + have hd : dist (x i) ((0 : ι → ℝ) i) ≤ dist x 0 := dist_le_pi_dist x 0 i + rw [Real.dist_eq, Pi.zero_apply, sub_zero] at hd + exact hd.trans (by simpa [Real.dist_eq] using hR hx) + rcases abs_le.mp hxi with ⟨hlo, hhi⟩ + have hn0 : (0 : ℝ) ≤ (n : ℝ) := Nat.cast_nonneg n + exact ⟨sub_le_sub_right (Int.ceil_le_ceil (by nlinarith)) 1, + sub_le_sub_right (Int.ceil_le_ceil (by nlinarith)) 1⟩ + +end Sublemmas + +end + +end Chebotarev From 79cc17e9536d3518543c140ffae81d0ccd8c22ae Mon Sep 17 00:00:00 2001 From: Xavier Roblot <46200072+xroblot@users.noreply.github.com> Date: Tue, 23 Jun 2026 15:14:38 +0200 Subject: [PATCH 2/2] refactor(IndexImageCount): drop vestigial Fintype variable, golf proof MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Remove the section-level [Fintype ι] (and its omit) now that the sole remaining lemma uses [Finite ι]. Golf: have over haveI, dot-notation .subset, and fold the cast-nonneg fact into nlinarith. Co-Authored-By: Claude Opus 4.8 --- CebotarevDensity/ForMathlib/IndexImageCount.lean | 8 +++----- 1 file changed, 3 insertions(+), 5 deletions(-) diff --git a/CebotarevDensity/ForMathlib/IndexImageCount.lean b/CebotarevDensity/ForMathlib/IndexImageCount.lean index 06b2454..d82abd7 100644 --- a/CebotarevDensity/ForMathlib/IndexImageCount.lean +++ b/CebotarevDensity/ForMathlib/IndexImageCount.lean @@ -32,19 +32,18 @@ namespace Chebotarev section Sublemmas -variable {ι : Type*} [Fintype ι] +variable {ι : Type*} -omit [Fintype ι] in /-- The `index n`-image of a bounded set is finite: only finitely many cells of the `n⁻¹ℤ^ι` grid meet a bounded set. -/ theorem setFinite_index_image_of_isBounded [Finite ι] (n : ℕ) {T : Set (ι → ℝ)} (hbdd : Bornology.IsBounded T) : (index n '' T).Finite := by classical - haveI : Fintype ι := Fintype.ofFinite ι + have : Fintype ι := Fintype.ofFinite ι obtain ⟨R, hR⟩ := hbdd.subset_closedBall (0 : ι → ℝ) set F : Finset (ι → ℤ) := Fintype.piFinset fun _ : ι ↦ Finset.Icc (⌈-((n : ℝ) * R)⌉ - 1) (⌈(n : ℝ) * R⌉ - 1) with hF - refine Set.Finite.subset (Finset.finite_toSet F) ?_ + refine (Finset.finite_toSet F).subset ?_ rintro _ ⟨x, hx, rfl⟩ simp only [hF, Finset.mem_coe, Fintype.mem_piFinset, Finset.mem_Icc, index_apply] intro i @@ -53,7 +52,6 @@ theorem setFinite_index_image_of_isBounded [Finite ι] (n : ℕ) {T : Set (ι rw [Real.dist_eq, Pi.zero_apply, sub_zero] at hd exact hd.trans (by simpa [Real.dist_eq] using hR hx) rcases abs_le.mp hxi with ⟨hlo, hhi⟩ - have hn0 : (0 : ℝ) ≤ (n : ℝ) := Nat.cast_nonneg n exact ⟨sub_le_sub_right (Int.ceil_le_ceil (by nlinarith)) 1, sub_le_sub_right (Int.ceil_le_ceil (by nlinarith)) 1⟩