RescaledSubmersiveScheme.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

A fixed submersive scheme for an actual sequence of rescalings

The subsequence and the word are selected from the actual coordinate laws, before any good sheets or successful parameter sets are selected.

def OAI.PolycyclicRecognition.HasSubmersiveWordSubsequence line 22

Source documentation

A convergent subsequence and a fixed word with full-rank limiting endpoint map. This packages only the explicit finite-dimensional data.

def HasSubmersiveWordSubsequence {I : Type*} {n c : ℕ}
    (a : DynkinCoefficients c 2)
    (S : Set (((Fin n → ℝ) →L[ℝ] (Fin n → ℝ) →L[ℝ] (Fin n → ℝ)) ×
      (I → Fin n → ℝ)))
    (p : ℕ → ((Fin n → ℝ) →L[ℝ] (Fin n → ℝ) →L[ℝ] (Fin n → ℝ)) ×
      (I → Fin n → ℝ)) : Prop :=
…

Mentions: OAI.PolycyclicRecognition.DynkinCoefficients

theorem OAI.PolycyclicRecognition.exists_submersive_scheme_of_normalized_sequence line 36

Source documentation

Compact normalized laws retain their basis-word identities and hence a submersive fixed word. This form keeps the compactness step independent of the choice of a matrix realization.

theorem exists_submersive_scheme_of_normalized_sequence
    {I : Type*} [Fintype I] {n c : ℕ} (a : DynkinCoefficients c 2)
    (w : Fin n → FreeMagma I) (C : ℝ)
    (p : ℕ → ((Fin n → ℝ) →L[ℝ] (Fin n → ℝ) →L[ℝ] (Fin n → ℝ)) ×
      (I → Fin n → ℝ))
    (hp : ∀ k, p k ∈ normalizedExponentialParameters a w (fun i => Pi.single i 1) C) :
    ∃ q ∈ normalizedExponentialParameters a w (fun i => Pi.single i 1) C,
      ∃ u : ℕ → ℕ, StrictMono u ∧ Tendsto (p ∘ u) atTop (𝓝 q) ∧
        ∃ (m : ℕ) (letters : Fin m → I) (t : Fin (m + m) → ℝ),
          differenceAmplitudeWordEndpoint a letters q t = 0 ∧
          Function.Surjective (fderiv ℝ (differenceAmplitudeWordEndpoint a letters q) t) := by
…

Mentions: OAI.PolycyclicRecognition.DynkinCoefficients, OAI.PolycyclicRecognition.normalizedExponentialParameters, OAI.PolycyclicRecognition.differenceAmplitudeWordEndpoint

theorem OAI.PolycyclicRecognition.exists_rescaled_submersive_scheme line 65

Source documentation

A genuine family of rescaled exponential-coordinate groups has a convergent subsequence and one fixed independent-difference word whose limiting derivative is onto. In particular rank is not an extra hypothesis on the subsequently retained good sets.

theorem exists_rescaled_submersive_scheme
    (X : I → L) {k : ℕ} (hk : LieModule.lowerCentralSeries ℝ L L k = ⊥)
    (hletters : ∀ i : I, FreeMagma.of i ∈ boundedBracketWords k)
    (b : Basis (Fin (finrank ℝ L)) ℝ L)
    (Exp : L → G) (hinj : Function.Injective Exp)
    (hzero : Exp 0 = 1) (hneg : ∀ x, Exp (-x) = (Exp x)⁻¹)
    (hadd : ∀ x (s t : ℝ), Exp ((s + t) • x) = Exp (s • x) * Exp (t • x))
    {c : ℕ} (a : DynkinCoefficients c 2)
    (hm : ∀ x y, Exp (finiteDynkinPolynomial a ![x, y]) = Exp x * Exp y)
    (j : L →ₗ⁅ℝ⁆ A) (ρ : G →* Aˣ) (hρ : Function.Injective ρ)
    (hmatch : ∀ x, ρ (Exp x) = algebraExpUnit (j x))
    (s : I → ℝ) (β : WordBasisSelections X (boundedBracketWords k))
…

Mentions: OAI.PolycyclicRecognition.boundedBracketWords, OAI.PolycyclicRecognition.DynkinCoefficients, OAI.PolycyclicRecognition.finiteDynkinPolynomial, OAI.PolycyclicRecognition.algebraExpUnit, OAI.PolycyclicRecognition.WordBasisSelections