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 : ℕ.

• p.radius: the largest r : ℝ≥0∞ such that ‖p n‖ * r^n grows subexponentially.
• p.le_radius_of_bound, p.le_radius_of_bound_nnreal, p.le_radius_of_isBigO: if ‖p n‖ * r ^ n is bounded above, then r ≤ p.radius;
• p.isLittleO_of_lt_radius, p.norm_mul_pow_le_mul_pow_of_lt_radius, p.isLittleO_one_of_lt_radius, p.norm_mul_pow_le_of_lt_radius, p.nnnorm_mul_pow_le_of_lt_radius: if r < p.radius, then ‖p n‖ * r ^ n tends to zero exponentially;
• p.lt_radius_of_isBigO: if r ≠ 0 and ‖p n‖ * r ^ n = O(a ^ n) for some -1 < a < 1, then r < p.radius;
• p.partialSum n x: the sum ∑_{i = 0}^{n-1} pᵢ xⁱ.
• p.sum x: the sum ∑'_{i = 0}^{∞} pᵢ xⁱ.

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

• HasFPowerSeriesOnBall f p x r: on the ball of center x with radius r, f (x + y) = ∑'_n pₙ yⁿ.
• HasFPowerSeriesAt f p x: on some ball of center x with positive radius, holds HasFPowerSeriesOnBall f p x r.
• AnalyticAt 𝕜 f x: there exists a power series p such that holds HasFPowerSeriesAt f p x.
• AnalyticOn 𝕜 f s: the function f is analytic at every point of s.

We develop the basic properties of these notions, notably:

• If a function admits a power series, it is continuous (see HasFPowerSeriesOnBall.continuousOn and HasFPowerSeriesAt.continuousAt and AnalyticAt.continuousAt).
• In a complete space, the sum of a formal power series with positive radius is well defined on the disk of convergence, see FormalMultilinearSeries.hasFPowerSeriesOnBall.
• If a function admits a power series in a ball, then it is analytic at any point y of this ball, and the power series there can be expressed in terms of the initial power series p as p.changeOrigin y. See HasFPowerSeriesOnBall.changeOrigin. It follows in particular that the set of points at which a given function is analytic is open, see isOpen_analyticAt.

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

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

• p.partialSum n x = (Finset.range n).sum fun (k : ℕ) => (p k) fun (x_1 : Fin k) => x

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

def FormalMultilinearSeries.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) : ENNReal

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

• p.radius = ⨆ (r : NNReal), ⨆ (C : ℝ), ⨆ (_ : ∀ (n : ℕ), ‖p n‖ * ↑r ^ n ≤ C), ↑r

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]

theorem FormalMultilinearSeries.constFormalMultilinearSeries_radius {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {v : F} : (constFormalMultilinearSeries 𝕜 E v).radius = ⊤

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) : ∃ a ∈ Set.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) : ∃ a ∈ Set.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.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 : E → F) (p : FormalMultilinearSeries 𝕜 E F) (x : E) (r : ENNReal) : Prop

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.

• r_le : r ≤ p.radius
• r_pos : 0 < r
• hasSum : ∀ {y : E}, y ∈ EMetric.ball 0 r → HasSum (fun (n : ℕ) => (p n) fun (x : Fin n) => y) (f (x + y))

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 : E → F} {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 : E → F} {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 : E → F} {p : FormalMultilinearSeries 𝕜 E F} {x : E} {r : ENNReal} (self : HasFPowerSeriesOnBall f p x r) {y : E} : y ∈ EMetric.ball 0 r → HasSum (fun (n : ℕ) => (p n) fun (x : Fin n) => y) (f (x + y))

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

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

• HasFPowerSeriesAt f p x = ∃ (r : ENNReal), HasFPowerSeriesOnBall f p x r

def AnalyticAt (𝕜 : Type u_1) {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (f : E → F) (x : E) : Prop

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

• AnalyticAt 𝕜 f x = ∃ (p : FormalMultilinearSeries 𝕜 E F), HasFPowerSeriesAt f p x

def AnalyticOn (𝕜 : Type u_1) {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (f : E → F) (s : Set E) : Prop

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

• AnalyticOn 𝕜 f s = ∀ x ∈ s, AnalyticAt 𝕜 f x

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

theorem HasFPowerSeriesAt.analyticAt {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {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 : E → F} {p : FormalMultilinearSeries 𝕜 E F} {x : E} {r : ENNReal} (hf : HasFPowerSeriesOnBall f p x r) : AnalyticAt 𝕜 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 : E → F} {g : E → F} {p : FormalMultilinearSeries 𝕜 E F} {x : E} {r : ENNReal} (hf : HasFPowerSeriesOnBall f p x r) (hg : Set.EqOn f g (EMetric.ball x r)) : HasFPowerSeriesOnBall g p x r

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 : E → F} {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 HasFPowerSeriesOnBall.hasSum_sub {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {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 : E → F} {p : FormalMultilinearSeries 𝕜 E F} {x : E} {r : ENNReal} (hf : HasFPowerSeriesOnBall f p 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 : E → F} {p : FormalMultilinearSeries 𝕜 E F} {x : E} (hf : HasFPowerSeriesAt f p x) : 0 < p.radius

theorem HasFPowerSeriesOnBall.mono {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {p : FormalMultilinearSeries 𝕜 E F} {x : E} {r : ENNReal} {r' : ENNReal} (hf : HasFPowerSeriesOnBall f p x r) (r'_pos : 0 < r') (hr : r' ≤ r) : HasFPowerSeriesOnBall f p 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 : E → F} {g : E → F} {p : FormalMultilinearSeries 𝕜 E F} {x : E} (hf : HasFPowerSeriesAt f p x) (hg : (nhds x).EventuallyEq f g) : HasFPowerSeriesAt g p x

theorem HasFPowerSeriesAt.eventually {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {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 : E → F} {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 : E → F} {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 : E → F} {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 : E → F} {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 : E → F} {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 : E → F} {x : E} (hf : HasFPowerSeriesAt f 0 x) : ∀ᶠ (z : E) in nhds x, f z = 0

theorem hasFPowerSeriesOnBall_const {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {c : F} {e : E} : HasFPowerSeriesOnBall (fun (x : E) => c) (constFormalMultilinearSeries 𝕜 E c) e ⊤

theorem hasFPowerSeriesAt_const {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {c : F} {e : E} : HasFPowerSeriesAt (fun (x : E) => c) (constFormalMultilinearSeries 𝕜 E c) e

theorem analyticAt_const {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {x : E} {v : F} : AnalyticAt 𝕜 (fun (x : E) => v) x

theorem analyticOn_const {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {v : F} {s : Set E} : AnalyticOn 𝕜 (fun (x : E) => v) s

theorem HasFPowerSeriesOnBall.add {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {g : E → F} {pf : FormalMultilinearSeries 𝕜 E F} {pg : FormalMultilinearSeries 𝕜 E F} {x : E} {r : ENNReal} (hf : HasFPowerSeriesOnBall f pf x r) (hg : HasFPowerSeriesOnBall g pg x r) : HasFPowerSeriesOnBall (f + g) (pf + pg) x r

theorem HasFPowerSeriesAt.add {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {g : E → F} {pf : FormalMultilinearSeries 𝕜 E F} {pg : FormalMultilinearSeries 𝕜 E F} {x : E} (hf : HasFPowerSeriesAt f pf x) (hg : HasFPowerSeriesAt g pg x) : HasFPowerSeriesAt (f + g) (pf + pg) 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 : E → F} {g : E → F} {x : E} (hf : AnalyticAt 𝕜 f x) (hg : (nhds x).EventuallyEq f 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 : E → F} {g : E → F} {x : E} (h : (nhds x).EventuallyEq f g) : AnalyticAt 𝕜 f x ↔ AnalyticAt 𝕜 g x

theorem AnalyticAt.add {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {g : E → F} {x : E} (hf : AnalyticAt 𝕜 f x) (hg : AnalyticAt 𝕜 g x) : AnalyticAt 𝕜 (f + g) x

theorem HasFPowerSeriesOnBall.neg {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {pf : FormalMultilinearSeries 𝕜 E F} {x : E} {r : ENNReal} (hf : HasFPowerSeriesOnBall f pf x r) : HasFPowerSeriesOnBall (-f) (-pf) x r

theorem HasFPowerSeriesAt.neg {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {pf : FormalMultilinearSeries 𝕜 E F} {x : E} (hf : HasFPowerSeriesAt f pf x) : HasFPowerSeriesAt (-f) (-pf) x

theorem AnalyticAt.neg {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {x : E} (hf : AnalyticAt 𝕜 f x) : AnalyticAt 𝕜 (-f) x

theorem HasFPowerSeriesOnBall.sub {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {g : E → F} {pf : FormalMultilinearSeries 𝕜 E F} {pg : FormalMultilinearSeries 𝕜 E F} {x : E} {r : ENNReal} (hf : HasFPowerSeriesOnBall f pf x r) (hg : HasFPowerSeriesOnBall g pg x r) : HasFPowerSeriesOnBall (f - g) (pf - pg) x r

theorem HasFPowerSeriesAt.sub {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {g : E → F} {pf : FormalMultilinearSeries 𝕜 E F} {pg : FormalMultilinearSeries 𝕜 E F} {x : E} (hf : HasFPowerSeriesAt f pf x) (hg : HasFPowerSeriesAt g pg x) : HasFPowerSeriesAt (f - g) (pf - pg) x

theorem AnalyticAt.sub {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {g : E → F} {x : E} (hf : AnalyticAt 𝕜 f x) (hg : AnalyticAt 𝕜 g x) : AnalyticAt 𝕜 (f - g) 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 : E → F} {s : Set E} {t : Set E} (hf : AnalyticOn 𝕜 f t) (hst : s ⊆ t) : AnalyticOn 𝕜 f s

theorem AnalyticOn.congr' {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {g : E → F} {s : Set E} (hf : AnalyticOn 𝕜 f s) (hg : (nhdsSet s).EventuallyEq f g) : AnalyticOn 𝕜 g s

theorem analyticOn_congr' {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {g : E → F} {s : Set E} (h : (nhdsSet s).EventuallyEq f g) : AnalyticOn 𝕜 f s ↔ AnalyticOn 𝕜 g s

theorem AnalyticOn.congr {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {g : E → F} {s : Set E} (hs : IsOpen s) (hf : AnalyticOn 𝕜 f s) (hg : Set.EqOn f g s) : AnalyticOn 𝕜 g s

theorem analyticOn_congr {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {g : E → F} {s : Set E} (hs : IsOpen s) (h : Set.EqOn f g s) : AnalyticOn 𝕜 f s ↔ AnalyticOn 𝕜 g s

theorem AnalyticOn.add {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {g : E → F} {s : Set E} (hf : AnalyticOn 𝕜 f s) (hg : AnalyticOn 𝕜 g s) : AnalyticOn 𝕜 (f + g) s

theorem AnalyticOn.sub {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {g : E → F} {s : Set E} (hf : AnalyticOn 𝕜 f s) (hg : AnalyticOn 𝕜 g s) : AnalyticOn 𝕜 (f - g) s

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 : E → F} {pf : FormalMultilinearSeries 𝕜 E F} {x : E} {r : ENNReal} (hf : HasFPowerSeriesOnBall f pf x r) (v : Fin 0 → E) : (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 : E → F} {pf : FormalMultilinearSeries 𝕜 E F} {x : E} (hf : HasFPowerSeriesAt f pf x) (v : Fin 0 → E) : (pf 0) v = f x

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 : E → F} {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 : E → F} {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 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 : E → F} {p : FormalMultilinearSeries 𝕜 E F} {x : E} {r : ENNReal} {r' : NNReal} (hf : HasFPowerSeriesOnBall f p x r) (h : ↑r' < r) : ∃ a ∈ Set.Ioo 0 1, ∃ C > 0, ∀ y ∈ Metric.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 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 : E → F} {p : FormalMultilinearSeries 𝕜 E F} {x : E} {r : ENNReal} {r' : NNReal} (hf : HasFPowerSeriesOnBall f p x r) (h : ↑r' < r) : ∃ a ∈ Set.Ioo 0 1, ∃ C > 0, ∀ y ∈ Metric.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 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 : E → F} {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 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 : E → F} {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 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 : E → F} {p : FormalMultilinearSeries 𝕜 E F} {x : E} {r : ENNReal} {r' : ENNReal} (hf : HasFPowerSeriesOnBall f p x r) (hr : r' < r) : ∃ (C : ℝ), ∀ y ∈ EMetric.ball x r', ∀ z ∈ 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ₙ 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 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 : E → F} {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 HasFPowerSeriesOnBall.tendstoUniformlyOn {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {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 HasFPowerSeriesOnBall.tendstoLocallyUniformlyOn {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {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 HasFPowerSeriesOnBall.tendstoUniformlyOn' {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {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 HasFPowerSeriesOnBall.tendstoLocallyUniformlyOn' {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {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 HasFPowerSeriesOnBall.continuousOn {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {p : FormalMultilinearSeries 𝕜 E F} {x : E} {r : ENNReal} (hf : HasFPowerSeriesOnBall f p x r) : ContinuousOn f (EMetric.ball x r)

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

theorem HasFPowerSeriesAt.continuousAt {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {p : FormalMultilinearSeries 𝕜 E F} {x : E} (hf : HasFPowerSeriesAt f p x) : ContinuousAt f 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 : E → F} {x : E} (hf : AnalyticAt 𝕜 f x) : ContinuousAt f x

theorem AnalyticOn.continuousOn {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {s : Set E} (hf : AnalyticOn 𝕜 f s) : ContinuousOn f s

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

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 HasFPowerSeriesOnBall.sum {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {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

theorem FormalMultilinearSeries.continuousOn {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {p : FormalMultilinearSeries 𝕜 E F} [CompleteSpace F] : ContinuousOn p.sum (EMetric.ball 0 p.radius)

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

Uniqueness of power series

If a function f : E → F has two representations as power series at a point x : E, corresponding to formal multilinear series p₁ and p₂, then these representations agree term-by-term. That is, for any n : ℕ and y : E, p₁ n (fun i ↦ y) = p₂ n (fun i ↦ y). In the one-dimensional case, when f : 𝕜 → E, the continuous multilinear maps p₁ n and p₂ n are given by ContinuousMultilinearMap.mkPiRing, and hence are determined completely by the value of p₁ n (fun i ↦ 1), so p₁ = p₂. Consequently, the radius of convergence for one series can be transferred to the other.

theorem Asymptotics.IsBigO.continuousMultilinearMap_apply_eq_zero {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : ℕ} {p : ContinuousMultilinearMap 𝕜 (fun (i : Fin n) => E) F} (h : (fun (y : E) => p fun (x : Fin n) => y) =O[nhds 0] fun (y : E) => ‖y‖ ^ (n + 1)) (y : E) : (p fun (x : Fin n) => y) = 0

theorem HasFPowerSeriesAt.apply_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} {x : E} (h : HasFPowerSeriesAt 0 p x) (n : ℕ) (y : E) : ((p n) fun (x : Fin n) => y) = 0

If a formal multilinear series p represents the zero function at x : E, then the terms p n (fun i ↦ y) appearing in the sum are zero for any n : ℕ, y : E.

theorem HasFPowerSeriesAt.eq_zero {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] {p : FormalMultilinearSeries 𝕜 𝕜 E} {x : 𝕜} (h : HasFPowerSeriesAt 0 p x) : p = 0

A one-dimensional formal multilinear series representing the zero function is zero.

theorem HasFPowerSeriesAt.eq_formalMultilinearSeries {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] {p₁ : FormalMultilinearSeries 𝕜 𝕜 E} {p₂ : FormalMultilinearSeries 𝕜 𝕜 E} {f : 𝕜 → E} {x : 𝕜} (h₁ : HasFPowerSeriesAt f p₁ x) (h₂ : HasFPowerSeriesAt f p₂ x) : p₁ = p₂

One-dimensional formal multilinear series representing the same function are equal.

theorem HasFPowerSeriesAt.eq_formalMultilinearSeries_of_eventually {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] {p : FormalMultilinearSeries 𝕜 𝕜 E} {q : FormalMultilinearSeries 𝕜 𝕜 E} {f : 𝕜 → E} {g : 𝕜 → E} {x : 𝕜} (hp : HasFPowerSeriesAt f p x) (hq : HasFPowerSeriesAt g q x) (heq : ∀ᶠ (z : 𝕜) in nhds x, f z = g z) : p = q

theorem HasFPowerSeriesAt.eq_zero_of_eventually {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] {p : FormalMultilinearSeries 𝕜 𝕜 E} {f : 𝕜 → E} {x : 𝕜} (hp : HasFPowerSeriesAt f p x) (hf : (nhds x).EventuallyEq f 0) : p = 0

A one-dimensional formal multilinear series representing a locally zero function is zero.

theorem HasFPowerSeriesOnBall.exchange_radius {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] {p₁ : FormalMultilinearSeries 𝕜 𝕜 E} {p₂ : FormalMultilinearSeries 𝕜 𝕜 E} {f : 𝕜 → E} {r₁ : ENNReal} {r₂ : ENNReal} {x : 𝕜} (h₁ : HasFPowerSeriesOnBall f p₁ x r₁) (h₂ : HasFPowerSeriesOnBall f p₂ x r₂) : HasFPowerSeriesOnBall f p₁ x r₂

If a function f : 𝕜 → E has two power series representations at x, then the given radii in which convergence is guaranteed may be interchanged. This can be useful when the formal multilinear series in one representation has a particularly nice form, but the other has a larger radius.

theorem HasFPowerSeriesOnBall.r_eq_top_of_exists {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜 → E} {r : ENNReal} {x : 𝕜} {p : FormalMultilinearSeries 𝕜 𝕜 E} (h : HasFPowerSeriesOnBall f p x r) (h' : ∀ (r' : NNReal), 0 < r' → ∃ (p' : FormalMultilinearSeries 𝕜 𝕜 E), HasFPowerSeriesOnBall f p' x ↑r') : HasFPowerSeriesOnBall f p x ⊤

If a function f : 𝕜 → E has power series representation p on a ball of some radius and for each positive radius it has some power series representation, then p converges to f on the whole 𝕜.

Changing origin in a power series

If a function is analytic in a disk D(x, R), then it is analytic in any disk contained in that one. Indeed, one can write $$ f (x + y + z) = \sum_{n} p_n (y + z)^n = \sum_{n, k} \binom{n}{k} p_n y^{n-k} z^k = \sum_{k} \Bigl(\sum_{n} \binom{n}{k} p_n y^{n-k}\Bigr) z^k. $$ The corresponding power series has thus a k-th coefficient equal to $\sum_{n} \binom{n}{k} p_n y^{n-k}$. In the general case where pₙ is a multilinear map, this has to be interpreted suitably: instead of having a binomial coefficient, one should sum over all possible subsets s of Fin n of cardinality k, and attribute z to the indices in s and y to the indices outside of s.

In this paragraph, we implement this. The new power series is called p.changeOrigin y. Then, we check its convergence and the fact that its sum coincides with the original sum. The outcome of this discussion is that the set of points where a function is analytic is open.

def FormalMultilinearSeries.changeOriginSeriesTerm {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (p : FormalMultilinearSeries 𝕜 E F) (k : ℕ) (l : ℕ) (s : Finset (Fin (k + l))) (hs : s.card = l) : ContinuousMultilinearMap 𝕜 (fun (i : Fin l) => E) (ContinuousMultilinearMap 𝕜 (fun (i : Fin k) => E) F)

A term of FormalMultilinearSeries.changeOriginSeries.

Given a formal multilinear series p and a point x in its ball of convergence, p.changeOrigin x is a formal multilinear series such that p.sum (x+y) = (p.changeOrigin x).sum y when this makes sense. Each term of p.changeOrigin x is itself an analytic function of x given by the series p.changeOriginSeries. Each term in changeOriginSeries is the sum of changeOriginSeriesTerm's over all s of cardinality l. The definition is such that p.changeOriginSeriesTerm k l s hs (fun _ ↦ x) (fun _ ↦ y) = p (k + l) (s.piecewise (fun _ ↦ x) (fun _ ↦ y))

Equations

• p.changeOriginSeriesTerm k l s hs = let a := ContinuousMultilinearMap.curryFinFinset 𝕜 E F hs ⋯; a (p (k + l))

theorem FormalMultilinearSeries.changeOriginSeriesTerm_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) (k : ℕ) (l : ℕ) (s : Finset (Fin (k + l))) (hs : s.card = l) (x : E) (y : E) : (((p.changeOriginSeriesTerm k l s hs) fun (x_1 : Fin l) => x) fun (x : Fin k) => y) = (p (k + l)) (s.piecewise (fun (x_1 : Fin (k + l)) => x) fun (x : Fin (k + l)) => y)

@[simp]

theorem FormalMultilinearSeries.norm_changeOriginSeriesTerm {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (p : FormalMultilinearSeries 𝕜 E F) (k : ℕ) (l : ℕ) (s : Finset (Fin (k + l))) (hs : s.card = l) : ‖p.changeOriginSeriesTerm k l s hs‖ = ‖p (k + l)‖

@[simp]

theorem FormalMultilinearSeries.nnnorm_changeOriginSeriesTerm {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (p : FormalMultilinearSeries 𝕜 E F) (k : ℕ) (l : ℕ) (s : Finset (Fin (k + l))) (hs : s.card = l) : ‖p.changeOriginSeriesTerm k l s hs‖₊ = ‖p (k + l)‖₊

theorem FormalMultilinearSeries.nnnorm_changeOriginSeriesTerm_apply_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) (k : ℕ) (l : ℕ) (s : Finset (Fin (k + l))) (hs : s.card = l) (x : E) (y : E) : ‖((p.changeOriginSeriesTerm k l s hs) fun (x_1 : Fin l) => x) fun (x : Fin k) => y‖₊ ≤ ‖p (k + l)‖₊ * ‖x‖₊ ^ l * ‖y‖₊ ^ k

def FormalMultilinearSeries.changeOriginSeries {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (p : FormalMultilinearSeries 𝕜 E F) (k : ℕ) : FormalMultilinearSeries 𝕜 E (ContinuousMultilinearMap 𝕜 (fun (i : Fin k) => E) F)

The power series for f.changeOrigin k.

Given a formal multilinear series p and a point x in its ball of convergence, p.changeOrigin x is a formal multilinear series such that p.sum (x+y) = (p.changeOrigin x).sum y when this makes sense. Its k-th term is the sum of the series p.changeOriginSeries k.

Equations

• p.changeOriginSeries k l = Finset.univ.sum fun (s : { s : Finset (Fin (k + l)) // s.card = l }) => p.changeOriginSeriesTerm k l ↑s ⋯

theorem FormalMultilinearSeries.nnnorm_changeOriginSeries_le_tsum {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (p : FormalMultilinearSeries 𝕜 E F) (k : ℕ) (l : ℕ) : ‖p.changeOriginSeries k l‖₊ ≤ ∑' (x : { s : Finset (Fin (k + l)) // s.card = l }), ‖p (k + l)‖₊

theorem FormalMultilinearSeries.nnnorm_changeOriginSeries_apply_le_tsum {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (p : FormalMultilinearSeries 𝕜 E F) (k : ℕ) (l : ℕ) (x : E) : ‖(p.changeOriginSeries k l) fun (x_1 : Fin l) => x‖₊ ≤ ∑' (x_1 : { s : Finset (Fin (k + l)) // s.card = l }), ‖p (k + l)‖₊ * ‖x‖₊ ^ l

def FormalMultilinearSeries.changeOrigin {𝕜 : 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) : FormalMultilinearSeries 𝕜 E F

Changing the origin of a formal multilinear series p, so that p.sum (x+y) = (p.changeOrigin x).sum y when this makes sense.

Equations

• p.changeOrigin x k = (p.changeOriginSeries k).sum x

@[simp]

theorem FormalMultilinearSeries.changeOriginIndexEquiv_apply_snd (s : (k : ℕ) × (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l }) : (FormalMultilinearSeries.changeOriginIndexEquiv s).snd = ↑s.snd.snd

@[simp]

theorem FormalMultilinearSeries.changeOriginIndexEquiv_apply_fst (s : (k : ℕ) × (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l }) : (FormalMultilinearSeries.changeOriginIndexEquiv s).fst = s.fst + s.snd.fst

@[simp]

theorem FormalMultilinearSeries.changeOriginIndexEquiv_symm_apply_snd_fst (s : (n : ℕ) × Finset (Fin n)) : (FormalMultilinearSeries.changeOriginIndexEquiv.symm s).snd.fst = s.snd.card

@[simp]

theorem FormalMultilinearSeries.changeOriginIndexEquiv_symm_apply_snd_snd_coe (s : (n : ℕ) × Finset (Fin n)) : ↑(FormalMultilinearSeries.changeOriginIndexEquiv.symm s).snd.snd = Finset.map (Fin.castIso ⋯).toEmbedding s.snd

@[simp]

theorem FormalMultilinearSeries.changeOriginIndexEquiv_symm_apply_fst (s : (n : ℕ) × Finset (Fin n)) : (FormalMultilinearSeries.changeOriginIndexEquiv.symm s).fst = s.fst - s.snd.card

def FormalMultilinearSeries.changeOriginIndexEquiv : (k : ℕ) × (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l } ≃ (n : ℕ) × Finset (Fin n)

An auxiliary equivalence useful in the proofs about FormalMultilinearSeries.changeOriginSeries: the set of triples (k, l, s), where s is a Finset (Fin (k + l)) of cardinality l is equivalent to the set of pairs (n, s), where s is a Finset (Fin n).

The forward map sends (k, l, s) to (k + l, s) and the inverse map sends (n, s) to (n - Finset.card s, Finset.card s, s). The actual definition is less readable because of problems with non-definitional equalities.

Equations

• One or more equations did not get rendered due to their size.

theorem FormalMultilinearSeries.changeOriginSeriesTerm_changeOriginIndexEquiv_symm {𝕜 : 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} {y : E} (n : ℕ) (t : Finset (Fin n)) : let s := FormalMultilinearSeries.changeOriginIndexEquiv.symm ⟨n, t⟩; (((p.changeOriginSeriesTerm s.fst s.snd.fst ↑s.snd.snd ⋯) fun (x_1 : Fin s.snd.fst) => x) fun (x : Fin s.fst) => y) = (p n) (t.piecewise (fun (x_1 : Fin n) => x) fun (x : Fin n) => y)

theorem FormalMultilinearSeries.changeOriginSeries_summable_aux₁ {𝕜 : 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} {r' : NNReal} (hr : ↑r + ↑r' < p.radius) : Summable fun (s : (k : ℕ) × (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l }) => ‖p (s.fst + s.snd.fst)‖₊ * r ^ s.snd.fst * r' ^ s.fst

theorem FormalMultilinearSeries.changeOriginSeries_summable_aux₂ {𝕜 : 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} (hr : ↑r < p.radius) (k : ℕ) : Summable fun (s : (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l }) => ‖p (k + s.fst)‖₊ * r ^ s.fst

theorem FormalMultilinearSeries.changeOriginSeries_summable_aux₃ {𝕜 : 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} (hr : ↑r < p.radius) (k : ℕ) : Summable fun (l : ℕ) => ‖p.changeOriginSeries k l‖₊ * r ^ l

theorem FormalMultilinearSeries.le_changeOriginSeries_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) (k : ℕ) : p.radius ≤ (p.changeOriginSeries k).radius

theorem FormalMultilinearSeries.nnnorm_changeOrigin_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) {x : E} (k : ℕ) (h : ↑‖x‖₊ < p.radius) : ‖p.changeOrigin x k‖₊ ≤ ∑' (s : (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l }), ‖p (k + s.fst)‖₊ * ‖x‖₊ ^ s.fst

theorem FormalMultilinearSeries.changeOrigin_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) {x : E} : p.radius - ↑‖x‖₊ ≤ (p.changeOrigin x).radius

The radius of convergence of p.changeOrigin x is at least p.radius - ‖x‖. In other words, p.changeOrigin x is well defined on the largest ball contained in the original ball of convergence.

def FormalMultilinearSeries.derivSeries {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (p : FormalMultilinearSeries 𝕜 E F) : FormalMultilinearSeries 𝕜 E (E →L[𝕜] F)

derivSeries p is a power series for fderiv 𝕜 f if p is a power series for f, see HasFPowerSeriesOnBall.fderiv.

Equations

• One or more equations did not get rendered due to their size.

theorem FormalMultilinearSeries.hasFPowerSeriesOnBall_changeOrigin {𝕜 : 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) (k : ℕ) (hr : 0 < p.radius) : HasFPowerSeriesOnBall (fun (x : E) => p.changeOrigin x k) (p.changeOriginSeries k) 0 p.radius

theorem FormalMultilinearSeries.changeOrigin_eval {𝕜 : 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} {y : E} (h : ↑‖x‖₊ + ↑‖y‖₊ < p.radius) : (p.changeOrigin x).sum y = p.sum (x + y)

Summing the series p.changeOrigin x at a point y gives back p (x + y).

theorem FormalMultilinearSeries.analyticAt_changeOrigin {𝕜 : 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) (rp : p.radius > 0) (n : ℕ) : AnalyticAt 𝕜 (fun (x : E) => p.changeOrigin x n) 0

Power series terms are analytic as we vary the origin

theorem HasFPowerSeriesOnBall.changeOrigin {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace F] {f : E → F} {p : FormalMultilinearSeries 𝕜 E F} {x : E} {y : E} {r : ENNReal} (hf : HasFPowerSeriesOnBall f p x r) (h : ↑‖y‖₊ < r) : HasFPowerSeriesOnBall f (p.changeOrigin y) (x + y) (r - ↑‖y‖₊)

If a function admits a power series expansion p on a ball B (x, r), then it also admits a power series on any subball of this ball (even with a different center), given by p.changeOrigin.

theorem HasFPowerSeriesOnBall.analyticAt_of_mem {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace F] {f : E → F} {p : FormalMultilinearSeries 𝕜 E F} {x : E} {y : E} {r : ENNReal} (hf : HasFPowerSeriesOnBall f p x r) (h : y ∈ EMetric.ball x r) : AnalyticAt 𝕜 f y

If a function admits a power series expansion p on an open ball B (x, r), then it is analytic at every point of this ball.

theorem HasFPowerSeriesOnBall.analyticOn {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace F] {f : E → F} {p : FormalMultilinearSeries 𝕜 E F} {x : E} {r : ENNReal} (hf : HasFPowerSeriesOnBall f p x r) : AnalyticOn 𝕜 f (EMetric.ball x r)

theorem isOpen_analyticAt (𝕜 : Type u_1) {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace F] (f : E → F) : IsOpen {x : E | AnalyticAt 𝕜 f x}

For any function f from a normed vector space to a Banach space, the set of points x such that f is analytic at x is open.

theorem AnalyticAt.eventually_analyticAt {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace F] {f : E → F} {x : E} (h : AnalyticAt 𝕜 f x) : ∀ᶠ (y : E) in nhds x, AnalyticAt 𝕜 f y

theorem AnalyticAt.exists_mem_nhds_analyticOn {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace F] {f : E → F} {x : E} (h : AnalyticAt 𝕜 f x) : ∃ s ∈ nhds x, AnalyticOn 𝕜 f s

theorem AnalyticAt.exists_ball_analyticOn {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace F] {f : E → F} {x : E} (h : AnalyticAt 𝕜 f x) : ∃ (r : ℝ), 0 < r ∧ AnalyticOn 𝕜 f (Metric.ball x r)

If we're analytic at a point, we're analytic in a nonempty ball

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)