SubgroupPacking.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Packing on the identity slice of a closed subgroup

For segment comparison the source pivot is the identity. Haar invariance under left translations alone bounds every pulled-back ambient ball.

theorem OAI.PolycyclicRecognition.subgroup_ball_measure line 25
Source documentation
Left invariance controls all ambient balls on the identity subgroup slice.
```
theorem subgroup_ball_measure (v : N) (r : ℝ) :
    μ (ι ⁻¹' closedBall (ι v) r) = μ (ι ⁻¹' closedBall (1 : G) r) := by
…
```

theorem OAI.PolycyclicRecognition.exists_subgroup_separated_net line 39

Source documentation

Every relatively compact subgroup endpoint set has a separated net with a cardinality lower bound in terms of its Haar mass.

theorem exists_subgroup_separated_net (hι : Continuous ι) {K S : Set N}
    (hK : IsCompact K) (hS : S ⊆ K) {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
…