OAI/Geometry/SurfaceImmersion/Correction/PolynomialBudgetAlgebra.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Finite composition and inverse-scale evaluation of the polynomial budgets in the correction construction.

  1. lemma OAI.ClosedSurfaceR4.RealModes.HasPolynomialBound.of_le line 10
  2. lemma OAI.ClosedSurfaceR4.RealModes.HasPolynomialBound.max line 16
  3. lemma OAI.ClosedSurfaceR4.RealModes.HasPolynomialBound.sum line 27
  4. lemma OAI.ClosedSurfaceR4.RealModes.HasPolynomialBound.comp line 38
  5. theorem OAI.ClosedSurfaceR4.RealModes.HasPolynomialBound.at_inverse_scale line 53

    Source documentation

    Polynomial degree is chosen before all multiplicative constants.

    theorem HasPolynomialBound.at_inverse_scale {f : ℝ → ℝ} (hf : HasPolynomialBound f)
    (p : ℕ) : ∃ d : ℕ, ∀ D : ℝ, 1 ≤ D → ∃ C : ℝ, 1 ≤ C ∧
      ∀ z : ℝ, 0 < z → z ≤ 1 → 0 ≤ f (D/z^p) ∧ f (D/z^p) ≤ C/z^d := by
…

    Mentions: OAI.ClosedSurfaceR4.RealModes.HasPolynomialBound