PolynomialChartedMetricMean.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Polynomial bounds for the actual charted metric mean, with no polynomial differential perturbation.

lemma OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.ChartedMeanData.mean_unperturbed line 22

theorem OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.polynomial_charted_metric_mean line 41

Source documentation

The exponent and coefficient are uniform over the actual solver data; only its explicitly supplied geometric profile varies.

theorem polynomial_charted_metric_mean (q : ℕ) :
    ∃ (p : ℕ → ℕ) (C : ℕ → ℝ), (∀ m, 1 ≤ C m) ∧
    ∀ {n : ℕ} {P : Fin 3 → Fin n → Expression} {τ : ℝ}
      {G : Base → Space} {hG : ContDiff ℝ ∞ G} {φ : Base → ℝ}
      {K : Compacts Base} {s : ℝ≥0} (c : PolynomialSolveData P 0 G hG φ K τ s)
      {r ρ R : ℝ} {reference : SmallModes.Base → Tensor}
      (d : ChartedMeanData c r ρ R reference),
      ∀ hρ : 0 < ρ, 0 < τ → 0 < (s : ℝ) → τ ≤ s → s ≤ 1 →
      ∀ J : ℕ → ℝ, (∀ m, 1 ≤ J m) →
      (∀ m, ρ⁻¹ ≤ J m ∧ d.budgets.inv (m+q+2) ≤ J m ∧
        d.budgets.forms (m+q+2) ≤ J m ∧ d.budgets.psi (m+q+2) ≤ J m ∧
        d.budgets.mode (m+q+2) ≤ J m ∧ d.budgets.normal (m+q+2) ≤ J m ∧
…

Mentions: OAI.ClosedSurfaceR4.JetPolynomial.Expression, OAI.ClosedSurfaceR4.JetPolynomial.Base, OAI.ClosedSurfaceR4.JetPolynomial.Space, OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.PolynomialSolveData, OAI.ClosedSurfaceR4.SmallModes.Base, OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.ChartedMeanData