MeasurePacking.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Counting separated endpoints using Haar volume

Disjoint fixed-radius balls around separated endpoints have the same positive Haar mass. A polynomial-volume region containing their thickening therefore gives a polynomial cardinal bound. This is the counting step of the path packing lemma, separated from its Lie-coordinate estimate.

theorem OAI.PolycyclicRecognition.measure_ball_eq_identity line 28

theorem OAI.PolycyclicRecognition.separated_card_mul_ball_le line 35

Source documentation

The Haar volume of a thickening bounds the number of separated centers.

theorem separated_card_mul_ball_le (μ : Measure G) [IsMulLeftInvariant μ]
    (s : Finset G) (r : ℝ) (region : Set G)
    (hsep : ∀ x ∈ s, ∀ y ∈ s, x ≠ y → r + r ≤ dist x y)
    (hthick : ∀ x ∈ s, ball x r ⊆ region) :
    (s.card : ℝ≥0∞) * μ (ball (1 : G) r) ≤ μ region := by
…

theorem OAI.PolycyclicRecognition.separated_card_le_polynomial line 53

Source documentation

A polynomial Haar-volume upper bound becomes a polynomial bound on every finite separated subset. The ball mass is canceled with its nonzero/finite hypotheses explicit.

theorem separated_card_le_polynomial (μ : Measure G) [IsMulLeftInvariant μ]
    (s : Finset G) (r : ℝ) (region : Set G) (C b t : ℕ)
    (hq0 : μ (ball (1 : G) r) ≠ 0) (hqtop : μ (ball (1 : G) r) ≠ ⊤)
    (hsep : ∀ x ∈ s, ∀ y ∈ s, x ≠ y → r + r ≤ dist x y)
    (hthick : ∀ x ∈ s, ball x r ⊆ region)
    (hvol : μ region ≤ ((C * (1 + t) ^ b : ℕ) : ℝ≥0∞) * μ (ball (1 : G) r)) :
    s.card ≤ C * (1 + t) ^ b := by
…

theorem OAI.PolycyclicRecognition.finite_cover_of_separated_bound line 67

Source documentation

A cardinal bound on separated subsets gives a finite cover of the original finite set. Endpoint sets need not be measurable.

theorem finite_cover_of_separated_bound {X : Type*} [PseudoMetricSpace X]
    (s : Finset X) {r : ℝ} (hr : 0 ≤ r) (N : ℕ)
    (hbound : ∀ t : Finset X, t ⊆ s →
      (∀ x ∈ t, ∀ y ∈ t, x ≠ y → r < dist x y) → t.card ≤ N) :
    ∃ t : Finset X, t ⊆ s ∧ t.card ≤ N ∧
      ∀ x ∈ s, ∃ y ∈ t, dist x y ≤ r := by
…

theorem OAI.PolycyclicRecognition.finite_separated_cover_set_of_bound line 110

Source documentation

The same maximal-packing argument applies to arbitrary endpoint sets. A bound on their finite separated subsets already supplies a finite net; no measurability or compactness of the endpoint set is needed.

theorem finite_separated_cover_set_of_bound {X : Type*} [PseudoMetricSpace X]
    (S : Set X) {r : ℝ} (hr : 0 ≤ r) (N : ℕ)
    (hbound : ∀ t : Finset X, (↑t : Set X) ⊆ S →
      (∀ x ∈ t, ∀ y ∈ t, x ≠ y → r < dist x y) → t.card ≤ N) :
    ∃ t : Finset X, (↑t : Set X) ⊆ S ∧
      (∀ x ∈ t, ∀ y ∈ t, x ≠ y → r < dist x y) ∧ t.card ≤ N ∧
      ∀ x ∈ S, ∃ y ∈ t, dist x y ≤ r := by
…

theorem OAI.PolycyclicRecognition.finite_cover_set_of_separated_bound line 156

Source documentation

Retain the covering conclusion when separation of the centers is not needed.

theorem finite_cover_set_of_separated_bound {X : Type*} [PseudoMetricSpace X]
    (S : Set X) {r : ℝ} (hr : 0 ≤ r) (N : ℕ)
    (hbound : ∀ t : Finset X, (↑t : Set X) ⊆ S →
      (∀ x ∈ t, ∀ y ∈ t, x ≠ y → r < dist x y) → t.card ≤ N) :
    ∃ t : Finset X, (↑t : Set X) ⊆ S ∧ t.card ≤ N ∧
      ∀ x ∈ S, ∃ y ∈ t, dist x y ≤ r := by
…