OAI/GroupTheory/PolycyclicRecognition/Geometry/CartanScaleTransition.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Exact scale transport of the actual Cartan profiles on a fixed ball

  1. def OAI.PolycyclicRecognition.wordBallScaleTransition line 19

    Source documentation

    The same group point in the two word charts, restricted to a fixed coordinate ball. Larger physical scales contract this ball.

    def wordBallScaleTransition
    (X : I → L) (S : Finset (FreeMagma I)) (β : WordBasisSelections X S)
    (R : ℝ) {r t : ℝ} (hr : 0 < r) (hrt : r ≤ t) :
    C(Metric.closedBall (0 : Fin (finrank ℝ L) → ℝ) R,
      Metric.closedBall (0 : Fin (finrank ℝ L) → ℝ) R) :=
…

    Mentions: OAI.PolycyclicRecognition.WordBasisSelections

  2. theorem OAI.PolycyclicRecognition.wordBallScaleTransition_height line 31
  3. theorem OAI.PolycyclicRecognition.CartanFactorModel.wordBall_profile_scale_eq line 56