LowerPacking.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Lower packing bounds from Haar volume

A totally bounded endpoint set has a finite separated net. Its volume is at most the cardinality of that net times the mass of a fixed-radius ball. This is the lower packing estimate used after stationary mesh selection.

theorem OAI.PolycyclicRecognition.exists_separated_net_of_totallyBounded line 22

Source documentation

A totally bounded set admits a finite separated net with its centers inside the set. The set itself need not be closed or measurable.

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

theorem OAI.PolycyclicRecognition.measure_closedBall_eq_identity line 57

Source documentation

Haar mass of a closed ball is independent of its center.

theorem measure_closedBall_eq_identity (μ : Measure G) [μ.IsMulLeftInvariant]
    (x : G) (r : ℝ) : μ (closedBall x r) = μ (closedBall (1 : G) r) := by
…

theorem OAI.PolycyclicRecognition.exists_separated_net_volume_bound line 66

Source documentation

The volume of an arbitrary endpoint set bounds below the cardinality of one finite separated subset. No measurability of the endpoint set is needed.

theorem exists_separated_net_volume_bound (μ : Measure G) [μ.IsMulLeftInvariant]
    {S : Set G} (hS : TotallyBounded S) {r : ℝ} (hr : 0 < r) :
    ∃ t : Finset G, (↑t : Set G) ⊆ S ∧
      (∀ x ∈ t, ∀ y ∈ t, x ≠ y → r < dist x y) ∧
      μ S ≤ (t.card : ℝ≥0∞) * μ (closedBall (1 : G) r) := by
…