IntegerCellBounds.lean

1 import Mathlib.Analysis.Normed.Group.Basic
2 import Mathlib.Topology.MetricSpace.Pseudo.Pi
3 import Mathlib.Topology.MetricSpace.Bounded
4 import Mathlib.Data.Int.Interval
5 import Mathlib.Data.Set.Card
6 import Mathlib.Data.Fintype.BigOperators
7 import Mathlib.Tactic
8 
9 open scoped BigOperators
10 open Set
11 
12 namespace PaperX.IntegerCellBounds
13 
14 variable {ι : Type*} [Fintype ι]
15 
16 /-- Closed unit cells in the standard integer lattice. -/
17 def closedCell (z : ι → ℤ) : Set (ι → ℝ) :=
18   Set.Icc (fun i => (z i : ℝ)) (fun i => (z i : ℝ) + 1)
19 
20 /-- Integer indices of closed unit cells that touch a set. -/
21 def touching (S : Set (ι → ℝ)) : Set (ι → ℤ) :=
22   {z | (closedCell z ∩ S).Nonempty}
23 
24 /-- A finite containing box, centered at coordinatewise integer floors. -/
25 noncomputable def indexBox (c : ι → ℝ) (r : ℕ) : Finset (ι → ℤ) := by
26   classical
27   exact Fintype.piFinset fun i =>
28     Finset.Icc (⌊c i⌋ - (r : ℤ) - 1) (⌊c i⌋ + (r : ℤ) + 1)
29 
30 theorem card_indexBox (c : ι → ℝ) (r : ℕ) :
31     (indexBox c r).card = (2 * r + 3) ^ Fintype.card ι := by
32   classical
33   simp only [indexBox, Fintype.card_piFinset, Int.card_Icc]
34   have h : ∀ i, ((⌊c i⌋ + (r : ℤ) + 1 + 1 - (⌊c i⌋ - (r : ℤ) - 1)).toNat)
35       = 2 * r + 3 := by
36     intro i
37     omega
38   simp only [h, Finset.prod_const, Finset.card_univ]
39 
40 theorem mem_indexBox_of_coord_bound (c : ι → ℝ) (r : ℕ) (z : ι → ℤ)
41     (h : ∀ i, |(z i : ℝ) - c i| ≤ r) : z ∈ indexBox c r := by
42   classical
43   apply Fintype.mem_piFinset.mpr
44   intro i
45   have hc := Int.floor_le (c i)
46   have hd := Int.lt_floor_add_one (c i)
47   obtain ⟨hl, hu⟩ := abs_le.mp (h i)
48   apply Finset.mem_Icc.mpr
49   constructor
50   · exact_mod_cast (show (⌊c i⌋ : ℝ) - (r : ℝ) - 1 ≤ (z i : ℝ) by linarith)
51   · exact_mod_cast (show (z i : ℝ) ≤ (⌊c i⌋ : ℝ) + (r : ℝ) + 1 by linarith)
52 
53 theorem touching_closedBall_subset_indexBox (c : ι → ℝ) (R : ℝ) :
54     touching (Metric.closedBall c R) ⊆ (indexBox c (Nat.ceil (R + 1)) : Set (ι → ℤ)) := by
55   intro z hz
56   obtain ⟨x, hx, hxc⟩ := hz
57   apply mem_indexBox_of_coord_bound
58   intro i
59   have hd : dist x c ≤ R := hxc
60   have hi : dist (x i) (c i) ≤ dist x c := dist_le_pi_dist x c i
61   have hc : R + 1 ≤ (Nat.ceil (R + 1) : ℝ) := Nat.le_ceil _
62   have hxlo := hx.1 i
63   have hxhi := hx.2 i
64   rw [Real.dist_eq] at hi
65   obtain ⟨hlo, hhi⟩ := abs_le.mp (hi.trans hd)
66   apply abs_le.mpr
67   constructor <;> linarith
68 
69 theorem finite_touching_closedBall (c : ι → ℝ) (R : ℝ) :
70     (touching (Metric.closedBall c R)).Finite :=
71   (indexBox c (Nat.ceil (R + 1))).finite_toSet.subset
72     (touching_closedBall_subset_indexBox c R)
73 
74 theorem ncard_touching_closedBall_le (c : ι → ℝ) (R : ℝ) :
75     (touching (Metric.closedBall c R)).ncard ≤
76       (2 * Nat.ceil (R + 1) + 3) ^ Fintype.card ι := by
77   calc
78     _ ≤ ((indexBox c (Nat.ceil (R + 1))) : Set (ι → ℤ)).ncard :=
79       Set.ncard_le_ncard (touching_closedBall_subset_indexBox c R)
80         (Finset.finite_toSet _)
81     _ = _ := by rw [Set.ncard_coe_finset, card_indexBox]
82 
83 omit [Fintype ι] in
84 theorem touching_mono {S T : Set (ι → ℝ)} (h : S ⊆ T) : touching S ⊆ touching T := by
85   rintro z ⟨x, hx, hxs⟩
86   exact ⟨x, hx, h hxs⟩
87 
88 /-- A finite cover by uniformly bounded balls gives a uniform cell-count bound. -/
89 theorem touching_of_finite_ball_cover {β : Type*} [Fintype β]
90     (S : Set (ι → ℝ)) (c : β → (ι → ℝ)) (R : ℝ)
91     (hcover : S ⊆ ⋃ b, Metric.closedBall (c b) R) :
92     (touching S).Finite ∧ (touching S).ncard ≤
93       Fintype.card β * (2 * Nat.ceil (R + 1) + 3) ^ Fintype.card ι := by
94   classical
95   let B : Finset (ι → ℤ) := Finset.univ.biUnion fun b => indexBox (c b) (Nat.ceil (R + 1))
96   have hsub : touching S ⊆ (B : Set (ι → ℤ)) := by
97     rintro z ⟨x, hx, hxs⟩
98     obtain ⟨b, hb⟩ := Set.mem_iUnion.mp (hcover hxs)
99     apply Finset.mem_biUnion.mpr
100     exact ⟨b, Finset.mem_univ _, touching_closedBall_subset_indexBox (c b) R ⟨x, hx, hb⟩⟩
101   refine ⟨B.finite_toSet.subset hsub, ?_⟩
102   calc
103     (touching S).ncard ≤ (B : Set (ι → ℤ)).ncard := Set.ncard_le_ncard hsub B.finite_toSet
104     _ = B.card := Set.ncard_coe_finset _
105     _ ≤ ∑ b : β, (indexBox (c b) (Nat.ceil (R + 1))).card := Finset.card_biUnion_le
106     _ = _ := by simp [card_indexBox]
107 
108 /-- Bounded sets meet only finitely many closed integer unit cells. -/
109 theorem finite_touching_of_isBounded {S : Set (ι → ℝ)} (hS : Bornology.IsBounded S) :
110     (touching S).Finite := by
111   obtain ⟨R, hR⟩ := hS.subset_closedBall (0 : ι → ℝ)
112   exact (finite_touching_closedBall _ R).subset (touching_mono hR)
113 
114 /-- The upper-right unit-cell tags lying in a bounded set form a finite set. -/
115 theorem finite_upper_tags_of_isBounded {S : Set (ι → ℝ)} (hS : Bornology.IsBounded S) :
116     {z : ι → ℤ | (fun i => (z i : ℝ) + 1) ∈ S}.Finite := by
117   apply (finite_touching_of_isBounded hS).subset
118   intro z hz
119   refine ⟨fun i => (z i : ℝ) + 1, ⟨?_, le_rfl⟩, hz⟩
120   intro i
121   exact le_add_of_nonneg_right zero_le_one
122 
123 end PaperX.IntegerCellBounds

Back to source controls