PolynomialEndpointSchemes.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Smooth generator endpoint maps for varying polynomial laws

Each scheme is a fixed finite expression in the bracket, generators, and its variable amplitudes. Consequently it remains smooth outside the set of valid group laws, as required for the parameter-preserving submersion theorem.

def OAI.PolycyclicRecognition.polynomialListProduct line 23
theorem OAI.PolycyclicRecognition.exp_polynomialListProduct line 27
theorem OAI.PolycyclicRecognition.contDiff_polynomialWord line 38
theorem OAI.PolycyclicRecognition.contDiff_polynomialListProduct_ofFn line 49
def OAI.PolycyclicRecognition.polynomialEndpointScheme line 64
Source documentation
The expanded conjugate scheme, evaluated as a polynomial in every parameter, whether or not that parameter defines a group law.
```
def polynomialEndpointScheme {c n : ℕ} (a : DynkinCoefficients c 2)
    (w : Fin n → List (I × ℝ)) (i : Fin n → I)
    (p : (V →L[ℝ] V →L[ℝ] V) × (I → V)) (t : Fin n → ℝ) : V :=
…
```
Mentions: OAI.PolycyclicRecognition.DynkinCoefficients
theorem OAI.PolycyclicRecognition.contDiff_polynomialEndpointScheme line 77
Source documentation
Joint smoothness includes the law and generator data, rather than just the inserted amplitudes at one fixed law.
```
theorem contDiff_polynomialEndpointScheme {c n : ℕ} {k : ℕ∞}
    (a : DynkinCoefficients c 2) (w : Fin n → List (I × ℝ)) (i : Fin n → I) :
    ContDiff ℝ k (fun z : ((V →L[ℝ] V →L[ℝ] V) × (I → V)) × (Fin n → ℝ) =>
      polynomialEndpointScheme a w i z.1 z.2) := by
…
```
Mentions: OAI.PolycyclicRecognition.DynkinCoefficients, OAI.PolycyclicRecognition.polynomialEndpointScheme