OAI/GroupTheory/PolycyclicRecognition/Geometry/CartanMeasuredProbeRegions.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.CartanWordModel.exists_measured_two_path_probe_regions line 40

   Source documentation

   The two actual target paths give quotient/ideal/Cartan regions in one fixed section. All their volume estimates follow from exponential Haar coordinates, and no target-coordinate volume bound is an assumption.

   theorem exists_measured_two_path_probe_regions
       (b₀ : Basis (Fin (finrank ℝ (cartanRootIdeal H))) ℝ (cartanRootIdeal H))
       (γ₀ : M.Bases) {cell : Set (F.N.carrier × F.D.carrier)} (hcell : IsCompact cell)
       (hφ : ∀ d, F.action d = M.adjointGroupAutomorphism T F.N.equiv F.ExpN F.isExpN
         hbijN dynkinN (cartanLog H F.D.equiv F.ExpD hbijD d))
       (hpath : ∀ g : G, ∃ γ : ℝ → G, γ 0 = 1 ∧ γ 1 = g ∧
         ∀ t ∈ Icc (0 : ℝ) 1, ∀ u ∈ Icc (0 : ℝ) 1,
           dist (γ t) (γ u) ≤ dist 1 g * |t - u|)
       {Kπ : ℝ} (hKπ : 0 ≤ Kπ)
       (hLip : ∀ x y, ‖(π x).toAdd - (π y).toAdd‖ ≤ Kπ * dist x y)
       (C : Set (H →ₗ[ℝ] ℝ))
       (Q : NilpotentLieModel ((cartanRootIdeal H) ⧸ M.coneWordIdeal C))
   …

   Mentions: OAI.PolycyclicRecognition.cartanRootIdeal, OAI.PolycyclicRecognition.cartanLog, OAI.PolycyclicRecognition.NilpotentLieModel