Theorems · Theorem · several complex variables

HasFPowerSeriesWithinOnBall.isBigO_image_sub_image_sub_deriv_principal

∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {p : FormalMultilinearSeries 𝕜 E F} {s : Set E} {x : E} {r r' : ENNReal},
  HasFPowerSeriesWithinOnBall f p s x r →
    r' < r →
      (fun y =>
          f y.1 - f y.2 -
            (p 1) fun x => y.1 - y.2) =O[Filter.principal (Metric.eball (x, x) r' ∩ insert x s ×ˢ insert x s)]
        fun y => ‖y - (x, x)‖ * ‖y.1 - y.2‖

If f has formal power series ∑ n, pₙ in a set, within a ball of radius r, then for y, z in any smaller ball, the norm of the difference f y - f z - p 1 (fun _ ↦ y - z) is bounded above by C * (max ‖y - x‖ ‖z - x‖) * ‖y - z‖. This lemma formulates this property using IsBigO and Filter.principal on E × E.

Defined in

Mathlib.Analysis.Analytic.Basic

Cited by

3 results in Mathlib

Foundations

Depth 175 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NontriviallyNormedFieldNormedAddCommGroupNormedSpaceNormedAddCommGroupNormedSpace