OAI/GroupTheory/PolycyclicRecognition/Geometry/CartanBoundaryBoundedHeight.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.CartanWordModel.uniform_transversal_traces_of_boundary_comparisons line 47

   Source documentation

   Finitely many boundary characters give one common transversal bound.

   theorem uniform_transversal_traces_of_boundary_comparisons
       {L : ℝ} (hleaf : ∀ p x (n : F.N.carrier),
         ‖(height (f p (x * F.inclusionN n))).toAdd - (height (f p x)).toAdd‖ ≤ L) :
       ∃ B : ℝ, 0 ≤ B ∧ ∀ p d i,
         |(C i).targetRate * (M.supportIn T hunimod eW).weight i ((height (f p (F.inclusionD d))).toAdd - (height (f p 1)).toAdd) -
           (C i).sourceRate * (M.supportIn T hunimod eW).weight i (A.val (height (F.inclusionD d)).toAdd)| ≤ B := by
   …

2. theorem OAI.PolycyclicRecognition.CartanWordModel.uniform_affine_bound_of_boundary_comparisons line 77

   Source documentation

   The leaf and averaged traces now come from the constructed boundary volume data. Only the already proved sublinear estimate is retained here.

   theorem uniform_affine_bound_of_boundary_comparisons
       (hheight : ∀ x, (height (ExpG x)).toAdd = eW (heightProjection T.character x))
       (haarN : NilpotentExponentialHaarInput F.N.modelSpace F.N.carrier)
       (b₀ : Basis (Fin (finrank ℝ (cartanRootIdeal H))) ℝ (cartanRootIdeal H)) (γ₀ : M.Bases)
       (hsub : ∀ p ε, 0 < ε → ∃ B : ℝ, ∀ g,
         ‖(height (f p g)).toAdd - (height (f p 1)).toAdd - A.val (height g).toAdd‖ ≤
           ε * dist 1 g + B) :
       ∃ K : ℝ, 0 ≤ K ∧ ∀ p g,
         ‖(height (f p g)).toAdd - ((height (f p 1)).toAdd + A.val (height g).toAdd)‖ ≤ K := by
   …

   Mentions: OAI.PolycyclicRecognition.heightProjection, OAI.PolycyclicRecognition.NilpotentExponentialHaarInput, OAI.PolycyclicRecognition.cartanRootIdeal