OAI/GroupTheory/PolycyclicRecognition/Geometry/CartanFacetSupportedAgreement.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Contact-facet equality in the support of the actual joint law

  1. theorem OAI.PolycyclicRecognition.supported_profiles_agree_on_contact_facet line 21
  2. theorem OAI.PolycyclicRecognition.CartanWordModel.supported_word_profiles_agree_on_facet line 95

    Source documentation

    Exact facet agreement for the actual polynomial Cartan chart. The polynomial position bound and the chart's exact height are proved here.

    theorem supported_word_profiles_agree_on_facet
    (Exp : GroupLieAlgebra (𝓘(ℝ, EG)) G → G) (hExp : IsGroupExponential Exp)
    (realize : ExponentialLinearRealizationInput (EG := EG) (G := G))
…

    Mentions: OAI.PolycyclicRecognition.ExponentialLinearRealizationInput