ConeIdealBoxCalculus.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

Product and Haar estimates for the actual cone ideal boxes

def OAI.PolycyclicRecognition.CartanWordModel.coneIdealBoxBasis line 18
def OAI.PolycyclicRecognition.CartanWordModel.coneIdealBox line 24
def OAI.PolycyclicRecognition.CartanWordModel.IsMaximizingConeIdealBasis line 28
theorem OAI.PolycyclicRecognition.CartanWordModel.exists_maximizing_coneIdealBasis line 35
theorem OAI.PolycyclicRecognition.CartanWordModel.coneIdealWordCost_smul line 41
theorem OAI.PolycyclicRecognition.CartanWordModel.maximizing_coneIdealBasis_smul line 50
theorem OAI.PolycyclicRecognition.CartanWordModel.exists_uniform_coneIdeal_structureConstant_bound line 60
theorem OAI.PolycyclicRecognition.CartanWordModel.exists_coneIdealBox_product_bound line 78
theorem OAI.PolycyclicRecognition.CartanWordModel.coneIdealBox_inv_mem line 94

theorem OAI.PolycyclicRecognition.CartanWordModel.exists_coneIdealBox_haar_volume line 104

Source documentation

The ideal volume exponent is the sum of the original mixed-word widths. The formula holds for every selected basis, before maximizing.

theorem exists_coneIdealBox_haar_volume (haar : NilpotentExponentialHaarInput E G)
    (b₀ : Basis (Fin (finrank ℝ (M.coneWordIdeal C))) ℝ (M.coneWordIdeal C)) :
    ∃ μ : Measure G, μ.IsHaarMeasure ∧
      ∀ (s : Fin M.letterCount → ℝ) (β : M.ConeIdealBases C) (r R : ℝ), 0 ≤ R →
      μ (M.coneIdealBox C (Exp ∘ e) s β r R) =
        ENNReal.ofReal |(columnBasisMatrix
          (wordListCoordinates (M.coneMixedVector C) (M.coneIdealWordList C) b₀)
          β.val).det| *
        ENNReal.ofReal (Real.exp (r * ∑ j,
          bracketWordExponent s (M.coneOriginalWord C (β.val j)))) *
        ENNReal.ofReal (2 * R) ^ finrank ℝ (M.coneWordIdeal C) := by
…

Mentions: OAI.PolycyclicRecognition.NilpotentExponentialHaarInput, OAI.PolycyclicRecognition.columnBasisMatrix, OAI.PolycyclicRecognition.wordListCoordinates, OAI.PolycyclicRecognition.bracketWordExponent