OAI/Geometry/SurfaceImmersion/Correction/JetPolynomialAlgebra.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

Finite polynomials in actual coordinate jets, with coefficients smooth in position, the second jet, and the periodic variable.

  1. inductive OAI.ClosedSurfaceR4.JetPolynomial.Expression line 14

    Source documentation

    A sum of monomials. Jet factors are independent of the angular variable.

    inductive Expression where
…
  2. def OAI.ClosedSurfaceR4.JetPolynomial.Expression.eval line 21
  3. def OAI.ClosedSurfaceR4.JetPolynomial.Expression.mapCoeff line 26
  4. def OAI.ClosedSurfaceR4.JetPolynomial.Expression.mul line 31
  5. def OAI.ClosedSurfaceR4.JetPolynomial.Expression.order line 37

    Source documentation

    Largest order of a jet factor. Coefficients themselves use jets through order two.

    def order : Expression → ℕ
  | .coeff _ => 2
  | .atom w _ e => max w.length e.order
  | .add e f => max e.order f.order

/-- Scale loss when the second jet is controlled. -/

    Mentions: OAI.ClosedSurfaceR4.JetPolynomial.Expression, OAI.ClosedSurfaceR4.JetPolynomial.Expression.loss, OAI.ClosedSurfaceR4.JetPolynomial.jet

  6. def OAI.ClosedSurfaceR4.JetPolynomial.Expression.loss line 43

    Source documentation

    Scale loss when the second jet is controlled.

    def loss : Expression → ℕ
  | .coeff _ => 0
  | .atom w _ e => (w.length - 2) + e.loss
  | .add e f => max e.loss f.loss

    Mentions: OAI.ClosedSurfaceR4.JetPolynomial.Expression

  7. def OAI.ClosedSurfaceR4.JetPolynomial.Expression.SmoothCoeffs line 48
  8. lemma OAI.ClosedSurfaceR4.JetPolynomial.Expression.eval_mapCoeff_mul line 53
  9. lemma OAI.ClosedSurfaceR4.JetPolynomial.Expression.eval_mul line 61
  10. lemma OAI.ClosedSurfaceR4.JetPolynomial.Expression.order_mapCoeff line 68
  11. lemma OAI.ClosedSurfaceR4.JetPolynomial.Expression.loss_mapCoeff line 74
  12. lemma OAI.ClosedSurfaceR4.JetPolynomial.Expression.order_mul_le line 80
  13. lemma OAI.ClosedSurfaceR4.JetPolynomial.Expression.loss_mul_le line 86
  14. lemma OAI.ClosedSurfaceR4.JetPolynomial.Expression.smoothCoeffs_map line 92
  15. lemma OAI.ClosedSurfaceR4.JetPolynomial.Expression.smoothCoeffs_mul line 100
  16. lemma OAI.ClosedSurfaceR4.JetPolynomial.Expression.eval_smooth line 107