OAI/GroupTheory/PolycyclicRecognition/Geometry/GoodRescaledFlowLegs.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.exists_good_rescaled_flow_legs line 18

   Source documentation

   Combine the slow good-sheet selection, proved graded-flow convergence, and the exact exponential-coordinate identity. The conclusion is expressed at physical scale r, along the original one-parameter subgroup.

   theorem exists_good_rescaled_flow_legs
       {L D N G W : Type*} [LieRing L] [LieAlgebra ℝ L]
       [Group D] [Group N] [Group G] [MeasurableSpace N]
       [NormedAddCommGroup W] [NormedSpace ℝ W] {n c : ℕ}
       (ExpD : L → D) (b : Basis (Fin n) ℝ L) (cost : Fin n → ℝ)
       (a : DynkinCoefficients c 2)
       (hm : ∀ x y, ExpD (finiteDynkinPolynomial a ![x, y]) = ExpD x * ExpD y)
       (hweight : ∀ i j k, b.repr ⁅b i, b j⁆ k ≠ 0 → cost i + cost j ≤ cost k)
       (v : L) (hv : ∀ j, b.repr v j ≠ 0 → 1 ≤ cost j)
       (ι : N →* G) (κ : D →* G) (J : ℝ → G → W) (x : ℝ → G)
       (S : Set C((Fin n → ℝ), W)) [MeasurableSpace S] [BorelSpace S] [HasOuterApproxClosed S]
       (samples : ℝ → ProbabilityMeasure N) (profile : ℝ → N → S)
   …

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