PolynomialSlowFamily.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The finite family solving the perturbed mean equation to successively higher amplitude orders. Every member is an actual smooth map.

def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.HasPolynomialSlowFamily line 20
Source documentation
Uniform profiles for the nearby smooth maps at one finite stage.
```
def HasPolynomialSlowFamily {n : A.centers → ℕ}
    (Pol : ∀ i : A.centers, Fin 3 → Fin (n i) → Expression)
    (γ : ∀ x : M, CovariantTwoTensor x) (F : M → Space) (d b : ℝ) : Prop :=
…
```
Mentions: OAI.ClosedSurfaceR4.FiniteOrderSmoothing.CovariantTwoTensor, OAI.ClosedSurfaceR4.Space
lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.polynomial_slow_seed line 33

theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.MetricGoodPhaseData.polynomial_finite_slow_family line 70

Source documentation

The number of stages and the loss determine the slow scales before any accuracy order. This finite induction uses only constructed increments.

theorem polynomial_finite_slow_family (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)
    (steps : ℕ) (hsteps : 1 ≤ steps) (σmax : ℝ) (hσmax : 0 < σmax) :
    ∃ σ : ℝ, 0 < σ ∧ σ < 1/16 ∧ σ < σmax ∧ ∀ j : ℕ, j ≤ steps →
      data.A.HasPolynomialSlowFamily Pol g.inner F (amplitudeExponent j) (scaleExponent σ steps j) := by
…

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