PopularGroups.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Actual finite groups from intersecting popularity projections. Their representatives have the packing bound, and every group lies in a long interval of the size of its representative.

theorem OAI.LipschitzHilbert.Rectangle.projected_popularity_directions line 18
theorem OAI.LipschitzHilbert.Rectangle.projected_group_localization line 34

theorem OAI.LipschitzHilbert.exists_projected_popularity_groups line 61

Source documentation

The representatives are selected by maximal length. No geometric packing hypothesis is assumed: their projected popularity sets are disjoint by construction.

theorem exists_projected_popularity_groups {ι : Type*} [DecidableEq ι]
    (R : ι → Rectangle) (s : Finset ι) (S : Rectangle)
    {v : Plane → Plane} {K δ : ℝ≥0} (hv : Continuous v) (hδ : 0 < δ)
    (hR : ∀ j ∈ s, (R j).Admissible v K δ)
    (hL : ∀ j ∈ s, (R j).long ≤ S.long)
    (hinter : ∀ j ∈ s, ((R j).carrier ∩ S.carrier).Nonempty)
    (hangle : ∀ j ∈ s, dist ((R j).axes 0) (S.axes 0) ≤ 1/4) :
    ∃ centers : Finset ι, centers ⊆ s ∧
      (δ : ℝ≥0∞)*(∑ i ∈ centers, ENNReal.ofReal (R i).long) ≤ 12*ENNReal.ofReal S.long ∧
      ∀ j ∈ s, ∃ i ∈ centers, (R j).long ≤ (R i).long ∧
        (S.coordinateProjection ((R i).popularSet v) ∩
          S.coordinateProjection ((R j).popularSet v)).Nonempty := by
…

Mentions: OAI.LipschitzHilbert.Rectangle, OAI.LipschitzHilbert.Plane