OAI/Geometry/SurfaceImmersion/Correction/JetPolynomialFullCorrector.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ClosedSurfaceR4.JetPolynomial.spanCoefficient line 17
2. def OAI.ClosedSurfaceR4.JetPolynomial.metricCoefficient line 20
3. def OAI.ClosedSurfaceR4.JetPolynomial.Expression.spanTerm line 26
4. def OAI.ClosedSurfaceR4.JetPolynomial.Expression.angularSource line 30
5. def OAI.ClosedSurfaceR4.JetPolynomial.Expression.fullComponent line 35
6. lemma OAI.ClosedSurfaceR4.JetPolynomial.Expression.smoothCoeffs_spanTerm line 42
7. lemma OAI.ClosedSurfaceR4.JetPolynomial.Expression.smoothCoeffs_angularSource line 53
8. lemma OAI.ClosedSurfaceR4.JetPolynomial.Expression.smoothCoeffs_fullComponent line 67
9. lemma OAI.ClosedSurfaceR4.JetPolynomial.Expression.order_spanTerm_le line 84
10. lemma OAI.ClosedSurfaceR4.JetPolynomial.Expression.loss_spanTerm_le line 90
11. lemma OAI.ClosedSurfaceR4.JetPolynomial.Expression.order_angularSource_le line 96
12. lemma OAI.ClosedSurfaceR4.JetPolynomial.Expression.loss_angularSource_le line 106
13. theorem OAI.ClosedSurfaceR4.JetPolynomial.Expression.fullComponent_bounds line 117

    Source documentation

    One full periodic solve raises the jet order and scale loss by at most one.

    theorem fullComponent_bounds (Y C X₀ : LowJet → E) (V : LowJet → C(Period, E))
        (q : LowJet → ℝ) (L : E →L[ℝ] ℝ) (v : Fin 2) (h j e : Expression)
        (N R : ℕ) (hN : 2 ≤ N) (hh : h.order ≤ N) (hj : j.order ≤ N) (he : e.order ≤ N)
        (lh : h.loss ≤ R) (lj : j.loss ≤ R) (le : e.loss ≤ R) :
        (fullComponent Y C X₀ V q L v h j e).order ≤ N + 1 ∧
          (fullComponent Y C X₀ V q L v h j e).loss ≤ R + 1 := by
    …

    Mentions: OAI.ClosedSurfaceR4.JetPolynomial.LowJet, OAI.ClosedSurfaceR4.JetPolynomial.Expression, OAI.ClosedSurfaceR4.JetPolynomial.Expression.fullComponent, OAI.ClosedSurfaceR4.JetPolynomial.Expression.order, OAI.ClosedSurfaceR4.JetPolynomial.Expression.loss