feat(ForMathlib): index-image finiteness for bounded sets (1/4)

CebotarevDensity.lean

@@ -1,3 +1,4 @@
 import CebotarevDensity.Density
+import CebotarevDensity.ForMathlib.IndexImageCount
 import CebotarevDensity.ForMathlib.LogOneDivSubOne
 import CebotarevDensity.Main

CebotarevDensity/ForMathlib/IndexImageCount.lean

@@ -0,0 +1,62 @@
+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*}
+
+/-- 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
+  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 (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
+  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⟩
+  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