MixedJetPolynomial.lean`

13 declarations, 0 contain sorry, 0 declared as axioms

Polynomials in the base-map jet and three independent variation jets. Differentiating the base map increases the scale loss by at most two.

inductive OAI.ClosedSurfaceR4.JetPolynomial.MixedExpression line 12
def OAI.ClosedSurfaceR4.JetPolynomial.MixedExpression.eval line 19
def OAI.ClosedSurfaceR4.JetPolynomial.MixedExpression.loss line 24
def OAI.ClosedSurfaceR4.JetPolynomial.MixedExpression.SmoothCoeffs line 29
def OAI.ClosedSurfaceR4.JetPolynomial.MixedExpression.ofExpression line 34
lemma OAI.ClosedSurfaceR4.JetPolynomial.MixedExpression.ofExpression_eval line 39
lemma OAI.ClosedSurfaceR4.JetPolynomial.MixedExpression.ofExpression_loss line 46
def OAI.ClosedSurfaceR4.JetPolynomial.MixedExpression.sumList line 52
lemma OAI.ClosedSurfaceR4.JetPolynomial.MixedExpression.loss_sumList_le line 56
def OAI.ClosedSurfaceR4.JetPolynomial.MixedExpression.coefficientDerivative line 64
def OAI.ClosedSurfaceR4.JetPolynomial.MixedExpression.differentiate line 69
Source documentation
Only the base-map slot is differentiated. The new direction is one of the three variation slots, so a third variation uses no extra map slots.
```
def differentiate (j : Fin 3) : MixedExpression → MixedExpression
  | .coeff c => sumList Finset.univ.toList (fun i : Fin 7 × Fin 4 =>
      .atom j.succ (lowWord i.1) i.2 (.coeff (coefficientDerivative c i)))
  | .atom i w a e => if i = 0 then
      .add (.atom j.succ w a e) (.atom i w a (differentiate j e))
    else .atom i w a (differentiate j e)
  | .add e f => .add (differentiate j e) (differentiate j f)
```
Mentions: OAI.ClosedSurfaceR4.JetPolynomial.MixedExpression, OAI.ClosedSurfaceR4.JetPolynomial.MixedExpression.sumList, OAI.ClosedSurfaceR4.JetPolynomial.lowWord, OAI.ClosedSurfaceR4.JetPolynomial.MixedExpression.coefficientDerivative
theorem OAI.ClosedSurfaceR4.JetPolynomial.MixedExpression.loss_differentiate line 77
theorem OAI.ClosedSurfaceR4.JetPolynomial.MixedExpression.loss_third_variation line 98