IntegerCellFiniteCharts.lean

1 import PaperX.IntegerCellChartCounting
2 
3 open Set
4 open scoped NNReal
5 
6 namespace PaperX.IntegerCellBounds
7 
8 variable {ι κ β : Type*} [Fintype ι] [Fintype κ] [Fintype β]
9 
10 /-- Uniform cell bound for any set covered by finitely many dilated Lipschitz charts. -/
11 theorem touching_finite_charts_bound (S : Set (ι → ℝ))
12     (f : β → (κ → ℝ) → (ι → ℝ)) (L : ℝ≥0)
13     (hf : ∀ b, LipschitzOnWith L (f b) (Set.Icc (0 : κ → ℝ) 1))
14     (a : ι → ℝ) (t : ℝ) (ht : 1 ≤ t)
15     (hS : S ⊆ ⋃ b, (fun x => a + t • f b x) '' Set.Icc (0 : κ → ℝ) 1) :
16     (touching S).Finite ∧ (touching S).ncard ≤
17       Fintype.card β * (Nat.ceil t + 1) ^ Fintype.card κ *
18         (2 * Nat.ceil ((L : ℝ) + 1) + 3) ^ Fintype.card ι := by
19   classical
20   have hcover : S ⊆ ⋃ bk : β × (κ → Fin (Nat.ceil t + 1)),
21       Metric.closedBall (a + t • f bk.1 (meshPoint (Nat.ceil t) bk.2)) (L : ℝ) := by
22     intro x hx
23     obtain ⟨b, hb⟩ := Set.mem_iUnion.mp (hS hx)
24     obtain ⟨k, hk⟩ := Set.mem_iUnion.mp (chart_image_ball_cover (f b) L (hf b) a t ht hb)
25     exact Set.mem_iUnion.mpr ⟨(b, k), hk⟩
26   simpa [Fintype.card_prod, Fintype.card_fun] using touching_of_finite_ball_cover S
27     (fun bk : β × (κ → Fin (Nat.ceil t + 1)) =>
28       a + t • f bk.1 (meshPoint (Nat.ceil t) bk.2)) (L : ℝ) hcover
29 
30 omit [Fintype ι] [Fintype κ] [Fintype β] in
31 theorem ceil_add_one_le_three_mul (t : ℝ) (ht : 1 ≤ t) :
32     ((Nat.ceil t + 1 : ℕ) : ℝ) ≤ 3 * t := by
33   have h := Nat.ceil_lt_add_one (show 0 ≤ t by linarith)
34   push_cast
35   linarith
36 
37 /-- A real polynomial bound with degree equal to the chart-domain dimension. -/
38 theorem touching_finite_charts_polynomial_bound (S : Set (ι → ℝ))
39     (f : β → (κ → ℝ) → (ι → ℝ)) (L : ℝ≥0)
40     (hf : ∀ b, LipschitzOnWith L (f b) (Set.Icc (0 : κ → ℝ) 1))
41     (a : ι → ℝ) (t : ℝ) (ht : 1 ≤ t)
42     (hS : S ⊆ ⋃ b, (fun x => a + t • f b x) '' Set.Icc (0 : κ → ℝ) 1) :
43     (touching S).Finite ∧ ((touching S).ncard : ℝ) ≤
44       ((Fintype.card β : ℝ) * 3 ^ Fintype.card κ *
45         (2 * Nat.ceil ((L : ℝ) + 1) + 3) ^ Fintype.card ι) * t ^ Fintype.card κ := by
46   obtain ⟨hfin, hn⟩ := touching_finite_charts_bound S f L hf a t ht hS
47   refine ⟨hfin, ?_⟩
48   have hpow : (((Nat.ceil t + 1 : ℕ) : ℝ)) ^ Fintype.card κ ≤
49       (3 * t) ^ Fintype.card κ := by
50     gcongr
51     exact ceil_add_one_le_three_mul t ht
52   have hn' : ((touching S).ncard : ℝ) ≤
53       (Fintype.card β : ℝ) * ((Nat.ceil t + 1 : ℕ) : ℝ) ^ Fintype.card κ *
54         (2 * Nat.ceil ((L : ℝ) + 1) + 3) ^ Fintype.card ι := by exact_mod_cast hn
55   calc
56     _ ≤ (Fintype.card β : ℝ) * ((Nat.ceil t + 1 : ℕ) : ℝ) ^ Fintype.card κ *
57         (2 * Nat.ceil ((L : ℝ) + 1) + 3) ^ Fintype.card ι := hn'
58     _ ≤ (Fintype.card β : ℝ) * (3 * t) ^ Fintype.card κ *
59         (2 * Nat.ceil ((L : ℝ) + 1) + 3) ^ Fintype.card ι := by gcongr
60     _ = _ := by rw [mul_pow]; ring
61 
62 end PaperX.IntegerCellBounds

Back to source controls