IndependentPhaseMean.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.independent_phase_primitive_mean_realization line 42

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 independent_phase_primitive_mean_realization (data : MetricGoodPhaseData g F) (A₀ : SmoothingAtlas M)
    (hF : ContMDiff planeModel spaceModel ∞ F) (hmetric : g.inner = inducedTensor F)
    (i : 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)
    {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)
    {Q : Set LowJet} (hQ : IsCompact Q) (hQO : Q ⊆ O)
…

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