OAI/GroupTheory/PolycyclicRecognition/Geometry/CartanCoordinatePacking.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Separated counts for arbitrary good coordinate subsets

The coordinate Haar measure and the closed root-factor embedding give a single finite packing constant. Every subset of a bounded rescaled chart has its determinant volume bounded by the cardinality of an actual ambient separated net. The subset need not itself be measurable.

  1. theorem OAI.PolycyclicRecognition.CartanWordModel.exists_coordinate_subset_packing line 36

    Source documentation

    A uniform ambient separated count for any bounded coordinate subset in an actual rescaled word basis.

    theorem exists_coordinate_subset_packing
    (haarN : NilpotentExponentialHaarInput F.N.modelSpace F.N.carrier)
    (b₀ : Basis (Fin (finrank ℝ (cartanRootIdeal H))) ℝ (cartanRootIdeal H))
    {ρ : ℝ} (hρ : 0 < ρ) :
    ∃ C : ℝ≥0∞, C < ⊤ ∧ ∀ (cost : M.wordList → ℝ) (β : M.Bases) (r R : ℝ)
      (S : Set (Fin (finrank ℝ (cartanRootIdeal H)) → ℝ)), S ⊆ closedBall 0 R →
      let b := exponentialRescaleBasis (WordBasisSelections.basis M.letter M.wordList β)
…

    Mentions: OAI.PolycyclicRecognition.NilpotentExponentialHaarInput, OAI.PolycyclicRecognition.cartanRootIdeal, OAI.PolycyclicRecognition.exponentialRescaleBasis, OAI.PolycyclicRecognition.WordBasisSelections.basis