SwitchEndpoints.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

The polynomial difference word is the endpoint of the successful switches

def OAI.PolycyclicRecognition.switchEndpoint line 15
Source documentation
The last state after the specified sequence of switches.
```
def switchEndpoint : (m : ℕ) → G → SwitchParameters G m → G
  | 0, x, _ => x
  | m + 1, x, p => switchEndpoint m (x * p.1 * p.2.1⁻¹) p.2.2
```
Mentions: OAI.PolycyclicRecognition.SwitchParameters
theorem OAI.PolycyclicRecognition.switchEndpoint_vector line 19
theorem OAI.PolycyclicRecognition.mapSwitchParameters_vector line 32
theorem OAI.PolycyclicRecognition.sampledSwitchEndpoint_eq line 42

theorem OAI.PolycyclicRecognition.exp_differenceAmplitudeWordEndpoint line 54

Source documentation

Exponentiating the actual polynomial endpoint gives precisely the ordered product of the sampled difference increments.

theorem exp_differenceAmplitudeWordEndpoint {I : Type*} {n m c : ℕ}
    (a : DynkinCoefficients c 2)
    (B : (Fin n → ℝ) →L[ℝ] (Fin n → ℝ) →L[ℝ] (Fin n → ℝ))
    (hg : PolynomialGroupLaws (dynkinProduct a B)) (X : I → Fin n → ℝ)
    (letters : Fin m → I) (t : Fin (m + m) → ℝ) :
    PolynomialCoordinateGroup.exp (dynkinProduct a B) hg
      (differenceAmplitudeWordEndpoint a letters (B, X) t) =
    (List.ofFn (fun j => PolynomialCoordinateGroup.exp (dynkinProduct a B) hg
      ((t (Fin.castAdd m j) - t (Fin.natAdd m j)) • X (letters j)))).prod := by
…

Mentions: OAI.PolycyclicRecognition.DynkinCoefficients, OAI.PolycyclicRecognition.PolynomialGroupLaws, OAI.PolycyclicRecognition.dynkinProduct, OAI.PolycyclicRecognition.PolynomialCoordinateGroup.exp, OAI.PolycyclicRecognition.differenceAmplitudeWordEndpoint