theorem helperForProposition_4_2_3_notAnalyticAt_zero_abs : ¬AnalyticAt ℝ (fun (x : ℝ) => |x|) 0

Helper for Proposition 4.2.3: |x| is not real analytic at 0.

theorem helperForProposition_4_2_3_eventuallyEq_abs_id_of_pos {a : ℝ} (ha : 0 < a) : (fun (x : ℝ) => |x|) =ᶠ[nhds a] fun (x : ℝ) => x

Helper for Proposition 4.2.3: at positive points, |x| agrees locally with x.

theorem helperForProposition_4_2_3_eventuallyEq_abs_negId_of_neg {a : ℝ} (ha : a < 0) : (fun (x : ℝ) => |x|) =ᶠ[nhds a] fun (x : ℝ) => -x

Helper for Proposition 4.2.3: at negative points, |x| agrees locally with -x.

theorem helperForProposition_4_2_3_analyticAt_abs_of_ne_zero {a : ℝ} (ha : a ≠ 0) : AnalyticAt ℝ (fun (x : ℝ) => |x|) a

Helper for Proposition 4.2.3: |x| is real analytic at every nonzero real point.

theorem abs_notDifferentiableAt_zero_notAnalyticAt_zero_analyticAt_nonzero : ¬DifferentiableAt ℝ (fun (x : ℝ) => |x|) 0 ∧ ¬AnalyticAt ℝ (fun (x : ℝ) => |x|) 0 ∧ ∀ (a : ℝ), a ≠ 0 → AnalyticAt ℝ (fun (x : ℝ) => |x|) a

Proposition 4.2.3: for f(x) = |x|, the function is not differentiable at 0, hence not real analytic at 0; moreover, for every a ≠ 0, f is real analytic at a.

theorem helperForTheorem_4_2_1_hasNoIsolatedPoints_of_isOpen {E : Set ℝ} (hE : IsOpen E) : HasNoIsolatedPoints E

Helper for Theorem 4.2.1: every open subset of ℝ has no isolated points.

theorem helperForTheorem_4_2_1_intervalEventuallyEq_set_at_center {E : Set ℝ} {a r : ℝ} (hr : 0 < r) (hI : Set.Ioo (a - r) (a + r) ⊆ E) : Set.Ioo (a - r) (a + r) =ᶠ[nhds a] E

Helper for Theorem 4.2.1: local interval and ambient set are eventually equal at the center.

theorem helperForTheorem_4_2_1_analyticWithinAtSubtypeExtension_of_IsRealAnalyticAt {E : Set ℝ} (f : ↑E → ℝ) (a : ↑E) (ha : IsRealAnalyticAt E f a) : AnalyticWithinAt ℝ (SubtypeExtension E f) E ↑a

Helper for Theorem 4.2.1: a pointwise real-analytic witness yields analytic-within-at for the canonical extension.

theorem helperForTheorem_4_2_1_isRealAnalyticAt_of_analyticWithinAtSubtypeExtension_open {E : Set ℝ} (g : ↑E → ℝ) (hE : IsOpen E) (a : ↑E) (ha : AnalyticWithinAt ℝ (SubtypeExtension E g) E ↑a) : IsRealAnalyticAt E g a

Helper for Theorem 4.2.1: on open sets, analyticity of the canonical extension implies the custom pointwise real-analytic property.

theorem helperForTheorem_4_2_1_analyticOnSubtypeExtension_of_IsRealAnalyticOn {E : Set ℝ} (f : ↑E → ℝ) (hf : IsRealAnalyticOn E f) : AnalyticOn ℝ (SubtypeExtension E f) E

Helper for Theorem 4.2.1: convert the custom IsRealAnalyticOn notion to mathlib AnalyticOn for the canonical extension.

theorem helperForTheorem_4_2_1_isRealAnalyticOn_of_analyticOnSubtypeExtension {E : Set ℝ} (g : ↑E → ℝ) (hE : IsOpen E) (hAnalytic : AnalyticOn ℝ (SubtypeExtension E g) E) : IsRealAnalyticOn E g

Helper for Theorem 4.2.1: convert analyticity of the canonical extension on an open set back to the custom IsRealAnalyticOn predicate.

theorem helperForTheorem_4_2_1_analyticOnSubtypeExtension_iteratedDerivativeSub {E : Set ℝ} (f : ↑E → ℝ) (hE : IsOpen E) (hAnalytic : AnalyticOn ℝ (SubtypeExtension E f) E) (k : ℕ) : AnalyticOn ℝ (SubtypeExtension E (IteratedDerivativeSub E f k)) E

Helper for Theorem 4.2.1: analyticity of an extension propagates to all iterated subtype derivatives.

theorem helperForTheorem_4_2_1_isOnceDifferentiableSub_of_IsRealAnalyticOn {E : Set ℝ} (g : ↑E → ℝ) (hg : IsRealAnalyticOn E g) : IsOnceDifferentiableSub E g

Helper for Theorem 4.2.1: real-analytic-on implies once differentiable on the set.

theorem realAnalyticOn_isSmooth_and_iteratedDerivative_realAnalytic {E : Set ℝ} (f : ↑E → ℝ) (hf : IsRealAnalyticOn E f) : IsSmoothSub E f ∧ ∀ (k : ℕ), IsOnceDifferentiableSub E (IteratedDerivativeSub E f k) ∧ IsRealAnalyticOn E (IteratedDerivativeSub E f k)

Theorem 4.2.1: if f : E → ℝ is real analytic on E, then f is smooth on E. Moreover, for every integer k ≥ 0, the iterated derivative f^(k) exists at every point of E and is real analytic on E.

theorem helperForTheorem_4_2_2_iteratedDerivWithin_setChange_at_center {g : ℝ → ℝ} {a : ℝ} {s t : Set ℝ} (hst : s =ᶠ[nhds a] t) (k : ℕ) : iteratedDerivWithin k g s a = iteratedDerivWithin k g t a

Helper for Theorem 4.2.2: iterated derivatives within eventually equal sets agree at the center.

theorem helperForTheorem_4_2_2_iteratedDerivativeSub_eq_intervalRestriction_at_center {E : Set ℝ} (f : ↑E → ℝ) (a : ↑E) {r : ℝ} (hr : 0 < r) (hI : Set.Ioo (↑a - r) (↑a + r) ⊆ E) (haI : ↑a ∈ Set.Ioo (↑a - r) (↑a + r)) (k : ℕ) : IteratedDerivativeSub E f k a = IteratedDerivativeSub (Set.Ioo (↑a - r) (↑a + r)) (fun (x : ↑(Set.Ioo (↑a - r) (↑a + r))) => f ⟨↑x, ⋯⟩) k ⟨↑a, haI⟩

Helper for Theorem 4.2.2: identify ambient and interval iterated subtype derivatives at the center.

theorem helperForTheorem_4_2_2_interval_center_factorial_coeff {a r : ℝ} (hr : 0 < r) (f : ↑(Set.Ioo (a - r) (a + r)) → ℝ) (c : ℕ → ℝ) (hseries : ∀ (x : ℝ) (hx : x ∈ Set.Ioo (a - r) (a + r)), (Summable fun (n : ℕ) => c n * (x - a) ^ n) ∧ f ⟨x, hx⟩ = ∑' (n : ℕ), c n * (x - a) ^ n) (haI : a ∈ Set.Ioo (a - r) (a + r)) (k : ℕ) : IteratedDerivativeSub (Set.Ioo (a - r) (a + r)) f k ⟨a, haI⟩ = ↑k.factorial * c k

Helper for Theorem 4.2.2: the interval center value of the iterated derivative extracts factorial times the coefficient.

theorem helperForTheorem_4_2_2_coeff_rewrite_from_factorial_identity {E : Set ℝ} (f : ↑E → ℝ) (a : ↑E) (c : ℕ → ℝ) (hfac : ∀ (n : ℕ), IteratedDerivativeSub E f n a = ↑n.factorial * c n) (n : ℕ) : IteratedDerivativeSub E f n a / ↑n.factorial = c n

Helper for Theorem 4.2.2: divide the factorial identity to recover coefficients.

theorem taylorFormula_iteratedDerivativeSub_eq_factorial_mul_coeff {E : Set ℝ} (f : ↑E → ℝ) (a : ↑E) (hf : IsRealAnalyticAt E f a) {r : ℝ} (hr : 0 < r) (hI : Set.Ioo (↑a - r) (↑a + r) ⊆ E) (c : ℕ → ℝ) (hsummable : ∀ x ∈ Set.Ioo (↑a - r) (↑a + r), Summable fun (n : ℕ) => c n * (x - ↑a) ^ n) (hseries : ∀ (x : ℝ) (hx : x ∈ Set.Ioo (↑a - r) (↑a + r)), f ⟨x, ⋯⟩ = ∑' (n : ℕ), c n * (x - ↑a) ^ n) : (∀ (k : ℕ), IteratedDerivativeSub E f k a = ↑k.factorial * c k) ∧ ∀ (x : ℝ) (hx : x ∈ Set.Ioo (↑a - r) (↑a + r)), f ⟨x, ⋯⟩ = ∑' (n : ℕ), IteratedDerivativeSub E f n a / ↑n.factorial * (x - ↑a) ^ n

Theorem 4.2.2 (Taylor's formula): let E ⊆ ℝ, let a : E be an interior point, and let f : E → ℝ be real analytic at a. If for some r > 0 and coefficients c : ℕ → ℝ one has f(x) = ∑' n, c n (x-a)^n for all x ∈ (a-r, a+r), then for every k ≥ 0, f^(k)(a) = k! * c_k; in particular, f(x) = ∑' n, (f^(n)(a) / n!) (x-a)^n on (a-r, a+r).

theorem helperForTheorem_4_2_3_exists_commonIntervalRadius {E : Set ℝ} {a : ℝ} (ha : a ∈ interior E) {R_c R_d : ℝ} (hR_c : 0 < R_c) (hR_d : 0 < R_d) : ∃ (r : ℝ), 0 < r ∧ r ≤ R_c ∧ r ≤ R_d ∧ Set.Ioo (a - r) (a + r) ⊆ E

Helper for Theorem 4.2.3: from interior membership and two positive radii, construct a common positive interval radius contained in E and bounded by both given radii.

theorem helperForTheorem_4_2_3_seriesData_on_commonInterval {E : Set ℝ} {f : ↑E → ℝ} {a r R : ℝ} {u : ℕ → ℝ} (hI : Set.Ioo (a - r) (a + r) ⊆ E) (hrR : r ≤ R) (hu : ∀ (x : ℝ) (hxE : x ∈ E), |x - a| < R → (Summable fun (n : ℕ) => u n * (x - a) ^ n) ∧ f ⟨x, hxE⟩ = ∑' (n : ℕ), u n * (x - a) ^ n) (x : ℝ) (hx : x ∈ Set.Ioo (a - r) (a + r)) : (Summable fun (n : ℕ) => u n * (x - a) ^ n) ∧ f ⟨x, ⋯⟩ = ∑' (n : ℕ), u n * (x - a) ^ n

Helper for Theorem 4.2.3: transport power-series data from a radius condition |x-a| < R on E to data on a smaller symmetric interval around a.

theorem helperForTheorem_4_2_3_isRealAnalyticAt_of_intervalSeriesData {E : Set ℝ} (f : ↑E → ℝ) (a : ↑E) (ha : ↑a ∈ interior E) {r : ℝ} (hr : 0 < r) (hI : Set.Ioo (↑a - r) (↑a + r) ⊆ E) (u : ℕ → ℝ) (hseriesData : ∀ (x : ℝ) (hx : x ∈ Set.Ioo (↑a - r) (↑a + r)), (Summable fun (n : ℕ) => u n * (x - ↑a) ^ n) ∧ f ⟨x, ⋯⟩ = ∑' (n : ℕ), u n * (x - ↑a) ^ n) : IsRealAnalyticAt E f a

Helper for Theorem 4.2.3: interval power-series data gives real analyticity at the center.

theorem helperForTheorem_4_2_3_cancel_factorial {E : Set ℝ} {f : ↑E → ℝ} {a : ↑E} {c d : ℕ → ℝ} (hc : ∀ (n : ℕ), IteratedDerivativeSub E f n a = ↑n.factorial * c n) (hd : ∀ (n : ℕ), IteratedDerivativeSub E f n a = ↑n.factorial * d n) (n : ℕ) : c n = d n

Helper for Theorem 4.2.3: cancel a nonzero factorial factor in two identities for the same iterated derivative sequence.

theorem powerSeries_coefficients_unique {E : Set ℝ} (f : ↑E → ℝ) (a : ↑E) (ha : ↑a ∈ interior E) (c d : ℕ → ℝ) {R_c R_d : ℝ} (hR_c : 0 < R_c) (hR_d : 0 < R_d) (hc : ∀ (x : ℝ) (hxE : x ∈ E), |x - ↑a| < R_c → (Summable fun (n : ℕ) => c n * (x - ↑a) ^ n) ∧ f ⟨x, hxE⟩ = ∑' (n : ℕ), c n * (x - ↑a) ^ n) (hd : ∀ (x : ℝ) (hxE : x ∈ E), |x - ↑a| < R_d → (Summable fun (n : ℕ) => d n * (x - ↑a) ^ n) ∧ f ⟨x, hxE⟩ = ∑' (n : ℕ), d n * (x - ↑a) ^ n) (n : ℕ) : c n = d n

Theorem 4.2.3 (Uniqueness of power series): let E ⊆ ℝ, let a be an interior point of E, and let f : E → ℝ. If there are radii R_c, R_d > 0 and coefficient sequences c, d : ℕ → ℝ such that for every x ∈ E with |x-a| < R_c one has f(x) = ∑' n, c n * (x-a)^n with convergence, and for every x ∈ E with |x-a| < R_d one has f(x) = ∑' n, d n * (x-a)^n with convergence, then c n = d n for all n.

theorem helperForProposition_4_2_4_norm_lt_one_of_abs_lt_one {x : ℝ} (hx : |x| < 1) : ‖x‖ < 1

Helper for Proposition 4.2.4: convert |x| < 1 into the norm inequality ‖x‖ < 1 used by geometric-series lemmas.

theorem helperForProposition_4_2_4_hasSum_geometric {x : ℝ} (hx : ‖x‖ < 1) : HasSum (fun (n : ℕ) => x ^ n) (1 - x)⁻¹

Helper for Proposition 4.2.4: under ‖x‖ < 1, the geometric series has sum (1 - x)⁻¹.

theorem helperForProposition_4_2_4_tsum_eq_one_div_form {x : ℝ} (hx : ‖x‖ < 1) : ∑' (n : ℕ), x ^ n = 1 / (1 - x)

Helper for Proposition 4.2.4: rewrite the geometric-series sum in the form 1 / (1 - x).

theorem geometricSeries_converges_and_tsum_eq_inv_one_sub (x : ℝ) (hx : |x| < 1) : (Summable fun (n : ℕ) => x ^ n) ∧ ∑' (n : ℕ), x ^ n = 1 / (1 - x)

Proposition 4.2.4: for every real number x with |x| < 1, the geometric series ∑' n : ℕ, x^n converges and equals 1 / (1 - x).

theorem helperForProposition_4_2_5_norm_lt_one_scaledShift {x : ℝ} (hx : |x - 1 / 2| < 1 / 2) : ‖2 * (x - 1 / 2)‖ < 1

Helper for Proposition 4.2.5: convert |x - 1/2| < 1/2 into the norm bound ‖2 * (x - 1/2)‖ < 1 used by geometric-series lemmas.

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

Helper for Proposition 4.2.5: rewrite the centered-series term as a scaled geometric term in the ratio 2 * (x - 1/2).

theorem helperForProposition_4_2_5_hasSum_centeredSeries {x : ℝ} (hx : |x - 1 / 2| < 1 / 2) : HasSum (fun (n : ℕ) => 2 ^ (n + 1) * (x - 1 / 2) ^ n) (2 * (1 - 2 * (x - 1 / 2))⁻¹)

Helper for Proposition 4.2.5: the centered geometric series has the closed-form sum 2 * (1 - 2*(x - 1/2))⁻¹.

theorem helperForProposition_4_2_5_sumValue_rewrite (x : ℝ) : 2 * (1 - 2 * (x - 1 / 2))⁻¹ = 1 / (1 - x)

Helper for Proposition 4.2.5: simplify the centered closed form to 1 / (1 - x).

theorem centeredGeometricSeries_converges_and_tsum_eq_inv_one_sub (x : ℝ) (hx : |x - 1 / 2| < 1 / 2) : (Summable fun (n : ℕ) => 2 ^ (n + 1) * (x - 1 / 2) ^ n) ∧ ∑' (n : ℕ), 2 ^ (n + 1) * (x - 1 / 2) ^ n = 1 / (1 - x)

Proposition 4.2.5: if x : ℝ satisfies |x - 1/2| < 1/2, then the geometric series ∑' n : ℕ, 2^(n+1) * (x - 1/2)^n converges and equals 1 / (1 - x).