RootVelocityRecovery.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Recovering an actual root element from a pure root velocity

A curve in a closed subgroup whose velocity is one elementary matrix produces the corresponding root element by taking growing powers at reciprocal times. The proof compares those powers with the exact powers of a transvection. No diagonal normalization of the subgroup is needed.

lemma OAI.DukePrimeDegree.hasIdentityMatrixDerivative_rootCurve line 22
lemma OAI.DukePrimeDegree.transvection_nat_pow line 44

theorem OAI.DukePrimeDegree.tendsto_powers_of_pure_root_velocity line 60

Source documentation

Entrywise first-order control gives the norm control needed for growing products. All matrices here use the submultiplicative operator norm.

theorem tendsto_powers_of_pure_root_velocity {n : ℕ} {i j : Fin n}
    (hij : i ≠ j) (γ : ℝ → G n) (v : ℝ)
    (hvelocity : HasMatrixVelocity γ (Matrix.single i j v)) :
    Tendsto (fun N : ℕ => γ ((N + 1 : ℝ)⁻¹) ^ (N + 1)) atTop
      (𝓝 (Matrix.SpecialLinearGroup.transvection hij v)) := by
…

Mentions: OAI.DukePrimeDegree.HasMatrixVelocity

theorem OAI.DukePrimeDegree.root_mem_of_pure_matrix_velocity line 153

Source documentation

A pure root tangent direction in a closed matrix subgroup already gives an actual root element of that subgroup.

theorem root_mem_of_pure_matrix_velocity {n : ℕ} {i j : Fin n}
    (hij : i ≠ j) (L : Subgroup (G n)) (hclosed : IsClosed (L : Set (G n)))
    (γ : ℝ → G n) (hγ : ∀ t, γ t ∈ L) (v : ℝ)
    (hvelocity : HasMatrixVelocity γ (Matrix.single i j v)) :
    Matrix.SpecialLinearGroup.transvection hij v ∈ L := by
…

Mentions: OAI.DukePrimeDegree.HasMatrixVelocity

theorem OAI.DukePrimeDegree.root_mem_of_velocitySpace line 161
theorem OAI.DukePrimeDegree.root_direction_mem_velocitySpace_iff line 172
Source documentation
The elementary tangent-direction test is exactly full real-root invariance for a closed subgroup. A single nonzero root element alone would not suffice for this equivalence.
```
theorem root_direction_mem_velocitySpace_iff {n : ℕ} {i j : Fin n}
    (hij : i ≠ j) (L : Subgroup (G n)) (hclosed : IsClosed (L : Set (G n))) :
    Matrix.single i j (1 : ℝ) ∈ matrixVelocitySpace L ↔
      ∀ t : ℝ, Matrix.SpecialLinearGroup.transvection hij t ∈ L := by
…
```
Mentions: OAI.DukePrimeDegree.matrixVelocitySpace