FlowSegmentImages.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Exact height images of the graded horizontal segments

theorem OAI.PolycyclicRecognition.isCompact_segment_real line 13
theorem OAI.PolycyclicRecognition.SupportDatum.templateSupport_affine_segment line 18

theorem OAI.PolycyclicRecognition.gradedWordChartFlow_zero line 30

Source documentation

The zero-time point is retained by the limiting polynomial group law.

theorem gradedWordChartFlow_zero
    {L G I : Type*} [LieRing L] [LieAlgebra ℝ L] [Group G]
    [Fintype I] [DecidableEq I]
    (X : I → L) (S : Finset (FreeMagma I)) (β : WordBasisSelections X S)
    (Exp : L → G) (hinj : Function.Injective Exp) (hzero : Exp 0 = 1)
    (hneg : ∀ x, Exp (-x) = (Exp x)⁻¹)
    (hadd : ∀ x (s t : ℝ), Exp ((s + t) • x) = Exp (s • x) * Exp (t • x))
    {c : ℕ} (a : DynkinCoefficients c 2)
    (hm : ∀ x y, Exp (finiteDynkinPolynomial a ![x, y]) = Exp x * Exp y)
    (hweight : ∀ i j k,
      (WordBasisSelections.basis X S β).repr
          ⁅(WordBasisSelections.basis X S β) i, (WordBasisSelections.basis X S β) j⁆ k ≠ 0 →
…

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

theorem OAI.PolycyclicRecognition.affine_interval_image line 53

theorem OAI.PolycyclicRecognition.gradedWordChartFlow_height_image line 69

Source documentation

The entire limiting horizontal segment has exactly its expected affine height image, including both endpoints.

theorem gradedWordChartFlow_height_image
    {L G W I : Type*} [LieRing L] [LieAlgebra ℝ L]
    [Group G] [NormedAddCommGroup W] [NormedSpace ℝ W] [Fintype I] [DecidableEq I]
    (X : I → L) (S : Finset (FreeMagma I)) (β : WordBasisSelections X S)
    (h : L →ₗ[ℝ] W) (hh : ∀ x y : L, h ⁅x, y⁆ = 0)
    (Exp : L → G) (π : G →* Multiplicative W) (hπ : ∀ x, (π (Exp x)).toAdd = h x)
    {c : ℕ} (a : DynkinCoefficients c 2)
    (hm : ∀ x y, Exp (finiteDynkinPolynomial a ![x, y]) = Exp x * Exp y)
    (v : L) (z : Fin (finrank ℝ L) → ℝ) {T : ℝ} (hT : 0 < T)
    (hweight : ∀ i j k,
      (WordBasisSelections.basis X S β).repr
          ⁅(WordBasisSelections.basis X S β) i, (WordBasisSelections.basis X S β) j⁆ k ≠ 0 →
…