CartanRayBoundaryModel.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

Concrete ray quotients and their ambient actions

The model is chosen from the previously stated nilpotent existence, integration, and Haar inputs. Its action, section, topology and contraction are proved properties of that choice.

structure OAI.PolycyclicRecognition.CartanWordModel.RayBoundaryModel line 30
Source documentation
The actual integrated ray quotient, with its descended ambient action.
```
structure RayBoundaryModel where
…
```
def OAI.PolycyclicRecognition.CartanWordModel.RayBoundaryModel.sectionMap line 45
theorem OAI.PolycyclicRecognition.CartanWordModel.RayBoundaryModel.continuous_sectionMap line 48
theorem OAI.PolycyclicRecognition.CartanWordModel.RayBoundaryModel.section_rightInverse line 51
theorem OAI.PolycyclicRecognition.CartanWordModel.RayBoundaryModel.orbit_surjective line 55
theorem OAI.PolycyclicRecognition.CartanWordModel.RayBoundaryModel.orbit_isQuotientMap line 58
theorem OAI.PolycyclicRecognition.CartanWordModel.RayBoundaryModel.continuous_action line 71
theorem OAI.PolycyclicRecognition.CartanWordModel.RayBoundaryModel.contracts_compact_orbits line 81
theorem OAI.PolycyclicRecognition.CartanWordModel.nonempty_rayBoundaryModel_of_published_inputs line 106
Source documentation
No boundary or metric conclusion is assumed in the construction.
```
theorem nonempty_rayBoundaryModel_of_published_inputs
    (hExpG : IsGroupExponential ExpG)
    (realize : ExponentialLinearRealizationInput (EG := EG) (G := G))
…
```
Mentions: OAI.PolycyclicRecognition.ExponentialLinearRealizationInput