OAI/GroupTheory/PolycyclicRecognition/Geometry/ConeHeightMultiplier.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.CartanWordModel.exists_cone_haar_height_multiplier line 23

   Source documentation

   The positive trace coefficients give the exact Haar multiplier as a linear functional on the already chosen canonical height space.

   theorem exists_cone_haar_height_multiplier
       (C : Set (H →ₗ[ℝ] ℝ)) (hadd : ∀ x ∈ C, ∀ y ∈ C, x + y ∈ C)
       (Q : NilpotentLieModel ((cartanRootIdeal H) ⧸ M.coneWordIdeal C))
       (ExpQ : GroupLieAlgebra (𝓘(ℝ, Q.modelSpace)) Q.carrier → Q.carrier)
       (hExpQ : IsGroupExponential ExpQ) (hbij : Function.Bijective ExpQ)
       (haar : NilpotentExponentialHaarInput Q.modelSpace Q.carrier) :
       ∃ (μ : Measure Q.carrier) (ell : W →ₗ[ℝ] ℝ) (c : Fin M.letterCount → ℕ),
         μ.IsHaarMeasure ∧
         (∀ i, (M.weight i : H →ₗ[ℝ] ℝ) ∉ C → c i = 0) ∧
         (∀ i, (M.weight i : H →ₗ[ℝ] ℝ) ∈ C → 0 < c i) ∧
         ell = (∑ i, (c i : ℝ) • cartanHeightWeight T H (M.weight i)).comp
           eW.symm.toLinearMap ∧
   …

   Mentions: OAI.PolycyclicRecognition.NilpotentLieModel, OAI.PolycyclicRecognition.cartanRootIdeal, OAI.PolycyclicRecognition.NilpotentExponentialHaarInput, OAI.PolycyclicRecognition.cartanHeightWeight

2. theorem OAI.PolycyclicRecognition.haar_image_le_of_height_error line 56

   Source documentation

   A uniform height error controls the Haar multiplier at every anchor. The location of the translated quotient set never enters the estimate.

   theorem haar_image_le_of_height_error
       {W Q : Type*} [NormedAddCommGroup W] [NormedSpace ℝ W] [MeasurableSpace Q]
       (ell : W →L[ℝ] ℝ) (μ : Measure Q) (α : Q ≃ Q) (S : Set Q)
       (height offset : W) (r ε : ℝ)
       (hvol : μ (α '' S) = ENNReal.ofReal (Real.exp (ell height)) * μ S)
       (herror : ‖height + r • offset‖ ≤ ε) :
       μ (α '' S) ≤ ENNReal.ofReal
         (Real.exp (-ell offset * r + ‖ell‖ * ε)) * μ S := by
   …