structure FormalPowerSeriesCenteredAt (a : ℝ) : Type

Definition 4.1.1: For a ∈ ℝ, a formal power series centered at a is given by a sequence of real coefficients (c_n)_{n≥0}, corresponding to the formal expression ∑_{n=0}^∞ c_n (x - a)^n in the indeterminate x; its nth coefficient is coeff n.

• coeff : ℕ → ℝ

noncomputable def FormalPowerSeriesCenteredAt.radiusOfConvergence {a : ℝ} (f : FormalPowerSeriesCenteredAt a) : ENNReal

Definition 4.1.2 (Radius of convergence): for a formal power series ∑_{n=0}^∞ c_n (x-a)^n, let L = limsup_{n→∞} |c_n|^(1/n) (valued in [0, +∞]); the radius of convergence is R = 1 / L, with the conventions 1/0 = +∞ and 1/(+∞) = 0.

Equations

• f.radiusOfConvergence = (FormalMultilinearSeries.ofScalars ℝ f.coeff).radius

theorem FormalPowerSeriesCenteredAt.radiusOfConvergence_eq_ofScalarsRadius {a : ℝ} (f : FormalPowerSeriesCenteredAt a) : f.radiusOfConvergence = (FormalMultilinearSeries.ofScalars ℝ f.coeff).radius

Helper for Theorem 4.1.1: radiusOfConvergence is the radius of the associated scalar formal multilinear series.

noncomputable def reciprocalOneSub (x : { x : ℝ // x ≠ 1 }) : ℝ

Definition 4.1.3: Define the function f : ℝ \ {1} → ℝ by f(x) = 1 / (1 - x).

Equations

• reciprocalOneSub x = 1 / (1 - ↑x)

theorem ne_one_of_mem_Ioo_neg_one_one {x : ℝ} (hx : x ∈ Set.Ioo (-1) 1) : x ≠ 1

Points of (-1, 1) are distinct from 1.

noncomputable def reciprocalOneSub_ext : ℝ → ℝ

The total real extension of x ↦ 1 / (1 - x).

Equations

• reciprocalOneSub_ext y = 1 / (1 - y)

theorem reciprocalOneSub_ext_eq (x : ℝ) (hx : x ≠ 1) : reciprocalOneSub_ext x = reciprocalOneSub ⟨x, hx⟩

The total extension agrees with reciprocalOneSub away from 1.

theorem geometric_series_eq_reciprocalOneSub_and_analyticAt_zero : (∀ x ∈ Set.Ioo (-1) 1, ∑' (n : ℕ), x ^ n = 1 / (1 - x) ∧ 1 / (1 - x) = reciprocalOneSub_ext x) ∧ AnalyticAt ℝ reciprocalOneSub_ext 0

Lemma 4.1.1: For every x ∈ (-1, 1), one has ∑' n, x^n = 1/(1-x) = f(x) (with f = reciprocalOneSub), and in particular f is real analytic at 0.

theorem ne_one_of_mem_Ioo_one_three {x : ℝ} (hx : x ∈ Set.Ioo 1 3) : x ≠ 1

Points of (1, 3) are distinct from 1.

theorem helperForLemma_4_1_2_abs_shift_lt_one {x : ℝ} (hx : x ∈ Set.Ioo 1 3) : |x - 2| < 1

Helper for Lemma 4.1.2: for x ∈ (1,3), the shifted variable satisfies |x-2| < 1.

theorem helperForLemma_4_1_2_alternating_term_as_neg_geometric (x : ℝ) (n : ℕ) : (-1) ^ (n + 1) * (x - 2) ^ n = -(-1 * (x - 2)) ^ n

Helper for Lemma 4.1.2: rewrite each shifted alternating term as a negated geometric term.

theorem helperForLemma_4_1_2_tsum_identity {x : ℝ} (hx : x ∈ Set.Ioo 1 3) : ∑' (n : ℕ), (-1) ^ (n + 1) * (x - 2) ^ n = 1 / (1 - x)

Helper for Lemma 4.1.2: the shifted alternating geometric series sums to 1/(1-x) on (1,3).

theorem helperForLemma_4_1_2_analyticAt_two : AnalyticAt ℝ reciprocalOneSub_ext 2

Helper for Lemma 4.1.2: the extension reciprocalOneSub_ext is real-analytic at 2.

theorem shifted_geometric_series_eq_reciprocalOneSub_and_analyticAt_two : (∀ (x : ℝ) (hx : x ∈ Set.Ioo 1 3), ∑' (n : ℕ), (-1) ^ (n + 1) * (x - 2) ^ n = 1 / (1 - x) ∧ 1 / (1 - x) = reciprocalOneSub ⟨x, ⋯⟩) ∧ AnalyticAt ℝ reciprocalOneSub_ext 2

Lemma 4.1.2: For every x ∈ (1, 3), one has ∑' n, (-1)^(n+1) (x-2)^n = 1/(1-x) = f(x) (with f = reciprocalOneSub); in particular, f is real analytic at 2.

theorem FormalPowerSeriesCenteredAt.helperForTheorem_4_1_3_shiftedHasFPowerSeriesOnBall {a : ℝ} (p : FormalMultilinearSeries ℝ ℝ ℝ) (hpos : 0 < p.radius) : HasFPowerSeriesOnBall (fun (x : ℝ) => p.sum (x - a)) p a p.radius

Helper for Theorem 4.1.3: translate a scalar formal multilinear series to a ball expansion centered at a by composition with subtraction.

theorem FormalPowerSeriesCenteredAt.helperForTheorem_4_1_3_existsStrictIntermediateRadius {a r : ℝ} (f : FormalPowerSeriesCenteredAt a) (hrR : ENNReal.ofReal r < f.radiusOfConvergence) : ∃ (ρ : NNReal), ENNReal.ofReal r < ↑ρ ∧ ↑ρ < f.radiusOfConvergence

Helper for Theorem 4.1.3: pick an intermediate NNReal radius strictly between r and the convergence radius.

theorem FormalPowerSeriesCenteredAt.helperForTheorem_4_1_3_Icc_subset_ball {a r ρ : ℝ} (hrρ : r < ρ) : Set.Icc (a - r) (a + r) ⊆ Metric.ball a ρ

Helper for Theorem 4.1.3: if r < ρ, then [a-r, a+r] lies in the open ball Metric.ball a ρ.

theorem FormalPowerSeriesCenteredAt.helperForTheorem_4_1_3_rewriteSeriesForms {a : ℝ} (f : FormalPowerSeriesCenteredAt a) : ((fun (N : ℕ) (x : ℝ) => (FormalMultilinearSeries.ofScalars ℝ f.coeff).partialSum N (x - a)) = fun (N : ℕ) (x : ℝ) => ∑ n ∈ Finset.range N, f.coeff n * (x - a) ^ n) ∧ (fun (x : ℝ) => (FormalMultilinearSeries.ofScalars ℝ f.coeff).sum (x - a)) = fun (x : ℝ) => ∑' (n : ℕ), f.coeff n * (x - a) ^ n

Helper for Theorem 4.1.3: rewrite both partial sums and total sums in textbook coefficient form.

theorem FormalPowerSeriesCenteredAt.helperForTheorem_4_1_3_continuousAt_inside_radius {a x : ℝ} (f : FormalPowerSeriesCenteredAt a) (hx : ENNReal.ofReal |x - a| < f.radiusOfConvergence) : ContinuousAt (fun (y : ℝ) => ∑' (n : ℕ), f.coeff n * (y - a) ^ n) x

Helper for Theorem 4.1.3: inside the convergence radius, the scalar-series sum function is continuous.

theorem FormalPowerSeriesCenteredAt.helperForTheorem_4_1_1_radius_eq_ofScalarsRadius {a : ℝ} (f : FormalPowerSeriesCenteredAt a) : f.radiusOfConvergence = (FormalMultilinearSeries.ofScalars ℝ f.coeff).radius

Helper for Theorem 4.1.1: identify the textbook radius with the formal multilinear-series radius.

theorem FormalPowerSeriesCenteredAt.helperForTheorem_4_1_1_tendsto_weightedNorm_zero_of_summable {a x : ℝ} (f : FormalPowerSeriesCenteredAt a) (hs : Summable fun (n : ℕ) => f.coeff n * (x - a) ^ n) : Filter.Tendsto (fun (n : ℕ) => ‖f.coeff n‖ * ‖x - a‖ ^ n) Filter.atTop (nhds 0)

Helper for Theorem 4.1.1: summability of scalar terms forces weighted norms to tend to 0.

theorem FormalPowerSeriesCenteredAt.helperForTheorem_4_1_1_ofRealAbs_le_radius_of_summable {a x : ℝ} (f : FormalPowerSeriesCenteredAt a) (hs : Summable fun (n : ℕ) => f.coeff n * (x - a) ^ n) : ENNReal.ofReal |x - a| ≤ f.radiusOfConvergence

Helper for Theorem 4.1.1: if the scalar series at x is summable, then |x-a| lies within the radius.

theorem FormalPowerSeriesCenteredAt.diverges_outside_radius {a x : ℝ} (f : FormalPowerSeriesCenteredAt a) (hx : f.radiusOfConvergence < ENNReal.ofReal |x - a|) : ¬Summable fun (n : ℕ) => f.coeff n * (x - a) ^ n

Theorem 4.1.1: (Divergence outside the radius of convergence) for a power series with center a and coefficients c_n, if |x - a| > R where R is the radius of convergence, then ∑ n, c_n * (x - a)^n diverges at x.

theorem FormalPowerSeriesCenteredAt.converges_absolutely_inside_radius {a x : ℝ} (f : FormalPowerSeriesCenteredAt a) (hx : ENNReal.ofReal |x - a| < f.radiusOfConvergence) : Summable fun (n : ℕ) => |f.coeff n * (x - a) ^ n|

Theorem 4.1.2: If |x - a| < R for a power series ∑ n, c_n (x-a)^n with radius of convergence R, then ∑ n, c_n (x-a)^n converges absolutely at x.

theorem FormalPowerSeriesCenteredAt.uniformly_converges_on_compact_subintervals {a r : ℝ} (f : FormalPowerSeriesCenteredAt a) (hr0 : 0 < r) (hrR : ENNReal.ofReal r < f.radiusOfConvergence) : TendstoUniformlyOn (fun (N : ℕ) (x : ℝ) => ∑ n ∈ Finset.range N, f.coeff n * (x - a) ^ n) (fun (x : ℝ) => ∑' (n : ℕ), f.coeff n * (x - a) ^ n) Filter.atTop (Set.Icc (a - r) (a + r)) ∧ ∀ (x : ℝ), ENNReal.ofReal |x - a| < f.radiusOfConvergence → ContinuousAt (fun (y : ℝ) => ∑' (n : ℕ), f.coeff n * (y - a) ^ n) x

Theorem 4.1.3: (Uniform convergence on compact subintervals) for a power series centered at a, if 0 < r < R (with R the radius of convergence), then the partial sums converge uniformly on [a-r, a+r] to the series sum; in particular, the sum function is continuous at every point where |x-a| < R.

theorem FormalPowerSeriesCenteredAt.helperForTheorem_4_1_4_ball_eq_insideRadiusSet {a : ℝ} (f : FormalPowerSeriesCenteredAt a) : EMetric.ball a (FormalMultilinearSeries.ofScalars ℝ f.coeff).radius = {x : ℝ | ENNReal.ofReal |x - a| < f.radiusOfConvergence}

Helper for Theorem 4.1.4: identify the convergence-radius set with the corresponding emetric ball.

theorem FormalPowerSeriesCenteredAt.helperForTheorem_4_1_4_derivHasFPowerSeriesOnBall {a : ℝ} (f : FormalPowerSeriesCenteredAt a) (hRpos : 0 < f.radiusOfConvergence) : HasFPowerSeriesOnBall (fun (x : ℝ) => deriv (fun (y : ℝ) => (FormalMultilinearSeries.ofScalars ℝ f.coeff).sum (y - a)) x) (((ContinuousLinearMap.apply ℝ ℝ) 1).compFormalMultilinearSeries (FormalMultilinearSeries.ofScalars ℝ f.coeff).derivSeries) a (FormalMultilinearSeries.ofScalars ℝ f.coeff).radius

Helper for Theorem 4.1.4: derivative power-series expansion on the convergence ball.

theorem FormalPowerSeriesCenteredAt.helperForTheorem_4_1_4_rewriteDerivedPartialSums {a : ℝ} (f : FormalPowerSeriesCenteredAt a) : (fun (N : ℕ) (x : ℝ) => (((ContinuousLinearMap.apply ℝ ℝ) 1).compFormalMultilinearSeries (FormalMultilinearSeries.ofScalars ℝ f.coeff).derivSeries).partialSum N (x - a)) = fun (N : ℕ) (x : ℝ) => ∑ n ∈ Finset.range N, (↑n + 1) * f.coeff (n + 1) * (x - a) ^ n

Helper for Theorem 4.1.4: rewrite derivative-series partial sums in textbook coefficient form.

theorem FormalPowerSeriesCenteredAt.helperForTheorem_4_1_4_differentiableOn_insideRadius {a : ℝ} (f : FormalPowerSeriesCenteredAt a) (hRpos : 0 < f.radiusOfConvergence) : DifferentiableOn ℝ (fun (x : ℝ) => ∑' (n : ℕ), f.coeff n * (x - a) ^ n) {x : ℝ | ENNReal.ofReal |x - a| < f.radiusOfConvergence}

Helper for Theorem 4.1.4: differentiability of the power-series sum on its open convergence interval.

theorem FormalPowerSeriesCenteredAt.term_by_term_differentiation_of_power_series {a : ℝ} (f : FormalPowerSeriesCenteredAt a) (hRpos : 0 < f.radiusOfConvergence) : DifferentiableOn ℝ (fun (x : ℝ) => ∑' (n : ℕ), f.coeff n * (x - a) ^ n) {x : ℝ | ENNReal.ofReal |x - a| < f.radiusOfConvergence} ∧ ∀ (r : ℝ), 0 < r → ENNReal.ofReal r < f.radiusOfConvergence → TendstoUniformlyOn (fun (N : ℕ) (x : ℝ) => ∑ n ∈ Finset.range N, (↑n + 1) * f.coeff (n + 1) * (x - a) ^ n) (fun (x : ℝ) => deriv (fun (y : ℝ) => ∑' (n : ℕ), f.coeff n * (y - a) ^ n) x) Filter.atTop (Set.Icc (a - r) (a + r))

Theorem 4.1.4: (Term-by-term differentiation of a power series): if a power series centered at a has positive radius of convergence R, then its sum function is differentiable at every point x with |x - a| < R; moreover, for every r with 0 < r < R, the derived series converges uniformly to the derivative on [a - r, a + r].

theorem FormalPowerSeriesCenteredAt.helperForTheorem_4_1_5_endpoint_radius_bounds {a y z : ℝ} (f : FormalPowerSeriesCenteredAt a) (hsub : Set.uIcc y z ⊆ {x : ℝ | ENNReal.ofReal |x - a| < f.radiusOfConvergence}) : ENNReal.ofReal |y - a| < f.radiusOfConvergence ∧ ENNReal.ofReal |z - a| < f.radiusOfConvergence

Helper for Theorem 4.1.5: endpoints of Set.uIcc y z satisfy the same radius bound inherited from the interval hypothesis.

theorem FormalPowerSeriesCenteredAt.helperForTheorem_4_1_5_abs_sub_le_maxEndpoint {a y z x : ℝ} (hx : x ∈ Set.uIcc y z) : |x - a| ≤ max |y - a| |z - a|

Helper for Theorem 4.1.5: every point of Set.uIcc y z has distance to a bounded by the maximum endpoint distance.

theorem FormalPowerSeriesCenteredAt.helperForTheorem_4_1_5_term_continuous {a : ℝ} (f : FormalPowerSeriesCenteredAt a) (n : ℕ) : Continuous fun (x : ℝ) => f.coeff n * (x - a) ^ n

Helper for Theorem 4.1.5: each monomial term x ↦ c_n (x-a)^n is continuous.

noncomputable def FormalPowerSeriesCenteredAt.helperForTheorem_4_1_5_termContinuousMap {a : ℝ} (f : FormalPowerSeriesCenteredAt a) (n : ℕ) : C(ℝ, ℝ)

Helper for Theorem 4.1.5: package the nth term as a continuous map on ℝ.

Equations

• f.helperForTheorem_4_1_5_termContinuousMap n = { toFun := fun (x : ℝ) => f.coeff n * (x - a) ^ n, continuous_toFun := ⋯ }

theorem FormalPowerSeriesCenteredAt.helperForTheorem_4_1_5_summable_restrictedTermNorms {a y z : ℝ} (f : FormalPowerSeriesCenteredAt a) (hsub : Set.uIcc y z ⊆ {x : ℝ | ENNReal.ofReal |x - a| < f.radiusOfConvergence}) : Summable fun (n : ℕ) => ‖ContinuousMap.restrict (↑{ carrier := Set.uIcc y z, isCompact' := ⋯ }) (f.helperForTheorem_4_1_5_termContinuousMap n)‖

Helper for Theorem 4.1.5: the supremum norms of restricted terms on Set.uIcc y z form a summable series.

theorem FormalPowerSeriesCenteredAt.helperForTheorem_4_1_5_intervalIntegral_term_formula {a y z : ℝ} (f : FormalPowerSeriesCenteredAt a) (n : ℕ) : ∫ (x : ℝ) in y..z, f.coeff n * (x - a) ^ n = f.coeff n * (((z - a) ^ (n + 1) - (y - a) ^ (n + 1)) / (↑n + 1))

Helper for Theorem 4.1.5: the interval integral of each term has the textbook antiderivative form.

theorem FormalPowerSeriesCenteredAt.term_by_term_integration_of_power_series {a y z : ℝ} (f : FormalPowerSeriesCenteredAt a) (hRpos : 0 < f.radiusOfConvergence) (hsub : Set.uIcc y z ⊆ {x : ℝ | ENNReal.ofReal |x - a| < f.radiusOfConvergence}) : ∫ (x : ℝ) in y..z, ∑' (n : ℕ), f.coeff n * (x - a) ^ n = ∑' (n : ℕ), f.coeff n * (((z - a) ^ (n + 1) - (y - a) ^ (n + 1)) / (↑n + 1))

Theorem 4.1.5: (Term-by-term integration of a power series) let f(x) = ∑' n, c_n (x-a)^n be a power series with positive radius of convergence; for any closed interval [y, z] contained in the convergence region, ∫ x in y..z, f x equals the term-by-term antiderivative series evaluated at z and y.