OAI/Geometry/SurfaceImmersion/Correction/JetPolynomialDerivative.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

Differentiation preserves finite polynomial dependence on higher jets. The proof is for actual derivatives, including the low-jet chain rule.

  1. def OAI.ClosedSurfaceR4.JetPolynomial.Expression.sumList line 15
  2. lemma OAI.ClosedSurfaceR4.JetPolynomial.Expression.eval_sumList line 19
  3. lemma OAI.ClosedSurfaceR4.JetPolynomial.Expression.order_sumList_le line 25
  4. lemma OAI.ClosedSurfaceR4.JetPolynomial.Expression.loss_sumList_le line 33
  5. lemma OAI.ClosedSurfaceR4.JetPolynomial.Expression.smoothCoeffs_sumList line 41
  6. def OAI.ClosedSurfaceR4.JetPolynomial.Expression.lowFactor line 48
  7. lemma OAI.ClosedSurfaceR4.JetPolynomial.Expression.eval_lowFactor line 52
  8. lemma OAI.ClosedSurfaceR4.JetPolynomial.Expression.order_lowFactor line 58
  9. lemma OAI.ClosedSurfaceR4.JetPolynomial.Expression.loss_lowFactor line 67
  10. lemma OAI.ClosedSurfaceR4.JetPolynomial.Expression.smoothCoeffs_lowFactor line 76
  11. def OAI.ClosedSurfaceR4.JetPolynomial.Expression.slow line 84

    Source documentation

    The chain rule differentiates smooth low-jet coefficients and introduces one additional actual jet factor.

    def slow (v : Fin 2) : Expression → Expression
  | .coeff c => sumList Finset.univ.toList (fun i : LowIndex =>
      (lowFactor v i).mul (.coeff (slowDerivative c (lowBasis i))))
  | .atom w a e => .add (.atom (v :: w) a e) (.atom w a (slow v e))
  | .add e f => .add (slow v e) (slow v f)

    Mentions: OAI.ClosedSurfaceR4.JetPolynomial.Expression, OAI.ClosedSurfaceR4.JetPolynomial.Expression.sumList, OAI.ClosedSurfaceR4.JetPolynomial.LowIndex, OAI.ClosedSurfaceR4.JetPolynomial.Expression.lowFactor, OAI.ClosedSurfaceR4.JetPolynomial.Expression.mul, OAI.ClosedSurfaceR4.JetPolynomial.lowBasis

  12. lemma OAI.ClosedSurfaceR4.JetPolynomial.Expression.smoothCoeffs_slow line 90
  13. lemma OAI.ClosedSurfaceR4.JetPolynomial.Expression.order_slow_le line 101
  14. lemma OAI.ClosedSurfaceR4.JetPolynomial.Expression.loss_slow_le line 111
  15. lemma OAI.ClosedSurfaceR4.JetPolynomial.Expression.coefficient_chain_rule_joint line 120
  16. theorem OAI.ClosedSurfaceR4.JetPolynomial.Expression.eval_slow line 134

    Source documentation

    The syntactic derivative evaluates to the genuine derivative on every open region where the low-jet coefficients are smooth.

    theorem eval_slow {O : Set LowJet} {S : Set Base} (hO : IsOpen O) (hS : IsOpen S)
    {G : Base → Space} (hG : ContDiff ℝ ∞ G) (hQ : Set.MapsTo (lowJet G) S O)
    (v : Fin 2) {e : Expression} (he : e.SmoothCoeffs O) {p : Base} (hp : p ∈ S) (t : ℝ) :
    (e.slow v).eval G (p, t) = fderiv ℝ (fun q => e.eval G (q, t)) p (coordinateVector v) := by
…

    Mentions: OAI.ClosedSurfaceR4.JetPolynomial.LowJet, OAI.ClosedSurfaceR4.JetPolynomial.Base, OAI.ClosedSurfaceR4.JetPolynomial.Space, OAI.ClosedSurfaceR4.JetPolynomial.lowJet, OAI.ClosedSurfaceR4.JetPolynomial.Expression, OAI.ClosedSurfaceR4.JetPolynomial.Expression.eval, OAI.ClosedSurfaceR4.JetPolynomial.coordinateVector