CoveringNumber.lean`

18 declarations, 0 contain sorry, 0 declared as axioms

Finite covering numbers and the cube packing bound

Centers are arbitrary ambient vectors throughout. Attainment and lower bounds explicitly assume a finite cover exists, because the natural-number infimum of the empty set is zero. Compactness and a neighborhood of zero supply that hypothesis in the geometric application.

theorem OAI.MetricEntropyDuality.exists_fin_cover_of_fintype_cover line 28
Source documentation
A finite family can be enumerated without changing its centers or count.
```
theorem exists_fin_cover_of_fintype_cover {J : Type uJ} [Fintype J]
    (c : J → RealSpace ι) (hc : ∀ x ∈ A, ∃ j, x - c j ∈ B) :
    ∃ d : Fin (Fintype.card J) → RealSpace ι, Covers A B d := by
…
```
Mentions: OAI.MetricEntropyDuality.RealSpace, OAI.MetricEntropyDuality.Covers
theorem OAI.MetricEntropyDuality.exists_finset_cover line 39
Source documentation
Enumerate a finite set of indices, retaining exactly its cardinality.
```
theorem exists_finset_cover {J : Type uJ} (s : Finset J)
    (c : J → RealSpace ι) (hc : ∀ x ∈ A, ∃ j ∈ s, x - c j ∈ B) :
    ∃ d : Fin s.card → RealSpace ι, Covers A B d := by
…
```
Mentions: OAI.MetricEntropyDuality.RealSpace, OAI.MetricEntropyDuality.Covers
theorem OAI.MetricEntropyDuality.coveringNumber_le_of_covers line 49
Source documentation
Every actual finite cover bounds the literal natural infimum.
```
theorem coveringNumber_le_of_covers {M : ℕ} {c : Fin M → RealSpace ι}
    (hc : Covers A B c) : coveringNumber A B ≤ M :=
…
```
Mentions: OAI.MetricEntropyDuality.RealSpace, OAI.MetricEntropyDuality.Covers, OAI.MetricEntropyDuality.coveringNumber
theorem OAI.MetricEntropyDuality.coveringNumber_attained line 53
theorem OAI.MetricEntropyDuality.le_coveringNumber line 58
Source documentation
A lower bound on every finite cover bounds the actual minimum.
```
theorem le_coveringNumber {k : ℕ} (hfin : Coverable A B)
    (h : ∀ (M : ℕ) (c : Fin M → RealSpace ι), Covers A B c → k ≤ M) :
    k ≤ coveringNumber A B := by
…
```
Mentions: OAI.MetricEntropyDuality.Coverable, OAI.MetricEntropyDuality.RealSpace, OAI.MetricEntropyDuality.Covers, OAI.MetricEntropyDuality.coveringNumber
theorem OAI.MetricEntropyDuality.coveringNumber_pos line 64
theorem OAI.MetricEntropyDuality.Covers.mono_left line 71
theorem OAI.MetricEntropyDuality.Covers.mono_right line 76
theorem OAI.MetricEntropyDuality.Coverable.mono_left line 82
theorem OAI.MetricEntropyDuality.Coverable.mono_right line 87
theorem OAI.MetricEntropyDuality.coveringNumber_mono_left line 92
theorem OAI.MetricEntropyDuality.coveringNumber_mono_right line 97
theorem OAI.MetricEntropyDuality.coverable_of_isCompact_of_mem_nhds_zero line 103
Source documentation
Translates of any neighborhood of zero finitely cover a compact set.
```
theorem coverable_of_isCompact_of_mem_nhds_zero (hA : IsCompact A)
    (hB : B ∈ 𝓝 (0 : RealSpace ι)) : Coverable A B := by
…
```
Mentions: OAI.MetricEntropyDuality.RealSpace, OAI.MetricEntropyDuality.Coverable
theorem OAI.MetricEntropyDuality.cube_mem_nhds_zero line 122
Source documentation
The coordinate cube is a neighborhood of zero in a finite product.
```
theorem cube_mem_nhds_zero [Finite ι] : cube ι ∈ 𝓝 (0 : RealSpace ι) := by
…
```
Mentions: OAI.MetricEntropyDuality.cube, OAI.MetricEntropyDuality.RealSpace
theorem OAI.MetricEntropyDuality.coverable_cube_of_isCompact line 133
theorem OAI.MetricEntropyDuality.cube_translate_diameter line 138
Source documentation
A cube translate has coordinate diameter at most two, for any center.
```
theorem cube_translate_diameter {x y z : RealSpace ι}
    (hx : x - z ∈ cube ι) (hy : y - z ∈ cube ι) (i : ι) :
    |x i - y i| ≤ 2 := by
…
```
Mentions: OAI.MetricEntropyDuality.RealSpace, OAI.MetricEntropyDuality.cube

theorem OAI.MetricEntropyDuality.card_le_of_covers_cube line 150

Source documentation

Distinct points separated by more than two cannot share a cube translate.

theorem card_le_of_covers_cube {X : Type uX} [Fintype X]
    (p : X → RealSpace ι) (hp : ∀ x, p x ∈ A)
    (hsep : ∀ x y, x ≠ y → ∃ i, 2 < |p x i - p y i|)
    {M : ℕ} {c : Fin M → RealSpace ι} (hc : Covers A (cube ι) c) :
    Fintype.card X ≤ M := by
…

Mentions: OAI.MetricEntropyDuality.RealSpace, OAI.MetricEntropyDuality.Covers, OAI.MetricEntropyDuality.cube

theorem OAI.MetricEntropyDuality.card_le_coveringNumber_cube line 166
Source documentation
Packing lower bound for the genuine least number of arbitrary translates.
```
theorem card_le_coveringNumber_cube {X : Type uX} [Fintype X]
    (p : X → RealSpace ι) (hp : ∀ x, p x ∈ A)
    (hsep : ∀ x y, x ≠ y → ∃ i, 2 < |p x i - p y i|)
    (hfin : Coverable A (cube ι)) :
    Fintype.card X ≤ coveringNumber A (cube ι) := by
…
```
Mentions: OAI.MetricEntropyDuality.RealSpace, OAI.MetricEntropyDuality.Coverable, OAI.MetricEntropyDuality.cube, OAI.MetricEntropyDuality.coveringNumber