MatrixExponentialVelocity.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Exponential recovery from actual subgroup curves

The velocity of a curve in a closed matrix subgroup exponentiates inside that subgroup. The proof uses growing powers of the curve and the first-order approximation to the matrix exponential. Thus no matrix Lie-group classification or determinant formula for the exponential is needed. The converse supplies an exact exponential test for membership in the actual velocity subspace.

lemma OAI.DukePrimeDegree.eventual_exp_bound_of_scaled_increment line 25

theorem OAI.DukePrimeDegree.tendsto_matrix_powers_of_velocity line 47

Source documentation

The reciprocal-time powers of an actual curve converge to the matrix exponential of its velocity.

theorem tendsto_matrix_powers_of_velocity {n : ℕ} [Nonempty (Fin n)]
    (γ : ℝ → G n) (V : Matrix (Fin n) (Fin n) ℝ)
    (hvelocity : HasMatrixVelocity γ V) :
    Tendsto (fun N : ℕ => (γ ((N + 1 : ℝ)⁻¹)).val ^ (N + 1)) atTop
      (𝓝 (NormedSpace.exp V)) := by
…

Mentions: OAI.DukePrimeDegree.HasMatrixVelocity

theorem OAI.DukePrimeDegree.exists_subgroup_element_exp_velocity line 113

Source documentation

The determinant-one assertion is recovered from the approximating group elements, not assumed as a general exponential formula.

theorem exists_subgroup_element_exp_velocity {n : ℕ} [Nonempty (Fin n)]
    (L : Subgroup (G n)) (hL : IsClosed (L : Set (G n)))
    (γ : ℝ → G n) (hγ : ∀ t, γ t ∈ L)
    (V : Matrix (Fin n) (Fin n) ℝ) (hV : HasMatrixVelocity γ V) :
    ∃ g : G n, g ∈ L ∧ g.val = NormedSpace.exp V := by
…

Mentions: OAI.DukePrimeDegree.HasMatrixVelocity

theorem OAI.DukePrimeDegree.mem_matrixVelocitySpace_iff_exp line 141
Source documentation
Exact exponential characterization of the actual tangent subspace of a closed subgroup. This will allow measurable membership tests without choosing differentiable curves measurably.
```
theorem mem_matrixVelocitySpace_iff_exp {n : ℕ} [Nonempty (Fin n)]
    (L : Subgroup (G n)) (hL : IsClosed (L : Set (G n)))
    (V : Matrix (Fin n) (Fin n) ℝ) :
    V ∈ matrixVelocitySpace L ↔
      ∀ t : ℝ, ∃ g : G n, g ∈ L ∧ g.val = NormedSpace.exp (t • V) := by
…
```
Mentions: OAI.DukePrimeDegree.matrixVelocitySpace