IntegerCellChartCounting.lean

1 import PaperX.IntegerCellBounds
2 import Mathlib.Analysis.Normed.Module.Basic
3 import Mathlib.Topology.MetricSpace.Lipschitz
4 
5 open Set
6 open scoped NNReal
7 
8 namespace PaperX.IntegerCellBounds
9 
10 variable {ι κ : Type*} [Fintype ι] [Fintype κ]
11 
12 /-- Vertices of the regular mesh of denominator `m`. -/
13 noncomputable def meshPoint (m : ℕ) (k : κ → Fin (m + 1)) : κ → ℝ :=
14   fun i => (k i : ℕ) / (m : ℝ)
15 
16 omit [Fintype ι] [Fintype κ] in
17 theorem meshPoint_mem_unitBox (m : ℕ) (hm : 0 < m) (k : κ → Fin (m + 1)) :
18     meshPoint m k ∈ Set.Icc (0 : κ → ℝ) 1 := by
19   have hm' : (0 : ℝ) < m := by exact_mod_cast hm
20   constructor
21   · intro i
22     exact div_nonneg (Nat.cast_nonneg _) hm'.le
23   · intro i
24     apply (div_le_one hm').mpr
25     exact_mod_cast (Nat.le_of_lt_succ (k i).isLt)
26 
27 omit [Fintype ι] in
28 theorem exists_meshPoint_dist_le (m : ℕ) (hm : 0 < m) (x : κ → ℝ)
29     (hx : x ∈ Set.Icc (0 : κ → ℝ) 1) :
30     ∃ k : κ → Fin (m + 1), dist x (meshPoint m k) ≤ 1 / (m : ℝ) := by
31   have hm' : (0 : ℝ) < m := by exact_mod_cast hm
32   let k : κ → Fin (m + 1) := fun i =>
33     ⟨Nat.floor ((m : ℝ) * x i), Nat.lt_succ_of_le (Nat.floor_le_of_le (by
34       have hxi := hx.2 i
35       change x i ≤ 1 at hxi
36       nlinarith))⟩
37   refine ⟨k, (dist_pi_le_iff (by positivity)).mpr ?_⟩
38   intro i
39   have hx0 : 0 ≤ x i := hx.1 i
40   have hfloor := Nat.floor_le (mul_nonneg hm'.le hx0)
41   have hlt := Nat.lt_floor_add_one ((m : ℝ) * x i)
42   change |x i - (Nat.floor ((m : ℝ) * x i) : ℝ) / (m : ℝ)| ≤ 1 / (m : ℝ)
43   rw [abs_le]
44   constructor
45   · have h : (Nat.floor ((m : ℝ) * x i) : ℝ) / (m : ℝ) ≤ x i :=
46       (div_le_iff₀ hm').mpr (by nlinarith [hfloor])
47     have hinv : 0 ≤ 1 / (m : ℝ) := by positivity
48     linarith
49   · apply (le_div_iff₀ hm').mpr
50     have hid : ((Nat.floor ((m : ℝ) * x i) : ℝ) / (m : ℝ)) * m =
51         (Nat.floor ((m : ℝ) * x i) : ℝ) := div_mul_cancel₀ _ hm'.ne'
52     nlinarith
53 
54 /-- A dilated translated Lipschitz chart is covered by a regular finite family of balls. -/
55 theorem chart_image_ball_cover (f : (κ → ℝ) → (ι → ℝ)) (L : ℝ≥0)
56     (hf : LipschitzOnWith L f (Set.Icc (0 : κ → ℝ) 1))
57     (a : ι → ℝ) (t : ℝ) (ht : 1 ≤ t) :
58     (fun x => a + t • f x) '' Set.Icc (0 : κ → ℝ) 1 ⊆
59       ⋃ k : κ → Fin (Nat.ceil t + 1),
60         Metric.closedBall (a + t • f (meshPoint (Nat.ceil t) k)) (L : ℝ) := by
61   have ht0 : 0 ≤ t := by linarith
62   have hm : 0 < Nat.ceil t := Nat.ceil_pos.mpr (by linarith)
63   have hm' : (0 : ℝ) < Nat.ceil t := by exact_mod_cast hm
64   have htm : t ≤ (Nat.ceil t : ℝ) := Nat.le_ceil _
65   rintro y ⟨x, hx, rfl⟩
66   obtain ⟨k, hk⟩ := exists_meshPoint_dist_le (Nat.ceil t) hm x hx
67   apply Set.mem_iUnion.mpr
68   refine ⟨k, ?_⟩
69   change dist (a + t • f x) (a + t • f (meshPoint (Nat.ceil t) k)) ≤ (L : ℝ)
70   have hdist := hf.dist_le_mul x hx (meshPoint (Nat.ceil t) k)
71     (meshPoint_mem_unitBox _ hm k)
72   have hsmall : dist (f x) (f (meshPoint (Nat.ceil t) k)) ≤
73       (L : ℝ) / (Nat.ceil t : ℝ) := by
74     calc
75       _ ≤ (L : ℝ) * dist x (meshPoint (Nat.ceil t) k) := hdist
76       _ ≤ (L : ℝ) * (1 / (Nat.ceil t : ℝ)) := mul_le_mul_of_nonneg_left hk L.coe_nonneg
77       _ = _ := by ring
78   rw [dist_add_left, dist_eq_norm, ← smul_sub, norm_smul, Real.norm_eq_abs, abs_of_nonneg ht0]
79   have hdist' : ‖f x - f (meshPoint (Nat.ceil t) k)‖ ≤
80       (L : ℝ) / (Nat.ceil t : ℝ) := by simpa only [dist_eq_norm] using hsmall
81   calc
82     _ ≤ t * ((L : ℝ) / (Nat.ceil t : ℝ)) := mul_le_mul_of_nonneg_left hdist' ht0
83     _ ≤ (Nat.ceil t : ℝ) * ((L : ℝ) / (Nat.ceil t : ℝ)) :=
84       mul_le_mul_of_nonneg_right htm (div_nonneg L.coe_nonneg hm'.le)
85     _ = (L : ℝ) := mul_div_cancel₀ _ hm'.ne'
86 
87 /-- Explicit, translation-uniform cell bound for one Lipschitz chart. -/
88 theorem touching_chart_image_bound (f : (κ → ℝ) → (ι → ℝ)) (L : ℝ≥0)
89     (hf : LipschitzOnWith L f (Set.Icc (0 : κ → ℝ) 1))
90     (a : ι → ℝ) (t : ℝ) (ht : 1 ≤ t) :
91     let S := (fun x => a + t • f x) '' Set.Icc (0 : κ → ℝ) 1
92     (touching S).Finite ∧ (touching S).ncard ≤
93       (Nat.ceil t + 1) ^ Fintype.card κ *
94         (2 * Nat.ceil ((L : ℝ) + 1) + 3) ^ Fintype.card ι := by
95   classical
96   simpa [Fintype.card_fun] using touching_of_finite_ball_cover
97     ((fun x => a + t • f x) '' Set.Icc (0 : κ → ℝ) 1)
98     (fun k : κ → Fin (Nat.ceil t + 1) => a + t • f (meshPoint (Nat.ceil t) k))
99     (L : ℝ) (chart_image_ball_cover f L hf a t ht)
100 
101 end PaperX.IntegerCellBounds

Back to source controls