OAI/Geometry/SurfaceImmersion/Correction/PolynomialMeanIteration.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Polynomial growth of the actual finite mean iteration and of the finite value budget appearing in its explicit smallness threshold.

  1. lemma OAI.ClosedSurfaceR4.RealModes.HasPolynomialBound.nonneg line 11
  2. theorem OAI.ClosedSurfaceR4.PhaseMean.polynomialMeanProfile_growth line 21
  3. def OAI.ClosedSurfaceR4.PhaseMean.polynomialMeanSize line 28
  4. def OAI.ClosedSurfaceR4.PhaseMean.polynomialMeanDifference line 32
  5. theorem OAI.ClosedSurfaceR4.PhaseMean.polynomialMeanSize_growth line 37
  6. theorem OAI.ClosedSurfaceR4.PhaseMean.polynomialMeanDifference_growth line 46
  7. theorem OAI.ClosedSurfaceR4.PhaseMean.polynomialMean_threshold_budget line 59

    Source documentation

    A polynomial upper bound for the finite quantity controlling the radius of the mean iteration; it is uniform in the iteration index.

    theorem polynomialMean_threshold_budget (L : ℕ) (p : ℕ → ℕ) (C : ℕ → ℝ)
    (G H : ℕ → ℝ → ℝ) (hC : ∀ m, 0 ≤ C m)
    (hG : ∀ m, HasPolynomialBound (G m)) (hH : ∀ m, HasPolynomialBound (H m)) (n : ℕ) :
    ∃ d : ℕ, ∃ A : ℝ, 1 ≤ A ∧ ∀ x : ℝ, 1 ≤ x → ∀ j ≤ n,
      polynomialMeanProfile p C (fun r => G r x) 0 (polynomialMeanSize L p C G H j L x) ≤ A*x^d := by
…

    Mentions: OAI.ClosedSurfaceR4.PhaseMean.polynomialMeanProfile, OAI.ClosedSurfaceR4.PhaseMean.polynomialMeanSize