Theorems · Theorem · several complex variables

HasFPowerSeriesWithinOnBall.image_sub_sub_deriv_le

∀ {𝕜 : 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 →
      ∃ C,
        ∀ y ∈ insert x s ∩ Metric.eball x r',
          ∀ z ∈ insert x s ∩ Metric.eball x r', ‖f y - f z - (p 1) fun x => y - z‖ ≤ C * max ‖y - x‖ ‖z - x‖ * ‖y - z‖

If f has formal power series ∑ n, pₙ within a set, on 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‖.

Defined in

Mathlib.Analysis.Analytic.Basic

Cited by

1 results in Mathlib

Foundations

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

Assumes

NontriviallyNormedFieldNormedAddCommGroupNormedSpaceNormedAddCommGroupNormedSpace