MetricPolynomialIncrement.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

An actual metric-adapted immersion supplies all the small-increment geometry.

theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.MetricGoodPhaseData.polynomial_small_increment line 29

Source documentation

All geometric and mean-solver inputs are constructed from the metric and immersion. Only the nearby map's explicit analytic bounds remain.

theorem polynomial_small_increment (d : MetricGoodPhaseData g F)
    {n : d.A.centers → ℕ}
    (Pol : ∀ i : d.A.centers, Fin 3 → Fin (n i) → Expression)
    (hPol : ∀ i k l, (Pol i k l).SmoothCoeffs univ)
    (hF : ContMDiff planeModel spaceModel ∞ F) :
    ∃ loss : ℕ, ∀ (P : ℕ → ℝ), (∀ m, 0 ≤ P m) →
    (∀ m, d.A.ShiftedBound 2 m 1 (P m) F) → ∀ q : ℕ,
    ∃ r : ℝ, 0 < r ∧ ∀ C : ℕ → ℝ, (∀ m, 1 ≤ C m) →
      ∃ (ρ₀ η₀ : ℝ) (B T : ℕ → ℝ), 0 < ρ₀ ∧ 0 < η₀ ∧ η₀ ≤ 1 ∧
        (∀ m, 0 ≤ B m) ∧ (∀ m, 0 ≤ T m) ∧
      ∀ (G : M → Space), ContMDiff planeModel spaceModel ∞ G → ∀ b : ℝ,
        0 ≤ b → b < ρ₀ → d.A.WeightedBound 1 2 b (G-F) →
…

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