RootContraction.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Contraction of root pairs under neutral diagonal flows

The acting root group is the additive real line. If a diagonal direction expands the corresponding root character, forward right translation contracts the relative root parameter. This supplies the geometric hypothesis of the Hopf lemma even when the orbit leaves compact sets.

def OAI.DukePrimeDegree.rootTranslationAction line 23

Source documentation

The real root group acts on the lattice space by right translation.

@[instance_reducible] def rootTranslationAction {n : ℕ} {i j : Fin n} (hij : i ≠ j) :
    MulAction (Multiplicative ℝ) (X n) where
…

lemma OAI.DukePrimeDegree.rootTranslationAction_continuous line 35
lemma OAI.DukePrimeDegree.root_pair_diagonal_translate line 53
lemma OAI.DukePrimeDegree.diagonal_right_iterate line 73

lemma OAI.DukePrimeDegree.root_parameter_contracts line 84

Source documentation

With root weight one, the relative root parameter decays exponentially.

lemma root_parameter_contracts {n : ℕ} {i j : Fin n}
    (ell : Fin n → ℝ) (hweight : ell i - ell j = 1) (s : ℝ) :
    Tendsto (fun m : ℕ =>
      Multiplicative.ofAdd (Real.exp ((ell j - ell i) * (m : ℝ)) * s))
      atTop (𝓝 1) := by
…