OAI/GroupTheory/PolycyclicRecognition/Geometry/RootSwitchCurves.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Continuous short switches with constant height

Use the actual root one-parameter subgroup for a switch. Every pair of its points has logarithmic distance at a supporting Cartan position, while its canonical height is exactly constant. No choice of geodesics is needed.

  1. def OAI.PolycyclicRecognition.rootSwitchCurve line 20
  2. theorem OAI.PolycyclicRecognition.rootSwitchCurve_endpoints line 24
  3. theorem OAI.PolycyclicRecognition.continuous_rootSwitchCurve line 41
  4. theorem OAI.PolycyclicRecognition.cartan_letter_exp_height_eq_one line 50
  5. theorem OAI.PolycyclicRecognition.rootSwitchCurve_height line 63
  6. theorem OAI.PolycyclicRecognition.CartanWordModel.exists_uniform_support_switch_curve_bound line 78

    Source documentation

    One logarithmic diameter bound for all actual root switch curves.

    theorem CartanWordModel.exists_uniform_support_switch_curve_bound
    {A B : ℝ} (hA : 0 ≤ A) (hB : 0 ≤ B) (p : ℕ) :
    ∃ K : ℝ, 0 < K ∧ ∀ (i : Fin M.letterCount) (r : ℝ), 0 ≤ r →
      ∀ (x : G) (h : H) (s b : ℝ),
      ‖(finBasis ℝ H).equivFun h‖ ≤ A * (1 + r) ^ p →
      M.weight i h = r * s → |b| ≤ B * Real.exp (r * s) →
      ∀ t ∈ Set.Icc (0 : ℝ) 1, ∀ u ∈ Set.Icc (0 : ℝ) 1,
      dist (rootSwitchCurve Exp (M.letter i) b x (Exp h) t)
        (rootSwitchCurve Exp (M.letter i) b x (Exp h) u) ≤ K * Real.log (2 + r) := by
…

    Mentions: OAI.PolycyclicRecognition.rootSwitchCurve