ExpandedSchemeAmplitudes.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

The conjugate scheme inside a word with independent amplitudes

def OAI.PolycyclicRecognition.schemeAmplitudeSlots line 15
Source documentation
Each slot remembers either a fixed amplitude or one inserted coordinate.
```
def schemeAmplitudeSlots (w : Fin n → List (I × ℝ)) (i : Fin n → I) :
    List (I × (ℝ ⊕ Fin n)) :=
…
```
def OAI.PolycyclicRecognition.evaluateAmplitudeSlot line 21
theorem OAI.PolycyclicRecognition.map_schemeAmplitudeSlots line 24
theorem OAI.PolycyclicRecognition.contDiff_evaluateAmplitudeSlots line 33
Source documentation
All amplitudes of the expanded word are smooth affine functions of the original inserted coordinates.
```
theorem contDiff_evaluateAmplitudeSlots (l : List (I × (ℝ ⊕ Fin n))) {q : ℕ∞} :
    ContDiff ℝ q (fun t : Fin n → ℝ => fun j : Fin l.length =>
      evaluateAmplitudeSlot t (l.get j).2) := by
…
```
Mentions: OAI.PolycyclicRecognition.evaluateAmplitudeSlot
theorem OAI.PolycyclicRecognition.polynomialWord_eq_listProduct line 42

theorem OAI.PolycyclicRecognition.amplitudeWord_scheme_eq line 53

Source documentation

Flattening the slots preserves the genuine endpoint at every group law.

theorem amplitudeWord_scheme_eq (a : DynkinCoefficients c 2)
    (B : (Fin d → ℝ) →L[ℝ] (Fin d → ℝ) →L[ℝ] (Fin d → ℝ))
    (hB : IsLieBracket B) (hg : PolynomialGroupLaws (dynkinProduct a B))
    (X : I → Fin d → ℝ) (w : Fin n → List (I × ℝ)) (i : Fin n → I)
    (t : Fin n → ℝ) :
    amplitudeWordEndpoint a (fun j => ((schemeAmplitudeSlots w i).get j).1) (B, X)
      (fun j => evaluateAmplitudeSlot t ((schemeAmplitudeSlots w i).get j).2) =
        polynomialEndpointScheme a w i (B, X) t := by
…

Mentions: OAI.PolycyclicRecognition.DynkinCoefficients, OAI.PolycyclicRecognition.IsLieBracket, OAI.PolycyclicRecognition.PolynomialGroupLaws, OAI.PolycyclicRecognition.dynkinProduct, OAI.PolycyclicRecognition.amplitudeWordEndpoint, OAI.PolycyclicRecognition.schemeAmplitudeSlots, OAI.PolycyclicRecognition.evaluateAmplitudeSlot, OAI.PolycyclicRecognition.polynomialEndpointScheme