theorem helperForProposition_4_2_6_contDiff_shiftedMonomial_constMul (n : ℕ) (a c : ℝ) : ContDiff ℝ ⊤ fun (x : ℝ) => c * (x - a) ^ n

Helper for Proposition 4.2.6: smoothness of the shifted monomial with constant factor.

theorem helperForProposition_4_2_6_iteratedDeriv_shiftedMonomial_fallingProd (n k : ℕ) (a x : ℝ) : iteratedDeriv k (fun (y : ℝ) => (y - a) ^ n) x = (∏ i ∈ Finset.range k, (↑n - ↑i)) * (x - a) ^ (n - k)

Helper for Proposition 4.2.6: explicit iterated derivative formula for (x - a)^n with falling-product coefficient.

theorem helperForProposition_4_2_6_iteratedDeriv_constMul_shiftedMonomial_fallingProd (n k : ℕ) (a c x : ℝ) : iteratedDeriv k (fun (y : ℝ) => c * (y - a) ^ n) x = c * ((∏ i ∈ Finset.range k, (↑n - ↑i)) * (x - a) ^ (n - k))

Helper for Proposition 4.2.6: pull the constant factor c out of iterated derivatives of the shifted monomial.

theorem helperForProposition_4_2_6_fallingProd_eq_factorialRatio (n : ℕ) {k : ℕ} (hk : k ≤ n) : ∏ i ∈ Finset.range k, (↑n - ↑i) = ↑n.factorial / ↑(n - k).factorial

Helper for Proposition 4.2.6: convert the falling-product coefficient to the factorial-ratio coefficient when k ≤ n.

theorem helperForProposition_4_2_6_fallingProd_eq_zero_of_lt (n : ℕ) {k : ℕ} (hnk : n < k) : ∏ i ∈ Finset.range k, (↑n - ↑i) = 0

Helper for Proposition 4.2.6: the falling-product coefficient vanishes when k > n.

theorem iteratedDeriv_monomial_shifted_const_mul (n : ℕ) (a c : ℝ) : (ContDiff ℝ ⊤ fun (x : ℝ) => c * (x - a) ^ n) ∧ (∀ k ≤ n, ∀ (x : ℝ), iteratedDeriv k (fun (y : ℝ) => c * (y - a) ^ n) x = c * (↑n.factorial / ↑(n - k).factorial) * (x - a) ^ (n - k)) ∧ ∀ (k : ℕ), n < k → ∀ (x : ℝ), iteratedDeriv k (fun (y : ℝ) => c * (y - a) ^ n) x = 0

Proposition 4.2.6: let n : ℕ and a c : ℝ, and define f(x) = c * (x - a)^n. Then f is infinitely differentiable on ℝ. Moreover, for every k with k ≤ n, iteratedDeriv k f x = c * (n! / (n-k)!) * (x-a)^(n-k) for all x : ℝ, and for every k > n, iteratedDeriv k f x = 0 for all x : ℝ.

theorem shiftedPower_eq_sum_factorial_ratio_mul_shiftedPowers (a b : ℝ) (n : ℕ) (x : ℝ) : (x - a) ^ n = ∑ m ∈ Finset.range (n + 1), ↑n.factorial / (↑m.factorial * ↑(n - m).factorial) * (b - a) ^ (n - m) * (x - b) ^ m

Proposition 4.2.7: let a, b ∈ ℝ and n ≥ 0 be an integer. Then for every x ∈ ℝ, (x - a)^n = ∑_{m=0}^n (n! / (m!(n-m)!)) (b - a)^(n-m) (x - b)^m.

theorem helperForProposition_4_2_8_absRatio_lt_one (r x : ℝ) (hr : 0 < r) (hx : |x| < r) : |x / r| < 1

Helper for Proposition 4.2.8: convert |x| < r with r > 0 into the geometric-series ratio bound |x / r| < 1.

theorem helperForProposition_4_2_8_geometricRatioPow_rewrite (r x : ℝ) : (fun (n : ℕ) => (x / r) ^ n) = fun (n : ℕ) => x ^ n * r⁻¹ ^ n

Helper for Proposition 4.2.8: rewrite powers of x / r into x^n * (r⁻¹)^n.

theorem helperForProposition_4_2_8_scaledFraction_eq_geometricClosedForm (r x : ℝ) (hr : 0 < r) (hx : |x| < r) : r / (r - x) = (1 - x / r)⁻¹

Helper for Proposition 4.2.8: identify the scaled rational expression with the closed form of the geometric series.

theorem scaledGeometricSeries_tsum_eq_r_div_r_sub (r x : ℝ) (hr : 0 < r) (hx : |x| < r) : r / (r - x) = ∑' (n : ℕ), x ^ n * r⁻¹ ^ n

Proposition 4.2.8: if r > 0 and |x| < r, then r / (r - x) = ∑' n = 0..∞, x^n r^{-n}.

theorem helperForProposition_4_2_9_factorialRatioTerm_eq_scaledChooseGeometricTerm (r x : ℝ) (m n : ℕ) : ↑(n + m).factorial / (↑m.factorial * ↑n.factorial) * x ^ n * r⁻¹ ^ (n + m) = r⁻¹ ^ m * (↑((n + m).choose m) * (x / r) ^ n)

Helper for Proposition 4.2.9: rewrite the factorial-ratio summand into a constant multiple of the standard choose-geometric term.

theorem helperForProposition_4_2_9_lhs_eq_scaledClosedForm (r x : ℝ) (m : ℕ) (hr : 0 < r) (hx : |x| < r) : r / (r - x) ^ (m + 1) = r⁻¹ ^ m * (1 / (1 - x / r) ^ (m + 1))

Helper for Proposition 4.2.9: rewrite the left-hand side as the scaled closed form matching the choose-geometric generating function.

theorem helperForProposition_4_2_9_tsum_targetTerm_eq_scaledClosedForm (r x : ℝ) (m : ℕ) (hr : 0 < r) (hx : |x| < r) : ∑' (n : ℕ), ↑(n + m).factorial / (↑m.factorial * ↑n.factorial) * x ^ n * r⁻¹ ^ (n + m) = r⁻¹ ^ m * (1 / (1 - x / r) ^ (m + 1))

Helper for Proposition 4.2.9: evaluate the reindexed factorial-ratio series as the same scaled closed form.

theorem helperForProposition_4_2_9_summable_abs_targetTerm (r x : ℝ) (m : ℕ) (hr : 0 < r) (hx : |x| < r) : Summable fun (n : ℕ) => |↑(n + m).factorial / (↑m.factorial * ↑n.factorial) * x ^ n * r⁻¹ ^ (n + m)|

Helper for Proposition 4.2.9: absolute convergence of the reindexed factorial-ratio series for |x| < r.

theorem scaledGeometricSeries_higherDerivative_tsum_and_absConvergence (r x : ℝ) (m : ℕ) (hr : 0 < r) (hx : |x| < r) : r / (r - x) ^ (m + 1) = ∑' (n : ℕ), ↑(n + m).factorial / (↑m.factorial * ↑n.factorial) * x ^ n * r⁻¹ ^ (n + m) ∧ Summable fun (n : ℕ) => |↑(n + m).factorial / (↑m.factorial * ↑n.factorial) * x ^ n * r⁻¹ ^ (n + m)|

Proposition 4.2.9: if r > 0, m : ℕ, and |x| < r, then r / (r - x)^(m+1) equals the binomial-coefficient power series, written in the reindexed form ∑' n, ((n+m)!/(m!n!)) x^n r^{-(n+m)} (equivalent to summing from n = m); moreover this series converges absolutely for every such x.

theorem helperForProposition_4_2_10_interval_left_right_strict (b s : ℝ) (hs : 0 < s) : b - s < b + s

Helper for Proposition 4.2.10: if s > 0 then (b - s, b + s) is nonempty.

theorem helperForProposition_4_2_10_endpoint_bounds_of_Ioo_subset (a0 b r s : ℝ) (hs : 0 < s) (hsub : Set.Ioo (b - s) (b + s) ⊆ Set.Ioo (a0 - r) (a0 + r)) : a0 - r ≤ b - s ∧ b + s ≤ a0 + r

Helper for Proposition 4.2.10: inclusion of open intervals yields endpoint bounds.

theorem helperForProposition_4_2_10_abs_le_radius_subradius (a0 b r s : ℝ) (hleft : a0 - r ≤ b - s) (hright : b + s ≤ a0 + r) : |a0 - b| ≤ r - s

Helper for Proposition 4.2.10: endpoint bounds control center distance by r - s.

theorem helperForProposition_4_2_10_abs_lt_radius_of_subradius_bound (a0 b r s : ℝ) (habs : |a0 - b| ≤ r - s) (hs : 0 < s) : |a0 - b| < r

Helper for Proposition 4.2.10: a bound by r - s improves to a strict bound by r.

theorem center_distance_le_radius_subradius_of_interval_subset {E : Set ℝ} (a : ↑E) (f : ↑E → ℝ) (hanalytic : IsRealAnalyticAt E f a) {r : ℝ} (hr : 0 < r) (c : ℕ → ℝ) (hI : Set.Ioo (↑a - r) (↑a + r) ⊆ E) (hsummable : ∀ x ∈ Set.Ioo (↑a - r) (↑a + r), Summable fun (n : ℕ) => c n * (x - ↑a) ^ n) (hpowerSeries : ∀ (x : ℝ) (hx : x ∈ Set.Ioo (↑a - r) (↑a + r)), f ⟨x, ⋯⟩ = ∑' (n : ℕ), c n * (x - ↑a) ^ n) {b s : ℝ} (hs : 0 < s) (hsub : Set.Ioo (b - s) (b + s) ⊆ Set.Ioo (↑a - r) (↑a + r)) : |↑a - b| ≤ r - s ∧ |↑a - b| < r

Proposition 4.2.10: let E ⊆ ℝ, let a be an interior point of E, and let f : E → ℝ be real analytic at a with a power-series expansion f(x) = ∑' n, c n * (x-a)^n converging for all x ∈ (a-r, a+r) for some r > 0. If (b-s, b+s) with s > 0 is any open interval contained in (a-r, a+r), then |a-b| ≤ r-s; in particular |a-b| < r.

theorem helperForProposition_4_2_11_subradius_point_mem_interval (a r ε : ℝ) (hr : 0 < r) (hε0 : 0 < ε) (hεr : ε < r) : a + (r - ε) ∈ Set.Ioo (a - r) (a + r)

Helper for Proposition 4.2.11: the point a + (r - ε) lies in (a-r, a+r) whenever 0 < ε < r.

theorem helperForProposition_4_2_11_summable_scaled_terms_at_subradius {E : Set ℝ} (a : ↑E) {r ε : ℝ} (c : ℕ → ℝ) (hsummable : ∀ x ∈ Set.Ioo (↑a - r) (↑a + r), Summable fun (n : ℕ) => c n * (x - ↑a) ^ n) (hr : 0 < r) (hε0 : 0 < ε) (hεr : ε < r) : Summable fun (n : ℕ) => c n * (r - ε) ^ n

Helper for Proposition 4.2.11: evaluating the interval summability hypothesis at x = a + (r - ε) yields summability of n ↦ c n * (r - ε)^n.

theorem helperForProposition_4_2_11_exists_abs_bound_of_summable (u : ℕ → ℝ) (hu : Summable u) : ∃ (B : ℝ), ∀ (n : ℕ), |u n| ≤ B

Helper for Proposition 4.2.11: every summable real sequence has a uniform absolute-value bound.

theorem helperForProposition_4_2_11_coeff_bound_from_scaled_bound (c : ℕ → ℝ) {ρ K : ℝ} (hρ : 0 < ρ) (hK : ∀ (n : ℕ), |c n * ρ ^ n| ≤ K) (n : ℕ) : |c n| ≤ K * ρ⁻¹ ^ n

Helper for Proposition 4.2.11: from a uniform bound on |c n * ρ^n|, recover a coefficient bound with inverse powers.

theorem powerSeries_coeff_norm_le_of_subradius {E : Set ℝ} (a : ↑E) (f : ↑E → ℝ) (hanalytic : IsRealAnalyticAt E f a) {r : ℝ} (hr : 0 < r) (c : ℕ → ℝ) (hI : Set.Ioo (↑a - r) (↑a + r) ⊆ E) (hsummable : ∀ x ∈ Set.Ioo (↑a - r) (↑a + r), Summable fun (n : ℕ) => c n * (x - ↑a) ^ n) (hpowerSeries : ∀ (x : ℝ) (hx : x ∈ Set.Ioo (↑a - r) (↑a + r)), f ⟨x, ⋯⟩ = ∑' (n : ℕ), c n * (x - ↑a) ^ n) (ε : ℝ) (hε0 : 0 < ε) (hεr : ε < r) : ∃ (C : ℝ), 0 < C ∧ ∀ (n : ℕ), |c n| ≤ C * (r - ε)⁻¹ ^ n

Proposition 4.2.11: under the same hypotheses and notation as the preceding power-series setup, for every ε with 0 < ε < r there exists C > 0 such that |c n| ≤ C * (r - ε)^{-n} for all integers n ≥ 0 (encoded with n : ℕ).

theorem shifted_coeffSeries_absSummable_of_interval_subset {E : Set ℝ} (a : ↑E) (f : ↑E → ℝ) (hanalytic : IsRealAnalyticAt E f a) {r : ℝ} (hr : 0 < r) (c : ℕ → ℝ) (hI : Set.Ioo (↑a - r) (↑a + r) ⊆ E) (hsummable : ∀ x ∈ Set.Ioo (↑a - r) (↑a + r), Summable fun (n : ℕ) => c n * (x - ↑a) ^ n) (hpowerSeries : ∀ (x : ℝ) (hx : x ∈ Set.Ioo (↑a - r) (↑a + r)), f ⟨x, ⋯⟩ = ∑' (n : ℕ), c n * (x - ↑a) ^ n) {b s : ℝ} (hs : 0 < s) (hsub : Set.Ioo (b - s) (b + s) ⊆ Set.Ioo (↑a - r) (↑a + r)) (m : ℕ) : Summable fun (n : ℕ) => |↑(n + m).factorial / (↑m.factorial * ↑n.factorial) * (b - ↑a) ^ n * c (n + m)|

Proposition 4.2.12: under the hypotheses and notation of the local power-series setup, if (b-s, b+s) ⊆ (a-r, a+r) with s > 0, then for every m : ℕ the shifted coefficient series ∑' n, ((n+m)!/(m!n!)) * (b-a)^n * c (n+m) (equivalently the original sum from n = m) is absolutely convergent; hence the corresponding d_m is well-defined.