RootCurveExtraction.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

Extracting a root from a differentiable curve

A diagonal with a unique maximal root rescales a curve at the identity. Its limit is the elementary matrix given by that root component of the velocity. Closedness then puts this actual root element in the subgroup. This is a direct matrix argument, with no Lie-subgroup classification.

def OAI.DukePrimeDegree.rootIsolationWeights line 23
lemma OAI.DukePrimeDegree.rootIsolationWeights_sum line 26
lemma OAI.DukePrimeDegree.rootIsolationWeights_peak line 30
lemma OAI.DukePrimeDegree.rootIsolationWeights_lt_peak line 34
lemma OAI.DukePrimeDegree.diagonal_conjugate_matrix_entry line 41
def OAI.DukePrimeDegree.HasMatrixVelocity line 50
Source documentation
Entrywise velocity at the identity; the parameter approaches zero through positive real values, exactly as in the rescaling argument.
```
def HasMatrixVelocity {n : ℕ} (γ : ℝ → G n)
    (V : Matrix (Fin n) (Fin n) ℝ) : Prop :=
…
```
lemma OAI.DukePrimeDegree.hasMatrixVelocity_of_hasDerivAt line 55

theorem OAI.DukePrimeDegree.tendsto_diagonal_rescale_curve line 64

Source documentation

Rescaling isolates a single root component of a curve's velocity.

theorem tendsto_diagonal_rescale_curve {n : ℕ}
    (i j : Fin n) (hij : i ≠ j) (γ : ℝ → G n)
    (V : Matrix (Fin n) (Fin n) ℝ) (hvelocity : HasMatrixVelocity γ V) :
    Tendsto (fun m : ℕ =>
      diagonalOneParameter (rootIsolationWeights i j) (rootIsolationWeights_sum i j) (m : ℝ) *
        γ (Real.exp (-2 * (m : ℝ))) *
        diagonalOneParameter (rootIsolationWeights i j) (rootIsolationWeights_sum i j) (-(m : ℝ)))
      atTop (𝓝 (Matrix.SpecialLinearGroup.transvection hij (V i j))) := by
…

Mentions: OAI.DukePrimeDegree.HasMatrixVelocity, OAI.DukePrimeDegree.rootIsolationWeights, OAI.DukePrimeDegree.rootIsolationWeights_sum

theorem OAI.DukePrimeDegree.root_mem_of_matrix_velocity line 135

Source documentation

A closed subgroup normalized by all split diagonals contains each root component isolated from one of its curves at the identity.

theorem root_mem_of_matrix_velocity {n : ℕ}
    (L : Subgroup (G n)) (hclosed : IsClosed (L : Set (G n)))
    (hnormal : ∀ (ell : Fin n → ℝ) (hsum : ∑ a, ell a = 0) (t : ℝ),
      ∀ g ∈ L, diagonalOneParameter ell hsum t * g * diagonalOneParameter ell hsum (-t) ∈ L)
    (γ : ℝ → G n) (hγ : ∀ t, γ t ∈ L)
    (V : Matrix (Fin n) (Fin n) ℝ) (hvelocity : HasMatrixVelocity γ V)
    (i j : Fin n) (hij : i ≠ j) :
    Matrix.SpecialLinearGroup.transvection hij (V i j) ∈ L := by
…

Mentions: OAI.DukePrimeDegree.HasMatrixVelocity