PolynomialFiniteMeanFamily.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Finite local mean families retain polynomial majorants even when the number of summands grows. The degree depends on the local estimate, not on the number of charts.

lemma OAI.ClosedSurfaceR4.FiniteMean.MeanBounds.mono_majorants line 17
lemma OAI.ClosedSurfaceR4.PhaseMean.polynomialMeanProfile_sum_bound line 40

theorem OAI.ClosedSurfaceR4.PhaseMean.polynomial_finite_mean_family line 63

Source documentation

A growing finite number of local terms costs one additional polynomial power when its cardinality is included in the geometric profile.

theorem polynomial_finite_mean_family {ι : Type*} {U : Set E}
    (hU : UniqueDiffOn ℝ U) {s : ℝ} (hs : 0 ≤ s)
    {reference : E → F} {r : ℝ} {L : ℕ} (a : Finset ι)
    (T : ι → ℝ → (E → F) → E → F) (p : ℕ → ℕ) (C G : ℕ → ℝ)
    (hC : ∀ m, 0 ≤ C m) (hG : ∀ m, 1 ≤ G m)
    (ha : ∀ m, (a.card : ℝ) ≤ G m)
    (hT : ∀ i ∈ a, MeanBounds U s reference r L (T i)
      (polynomialMeanProfile p C G) (polynomialMeanProfile p C G)) :
    MeanBounds U s reference r L (fun η f x => ∑ i ∈ a, T i η f x)
      (polynomialMeanProfile (fun m => p m+1) (fun m => 1+C m) G)
      (polynomialMeanProfile (fun m => p m+1) (fun m => 1+C m) G) := by
…

Mentions: OAI.ClosedSurfaceR4.PhaseMean.polynomialMeanProfile