PatchCover.lean`

14 declarations, 0 contain sorry, 0 declared as axioms

Finite patch nets and volume bounds for their active multiplicity

The net is chosen by maximal cardinality inside a totally bounded domain. The active cardinality estimate is proved by disjoint half-radius balls; the distance of active centers from the testing point is kept explicit.

theorem OAI.RegularPointCoordinates.packingNumber_ne_top_of_totallyBounded line 28
Source documentation
Total boundedness makes every positive-radius packing number finite.
```
theorem packingNumber_ne_top_of_totallyBounded {A : Set X} (hA : TotallyBounded A)
    {r : ℝ≥0} (hr : r ≠ 0) : Metric.packingNumber r A ≠ ⊤ := by
…
```
theorem OAI.RegularPointCoordinates.finite_maximalSeparatedSet line 41
Source documentation
The standard maximal separated set is finite even in the fallback case.
```
theorem finite_maximalSeparatedSet (r : ℝ≥0) (A : Set X) :
    (Metric.maximalSeparatedSet r A).Finite := by
…
```
def OAI.RegularPointCoordinates.maximalPatchNet line 49
Source documentation
A concrete finite maximal-cardinality net.
```
def maximalPatchNet (r : ℝ≥0) (A : Set X) : Finset X :=
…
```
theorem OAI.RegularPointCoordinates.coe_maximalPatchNet line 52
theorem OAI.RegularPointCoordinates.maximalPatchNet_subset line 56
theorem OAI.RegularPointCoordinates.maximalPatchNet_separated line 61
theorem OAI.RegularPointCoordinates.maximalPatchNet_covers line 71
theorem OAI.RegularPointCoordinates.maximalPatchNet_card_maximal line 87
Source documentation
Maximality is by cardinality, and therefore also rules out adding any new separated point from the original domain.
```
theorem maximalPatchNet_card_maximal {r : ℝ≥0} {A : Set X}
    (hr : r ≠ 0) (hA : TotallyBounded A) (s : Finset X)
    (hsub : (s : Set X) ⊆ A) (hsep : Metric.IsSeparated r (s : Set X)) :
    s.card ≤ (maximalPatchNet r A).card := by
…
```
Mentions: OAI.RegularPointCoordinates.maximalPatchNet
theorem OAI.RegularPointCoordinates.maximalPatchNet_covers_bounded line 98
Source documentation
In a proper metric space every bounded domain admits the finite net, even when the domain is not closed.
```
theorem maximalPatchNet_covers_bounded [ProperSpace X] {r : ℝ≥0} {A : Set X}
    (hr : r ≠ 0) (hA : Bornology.IsBounded A) :
    ∀ x ∈ A, ∃ y ∈ maximalPatchNet r A, dist x y ≤ r :=
…
```
Mentions: OAI.RegularPointCoordinates.maximalPatchNet

theorem OAI.RegularPointCoordinates.separated_half_balls_disjoint line 104

Source documentation

Half-radius balls around separated centers are pairwise disjoint.

theorem separated_half_balls_disjoint (s : Finset X) {r : ℝ}
    (hsep : (s : Set X).Pairwise (fun x y => r ≤ dist x y)) :
    Set.PairwiseDisjoint (s : Set X) (fun y => Metric.ball y (r / 2)) := by
…

theorem OAI.RegularPointCoordinates.separated_card_mul_volume_le line 118

Source documentation

The disjoint-ball packing estimate, with no volume comparison hidden in the statement. Finite measure is only required for the containing ball.

theorem separated_card_mul_volume_le (μ : Measure X) (s : Finset X) (x : X)
    {r R v : ℝ}
    (hsep : (s : Set X).Pairwise (fun y z => r ≤ dist y z))
    (hnear : ∀ y ∈ s, dist y x ≤ R)
    (hlower : ∀ y ∈ s, v ≤ μ.real (Metric.ball y (r / 2)))
    (hfinite : μ (Metric.ball x (R + r / 2)) ≠ ∞) :
    (s.card : ℝ) * v ≤ μ.real (Metric.ball x (R + r / 2)) := by
…

theorem OAI.RegularPointCoordinates.separated_card_le_of_euclidean_volume line 142

Source documentation

Two-sided Euclidean volume bounds yield a radius-independent real cardinality bound for centers within C₀ * r of the testing point.

theorem separated_card_le_of_euclidean_volume (μ : Measure X) (s : Finset X) (x : X)
    (n : ℕ) {r C₀ a b : ℝ} (hr : 0 < r) (ha : 0 < a)
    (hsep : (s : Set X).Pairwise (fun y z => r ≤ dist y z))
    (hnear : ∀ y ∈ s, dist y x ≤ C₀ * r)
    (hlower : ∀ y ∈ s, a * (r / 2) ^ n ≤ μ.real (Metric.ball y (r / 2)))
    (hupper : μ.real (Metric.ball x (C₀ * r + r / 2)) ≤ b * (C₀ * r + r / 2) ^ n)
    (hfinite : μ (Metric.ball x (C₀ * r + r / 2)) ≠ ∞) :
    (s.card : ℝ) ≤ b / a * (2 * C₀ + 1) ^ n := by
…

theorem OAI.RegularPointCoordinates.separated_card_le_ceil_of_euclidean_volume line 163

Source documentation

An integer uniform multiplicity constant extracted from the volume ratio. No cardinal bound is supplied as a premise.

theorem separated_card_le_ceil_of_euclidean_volume (μ : Measure X) (s : Finset X) (x : X)
    (n : ℕ) {r C₀ a b : ℝ} (hr : 0 < r) (ha : 0 < a)
    (hsep : (s : Set X).Pairwise (fun y z => r ≤ dist y z))
    (hnear : ∀ y ∈ s, dist y x ≤ C₀ * r)
    (hlower : ∀ y ∈ s, a * (r / 2) ^ n ≤ μ.real (Metric.ball y (r / 2)))
    (hupper : μ.real (Metric.ball x (C₀ * r + r / 2)) ≤ b * (C₀ * r + r / 2) ^ n)
    (hfinite : μ (Metric.ball x (C₀ * r + r / 2)) ≠ ∞) :
    s.card ≤ ⌈b / a * (2 * C₀ + 1) ^ n⌉₊ := by
…

theorem OAI.RegularPointCoordinates.active_maximalPatchNet_card_le line 176

Source documentation

The active subfamily of a net satisfies the same uniform cardinal bound whenever active centers lie within C₀ * r of the point.

theorem active_maximalPatchNet_card_le (μ : Measure X) (A : Set X)
    (r : ℝ≥0) (x : X) (active : X → Prop) [DecidablePred active] (n : ℕ)
    (hr : 0 < r) {C₀ a b : ℝ} (ha : 0 < a)
    (hnear : ∀ y ∈ maximalPatchNet r A, active y → dist y x ≤ C₀ * r)
    (hlower : ∀ y ∈ maximalPatchNet r A, active y →
      a * ((r : ℝ) / 2) ^ n ≤ μ.real (Metric.ball y (r / 2)))
    (hupper : μ.real (Metric.ball x (C₀ * r + r / 2)) ≤ b * (C₀ * r + r / 2) ^ n)
    (hfinite : μ (Metric.ball x (C₀ * r + r / 2)) ≠ ∞) :
    ((maximalPatchNet r A).filter active).card ≤ ⌈b / a * (2 * C₀ + 1) ^ n⌉₊ := by
…

Mentions: OAI.RegularPointCoordinates.maximalPatchNet