GoodPhaseSolver.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Actual unit-scale linear metric solvers on the constructed good phase charts.

theorem OAI.ClosedSurfaceR4.PhaseGeometry.GoodPhaseChart.exists_unperturbed_solver line 15

Source documentation

Every compact target supported in a constructed good chart has the actual unperturbed solver data required by the finite cancellation theorem.

theorem GoodPhaseChart.exists_unperturbed_solver
    {G : JetPolynomial.Base → JetPolynomial.Space} (hG : ContDiff ℝ ∞ G)
    {φ : JetPolynomial.Base → ℝ} (hφ : ContDiff ℝ ∞ φ)
    (c : GoodPhaseChart (G ∘ planeCoordinateIsometry.symm) (coordinatePhase φ))
    (K : Compacts JetPolynomial.Base)
    (hK : (modeSupport K : Set SmallModes.Base) ⊆ c.chart.source) :
    ∃ d : PolynomialSolveData emptyMetricPolynomial 0 G hG φ K 1 1,
      d.e = c.chart ∧ (∀ m, d.D m = 0) :=
…

Mentions: OAI.ClosedSurfaceR4.JetPolynomial.Base, OAI.ClosedSurfaceR4.JetPolynomial.Space, OAI.ClosedSurfaceR4.PhaseGeometry.GoodPhaseChart, OAI.ClosedSurfaceR4.SmallModes.Base