MetricPolynomialSlowStep.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

One uniform step of the finite slow-map construction. The derivative profiles and the small parameter threshold precede the nearby map.

theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.MetricGoodPhaseData.polynomial_slow_step line 32

Source documentation

An actual primitive update improves the amplitude exponent and retains uniform all-order profiles. The fixed loss is chosen before every scale.

theorem polynomial_slow_step (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) :
    ∃ loss : ℕ, ∀ (b b' d d' a u : ℝ), 0 ≤ b → b < b' → b'*(loss : ℝ) < 1 →
      2*b' < d → d < d' → 2*d' < 3*d-b' → 0 < a → 0 < u →
    ∀ (P D : ℕ → ℝ) (L : ℝ), (∀ m, 0 ≤ P m) → (∀ m, 0 ≤ D m) → 0 ≤ L →
      (∀ m, data.A.ShiftedBound 2 m 1 (P m) F) →
    ∃ (a' η L' : ℝ) (P' D' : ℕ → ℝ), 0 < a' ∧ 0 < η ∧ η ≤ 1 ∧ 0 ≤ L' ∧
      (∀ m, 0 ≤ P' m) ∧ (∀ m, 0 ≤ D' m) ∧
    ∀ z : ℝ, 0 < z → z < η → ∀ G : M → Space,
…

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