theorem shifted_coefficients_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) {b s : ℝ} (hs : 0 < s) (hsub : Set.Ioo (b - s) (b + s) ⊆ Set.Ioo (↑a - r) (↑a + r)) (d : ℕ → ℝ) (hdSummable : ∀ (m : ℕ), Summable fun (n : ℕ) => ↑(n + m).factorial / (↑m.factorial * ↑n.factorial) * (b - ↑a) ^ n * c (n + m)) (hd : ∀ (m : ℕ), d m = ∑' (n : ℕ), ↑(n + m).factorial / (↑m.factorial * ↑n.factorial) * (b - ↑a) ^ n * c (n + m)) (ε : ℝ) (hε0 : 0 < ε) (hεs : ε < s) : ∃ (C : ℝ), 0 < C ∧ ∀ (m : ℕ), |d m| ≤ C * (s - ε)⁻¹ ^ m

Proposition 4.2.13: assume the hypotheses and notation of the shifted power-series setup centered at a, and let d m = ∑' n, ((n+m)!/(m!n!)) * (b-a)^n * c (n+m), with this defining series convergent for each m. Then for every ε with 0 < ε < s, there exists C > 0 such that |d m| ≤ C * (s - ε)^{-m} for all integers m ≥ 0 (encoded as m : ℕ).

theorem helperForProposition_4_2_14_exists_subradius_gap_at_point {b s x : ℝ} (hs : 0 < s) (hx : x ∈ Set.Ioo (b - s) (b + s)) : ∃ (ε : ℝ), 0 < ε ∧ ε < s ∧ |x - b| < s - ε

Helper for Proposition 4.2.14: for a point in (b-s, b+s), one can choose ε with 0 < ε < s and still keep a strict gap |x-b| < s-ε.

theorem helperForProposition_4_2_14_absSummable_shifted_series_at_point {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)) (d : ℕ → ℝ) (hdSummable : ∀ (m : ℕ), Summable fun (n : ℕ) => ↑(n + m).factorial / (↑m.factorial * ↑n.factorial) * (b - ↑a) ^ n * c (n + m)) (hd : ∀ (m : ℕ), d m = ∑' (n : ℕ), ↑(n + m).factorial / (↑m.factorial * ↑n.factorial) * (b - ↑a) ^ n * c (n + m)) (x : ℝ) (hx : x ∈ Set.Ioo (b - s) (b + s)) : Summable fun (m : ℕ) => |d m * (x - b) ^ m|

Helper for Proposition 4.2.14: the shifted series is absolutely summable at every point of (b-s, b+s).

theorem helperForProposition_4_2_14_expand_original_series_termwise {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)) (x : ℝ) (hx : x ∈ Set.Ioo (b - s) (b + s)) : f ⟨x, ⋯⟩ = ∑' (n : ℕ), ∑ m ∈ Finset.range (n + 1), ↑n.factorial / (↑m.factorial * ↑(n - m).factorial) * (b - ↑a) ^ (n - m) * c n * (x - b) ^ m

Helper for Proposition 4.2.14: expand the original power series around a at a point x ∈ (b-s, b+s) into a triangular finite sum in powers of (x - b).

theorem helperForProposition_4_2_14_row_tsum_eq_d_times_shiftedPower {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)) (d : ℕ → ℝ) (hdSummable : ∀ (m : ℕ), Summable fun (n : ℕ) => ↑(n + m).factorial / (↑m.factorial * ↑n.factorial) * (b - ↑a) ^ n * c (n + m)) (hd : ∀ (m : ℕ), d m = ∑' (n : ℕ), ↑(n + m).factorial / (↑m.factorial * ↑n.factorial) * (b - ↑a) ^ n * c (n + m)) (x : ℝ) (m : ℕ) : ∑' (n : ℕ), ↑(n + m).factorial / (↑m.factorial * ↑n.factorial) * (b - ↑a) ^ n * c (n + m) * (x - b) ^ m = d m * (x - b) ^ m

Helper for Proposition 4.2.14: each row sum in the triangular rearrangement is exactly d m * (x - b)^m.

theorem helperForProposition_4_2_14_triangular_reindex_tsum_via_prod (K : ℕ → ℕ → ℝ) (hK : Summable fun (p : ℕ × ℕ) => K p.1 p.2) : ∑' (n : ℕ), ∑ m ∈ Finset.range (n + 1), K m (n - m) = ∑' (p : ℕ × ℕ), K p.1 p.2

Helper for Proposition 4.2.14: if a kernel on ℕ × ℕ is summable, then the triangular range-indexed tsum can be rewritten as the corresponding product-indexed tsum via antidiagonal reindexing.

theorem helperForProposition_4_2_14_prod_rows_to_shifted_coeff_tsum (K : ℕ → ℕ → ℝ) (d : ℕ → ℝ) (x b : ℝ) (hK : Summable fun (p : ℕ × ℕ) => K p.1 p.2) (hRows : ∀ (m : ℕ), ∑' (n : ℕ), K m n = d m * (x - b) ^ m) : ∑' (p : ℕ × ℕ), K p.1 p.2 = ∑' (m : ℕ), d m * (x - b) ^ m

Helper for Proposition 4.2.14: once a product-indexed kernel is summable, its tsum can be identified with the shifted-coefficient series by evaluating row tsums.

theorem helperForProposition_4_2_14_summable_prod_shifted_kernel_at_point {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)) (x : ℝ) (hx : x ∈ Set.Ioo (b - s) (b + s)) : Summable fun (p : ℕ × ℕ) => ↑(p.1 + p.2).factorial / (↑p.1.factorial * ↑p.2.factorial) * (b - ↑a) ^ p.2 * c (p.1 + p.2) * (x - b) ^ p.1

Helper for Proposition 4.2.14: for fixed x ∈ (b-s, b+s), the product kernel (m,k) ↦ ((m+k)!/(m!k!)) * (b-a)^k * c (m+k) * (x-b)^m is summable on ℕ × ℕ.

theorem helperForProposition_4_2_14_triangular_tsum_to_shifted_coeff_tsum {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)) (d : ℕ → ℝ) (hdSummable : ∀ (m : ℕ), Summable fun (n : ℕ) => ↑(n + m).factorial / (↑m.factorial * ↑n.factorial) * (b - ↑a) ^ n * c (n + m)) (hd : ∀ (m : ℕ), d m = ∑' (n : ℕ), ↑(n + m).factorial / (↑m.factorial * ↑n.factorial) * (b - ↑a) ^ n * c (n + m)) (x : ℝ) (hx : x ∈ Set.Ioo (b - s) (b + s)) : ∑' (n : ℕ), ∑ m ∈ Finset.range (n + 1), ↑n.factorial / (↑m.factorial * ↑(n - m).factorial) * (b - ↑a) ^ (n - m) * c n * (x - b) ^ m = ∑' (m : ℕ), d m * (x - b) ^ m

Helper for Proposition 4.2.14: the triangular expansion obtained from the original series can be reordered into the shifted coefficient series.

theorem shifted_powerSeries_absConvergent_and_eq_on_interval {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)) (d : ℕ → ℝ) (hdSummable : ∀ (m : ℕ), Summable fun (n : ℕ) => ↑(n + m).factorial / (↑m.factorial * ↑n.factorial) * (b - ↑a) ^ n * c (n + m)) (hd : ∀ (m : ℕ), d m = ∑' (n : ℕ), ↑(n + m).factorial / (↑m.factorial * ↑n.factorial) * (b - ↑a) ^ n * c (n + m)) (x : ℝ) (hx : x ∈ Set.Ioo (b - s) (b + s)) : (Summable fun (m : ℕ) => |d m * (x - b) ^ m|) ∧ f ⟨x, ⋯⟩ = ∑' (m : ℕ), d m * (x - b) ^ m

Proposition 4.2.14: assume the hypotheses and notation of the shifted power-series setup (with coefficients d). Then for every x ∈ (b-s, b+s), the power series ∑' m, d m * (x-b)^m is absolutely convergent, and one has f(x) = ∑' m, d m * (x-b)^m on that interval.

theorem realAnalyticAt_every_point_of_localPowerSeriesInterval {E : Set ℝ} (a : ↑E) (f : ↑E → ℝ) {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 : ℝ) (hb : b ∈ Set.Ioo (↑a - r) (↑a + r)) : IsRealAnalyticAt E f ⟨b, ⋯⟩

Proposition 4.2.15: assume the hypotheses and notation of the local power-series setup centered at a. Then f is real analytic at every b ∈ (a-r, a+r).