OAI/GroupTheory/PolycyclicRecognition/Analysis/DiagonalCellProfilePairs.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The diagonal's two profiles retain subexponential relative Haar mass

  1. theorem OAI.PolycyclicRecognition.compact_eventually_subset_coordinate_balls line 15

    Source documentation

    The concrete coordinate balls absorb every later compact path set.

    theorem compact_eventually_subset_coordinate_balls
    {V : Type*} [PseudoMetricSpace V] (x : V) (C : Set V) (hC : IsCompact C) :
    ∀ᶠ n : ℕ in atTop, C ⊆ Metric.closedBall x ((n : ℝ) + 1) := by
…
  2. theorem OAI.PolycyclicRecognition.exists_diagonal_good_cell_profile_pairs line 23