OAI/GroupTheory/PolycyclicRecognition/Algebra/DifferenceAmplitudeWord.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PolycyclicRecognition.differenceParameters line 15

   Source documentation

   First samples minus second samples, with the same fixed order of letters.

   def differenceParameters (m : ℕ) : (Fin (m + m) → ℝ) →L[ℝ] (Fin m → ℝ) :=
   …

2. theorem OAI.PolycyclicRecognition.differenceParameters_apply line 20
3. theorem OAI.PolycyclicRecognition.differenceParameters_append line 23
4. theorem OAI.PolycyclicRecognition.differenceParameters_surjective line 26
5. def OAI.PolycyclicRecognition.differenceAmplitudeWordEndpoint line 30
6. theorem OAI.PolycyclicRecognition.hasPolynomialCoordinates_differenceAmplitudeWord line 36
7. theorem OAI.PolycyclicRecognition.contDiff_differenceAmplitudeWord line 52
8. theorem OAI.PolycyclicRecognition.differenceAmplitudeWord_surjective_fderiv line 71

   Source documentation

   The independent-difference parametrization retains the full rank proved for the fixed generator word.

   theorem differenceAmplitudeWord_surjective_fderiv {I : Type*} [Fintype I] {n m c : ℕ}
       (a : DynkinCoefficients c 2) (letters : Fin m → I)
       (p : ((Fin n → ℝ) →L[ℝ] (Fin n → ℝ) →L[ℝ] (Fin n → ℝ)) × (I → Fin n → ℝ))
       (t₀ : Fin m → ℝ)
       (hs : Function.Surjective (fderiv ℝ (amplitudeWordEndpoint a letters p) t₀)) :
       Function.Surjective (fderiv ℝ (differenceAmplitudeWordEndpoint a letters p) (Fin.append t₀ 0)) := by
   …

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

9. theorem OAI.PolycyclicRecognition.exists_submersive_differenceAmplitudeWord line 88