Doubling.lean`

21 declarations, 0 contain sorry, 0 declared as axioms

Intrinsic doubling of the same fixed Hilbert subset.

def OAI.DoublingHilbert.nearbyStripIndices line 15
Source documentation
A uniform finite set of strips meeting an interval shorter than 128 strip widths.
```
def nearbyStripIndices (c width : ℝ) : Finset ℤ :=
…
```
theorem OAI.DoublingHilbert.nearbyStripIndices_card line 18
theorem OAI.DoublingHilbert.mem_nearbyStripIndices line 22
def OAI.DoublingHilbert.coordinateCell line 39
Source documentation
Sixteen cells of width t/8 cover the coordinate projection of a radius-t ball.
```
def coordinateCell (c t x : ℝ) : ℤ := ⌊8 * (x - (c - t)) / t⌋
```
theorem OAI.DoublingHilbert.coordinateCell_mem line 41
theorem OAI.DoublingHilbert.abs_sub_lt_of_coordinateCell_eq line 54

theorem OAI.DoublingHilbert.cover_of_finite_code line 76

Source documentation

A finite coding with fibers of small diameter supplies intrinsic covering centers.

theorem cover_of_finite_code {X I : Type*} [PseudoMetricSpace X] [Fintype I]
    (s : Set X) (code : s → I) {r : ℝ}
    (hcode : ∀ x y : s, code x = code y → dist (x : X) (y : X) < r) :
    ∃ centers : Finset X, centers.card ≤ Fintype.card I ∧
      (↑centers : Set X) ⊆ s ∧ ∀ x ∈ s, ∃ y ∈ centers, dist x y < r := by
…

theorem OAI.DoublingHilbert.isCompact_exists_packing_bound line 101

Source documentation

Compact metric sets admit a finite upper bound for any fixed positive separation.

theorem isCompact_exists_packing_bound {X : Type*} [PseudoMetricSpace X]
    {s : Set X} (hs : IsCompact s) {r : ℝ} (hr : 0 < r) :
    ∃ bound : ℕ, ∀ {n : ℕ} (z : Fin n → X), (∀ i, z i ∈ s) →
      (∀ i j, i ≠ j → r ≤ dist (z i) (z j)) → n ≤ bound := by
…

def OAI.DoublingHilbert.nearbyLabels line 135
Source documentation
The finite list of intermediate-level choices near a base point.
```
def nearbyLabels (c : Base) (j : ℕ) : Finset ℕ :=
…
```
Mentions: OAI.DoublingHilbert.Base
theorem OAI.DoublingHilbert.nearbyLabels_card line 141
theorem OAI.DoublingHilbert.admissible_mem_nearbyLabels line 151
theorem OAI.DoublingHilbert.point_dist_lt_half line 172
Source documentation
Same coarse and intermediate coordinates, and one base cell, force small diameter.
```
theorem point_dist_lt_half {p q : Base} {w w' : Tuple} {t : ℝ} (ht : 0 < t)
    (hx : |p.1 - q.1| < t / 8) (hy : |p.2 - q.2| < t / 8)
    (hlarge : ∀ j, t / 64 < scale j → w j = w' j) :
    dist (point p w) (point q w') < t / 2 := by
…
```
Mentions: OAI.DoublingHilbert.Base, OAI.DoublingHilbert.Tuple, OAI.DoublingHilbert.scale, OAI.DoublingHilbert.point
def OAI.DoublingHilbert.sourceBase line 197
def OAI.DoublingHilbert.sourceTuple line 198
theorem OAI.DoublingHilbert.source_admissible line 201
theorem OAI.DoublingHilbert.source_eq_point line 204
theorem OAI.DoublingHilbert.sourceBase_fst_dist_le line 207
theorem OAI.DoublingHilbert.sourceBase_snd_dist_le line 213
theorem OAI.DoublingHilbert.sourceTuple_coarse_eq line 219

theorem OAI.DoublingHilbert.source_cover_of_label line 225

Source documentation

Intrinsic centers for any valid intermediate coordinate coding.

theorem source_cover_of_label (x : constructedSet) {t : ℝ} (ht : 0 < t)
    (labels : Finset ℕ) (hcard : labels.card ≤ 300)
    (label : Metric.ball x t → {i // i ∈ labels})
    (hlabel : ∀ y z : Metric.ball x t, label y = label z →
      ∀ j, t / 64 < scale j → sourceTuple y.val j = sourceTuple z.val j) :
    ∃ centers : Finset constructedSet, centers.card ≤ 76800 ∧
      ∀ y : constructedSet, dist y x < t → ∃ c ∈ centers, dist y c < t / 2 := by
…

Mentions: OAI.DoublingHilbert.constructedSet, OAI.DoublingHilbert.scale, OAI.DoublingHilbert.sourceTuple

theorem OAI.DoublingHilbert.constructedSet_cover line 258

Source documentation

The fixed Hilbert subset has an intrinsic open-ball doubling bound of 76800.

theorem constructedSet_cover (x : constructedSet) {t : ℝ} (ht : 0 < t) :
    ∃ centers : Finset constructedSet, centers.card ≤ 76800 ∧
      ∀ y : constructedSet, dist y x < t → ∃ c ∈ centers, dist y c < t / 2 := by
…

Mentions: OAI.DoublingHilbert.constructedSet