OAI/GroupTheory/PolycyclicRecognition/Geometry/CartanBasepointProfileIdentity.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.CartanFactorModel.profileChart_basepoint_change line 30

   Source documentation

   The group identity underlying basepoint comparison uses the actual Cartan charts and the actual conjugation action.

   theorem profileChart_basepoint_change
       (source target : Basis (Fin (finrank ℝ H)) ℝ H)
       (x : G) (u a : F.N.carrier) (k : F.D.carrier) (z : Fin (finrank ℝ H) → ℝ) :
       x * F.inclusionN a * F.profileChart source z =
         (x * (F.inclusionN u * F.inclusionD k)) *
           F.inclusionN (F.action k⁻¹ (u⁻¹ * a)) *
             F.profileChart target (wordChartLeftShift F.D.equiv chartD source target k z) := by
   …

   Mentions: OAI.PolycyclicRecognition.wordChartLeftShift

2. theorem OAI.PolycyclicRecognition.CartanFactorModel.realScaleProfile_basepoint_change line 50

   Source documentation

   The raw normalized profiles satisfy the exact change-of-center identity; all errors arise later from affine approximation, not from this formula.

   theorem realScaleProfile_basepoint_change
       (hD : Continuous F.ExpD) (J : G → W) (hJ : Continuous J)
       (x : G) (u a : F.N.carrier) (k : F.D.carrier)
       (X : I → H) (S : Finset (FreeMagma I)) (β : WordBasisSelections X S)
       {r s : ℝ} (hr : 1 ≤ r) (hs : 1 ≤ s) (z : Fin (finrank ℝ H) → ℝ) :
       let b := WordBasisSelections.basis X S β
   …

   Mentions: OAI.PolycyclicRecognition.WordBasisSelections, OAI.PolycyclicRecognition.WordBasisSelections.basis