CoordinateFlowProfileIdentity.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Exact increments for the actual polynomial horizontal flow

theorem OAI.PolycyclicRecognition.exp_basis_horizontal_flow line 15

theorem OAI.PolycyclicRecognition.coordinate_rescaled_profile_increment line 29

Source documentation

The profile and occupation chart use identical scaling and basepoints, so their horizontal increments agree exactly before passing to a limit.

theorem coordinate_rescaled_profile_increment
    {G N D LN LD W : Type*} [Group G] [MetricSpace G] [ProperSpace G]
    [IsTopologicalGroup G] [IsIsometricSMul G G] [Group N] [Group D]
    [LieRing LN] [LieAlgebra ℝ LN] [LieRing LD] [LieAlgebra ℝ LD]
    [NormedAddCommGroup W] [NormedSpace ℝ W] {n m c : ℕ} {Λ : ℝ≥0}
    (π : G →* Multiplicative W) (p : NormalizedPair G Λ) (x : G)
    (ι : N →* G) (κ : D →* G) (ExpN : LN → N) (ExpD : LD → D)
    (bN : Basis (Fin n) ℝ LN) (bD : Basis (Fin m) ℝ LD) (k : N)
    (a : DynkinCoefficients c 2)
    (hm : ∀ x y, ExpD (finiteDynkinPolynomial a ![x, y]) = ExpD x * ExpD y)
    (v : LD) (s T : ℝ) (y : Fin n → ℝ) (z : Fin m → ℝ) :
    let φ := fun z => κ (ExpD (bD.equivFun.symm z))
…

Mentions: OAI.PolycyclicRecognition.NormalizedPair, OAI.PolycyclicRecognition.DynkinCoefficients, OAI.PolycyclicRecognition.finiteDynkinPolynomial