OAI/GroupTheory/PolycyclicRecognition/Geometry/CartanProfilePacking.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.CartanWordModel.templateSupport_le_of_good_profile_paths line 38

   Source documentation

   The good-sheet leg estimates and short root switches supply the full controlled-path premise of the Cartan volume comparison.

   theorem templateSupport_le_of_good_profile_paths
       (b₀ : Basis (Fin (finrank ℝ (cartanRootIdeal H))) ℝ (cartanRootIdeal H))
       (source E : Set W) (hE : IsCompact E) (hne : E.Nonempty) (w₀ : W)
       (β : M.Bases)
       (hβ : IsMaximizingColumnBasis (wordListCoordinates M.letter M.wordList b₀)
         (M.boxCost T hunimod eW source) β.val)
       (C : ℝ → Set (Fin (finrank ℝ (cartanRootIdeal H)) → ℝ))
       (hC : ∀ r, IsCompact (C r))
       (hvol : HasSubexponentialLowerBound (fun r => (volume (C r)).toReal))
       (x : ℝ → G) (d₀ : ℝ → F.D.carrier) (n₀ : ℝ → F.N.carrier)
       (A : ℝ → Set F.N.carrier) (hn₀ : ∀ r, n₀ r ∈ A r)
       (f : ℝ → NormalizedPair G Λ) (hΛ : 0 < (Λ : ℝ))
   …

   Mentions: OAI.PolycyclicRecognition.cartanRootIdeal, OAI.PolycyclicRecognition.IsMaximizingColumnBasis, OAI.PolycyclicRecognition.wordListCoordinates, OAI.PolycyclicRecognition.HasSubexponentialLowerBound, OAI.PolycyclicRecognition.NormalizedPair