PolynomialMeanApproximation.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The finite slow iteration solves the actual restored polynomial mean metric to any prescribed finite unweighted order.

lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.tensorWeightedBound_unscaled line 28
lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.polynomial_metric_error_of_defect line 36

theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.MetricGoodPhaseData.polynomial_mean_approximation line 67

Source documentation

Finite-order approximation of the actual polynomial mean, with all slow-map derivative profiles and a vanishing C3 displacement.

theorem polynomial_mean_approximation (data : MetricGoodPhaseData g F)
    {n : data.A.centers → ℕ}
    (Pol : ∀ i : data.A.centers, Fin 3 → Fin (n i) → Expression)
    (hPol : ∀ i k l, (Pol i k l).SmoothCoeffs univ)
    (hF : ContMDiff planeModel spaceModel ∞ F) (hmetric : g.inner = inducedTensor F)
    (R N : ℕ) (σmax : ℝ) (hσmax : 0 < σmax) :
    ∃ (b u η L C : ℝ) (P : ℕ → ℝ), 0 ≤ b ∧ b < 1/16 ∧ b < σmax ∧ 0 < u ∧
      0 < η ∧ η ≤ 1 ∧ 0 ≤ L ∧ 0 ≤ C ∧ (∀ m, 0 ≤ P m) ∧
    ∀ z : ℝ, 0 < z → z < η → ∃ G : M → Space,
      ContMDiff planeModel spaceModel ∞ G ∧
      data.A.WeightedBound 1 3 (L*z^u) (G-F) ∧
      (∀ m, data.A.ShiftedBound 2 m (z^b) (P m) G) ∧
…

Mentions: OAI.ClosedSurfaceR4.FiniteOrderSmoothing.MetricGoodPhaseData, OAI.ClosedSurfaceR4.planeModel, OAI.ClosedSurfaceR4.FiniteOrderSmoothing.inducedTensor, OAI.ClosedSurfaceR4.Space