CartanMeasuredCone.lean`

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The actual ideal, quotient and Haar measures for a fixed cone

structure OAI.PolycyclicRecognition.CartanWordModel.ConeGroupMaps line 25
Source documentation
Exponential and group maps for the one fixed mixed-word ideal.
```
structure ConeGroupMaps
    (Q : NilpotentLieModel ((cartanRootIdeal H) ⧸ M.coneWordIdeal C))
    (I : NilpotentLieModel (M.coneWordIdeal C)) where
…
```
Mentions: OAI.PolycyclicRecognition.NilpotentLieModel, OAI.PolycyclicRecognition.cartanRootIdeal
structure OAI.PolycyclicRecognition.CartanWordModel.ConeGroupMeasures line 51
Source documentation
Compatible Haar data; no profile, metric bound or offset is included.
```
structure ConeGroupMeasures
    (Q : NilpotentLieModel ((cartanRootIdeal H) ⧸ M.coneWordIdeal C))
    (I : NilpotentLieModel (M.coneWordIdeal C)) (D : M.ConeGroupMaps F C Q I) where
…
```
Mentions: OAI.PolycyclicRecognition.NilpotentLieModel, OAI.PolycyclicRecognition.cartanRootIdeal
structure OAI.PolycyclicRecognition.CartanWordModel.MeasuredCone line 68
Source documentation
The concrete groups, maps and compatible measures for one cone.
```
structure MeasuredCone where
…
```
theorem OAI.PolycyclicRecognition.CartanWordModel.nonempty_measuredCone line 80
Source documentation
The fixed cone's group models and compatible Haar measures follow from Lie integration and exponential Haar measure. Only the original published inputs are used; arbitrary pure-word sections can be installed afterward.
```
theorem nonempty_measuredCone
    (haarN : NilpotentExponentialHaarInput F.N.modelSpace F.N.carrier)
    (existQ : NilpotentLieExistenceInput ((cartanRootIdeal H) ⧸ M.coneWordIdeal C))
    (haarQ : ∀ Q : NilpotentLieModel ((cartanRootIdeal H) ⧸ M.coneWordIdeal C),
      NilpotentExponentialHaarInput Q.modelSpace Q.carrier)
    (integrateQ : ∀ Q : NilpotentLieModel ((cartanRootIdeal H) ⧸ M.coneWordIdeal C),
      NilpotentLieIntegrationInput (EN := F.N.modelSpace) (N := F.N.carrier)
…
```
Mentions: OAI.PolycyclicRecognition.NilpotentExponentialHaarInput, OAI.PolycyclicRecognition.NilpotentLieExistenceInput, OAI.PolycyclicRecognition.cartanRootIdeal, OAI.PolycyclicRecognition.NilpotentLieModel, OAI.PolycyclicRecognition.NilpotentLieIntegrationInput