UniformPhasePrimitive.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Construct the actual globally supported primitive from the finite recursion and its extended polynomial mean operator.

theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.MetricGoodPhaseData.uniform_phase_primitive_realization line 45

Source documentation

Arbitrary finite metric accuracy for the actual supported primitive in a fixed nonlinear phase chart, using only the proved polynomial mean iteration.

theorem uniform_phase_primitive_realization (data : MetricGoodPhaseData g F)
    (hF : ContMDiff planeModel spaceModel ∞ F) (hmetric : g.inner = inducedTensor F)
    (i : data.A.centers)
    (e : OpenPartialHomeomorph JetPolynomial.Base JetPolynomial.Base)
    (he : ContDiff ℝ ∞ e) (hi : ContDiff ℝ ∞ e.symm)
    {χ : JetPolynomial.Base → ℝ} (hχ : ContDiff ℝ ∞ χ)
    (hχc : HasCompactSupport χ) (hχs : tsupport χ ⊆ e.source)
    (hcover : (data.A.chartWeightCompact i : Set JetPolynomial.Base) ⊆ e.source)
    {O : TopologicalSpace.Opens LowJet} (l : SurfaceVelocityFamily.Loop O)
    {a : JetPolynomial.Base → ℝ} (ha : ContDiff ℝ ∞ a) (hamp : l.HasSpatialAmplitude a)
    (S : TopologicalSpace.Opens JetPolynomial.Base)
    (hSc : IsCompact (closure (S : Set JetPolynomial.Base))) (hTS : MapsTo e e.source S)
…

Mentions: OAI.ClosedSurfaceR4.FiniteOrderSmoothing.MetricGoodPhaseData, OAI.ClosedSurfaceR4.planeModel, OAI.ClosedSurfaceR4.FiniteOrderSmoothing.inducedTensor, OAI.ClosedSurfaceR4.JetPolynomial.Base, OAI.ClosedSurfaceR4.SurfaceVelocityFamily.Loop