OAI/GroupTheory/PolycyclicRecognition/Geometry/CoordinateProfileFlow.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.rescaled_horizontal_flow_tendsto line 19

   Source documentation

   The full rescaled flow converges as a continuous map, so the cutoff construction applies simultaneously to every compact time interval.

   theorem rescaled_horizontal_flow_tendsto
       {L : Type*} [LieRing L] [LieAlgebra ℝ L] {n c : ℕ}
       (a : DynkinCoefficients c 2) (b : Basis (Fin n) ℝ L) (cost : Fin n → ℝ)
       (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) :
       Tendsto (fun r => dynkinFlowMap a (basisBracket (exponentialRescaleBasis b cost r))
         ((exponentialRescaleBasis b cost r).equivFun (Real.exp r • v))) atTop
         (𝓝 (dynkinFlowMap a (gradedCoordinateBracket b cost) (gradedGenerator b cost 1 v))) := by
   …

   Mentions: OAI.PolycyclicRecognition.DynkinCoefficients, OAI.PolycyclicRecognition.dynkinFlowMap, OAI.PolycyclicRecognition.basisBracket, OAI.PolycyclicRecognition.exponentialRescaleBasis, OAI.PolycyclicRecognition.gradedCoordinateBracket, OAI.PolycyclicRecognition.gradedGenerator

2. theorem OAI.PolycyclicRecognition.measurePreserving_model_horizontal_flow line 32

   Source documentation

   In actual exponential coordinates the horizontal flow preserves the same Lebesgue measure at every scale and time.

   theorem measurePreserving_model_horizontal_flow
       {E D L : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
       [FiniteDimensional ℝ E] [TopologicalSpace D] [ChartedSpace E D] [Group D]
       [LieGroup (𝓘(ℝ, E)) ⊤ D] [T2Space D] [SimplyConnectedSpace D]
       [MeasurableSpace D] [BorelSpace D] [LieRing L] [LieAlgebra ℝ L]
       (haar : NilpotentExponentialHaarInput E D)
       (Exp : GroupLieAlgebra (𝓘(ℝ, E)) D → D) (hExp : IsGroupExponential Exp)
       (e : L ≃ₗ⁅ℝ⁆ GroupLieAlgebra (𝓘(ℝ, E)) D)
       (hnil : LieRing.IsNilpotent (GroupLieAlgebra (𝓘(ℝ, E)) D))
       {n c : ℕ} (b : Basis (Fin n) ℝ L) (a : DynkinCoefficients c 2)
       (hm : ∀ x y, Exp (finiteDynkinPolynomial a ![x, y]) = Exp x * Exp y)
       (r t : ℝ) (v : L) :
   …

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

3. theorem OAI.PolycyclicRecognition.coordinateChartPoint_horizontal_flow line 53

   Source documentation

   Right translation in the ambient group changes the second coordinate by exactly the polynomial flow used in the cutoff construction.

   theorem coordinateChartPoint_horizontal_flow
       {G N D LN LD : Type*} [Group G] [MetricSpace G]
       [IsTopologicalGroup G] [IsIsometricSMul G G] [Group N] [Group D]
       [LieRing LN] [LieAlgebra ℝ LN] [LieRing LD] [LieAlgebra ℝ LD]
       {n m c : ℕ} {Λ : ℝ≥0}
       (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) (r t : ℝ) (z : (Fin n → ℝ) × (Fin m → ℝ)) :
       (κ (ExpD ((r * t) • v)))⁻¹ • coordinateChartPoint p x ι κ ExpN ExpD bN bD k z =
   …

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