Documentation

Mathlib.Analysis.Analytic.Basic

Analytic functions #

A function is analytic in one dimension around 0 if it can be written as a converging power series Σ pₙ zⁿ. This definition can be extended to any dimension (even in infinite dimension) by requiring that pₙ is a continuous n-multilinear map. In general, pₙ is not unique (in two dimensions, taking p₂ (x, y) (x', y') = x y' or y x' gives the same map when applied to a vector (x, y) (x, y)). A way to guarantee uniqueness is to take a symmetric pₙ, but this is not always possible in nonzero characteristic (in characteristic 2, the previous example has no symmetric representative). Therefore, we do not insist on symmetry or uniqueness in the definition, and we only require the existence of a converging series.

The general framework is important to say that the exponential map on bounded operators on a Banach space is analytic, as well as the inverse on invertible operators.

Main definitions #

Let p be a formal multilinear series from E to F, i.e., p n is a multilinear map on E^n for n : ℕ.

Additionally, let f be a function from E to F.

We also define versions of HasFPowerSeriesOnBall, AnalyticAt, and AnalyticOnNhd restricted to a set, similar to ContinuousWithinAt. See Mathlib.Analysis.Analytic.Within for basic properties.

We develop the basic properties of these notions, notably:

Implementation details #

We only introduce the radius of convergence of a power series, as p.radius. For a power series in finitely many dimensions, there is a finer (directional, coordinate-dependent) notion, describing the polydisk of convergence. This notion is more specific, and not necessary to build the general theory. We do not define it here.

def FormalMultilinearSeries.sum {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [Ring 𝕜] [AddCommGroup E] [AddCommGroup F] [Module 𝕜 E] [Module 𝕜 F] [TopologicalSpace E] [TopologicalSpace F] [TopologicalAddGroup E] [TopologicalAddGroup F] [ContinuousConstSMul 𝕜 E] [ContinuousConstSMul 𝕜 F] (p : FormalMultilinearSeries 𝕜 E F) (x : E) :
F

Given a formal multilinear series p and a vector x, then p.sum x is the sum Σ pₙ xⁿ. A priori, it only behaves well when ‖x‖ < p.radius.

Equations
  • p.sum x = ∑' (n : ), (p n) fun (x_1 : Fin n) => x
Instances For
    def FormalMultilinearSeries.partialSum {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [Ring 𝕜] [AddCommGroup E] [AddCommGroup F] [Module 𝕜 E] [Module 𝕜 F] [TopologicalSpace E] [TopologicalSpace F] [TopologicalAddGroup E] [TopologicalAddGroup F] [ContinuousConstSMul 𝕜 E] [ContinuousConstSMul 𝕜 F] (p : FormalMultilinearSeries 𝕜 E F) (n : ) (x : E) :
    F

    Given a formal multilinear series p and a vector x, then p.partialSum n x is the sum Σ pₖ xᵏ for k ∈ {0,..., n-1}.

    Equations
    Instances For
      theorem FormalMultilinearSeries.partialSum_continuous {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [Ring 𝕜] [AddCommGroup E] [AddCommGroup F] [Module 𝕜 E] [Module 𝕜 F] [TopologicalSpace E] [TopologicalSpace F] [TopologicalAddGroup E] [TopologicalAddGroup F] [ContinuousConstSMul 𝕜 E] [ContinuousConstSMul 𝕜 F] (p : FormalMultilinearSeries 𝕜 E F) (n : ) :
      Continuous (p.partialSum n)

      The partial sums of a formal multilinear series are continuous.

      The radius of a formal multilinear series #

      The radius of a formal multilinear series is the largest r such that the sum Σ ‖pₙ‖ ‖y‖ⁿ converges for all ‖y‖ < r. This implies that Σ pₙ yⁿ converges for all ‖y‖ < r, but these definitions are not equivalent in general.

      Equations
      Instances For
        theorem FormalMultilinearSeries.le_radius_of_bound {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (p : FormalMultilinearSeries 𝕜 E F) (C : ) {r : NNReal} (h : ∀ (n : ), p n * r ^ n C) :
        r p.radius

        If ‖pₙ‖ rⁿ is bounded in n, then the radius of p is at least r.

        theorem FormalMultilinearSeries.le_radius_of_bound_nnreal {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (p : FormalMultilinearSeries 𝕜 E F) (C : NNReal) {r : NNReal} (h : ∀ (n : ), p n‖₊ * r ^ n C) :
        r p.radius

        If ‖pₙ‖ rⁿ is bounded in n, then the radius of p is at least r.

        theorem FormalMultilinearSeries.le_radius_of_isBigO {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (p : FormalMultilinearSeries 𝕜 E F) {r : NNReal} (h : (fun (n : ) => p n * r ^ n) =O[Filter.atTop] fun (x : ) => 1) :
        r p.radius

        If ‖pₙ‖ rⁿ = O(1), as n → ∞, then the radius of p is at least r.

        theorem FormalMultilinearSeries.le_radius_of_eventually_le {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (p : FormalMultilinearSeries 𝕜 E F) {r : NNReal} (C : ) (h : ∀ᶠ (n : ) in Filter.atTop, p n * r ^ n C) :
        r p.radius
        theorem FormalMultilinearSeries.le_radius_of_summable_nnnorm {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (p : FormalMultilinearSeries 𝕜 E F) {r : NNReal} (h : Summable fun (n : ) => p n‖₊ * r ^ n) :
        r p.radius
        theorem FormalMultilinearSeries.le_radius_of_summable {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (p : FormalMultilinearSeries 𝕜 E F) {r : NNReal} (h : Summable fun (n : ) => p n * r ^ n) :
        r p.radius
        theorem FormalMultilinearSeries.radius_eq_top_of_forall_nnreal_isBigO {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (p : FormalMultilinearSeries 𝕜 E F) (h : ∀ (r : NNReal), (fun (n : ) => p n * r ^ n) =O[Filter.atTop] fun (x : ) => 1) :
        p.radius =
        theorem FormalMultilinearSeries.radius_eq_top_of_eventually_eq_zero {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (p : FormalMultilinearSeries 𝕜 E F) (h : ∀ᶠ (n : ) in Filter.atTop, p n = 0) :
        p.radius =
        theorem FormalMultilinearSeries.radius_eq_top_of_forall_image_add_eq_zero {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (p : FormalMultilinearSeries 𝕜 E F) (n : ) (hn : ∀ (m : ), p (m + n) = 0) :
        p.radius =
        @[simp]

        0 has infinite radius of convergence

        theorem FormalMultilinearSeries.isLittleO_of_lt_radius {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (p : FormalMultilinearSeries 𝕜 E F) {r : NNReal} (h : r < p.radius) :
        aSet.Ioo 0 1, (fun (n : ) => p n * r ^ n) =o[Filter.atTop] fun (x : ) => a ^ x

        For r strictly smaller than the radius of p, then ‖pₙ‖ rⁿ tends to zero exponentially: for some 0 < a < 1, ‖p n‖ rⁿ = o(aⁿ).

        theorem FormalMultilinearSeries.isLittleO_one_of_lt_radius {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (p : FormalMultilinearSeries 𝕜 E F) {r : NNReal} (h : r < p.radius) :
        (fun (n : ) => p n * r ^ n) =o[Filter.atTop] fun (x : ) => 1

        For r strictly smaller than the radius of p, then ‖pₙ‖ rⁿ = o(1).

        theorem FormalMultilinearSeries.norm_mul_pow_le_mul_pow_of_lt_radius {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (p : FormalMultilinearSeries 𝕜 E F) {r : NNReal} (h : r < p.radius) :
        aSet.Ioo 0 1, C > 0, ∀ (n : ), p n * r ^ n C * a ^ n

        For r strictly smaller than the radius of p, then ‖pₙ‖ rⁿ tends to zero exponentially: for some 0 < a < 1 and C > 0, ‖p n‖ * r ^ n ≤ C * a ^ n.

        theorem FormalMultilinearSeries.lt_radius_of_isBigO {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (p : FormalMultilinearSeries 𝕜 E F) {r : NNReal} (h₀ : r 0) {a : } (ha : a Set.Ioo (-1) 1) (hp : (fun (n : ) => p n * r ^ n) =O[Filter.atTop] fun (x : ) => a ^ x) :
        r < p.radius

        If r ≠ 0 and ‖pₙ‖ rⁿ = O(aⁿ) for some -1 < a < 1, then r < p.radius.

        theorem FormalMultilinearSeries.norm_mul_pow_le_of_lt_radius {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (p : FormalMultilinearSeries 𝕜 E F) {r : NNReal} (h : r < p.radius) :
        C > 0, ∀ (n : ), p n * r ^ n C

        For r strictly smaller than the radius of p, then ‖pₙ‖ rⁿ is bounded.

        theorem FormalMultilinearSeries.norm_le_div_pow_of_pos_of_lt_radius {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (p : FormalMultilinearSeries 𝕜 E F) {r : NNReal} (h0 : 0 < r) (h : r < p.radius) :
        C > 0, ∀ (n : ), p n C / r ^ n

        For r strictly smaller than the radius of p, then ‖pₙ‖ rⁿ is bounded.

        theorem FormalMultilinearSeries.nnnorm_mul_pow_le_of_lt_radius {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (p : FormalMultilinearSeries 𝕜 E F) {r : NNReal} (h : r < p.radius) :
        C > 0, ∀ (n : ), p n‖₊ * r ^ n C

        For r strictly smaller than the radius of p, then ‖pₙ‖ rⁿ is bounded.

        theorem FormalMultilinearSeries.le_radius_of_tendsto {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {r : NNReal} (p : FormalMultilinearSeries 𝕜 E F) {l : } (h : Filter.Tendsto (fun (n : ) => p n * r ^ n) Filter.atTop (nhds l)) :
        r p.radius
        theorem FormalMultilinearSeries.le_radius_of_summable_norm {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {r : NNReal} (p : FormalMultilinearSeries 𝕜 E F) (hs : Summable fun (n : ) => p n * r ^ n) :
        r p.radius
        theorem FormalMultilinearSeries.not_summable_norm_of_radius_lt_nnnorm {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (p : FormalMultilinearSeries 𝕜 E F) {x : E} (h : p.radius < x‖₊) :
        ¬Summable fun (n : ) => p n * x ^ n
        theorem FormalMultilinearSeries.summable_norm_mul_pow {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (p : FormalMultilinearSeries 𝕜 E F) {r : NNReal} (h : r < p.radius) :
        Summable fun (n : ) => p n * r ^ n
        theorem FormalMultilinearSeries.summable_norm_apply {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (p : FormalMultilinearSeries 𝕜 E F) {x : E} (hx : x EMetric.ball 0 p.radius) :
        Summable fun (n : ) => (p n) fun (x_1 : Fin n) => x
        theorem FormalMultilinearSeries.summable_nnnorm_mul_pow {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (p : FormalMultilinearSeries 𝕜 E F) {r : NNReal} (h : r < p.radius) :
        Summable fun (n : ) => p n‖₊ * r ^ n
        theorem FormalMultilinearSeries.summable {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace F] (p : FormalMultilinearSeries 𝕜 E F) {x : E} (hx : x EMetric.ball 0 p.radius) :
        Summable fun (n : ) => (p n) fun (x_1 : Fin n) => x
        theorem FormalMultilinearSeries.radius_eq_top_of_summable_norm {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (p : FormalMultilinearSeries 𝕜 E F) (hs : ∀ (r : NNReal), Summable fun (n : ) => p n * r ^ n) :
        p.radius =
        theorem FormalMultilinearSeries.radius_eq_top_iff_summable_norm {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (p : FormalMultilinearSeries 𝕜 E F) :
        p.radius = ∀ (r : NNReal), Summable fun (n : ) => p n * r ^ n
        theorem FormalMultilinearSeries.le_mul_pow_of_radius_pos {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (p : FormalMultilinearSeries 𝕜 E F) (h : 0 < p.radius) :
        ∃ (C : ) (r : ) (_ : 0 < C) (_ : 0 < r), ∀ (n : ), p n C * r ^ n

        If the radius of p is positive, then ‖pₙ‖ grows at most geometrically.

        theorem FormalMultilinearSeries.radius_le_of_le {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {𝕜' : Type u_5} {E' : Type u_6} {F' : Type u_7} [NontriviallyNormedField 𝕜'] [NormedAddCommGroup E'] [NormedSpace 𝕜' E'] [NormedAddCommGroup F'] [NormedSpace 𝕜' F'] {p : FormalMultilinearSeries 𝕜 E F} {q : FormalMultilinearSeries 𝕜' E' F'} (h : ∀ (n : ), p n q n) :
        q.radius p.radius
        theorem FormalMultilinearSeries.min_radius_le_radius_add {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (p : FormalMultilinearSeries 𝕜 E F) (q : FormalMultilinearSeries 𝕜 E F) :
        min p.radius q.radius (p + q).radius

        The radius of the sum of two formal series is at least the minimum of their two radii.

        @[simp]
        theorem FormalMultilinearSeries.radius_neg {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (p : FormalMultilinearSeries 𝕜 E F) :
        (-p).radius = p.radius
        theorem FormalMultilinearSeries.hasSum {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace F] (p : FormalMultilinearSeries 𝕜 E F) {x : E} (hx : x EMetric.ball 0 p.radius) :
        HasSum (fun (n : ) => (p n) fun (x_1 : Fin n) => x) (p.sum x)
        theorem FormalMultilinearSeries.radius_le_radius_continuousLinearMap_comp {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedAddCommGroup G] [NormedSpace 𝕜 G] (p : FormalMultilinearSeries 𝕜 E F) (f : F →L[𝕜] G) :
        p.radius (f.compFormalMultilinearSeries p).radius

        Expanding a function as a power series #

        structure HasFPowerSeriesOnBall {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (f : EF) (p : FormalMultilinearSeries 𝕜 E F) (x : E) (r : ENNReal) :

        Given a function f : E → F and a formal multilinear series p, we say that f has p as a power series on the ball of radius r > 0 around x if f (x + y) = ∑' pₙ yⁿ for all ‖y‖ < r.

        Instances For
          theorem HasFPowerSeriesOnBall.r_le {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : EF} {p : FormalMultilinearSeries 𝕜 E F} {x : E} {r : ENNReal} (self : HasFPowerSeriesOnBall f p x r) :
          r p.radius
          theorem HasFPowerSeriesOnBall.r_pos {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : EF} {p : FormalMultilinearSeries 𝕜 E F} {x : E} {r : ENNReal} (self : HasFPowerSeriesOnBall f p x r) :
          0 < r
          theorem HasFPowerSeriesOnBall.hasSum {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : EF} {p : FormalMultilinearSeries 𝕜 E F} {x : E} {r : ENNReal} (self : HasFPowerSeriesOnBall f p x r) {y : E} :
          y EMetric.ball 0 rHasSum (fun (n : ) => (p n) fun (x : Fin n) => y) (f (x + y))
          structure HasFPowerSeriesWithinOnBall {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (f : EF) (p : FormalMultilinearSeries 𝕜 E F) (s : Set E) (x : E) (r : ENNReal) :

          Analogue of HasFPowerSeriesOnBall where convergence is required only on a set s. We also require convergence at x as the behavior of this notion is very bad otherwise.

          • r_le : r p.radius

            p converges on ball 0 r

          • r_pos : 0 < r

            The radius of convergence is positive

          • hasSum : ∀ {y : E}, x + y insert x sy EMetric.ball 0 rHasSum (fun (n : ) => (p n) fun (x : Fin n) => y) (f (x + y))

            p converges to f within s

          Instances For
            theorem HasFPowerSeriesWithinOnBall.r_le {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : EF} {p : FormalMultilinearSeries 𝕜 E F} {s : Set E} {x : E} {r : ENNReal} (self : HasFPowerSeriesWithinOnBall f p s x r) :
            r p.radius

            p converges on ball 0 r

            theorem HasFPowerSeriesWithinOnBall.r_pos {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : EF} {p : FormalMultilinearSeries 𝕜 E F} {s : Set E} {x : E} {r : ENNReal} (self : HasFPowerSeriesWithinOnBall f p s x r) :
            0 < r

            The radius of convergence is positive

            theorem HasFPowerSeriesWithinOnBall.hasSum {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : EF} {p : FormalMultilinearSeries 𝕜 E F} {s : Set E} {x : E} {r : ENNReal} (self : HasFPowerSeriesWithinOnBall f p s x r) {y : E} :
            x + y insert x sy EMetric.ball 0 rHasSum (fun (n : ) => (p n) fun (x : Fin n) => y) (f (x + y))

            p converges to f within s

            def HasFPowerSeriesAt {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (f : EF) (p : FormalMultilinearSeries 𝕜 E F) (x : E) :

            Given a function f : E → F and a formal multilinear series p, we say that f has p as a power series around x if f (x + y) = ∑' pₙ yⁿ for all y in a neighborhood of 0.

            Equations
            Instances For
              def HasFPowerSeriesWithinAt {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (f : EF) (p : FormalMultilinearSeries 𝕜 E F) (s : Set E) (x : E) :

              Analogue of HasFPowerSeriesAt where convergence is required only on a set s.

              Equations
              Instances For
                def AnalyticAt (𝕜 : Type u_1) {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (f : EF) (x : E) :

                Given a function f : E → F, we say that f is analytic at x if it admits a convergent power series expansion around x.

                Equations
                Instances For
                  def AnalyticWithinAt (𝕜 : Type u_1) {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (f : EF) (s : Set E) (x : E) :

                  f is analytic within s at x if it has a power series at x that converges on 𝓝[s] x

                  Equations
                  Instances For
                    def AnalyticOnNhd (𝕜 : Type u_1) {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (f : EF) (s : Set E) :

                    Given a function f : E → F, we say that f is analytic on a set s if it is analytic around every point of s.

                    Equations
                    Instances For
                      def AnalyticOn (𝕜 : Type u_1) {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (f : EF) (s : Set E) :

                      f is analytic within s if it is analytic within s at each point of s. Note that this is weaker than AnalyticOnNhd 𝕜 f s, as f is allowed to be arbitrary outside s.

                      Equations
                      Instances For
                        @[deprecated AnalyticOn]
                        def AnalyticWithinOn (𝕜 : Type u_1) {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (f : EF) (s : Set E) :

                        Alias of AnalyticOn.


                        f is analytic within s if it is analytic within s at each point of s. Note that this is weaker than AnalyticOnNhd 𝕜 f s, as f is allowed to be arbitrary outside s.

                        Equations
                        Instances For

                          HasFPowerSeriesOnBall and HasFPowerSeriesWithinOnBall #

                          theorem HasFPowerSeriesOnBall.hasFPowerSeriesAt {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : EF} {p : FormalMultilinearSeries 𝕜 E F} {x : E} {r : ENNReal} (hf : HasFPowerSeriesOnBall f p x r) :
                          theorem HasFPowerSeriesAt.analyticAt {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : EF} {p : FormalMultilinearSeries 𝕜 E F} {x : E} (hf : HasFPowerSeriesAt f p x) :
                          AnalyticAt 𝕜 f x
                          theorem HasFPowerSeriesOnBall.analyticAt {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : EF} {p : FormalMultilinearSeries 𝕜 E F} {x : E} {r : ENNReal} (hf : HasFPowerSeriesOnBall f p x r) :
                          AnalyticAt 𝕜 f x
                          theorem HasFPowerSeriesWithinOnBall.hasFPowerSeriesWithinAt {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : EF} {p : FormalMultilinearSeries 𝕜 E F} {s : Set E} {x : E} {r : ENNReal} (hf : HasFPowerSeriesWithinOnBall f p s x r) :
                          theorem HasFPowerSeriesWithinAt.analyticWithinAt {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : EF} {p : FormalMultilinearSeries 𝕜 E F} {s : Set E} {x : E} (hf : HasFPowerSeriesWithinAt f p s x) :
                          AnalyticWithinAt 𝕜 f s x
                          theorem HasFPowerSeriesWithinOnBall.analyticWithinAt {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : EF} {p : FormalMultilinearSeries 𝕜 E F} {s : Set E} {x : E} {r : ENNReal} (hf : HasFPowerSeriesWithinOnBall f p s x r) :
                          AnalyticWithinAt 𝕜 f s x
                          theorem HasFPowerSeriesOnBall.comp_sub {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : EF} {p : FormalMultilinearSeries 𝕜 E F} {x : E} {r : ENNReal} (hf : HasFPowerSeriesOnBall f p x r) (y : E) :
                          HasFPowerSeriesOnBall (fun (z : E) => f (z - y)) p (x + y) r

                          If a function f has a power series p around x, then the function z ↦ f (z - y) has the same power series around x + y.

                          theorem HasFPowerSeriesWithinOnBall.hasSum_sub {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : EF} {p : FormalMultilinearSeries 𝕜 E F} {s : Set E} {x : E} {r : ENNReal} (hf : HasFPowerSeriesWithinOnBall f p s x r) {y : E} (hy : y insert x s EMetric.ball x r) :
                          HasSum (fun (n : ) => (p n) fun (x_1 : Fin n) => y - x) (f y)
                          theorem HasFPowerSeriesOnBall.hasSum_sub {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : EF} {p : FormalMultilinearSeries 𝕜 E F} {x : E} {r : ENNReal} (hf : HasFPowerSeriesOnBall f p x r) {y : E} (hy : y EMetric.ball x r) :
                          HasSum (fun (n : ) => (p n) fun (x_1 : Fin n) => y - x) (f y)
                          theorem HasFPowerSeriesOnBall.radius_pos {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : EF} {p : FormalMultilinearSeries 𝕜 E F} {x : E} {r : ENNReal} (hf : HasFPowerSeriesOnBall f p x r) :
                          0 < p.radius
                          theorem HasFPowerSeriesWithinOnBall.radius_pos {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : EF} {p : FormalMultilinearSeries 𝕜 E F} {s : Set E} {x : E} {r : ENNReal} (hf : HasFPowerSeriesWithinOnBall f p s x r) :
                          0 < p.radius
                          theorem HasFPowerSeriesAt.radius_pos {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : EF} {p : FormalMultilinearSeries 𝕜 E F} {x : E} (hf : HasFPowerSeriesAt f p x) :
                          0 < p.radius
                          theorem HasFPowerSeriesWithinOnBall.of_le {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : EF} {p : FormalMultilinearSeries 𝕜 E F} {s : Set E} {x : E} {r : ENNReal} {r' : ENNReal} (hf : HasFPowerSeriesWithinOnBall f p s x r) (r'_pos : 0 < r') (hr : r' r) :
                          theorem HasFPowerSeriesOnBall.mono {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : EF} {p : FormalMultilinearSeries 𝕜 E F} {x : E} {r : ENNReal} {r' : ENNReal} (hf : HasFPowerSeriesOnBall f p x r) (r'_pos : 0 < r') (hr : r' r) :
                          theorem HasFPowerSeriesWithinOnBall.congr {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : EF} {g : EF} {p : FormalMultilinearSeries 𝕜 E F} {s : Set E} {x : E} {r : ENNReal} (h : HasFPowerSeriesWithinOnBall f p s x r) (h' : Set.EqOn g f (s EMetric.ball x r)) (h'' : g x = f x) :
                          theorem HasFPowerSeriesWithinOnBall.congr' {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : EF} {g : EF} {p : FormalMultilinearSeries 𝕜 E F} {s : Set E} {x : E} {r : ENNReal} (h : HasFPowerSeriesWithinOnBall f p s x r) (h' : Set.EqOn g f (insert x s EMetric.ball x r)) :

                          Variant of HasFPowerSeriesWithinOnBall.congr in which one requests equality on insert x s instead of separating x and s.

                          theorem HasFPowerSeriesWithinAt.congr {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : EF} {g : EF} {p : FormalMultilinearSeries 𝕜 E F} {s : Set E} {x : E} (h : HasFPowerSeriesWithinAt f p s x) (h' : g =ᶠ[nhdsWithin x s] f) (h'' : g x = f x) :
                          theorem HasFPowerSeriesOnBall.congr {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : EF} {g : EF} {p : FormalMultilinearSeries 𝕜 E F} {x : E} {r : ENNReal} (hf : HasFPowerSeriesOnBall f p x r) (hg : Set.EqOn f g (EMetric.ball x r)) :
                          theorem HasFPowerSeriesAt.congr {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : EF} {g : EF} {p : FormalMultilinearSeries 𝕜 E F} {x : E} (hf : HasFPowerSeriesAt f p x) (hg : f =ᶠ[nhds x] g) :
                          theorem HasFPowerSeriesWithinAt.eventually {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : EF} {p : FormalMultilinearSeries 𝕜 E F} {s : Set E} {x : E} (hf : HasFPowerSeriesWithinAt f p s x) :
                          ∀ᶠ (r : ENNReal) in nhdsWithin 0 (Set.Ioi 0), HasFPowerSeriesWithinOnBall f p s x r
                          theorem HasFPowerSeriesAt.eventually {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : EF} {p : FormalMultilinearSeries 𝕜 E F} {x : E} (hf : HasFPowerSeriesAt f p x) :
                          ∀ᶠ (r : ENNReal) in nhdsWithin 0 (Set.Ioi 0), HasFPowerSeriesOnBall f p x r
                          theorem HasFPowerSeriesOnBall.eventually_hasSum {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : EF} {p : FormalMultilinearSeries 𝕜 E F} {x : E} {r : ENNReal} (hf : HasFPowerSeriesOnBall f p x r) :
                          ∀ᶠ (y : E) in nhds 0, HasSum (fun (n : ) => (p n) fun (x : Fin n) => y) (f (x + y))
                          theorem HasFPowerSeriesAt.eventually_hasSum {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : EF} {p : FormalMultilinearSeries 𝕜 E F} {x : E} (hf : HasFPowerSeriesAt f p x) :
                          ∀ᶠ (y : E) in nhds 0, HasSum (fun (n : ) => (p n) fun (x : Fin n) => y) (f (x + y))
                          theorem HasFPowerSeriesOnBall.eventually_hasSum_sub {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : EF} {p : FormalMultilinearSeries 𝕜 E F} {x : E} {r : ENNReal} (hf : HasFPowerSeriesOnBall f p x r) :
                          ∀ᶠ (y : E) in nhds x, HasSum (fun (n : ) => (p n) fun (x_1 : Fin n) => y - x) (f y)
                          theorem HasFPowerSeriesAt.eventually_hasSum_sub {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : EF} {p : FormalMultilinearSeries 𝕜 E F} {x : E} (hf : HasFPowerSeriesAt f p x) :
                          ∀ᶠ (y : E) in nhds x, HasSum (fun (n : ) => (p n) fun (x_1 : Fin n) => y - x) (f y)
                          theorem HasFPowerSeriesOnBall.eventually_eq_zero {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : EF} {x : E} {r : ENNReal} (hf : HasFPowerSeriesOnBall f 0 x r) :
                          ∀ᶠ (z : E) in nhds x, f z = 0
                          theorem HasFPowerSeriesAt.eventually_eq_zero {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : EF} {x : E} (hf : HasFPowerSeriesAt f 0 x) :
                          ∀ᶠ (z : E) in nhds x, f z = 0
                          @[simp]
                          theorem hasFPowerSeriesWithinOnBall_univ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : EF} {p : FormalMultilinearSeries 𝕜 E F} {x : E} {r : ENNReal} :
                          @[simp]
                          theorem hasFPowerSeriesWithinAt_univ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : EF} {p : FormalMultilinearSeries 𝕜 E F} {x : E} :
                          theorem HasFPowerSeriesWithinOnBall.mono {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : EF} {p : FormalMultilinearSeries 𝕜 E F} {s : Set E} {t : Set E} {x : E} {r : ENNReal} (hf : HasFPowerSeriesWithinOnBall f p s x r) (h : t s) :
                          theorem HasFPowerSeriesOnBall.hasFPowerSeriesWithinOnBall {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : EF} {p : FormalMultilinearSeries 𝕜 E F} {s : Set E} {x : E} {r : ENNReal} (hf : HasFPowerSeriesOnBall f p x r) :
                          theorem HasFPowerSeriesWithinAt.mono {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : EF} {p : FormalMultilinearSeries 𝕜 E F} {s : Set E} {t : Set E} {x : E} (hf : HasFPowerSeriesWithinAt f p s x) (h : t s) :
                          theorem HasFPowerSeriesAt.hasFPowerSeriesWithinAt {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : EF} {p : FormalMultilinearSeries 𝕜 E F} {s : Set E} {x : E} (hf : HasFPowerSeriesAt f p x) :
                          theorem HasFPowerSeriesWithinAt.mono_of_mem {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : EF} {p : FormalMultilinearSeries 𝕜 E F} {s : Set E} {t : Set E} {x : E} (h : HasFPowerSeriesWithinAt f p s x) (hst : s nhdsWithin x t) :
                          @[simp]
                          theorem hasFPowerSeriesWithinOnBall_insert_self {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : EF} {p : FormalMultilinearSeries 𝕜 E F} {s : Set E} {x : E} {r : ENNReal} :
                          @[simp]
                          theorem hasFPowerSeriesWithinAt_insert {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : EF} {p : FormalMultilinearSeries 𝕜 E F} {s : Set E} {x : E} {y : E} :
                          theorem HasFPowerSeriesWithinOnBall.coeff_zero {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : EF} {pf : FormalMultilinearSeries 𝕜 E F} {s : Set E} {x : E} {r : ENNReal} (hf : HasFPowerSeriesWithinOnBall f pf s x r) (v : Fin 0E) :
                          (pf 0) v = f x
                          theorem HasFPowerSeriesOnBall.coeff_zero {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : EF} {pf : FormalMultilinearSeries 𝕜 E F} {x : E} {r : ENNReal} (hf : HasFPowerSeriesOnBall f pf x r) (v : Fin 0E) :
                          (pf 0) v = f x
                          theorem HasFPowerSeriesWithinAt.coeff_zero {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : EF} {pf : FormalMultilinearSeries 𝕜 E F} {s : Set E} {x : E} (hf : HasFPowerSeriesWithinAt f pf s x) (v : Fin 0E) :
                          (pf 0) v = f x
                          theorem HasFPowerSeriesAt.coeff_zero {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : EF} {pf : FormalMultilinearSeries 𝕜 E F} {x : E} (hf : HasFPowerSeriesAt f pf x) (v : Fin 0E) :
                          (pf 0) v = f x

                          Analytic functions #

                          @[simp]
                          theorem analyticWithinAt_univ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : EF} {x : E} :
                          AnalyticWithinAt 𝕜 f Set.univ x AnalyticAt 𝕜 f x
                          @[simp]
                          theorem analyticOn_univ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : EF} :
                          AnalyticOn 𝕜 f Set.univ AnalyticOnNhd 𝕜 f Set.univ
                          @[deprecated analyticOn_univ]
                          theorem analyticWithinOn_univ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : EF} :
                          AnalyticOn 𝕜 f Set.univ AnalyticOnNhd 𝕜 f Set.univ

                          Alias of analyticOn_univ.

                          theorem AnalyticWithinAt.mono {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : EF} {s : Set E} {t : Set E} {x : E} (hf : AnalyticWithinAt 𝕜 f s x) (h : t s) :
                          AnalyticWithinAt 𝕜 f t x
                          theorem AnalyticAt.analyticWithinAt {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : EF} {s : Set E} {x : E} (hf : AnalyticAt 𝕜 f x) :
                          AnalyticWithinAt 𝕜 f s x
                          theorem AnalyticOnNhd.analyticOn {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : EF} {s : Set E} (hf : AnalyticOnNhd 𝕜 f s) :
                          AnalyticOn 𝕜 f s
                          @[deprecated AnalyticOnNhd.analyticOn]
                          theorem AnalyticOn.analyticWithinOn {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : EF} {s : Set E} (hf : AnalyticOnNhd 𝕜 f s) :
                          AnalyticOn 𝕜 f s

                          Alias of AnalyticOnNhd.analyticOn.

                          theorem AnalyticWithinAt.congr_of_eventuallyEq {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : EF} {g : EF} {s : Set E} {x : E} (hf : AnalyticWithinAt 𝕜 f s x) (hs : g =ᶠ[nhdsWithin x s] f) (hx : g x = f x) :
                          AnalyticWithinAt 𝕜 g s x
                          theorem AnalyticWithinAt.congr_of_eventuallyEq_insert {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : EF} {g : EF} {s : Set E} {x : E} (hf : AnalyticWithinAt 𝕜 f s x) (hs : g =ᶠ[nhdsWithin x (insert x s)] f) :
                          AnalyticWithinAt 𝕜 g s x
                          theorem AnalyticWithinAt.congr {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : EF} {g : EF} {s : Set E} {x : E} (hf : AnalyticWithinAt 𝕜 f s x) (hs : Set.EqOn g f s) (hx : g x = f x) :
                          AnalyticWithinAt 𝕜 g s x
                          theorem AnalyticOn.congr {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : EF} {g : EF} {s : Set E} (hf : AnalyticOn 𝕜 f s) (hs : Set.EqOn g f s) :
                          AnalyticOn 𝕜 g s
                          @[deprecated AnalyticOn.congr]
                          theorem AnalyticWithinOn.congr {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : EF} {g : EF} {s : Set E} (hf : AnalyticOn 𝕜 f s) (hs : Set.EqOn g f s) :
                          AnalyticOn 𝕜 g s

                          Alias of AnalyticOn.congr.

                          theorem AnalyticAt.congr {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : EF} {g : EF} {x : E} (hf : AnalyticAt 𝕜 f x) (hg : f =ᶠ[nhds x] g) :
                          AnalyticAt 𝕜 g x
                          theorem analyticAt_congr {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : EF} {g : EF} {x : E} (h : f =ᶠ[nhds x] g) :
                          AnalyticAt 𝕜 f x AnalyticAt 𝕜 g x
                          theorem AnalyticOnNhd.mono {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : EF} {s : Set E} {t : Set E} (hf : AnalyticOnNhd 𝕜 f t) (hst : s t) :
                          AnalyticOnNhd 𝕜 f s
                          theorem AnalyticOnNhd.congr' {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : EF} {g : EF} {s : Set E} (hf : AnalyticOnNhd 𝕜 f s) (hg : f =ᶠ[nhdsSet s] g) :
                          AnalyticOnNhd 𝕜 g s
                          @[deprecated AnalyticOnNhd.congr']
                          theorem AnalyticOn.congr' {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : EF} {g : EF} {s : Set E} (hf : AnalyticOnNhd 𝕜 f s) (hg : f =ᶠ[nhdsSet s] g) :
                          AnalyticOnNhd 𝕜 g s

                          Alias of AnalyticOnNhd.congr'.

                          theorem analyticOnNhd_congr' {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : EF} {g : EF} {s : Set E} (h : f =ᶠ[nhdsSet s] g) :
                          AnalyticOnNhd 𝕜 f s AnalyticOnNhd 𝕜 g s
                          @[deprecated analyticOnNhd_congr']
                          theorem analyticOn_congr' {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : EF} {g : EF} {s : Set E} (h : f =ᶠ[nhdsSet s] g) :
                          AnalyticOnNhd 𝕜 f s AnalyticOnNhd 𝕜 g s

                          Alias of analyticOnNhd_congr'.

                          theorem AnalyticOnNhd.congr {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : EF} {g : EF} {s : Set E} (hs : IsOpen s) (hf : AnalyticOnNhd 𝕜 f s) (hg : Set.EqOn f g s) :
                          AnalyticOnNhd 𝕜 g s
                          theorem analyticOnNhd_congr {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : EF} {g : EF} {s : Set E} (hs : IsOpen s) (h : Set.EqOn f g s) :
                          AnalyticOnNhd 𝕜 f s AnalyticOnNhd 𝕜 g s
                          @[deprecated analyticOnNhd_congr]
                          theorem analyticOn_congr {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : EF} {g : EF} {s : Set E} (hs : IsOpen s) (h : Set.EqOn f g s) :
                          AnalyticOnNhd 𝕜 f s AnalyticOnNhd 𝕜 g s

                          Alias of analyticOnNhd_congr.

                          theorem AnalyticWithinAt.mono_of_mem {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : EF} {s : Set E} {t : Set E} {x : E} (h : AnalyticWithinAt 𝕜 f s x) (hst : s nhdsWithin x t) :
                          AnalyticWithinAt 𝕜 f t x
                          theorem AnalyticOn.mono {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : EF} {s : Set E} {t : Set E} (h : AnalyticOn 𝕜 f t) (hs : s t) :
                          AnalyticOn 𝕜 f s
                          @[deprecated AnalyticOn.mono]
                          theorem AnalyticWithinOn.mono {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : EF} {s : Set E} {t : Set E} (h : AnalyticOn 𝕜 f t) (hs : s t) :
                          AnalyticOn 𝕜 f s

                          Alias of AnalyticOn.mono.

                          @[simp]
                          theorem analyticWithinAt_insert {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : EF} {s : Set E} {x : E} {y : E} :
                          AnalyticWithinAt 𝕜 f (insert y s) x AnalyticWithinAt 𝕜 f s x

                          Composition with linear maps #

                          theorem ContinuousLinearMap.comp_hasFPowerSeriesWithinOnBall {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedAddCommGroup G] [NormedSpace 𝕜 G] {f : EF} {p : FormalMultilinearSeries 𝕜 E F} {s : Set E} {x : E} {r : ENNReal} (g : F →L[𝕜] G) (h : HasFPowerSeriesWithinOnBall f p s x r) :
                          HasFPowerSeriesWithinOnBall (g f) (g.compFormalMultilinearSeries p) s x r

                          If a function f has a power series p on a ball within a set and g is linear, then g ∘ f has the power series g ∘ p on the same ball.

                          theorem ContinuousLinearMap.comp_hasFPowerSeriesOnBall {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedAddCommGroup G] [NormedSpace 𝕜 G] {f : EF} {p : FormalMultilinearSeries 𝕜 E F} {x : E} {r : ENNReal} (g : F →L[𝕜] G) (h : HasFPowerSeriesOnBall f p x r) :
                          HasFPowerSeriesOnBall (g f) (g.compFormalMultilinearSeries p) x r

                          If a function f has a power series p on a ball and g is linear, then g ∘ f has the power series g ∘ p on the same ball.

                          theorem ContinuousLinearMap.comp_analyticOn {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedAddCommGroup G] [NormedSpace 𝕜 G] {f : EF} {s : Set E} (g : F →L[𝕜] G) (h : AnalyticOn 𝕜 f s) :
                          AnalyticOn 𝕜 (g f) s

                          If a function f is analytic on a set s and g is linear, then g ∘ f is analytic on s.

                          theorem ContinuousLinearMap.comp_analyticOnNhd {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedAddCommGroup G] [NormedSpace 𝕜 G] {f : EF} {s : Set E} (g : F →L[𝕜] G) (h : AnalyticOnNhd 𝕜 f s) :
                          AnalyticOnNhd 𝕜 (g f) s

                          If a function f is analytic on a set s and g is linear, then g ∘ f is analytic on s.

                          Relation between analytic function and the partial sums of its power series #

                          theorem HasFPowerSeriesWithinOnBall.tendsto_partialSum {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : EF} {p : FormalMultilinearSeries 𝕜 E F} {s : Set E} {x : E} {r : ENNReal} (hf : HasFPowerSeriesWithinOnBall f p s x r) {y : E} (hy : y EMetric.ball 0 r) (h'y : x + y insert x s) :
                          Filter.Tendsto (fun (n : ) => p.partialSum n y) Filter.atTop (nhds (f (x + y)))
                          theorem HasFPowerSeriesOnBall.tendsto_partialSum {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : EF} {p : FormalMultilinearSeries 𝕜 E F} {x : E} {r : ENNReal} (hf : HasFPowerSeriesOnBall f p x r) {y : E} (hy : y EMetric.ball 0 r) :
                          Filter.Tendsto (fun (n : ) => p.partialSum n y) Filter.atTop (nhds (f (x + y)))
                          theorem HasFPowerSeriesAt.tendsto_partialSum {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : EF} {p : FormalMultilinearSeries 𝕜 E F} {x : E} (hf : HasFPowerSeriesAt f p x) :
                          ∀ᶠ (y : E) in nhds 0, Filter.Tendsto (fun (n : ) => p.partialSum n y) Filter.atTop (nhds (f (x + y)))
                          theorem HasFPowerSeriesWithinOnBall.tendsto_partialSum_prod {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : EF} {p : FormalMultilinearSeries 𝕜 E F} {s : Set E} {x : E} {r : ENNReal} {y : E} (hf : HasFPowerSeriesWithinOnBall f p s x r) (hy : y EMetric.ball 0 r) (h'y : x + y insert x s) :
                          Filter.Tendsto (fun (z : × E) => p.partialSum z.1 z.2) (Filter.atTop ×ˢ nhds y) (nhds (f (x + y)))

                          If a function admits a power series expansion within a ball, then the partial sums p.partialSum n z converge to f (x + y) as n → ∞ and z → y. Note that x + z doesn't need to belong to the set where the power series expansion holds.

                          theorem HasFPowerSeriesOnBall.tendsto_partialSum_prod {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : EF} {p : FormalMultilinearSeries 𝕜 E F} {x : E} {r : ENNReal} {y : E} (hf : HasFPowerSeriesOnBall f p x r) (hy : y EMetric.ball 0 r) :
                          Filter.Tendsto (fun (z : × E) => p.partialSum z.1 z.2) (Filter.atTop ×ˢ nhds y) (nhds (f (x + y)))

                          If a function admits a power series on a ball, then the partial sums p.partialSum n z converges to f (x + y) as n → ∞ and z → y.

                          theorem HasFPowerSeriesWithinOnBall.uniform_geometric_approx' {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : EF} {p : FormalMultilinearSeries 𝕜 E F} {s : Set E} {x : E} {r : ENNReal} {r' : NNReal} (hf : HasFPowerSeriesWithinOnBall f p s x r) (h : r' < r) :
                          aSet.Ioo 0 1, C > 0, yMetric.ball 0 r', ∀ (n : ), x + y insert x sf (x + y) - p.partialSum n y C * (a * (y / r')) ^ n

                          If a function admits a power series expansion, then it is exponentially close to the partial sums of this power series on strict subdisks of the disk of convergence.

                          This version provides an upper estimate that decreases both in ‖y‖ and n. See also HasFPowerSeriesWithinOnBall.uniform_geometric_approx for a weaker version.

                          theorem HasFPowerSeriesOnBall.uniform_geometric_approx' {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : EF} {p : FormalMultilinearSeries 𝕜 E F} {x : E} {r : ENNReal} {r' : NNReal} (hf : HasFPowerSeriesOnBall f p x r) (h : r' < r) :
                          aSet.Ioo 0 1, C > 0, yMetric.ball 0 r', ∀ (n : ), f (x + y) - p.partialSum n y C * (a * (y / r')) ^ n

                          If a function admits a power series expansion, then it is exponentially close to the partial sums of this power series on strict subdisks of the disk of convergence.

                          This version provides an upper estimate that decreases both in ‖y‖ and n. See also HasFPowerSeriesOnBall.uniform_geometric_approx for a weaker version.

                          theorem HasFPowerSeriesWithinOnBall.uniform_geometric_approx {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : EF} {p : FormalMultilinearSeries 𝕜 E F} {s : Set E} {x : E} {r : ENNReal} {r' : NNReal} (hf : HasFPowerSeriesWithinOnBall f p s x r) (h : r' < r) :
                          aSet.Ioo 0 1, C > 0, yMetric.ball 0 r', ∀ (n : ), x + y insert x sf (x + y) - p.partialSum n y C * a ^ n

                          If a function admits a power series expansion within a set in a ball, then it is exponentially close to the partial sums of this power series on strict subdisks of the disk of convergence.

                          theorem HasFPowerSeriesOnBall.uniform_geometric_approx {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : EF} {p : FormalMultilinearSeries 𝕜 E F} {x : E} {r : ENNReal} {r' : NNReal} (hf : HasFPowerSeriesOnBall f p x r) (h : r' < r) :
                          aSet.Ioo 0 1, C > 0, yMetric.ball 0 r', ∀ (n : ), f (x + y) - p.partialSum n y C * a ^ n

                          If a function admits a power series expansion, then it is exponentially close to the partial sums of this power series on strict subdisks of the disk of convergence.

                          theorem HasFPowerSeriesWithinAt.isBigO_sub_partialSum_pow {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : EF} {p : FormalMultilinearSeries 𝕜 E F} {s : Set E} {x : E} (hf : HasFPowerSeriesWithinAt f p s x) (n : ) :
                          (fun (y : E) => f (x + y) - p.partialSum n y) =O[nhdsWithin 0 ((fun (x_1 : E) => x + x_1) ⁻¹' insert x s)] fun (y : E) => y ^ n

                          Taylor formula for an analytic function within a set, IsBigO version.

                          theorem HasFPowerSeriesAt.isBigO_sub_partialSum_pow {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : EF} {p : FormalMultilinearSeries 𝕜 E F} {x : E} (hf : HasFPowerSeriesAt f p x) (n : ) :
                          (fun (y : E) => f (x + y) - p.partialSum n y) =O[nhds 0] fun (y : E) => y ^ n

                          Taylor formula for an analytic function, IsBigO version.

                          theorem HasFPowerSeriesWithinOnBall.isBigO_image_sub_image_sub_deriv_principal {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : EF} {p : FormalMultilinearSeries 𝕜 E F} {s : Set E} {x : E} {r : ENNReal} {r' : ENNReal} (hf : HasFPowerSeriesWithinOnBall f p s x r) (hr : r' < r) :
                          (fun (y : E × E) => f y.1 - f y.2 - (p 1) fun (x : Fin 1) => y.1 - y.2) =O[Filter.principal (EMetric.ball (x, x) r' insert x s ×ˢ insert x s)] fun (y : E × E) => 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.

                          theorem HasFPowerSeriesOnBall.isBigO_image_sub_image_sub_deriv_principal {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : EF} {p : FormalMultilinearSeries 𝕜 E F} {x : E} {r : ENNReal} {r' : ENNReal} (hf : HasFPowerSeriesOnBall f p x r) (hr : r' < r) :
                          (fun (y : E × E) => f y.1 - f y.2 - (p 1) fun (x : Fin 1) => y.1 - y.2) =O[Filter.principal (EMetric.ball (x, x) r')] fun (y : E × E) => y - (x, x) * y.1 - y.2

                          If f has formal power series ∑ n, pₙ 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‖. This lemma formulates this property using IsBigO and Filter.principal on E × E.

                          theorem HasFPowerSeriesWithinOnBall.image_sub_sub_deriv_le {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : EF} {p : FormalMultilinearSeries 𝕜 E F} {s : Set E} {x : E} {r : ENNReal} {r' : ENNReal} (hf : HasFPowerSeriesWithinOnBall f p s x r) (hr : r' < r) :
                          ∃ (C : ), yinsert x s EMetric.ball x r', zinsert x s EMetric.ball x r', f y - f z - (p 1) fun (x : Fin 1) => 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‖.

                          theorem HasFPowerSeriesOnBall.image_sub_sub_deriv_le {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : EF} {p : FormalMultilinearSeries 𝕜 E F} {x : E} {r : ENNReal} {r' : ENNReal} (hf : HasFPowerSeriesOnBall f p x r) (hr : r' < r) :
                          ∃ (C : ), yEMetric.ball x r', zEMetric.ball x r', f y - f z - (p 1) fun (x : Fin 1) => y - z C * max y - x z - x * y - z

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

                          theorem HasFPowerSeriesWithinAt.isBigO_image_sub_norm_mul_norm_sub {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : EF} {p : FormalMultilinearSeries 𝕜 E F} {s : Set E} {x : E} (hf : HasFPowerSeriesWithinAt f p s x) :
                          (fun (y : E × E) => f y.1 - f y.2 - (p 1) fun (x : Fin 1) => y.1 - y.2) =O[nhdsWithin (x, x) (insert x s ×ˢ insert x s)] fun (y : E × E) => y - (x, x) * y.1 - y.2

                          If f has formal power series ∑ n, pₙ at x within a set s, then f y - f z - p 1 (fun _ ↦ y - z) = O(‖(y, z) - (x, x)‖ * ‖y - z‖) as (y, z) → (x, x) within s × s.

                          theorem HasFPowerSeriesAt.isBigO_image_sub_norm_mul_norm_sub {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : EF} {p : FormalMultilinearSeries 𝕜 E F} {x : E} (hf : HasFPowerSeriesAt f p x) :
                          (fun (y : E × E) => f y.1 - f y.2 - (p 1) fun (x : Fin 1) => y.1 - y.2) =O[nhds (x, x)] fun (y : E × E) => y - (x, x) * y.1 - y.2

                          If f has formal power series ∑ n, pₙ at x, then f y - f z - p 1 (fun _ ↦ y - z) = O(‖(y, z) - (x, x)‖ * ‖y - z‖) as (y, z) → (x, x). In particular, f is strictly differentiable at x.

                          theorem HasFPowerSeriesWithinOnBall.tendstoUniformlyOn {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : EF} {p : FormalMultilinearSeries 𝕜 E F} {s : Set E} {x : E} {r : ENNReal} {r' : NNReal} (hf : HasFPowerSeriesWithinOnBall f p s x r) (h : r' < r) :
                          TendstoUniformlyOn (fun (n : ) (y : E) => p.partialSum n y) (fun (y : E) => f (x + y)) Filter.atTop ((fun (x_1 : E) => x + x_1) ⁻¹' insert x s Metric.ball 0 r')

                          If a function admits a power series expansion within a set at x, then it is the uniform limit of the partial sums of this power series on strict subdisks of the disk of convergence, i.e., f (x + y) is the uniform limit of p.partialSum n y there.

                          theorem HasFPowerSeriesOnBall.tendstoUniformlyOn {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : EF} {p : FormalMultilinearSeries 𝕜 E F} {x : E} {r : ENNReal} {r' : NNReal} (hf : HasFPowerSeriesOnBall f p x r) (h : r' < r) :
                          TendstoUniformlyOn (fun (n : ) (y : E) => p.partialSum n y) (fun (y : E) => f (x + y)) Filter.atTop (Metric.ball 0 r')

                          If a function admits a power series expansion at x, then it is the uniform limit of the partial sums of this power series on strict subdisks of the disk of convergence, i.e., f (x + y) is the uniform limit of p.partialSum n y there.

                          theorem HasFPowerSeriesWithinOnBall.tendstoLocallyUniformlyOn {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : EF} {p : FormalMultilinearSeries 𝕜 E F} {s : Set E} {x : E} {r : ENNReal} (hf : HasFPowerSeriesWithinOnBall f p s x r) :
                          TendstoLocallyUniformlyOn (fun (n : ) (y : E) => p.partialSum n y) (fun (y : E) => f (x + y)) Filter.atTop ((fun (x_1 : E) => x + x_1) ⁻¹' insert x s EMetric.ball 0 r)

                          If a function admits a power series expansion within a set at x, then it is the locally uniform limit of the partial sums of this power series on the disk of convergence, i.e., f (x + y) is the locally uniform limit of p.partialSum n y there.

                          theorem HasFPowerSeriesOnBall.tendstoLocallyUniformlyOn {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : EF} {p : FormalMultilinearSeries 𝕜 E F} {x : E} {r : ENNReal} (hf : HasFPowerSeriesOnBall f p x r) :
                          TendstoLocallyUniformlyOn (fun (n : ) (y : E) => p.partialSum n y) (fun (y : E) => f (x + y)) Filter.atTop (EMetric.ball 0 r)

                          If a function admits a power series expansion at x, then it is the locally uniform limit of the partial sums of this power series on the disk of convergence, i.e., f (x + y) is the locally uniform limit of p.partialSum n y there.

                          theorem HasFPowerSeriesWithinOnBall.tendstoUniformlyOn' {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : EF} {p : FormalMultilinearSeries 𝕜 E F} {s : Set E} {x : E} {r : ENNReal} {r' : NNReal} (hf : HasFPowerSeriesWithinOnBall f p s x r) (h : r' < r) :
                          TendstoUniformlyOn (fun (n : ) (y : E) => p.partialSum n (y - x)) f Filter.atTop (insert x s Metric.ball x r')

                          If a function admits a power series expansion within a set at x, then it is the uniform limit of the partial sums of this power series on strict subdisks of the disk of convergence, i.e., f y is the uniform limit of p.partialSum n (y - x) there.

                          theorem HasFPowerSeriesOnBall.tendstoUniformlyOn' {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : EF} {p : FormalMultilinearSeries 𝕜 E F} {x : E} {r : ENNReal} {r' : NNReal} (hf : HasFPowerSeriesOnBall f p x r) (h : r' < r) :
                          TendstoUniformlyOn (fun (n : ) (y : E) => p.partialSum n (y - x)) f Filter.atTop (Metric.ball x r')

                          If a function admits a power series expansion at x, then it is the uniform limit of the partial sums of this power series on strict subdisks of the disk of convergence, i.e., f y is the uniform limit of p.partialSum n (y - x) there.

                          theorem HasFPowerSeriesWithinOnBall.tendstoLocallyUniformlyOn' {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : EF} {p : FormalMultilinearSeries 𝕜 E F} {s : Set E} {x : E} {r : ENNReal} (hf : HasFPowerSeriesWithinOnBall f p s x r) :
                          TendstoLocallyUniformlyOn (fun (n : ) (y : E) => p.partialSum n (y - x)) f Filter.atTop (insert x s EMetric.ball x r)

                          If a function admits a power series expansion within a set at x, then it is the locally uniform limit of the partial sums of this power series on the disk of convergence, i.e., f y is the locally uniform limit of p.partialSum n (y - x) there.

                          theorem HasFPowerSeriesOnBall.tendstoLocallyUniformlyOn' {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : EF} {p : FormalMultilinearSeries 𝕜 E F} {x : E} {r : ENNReal} (hf : HasFPowerSeriesOnBall f p x r) :
                          TendstoLocallyUniformlyOn (fun (n : ) (y : E) => p.partialSum n (y - x)) f Filter.atTop (EMetric.ball x r)

                          If a function admits a power series expansion at x, then it is the locally uniform limit of the partial sums of this power series on the disk of convergence, i.e., f y is the locally uniform limit of p.partialSum n (y - x) there.

                          theorem HasFPowerSeriesWithinOnBall.continuousOn {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : EF} {p : FormalMultilinearSeries 𝕜 E F} {s : Set E} {x : E} {r : ENNReal} (hf : HasFPowerSeriesWithinOnBall f p s x r) :

                          If a function admits a power series expansion within a set on a ball, then it is continuous there.

                          theorem HasFPowerSeriesOnBall.continuousOn {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : EF} {p : FormalMultilinearSeries 𝕜 E F} {x : E} {r : ENNReal} (hf : HasFPowerSeriesOnBall f p x r) :

                          If a function admits a power series expansion on a ball, then it is continuous there.

                          theorem HasFPowerSeriesWithinOnBall.continuousWithinAt_insert {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : EF} {p : FormalMultilinearSeries 𝕜 E F} {s : Set E} {x : E} {r : ENNReal} (hf : HasFPowerSeriesWithinOnBall f p s x r) :
                          theorem HasFPowerSeriesWithinOnBall.continuousWithinAt {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : EF} {p : FormalMultilinearSeries 𝕜 E F} {s : Set E} {x : E} {r : ENNReal} (hf : HasFPowerSeriesWithinOnBall f p s x r) :
                          theorem HasFPowerSeriesWithinAt.continuousWithinAt_insert {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : EF} {p : FormalMultilinearSeries 𝕜 E F} {s : Set E} {x : E} (hf : HasFPowerSeriesWithinAt f p s x) :
                          theorem HasFPowerSeriesWithinAt.continuousWithinAt {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : EF} {p : FormalMultilinearSeries 𝕜 E F} {s : Set E} {x : E} (hf : HasFPowerSeriesWithinAt f p s x) :
                          theorem HasFPowerSeriesAt.continuousAt {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : EF} {p : FormalMultilinearSeries 𝕜 E F} {x : E} (hf : HasFPowerSeriesAt f p x) :
                          theorem AnalyticWithinAt.continuousWithinAt_insert {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : EF} {s : Set E} {x : E} (hf : AnalyticWithinAt 𝕜 f s x) :
                          theorem AnalyticWithinAt.continuousWithinAt {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : EF} {s : Set E} {x : E} (hf : AnalyticWithinAt 𝕜 f s x) :
                          theorem AnalyticAt.continuousAt {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : EF} {x : E} (hf : AnalyticAt 𝕜 f x) :
                          theorem AnalyticOnNhd.continuousOn {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : EF} {s : Set E} (hf : AnalyticOnNhd 𝕜 f s) :
                          theorem AnalyticOn.continuousOn {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : EF} {s : Set E} (h : AnalyticOn 𝕜 f s) :
                          @[deprecated AnalyticOn.continuousOn]
                          theorem AnalyticWithinOn.continuousOn {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : EF} {s : Set E} (h : AnalyticOn 𝕜 f s) :

                          Alias of AnalyticOn.continuousOn.

                          theorem AnalyticOnNhd.continuous {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : EF} (fa : AnalyticOnNhd 𝕜 f Set.univ) :

                          Analytic everywhere implies continuous

                          @[deprecated AnalyticOnNhd.continuous]
                          theorem AnalyticOn.continuous {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : EF} (fa : AnalyticOnNhd 𝕜 f Set.univ) :

                          Alias of AnalyticOnNhd.continuous.


                          Analytic everywhere implies continuous

                          theorem FormalMultilinearSeries.hasFPowerSeriesOnBall {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace F] (p : FormalMultilinearSeries 𝕜 E F) (h : 0 < p.radius) :
                          HasFPowerSeriesOnBall p.sum p 0 p.radius

                          In a complete space, the sum of a converging power series p admits p as a power series. This is not totally obvious as we need to check the convergence of the series.

                          theorem HasFPowerSeriesWithinOnBall.sum {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : EF} {p : FormalMultilinearSeries 𝕜 E F} {s : Set E} {x : E} {r : ENNReal} (h : HasFPowerSeriesWithinOnBall f p s x r) {y : E} (h'y : x + y insert x s) (hy : y EMetric.ball 0 r) :
                          f (x + y) = p.sum y
                          theorem HasFPowerSeriesOnBall.sum {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : EF} {p : FormalMultilinearSeries 𝕜 E F} {x : E} {r : ENNReal} (h : HasFPowerSeriesOnBall f p x r) {y : E} (hy : y EMetric.ball 0 r) :
                          f (x + y) = p.sum y

                          The sum of a converging power series is continuous in its disk of convergence.

                          theorem hasFPowerSeriesAt_iff {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] {p : FormalMultilinearSeries 𝕜 𝕜 E} {f : 𝕜E} {z₀ : 𝕜} :
                          HasFPowerSeriesAt f p z₀ ∀ᶠ (z : 𝕜) in nhds 0, HasSum (fun (n : ) => z ^ n p.coeff n) (f (z₀ + z))

                          A function f : 𝕜 → E has p as power series expansion at a point z₀ iff it is the sum of p in a neighborhood of z₀. This makes some proofs easier by hiding the fact that HasFPowerSeriesAt depends on p.radius.

                          theorem hasFPowerSeriesAt_iff' {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] {p : FormalMultilinearSeries 𝕜 𝕜 E} {f : 𝕜E} {z₀ : 𝕜} :
                          HasFPowerSeriesAt f p z₀ ∀ᶠ (z : 𝕜) in nhds z₀, HasSum (fun (n : ) => (z - z₀) ^ n p.coeff n) (f z)