def IsRealAnalyticAt (E : Set ℝ) (f : ↑E → ℝ) (a : ↑E) : Prop

Definition 4.2.1 (Real analytic at a point): let E ⊆ ℝ, f : E → ℝ, and a ∈ E be an interior point of E. The function f is real analytic at a if there exist r > 0 and coefficients c : ℕ → ℝ such that (a-r, a+r) ⊆ E, the power series ∑ c n (x-a)^n converges for every x ∈ (a-r, a+r) (encoding radius of convergence at least r), and f x equals that series on (a-r, a+r).

Equations

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

def IsRealAnalyticOn (E : Set ℝ) (f : ↑E → ℝ) : Prop

A function on E is real analytic on E when E is open and the function is real analytic at each point of E.

Equations

• IsRealAnalyticOn E f = (IsOpen E ∧ ∀ (a : ↑E), IsRealAnalyticAt E f a)

def HasNoIsolatedPoints (E : Set ℝ) : Prop

A set of real numbers has no isolated points if every x ∈ E is a limit point of E.

Equations

• HasNoIsolatedPoints E = ∀ x ∈ E, x ∈ closure (E \ {x})

noncomputable def SubtypeExtension (E : Set ℝ) (f : ↑E → ℝ) : ℝ → ℝ

Canonical extension of f : E → ℝ to ℝ, taking value 0 off E.

Equations

• SubtypeExtension E f x = if hx : x ∈ E then f ⟨x, hx⟩ else 0

noncomputable def FirstDerivativeSub (E : Set ℝ) (f : ↑E → ℝ) : ↑E → ℝ

The first derivative f' : E → ℝ, defined by the within-set derivative on E.

Equations

• FirstDerivativeSub E f x = derivWithin (SubtypeExtension E f) E ↑x

noncomputable def IteratedDerivativeSub (E : Set ℝ) (f : ↑E → ℝ) : ℕ → ↑E → ℝ

Iterated derivatives on E: f^(0)=f and f^(n+1) is the first derivative of f^(n).

Equations

• IteratedDerivativeSub E f 0 = f
• IteratedDerivativeSub E f n.succ = FirstDerivativeSub E (IteratedDerivativeSub E f n)

def IsOnceDifferentiableSub (E : Set ℝ) (f : ↑E → ℝ) : Prop

A function f : E → ℝ is once differentiable on E when it is differentiable within E at every point of E.

Equations

• IsOnceDifferentiableSub E f = ∀ (x : ↑E), DifferentiableWithinAt ℝ (SubtypeExtension E f) E ↑x

def IsKTimesDifferentiableSub (E : Set ℝ) (f : ↑E → ℝ) : ℕ → Prop

Definition 4.2.2 (k-times differentiability on a set).

(i) once differentiable means differentiable at every point of E; (ii) for k ≥ 2, k-times differentiable is defined recursively via the derivative; (iii) iterated derivatives are f^(0)=f, f^(1)=f', f^(k)=((f^(k-1))'); (iv) infinitely differentiable (smooth) means k-times differentiable for every k ≥ 0.

The standing hypothesis that every point of E is a limit point of E is recorded by HasNoIsolatedPoints E as part of the definition.

Equations

• IsKTimesDifferentiableSub E f k = (HasNoIsolatedPoints E ∧ Nat.rec True (fun (n : ℕ) (ih : Prop) => IsOnceDifferentiableSub E (IteratedDerivativeSub E f n) ∧ ih) k)

def IsSmoothSub (E : Set ℝ) (f : ↑E → ℝ) : Prop

A function on E is smooth when it is k-times differentiable for every k : ℕ.

Equations

• IsSmoothSub E f = ∀ (k : ℕ), IsKTimesDifferentiableSub E f k

def absCube : ℝ → ℝ

The function x ↦ |x|^3 on ℝ.

Equations

• absCube x = |x| ^ 3

theorem helperForProposition_4_2_1_absCube_eq_absRpowThree : absCube = fun (x : ℝ) => |x| ^ 3

Helper for Proposition 4.2.1: rewrite absCube using real powers.

theorem helperForProposition_4_2_1_hasDerivAt_absCube (x : ℝ) : HasDerivAt absCube (3 * x * |x|) x

Helper for Proposition 4.2.1: derivative formula for x ↦ |x|^3.

theorem helperForProposition_4_2_1_hasDerivAt_xMulAbs (x : ℝ) : HasDerivAt (fun (y : ℝ) => y * |y|) (2 * |x|) x

Helper for Proposition 4.2.1: derivative formula for x ↦ x|x|.

theorem helperForProposition_4_2_1_hasDerivAt_derivAbsCube (x : ℝ) : HasDerivAt (deriv absCube) (6 * |x|) x

Helper for Proposition 4.2.1: derivative formula for deriv absCube.

theorem helperForProposition_4_2_1_notDifferentiableAt_zero_secondDeriv : ¬DifferentiableAt ℝ (fun (x : ℝ) => 6 * |x|) 0

Helper for Proposition 4.2.1: the second derivative x ↦ 6|x| is not differentiable at 0.

theorem absCube_twiceDifferentiable_and_not_threeTimesDifferentiableAt_zero : Differentiable ℝ absCube ∧ Differentiable ℝ (deriv absCube) ∧ (∀ (x : ℝ), deriv absCube x = 3 * x * |x|) ∧ (∀ (x : ℝ), deriv (deriv absCube) x = 6 * |x|) ∧ ¬DifferentiableAt ℝ (deriv (deriv absCube)) 0

Proposition 4.2.1: for f(x) = |x|^3, one has f'(x) = 3x|x| and f''(x) = 6|x| for all x ∈ ℝ; hence f is twice differentiable on ℝ, while f'' is not differentiable at 0 (equivalently, f is not three times differentiable at 0).

theorem helperForProposition_4_2_2_interval_hasNoIsolatedPoints (a r : ℝ) : HasNoIsolatedPoints (Set.Ioo (a - r) (a + r))

Helper for Proposition 4.2.2: open intervals in ℝ have no isolated points.

theorem helperForProposition_4_2_2_kZero_seriesTerm_eq (c : ℕ → ℝ) (a x : ℝ) : (fun (n : ℕ) => c (n + 0) * (↑(n + 0).factorial / ↑n.factorial) * (x - a) ^ n) = fun (n : ℕ) => c n * (x - a) ^ n

Helper for Proposition 4.2.2: the k = 0 termwise coefficient factor is 1.

theorem helperForProposition_4_2_2_seriesFormula_kZero {a r : ℝ} (f : ↑(Set.Ioo (a - r) (a + r)) → ℝ) (c : ℕ → ℝ) (hc : ∀ (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) (x : ℝ) (hx : x ∈ Set.Ioo (a - r) (a + r)) : (Summable fun (n : ℕ) => c (n + 0) * (↑(n + 0).factorial / ↑n.factorial) * (x - a) ^ n) ∧ IteratedDerivativeSub (Set.Ioo (a - r) (a + r)) f 0 ⟨x, hx⟩ = ∑' (n : ℕ), c (n + 0) * (↑(n + 0).factorial / ↑n.factorial) * (x - a) ^ n

Helper for Proposition 4.2.2: the target series identity for k = 0.

theorem helperForProposition_4_2_2_iteratedDerivativeSub_eq_iteratedDerivWithin (E : Set ℝ) (f : ↑E → ℝ) (k : ℕ) (x : ℝ) (hx : x ∈ E) : IteratedDerivativeSub E f k ⟨x, hx⟩ = iteratedDerivWithin k (SubtypeExtension E f) E x

Helper for Proposition 4.2.2: IteratedDerivativeSub agrees pointwise with iteratedDerivWithin on the underlying set.

theorem helperForProposition_4_2_2_isOnceDifferentiableSub_of_contDiffOn {E : Set ℝ} (f : ↑E → ℝ) (hcont : ContDiffOn ℝ ⊤ (SubtypeExtension E f) E) (hunique : UniqueDiffOn ℝ E) (n : ℕ) : IsOnceDifferentiableSub E (IteratedDerivativeSub E f n)

Helper for Proposition 4.2.2: smoothness of the ambient extension implies that every iterated subtype derivative is once differentiable on the set.

theorem helperForProposition_4_2_2_isKTimesDifferentiableSub_of_allOnceDifferentiable {E : Set ℝ} (f : ↑E → ℝ) (hNoIso : HasNoIsolatedPoints E) (hOnce : ∀ (n : ℕ), IsOnceDifferentiableSub E (IteratedDerivativeSub E f n)) (k : ℕ) : IsKTimesDifferentiableSub E f k

Helper for Proposition 4.2.2: if all iterated derivatives are once differentiable, then the recursive notion of k-times differentiability holds for every k.

theorem helperForProposition_4_2_2_hasFPowerSeriesWithinOnBall_of_seriesData {a r : ℝ} (hr : 0 < r) (f : ↑(Set.Ioo (a - r) (a + r)) → ℝ) (c : ℕ → ℝ) (hc : ∀ (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) : HasFPowerSeriesWithinOnBall (SubtypeExtension (Set.Ioo (a - r) (a + r)) f) (FormalMultilinearSeries.ofScalars ℝ c) (Set.Ioo (a - r) (a + r)) a (ENNReal.ofReal r)

Helper for Proposition 4.2.2: the interval series data gives HasFPowerSeriesWithinOnBall for the canonical extension.

theorem helperForProposition_4_2_2_iteratedFDerivSeriesCoeffOnes_step (c : ℕ → ℝ) (k n : ℕ) : ((((FormalMultilinearSeries.ofScalars ℝ c).iteratedFDerivSeries (k + 1)).coeff n) fun (x : Fin (k + 1)) => 1) = (↑n + 1) * (((FormalMultilinearSeries.ofScalars ℝ c).iteratedFDerivSeries k).coeff (n + 1)) fun (x : Fin k) => 1

Helper for Proposition 4.2.2: one-step coefficient recursion for iteratedFDerivSeries evaluated at all-ones.

theorem helperForProposition_4_2_2_iteratedFDerivSeriesCoeffOnes_closedForm (c : ℕ → ℝ) (k n : ℕ) : ((((FormalMultilinearSeries.ofScalars ℝ c).iteratedFDerivSeries k).coeff n) fun (x : Fin k) => 1) = c (n + k) * (↑(n + k).factorial / ↑n.factorial)

Helper for Proposition 4.2.2: closed-form coefficients for iteratedFDerivSeries of ofScalars, evaluated at all-ones.

theorem helperForProposition_4_2_2_iteratedFDerivSeries_term_formula (c : ℕ → ℝ) (k n : ℕ) (y : ℝ) : ((((FormalMultilinearSeries.ofScalars ℝ c).iteratedFDerivSeries k n) fun (x : Fin n) => y) fun (x : Fin k) => 1) = c (n + k) * (↑(n + k).factorial / ↑n.factorial) * y ^ n

Helper for Proposition 4.2.2: explicit term formula for iteratedFDerivSeries of ofScalars.

theorem helperForProposition_4_2_2_iteratedDerivWithin_series_formula {a r : ℝ} (hr : 0 < r) (f : ↑(Set.Ioo (a - r) (a + r)) → ℝ) (c : ℕ → ℝ) (hc : ∀ (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) (k : ℕ) (x : ℝ) (hx : x ∈ Set.Ioo (a - r) (a + r)) : (Summable fun (n : ℕ) => c (n + k) * (↑(n + k).factorial / ↑n.factorial) * (x - a) ^ n) ∧ iteratedDerivWithin k (SubtypeExtension (Set.Ioo (a - r) (a + r)) f) (Set.Ioo (a - r) (a + r)) x = ∑' (n : ℕ), c (n + k) * (↑(n + k).factorial / ↑n.factorial) * (x - a) ^ n

Helper for Proposition 4.2.2: series formula for iteratedDerivWithin on the interval.

theorem helperForProposition_4_2_2_onceDifferentiable_all_orders_of_analytic {a r : ℝ} (hr : 0 < r) (f : ↑(Set.Ioo (a - r) (a + r)) → ℝ) (c : ℕ → ℝ) (hc : ∀ (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) (n : ℕ) : IsOnceDifferentiableSub (Set.Ioo (a - r) (a + r)) (IteratedDerivativeSub (Set.Ioo (a - r) (a + r)) f n)

Helper for Proposition 4.2.2: the interval power-series representation implies that all iterated subtype derivatives are once differentiable.

theorem realAnalyticOnInterval_iteratedDerivative_eq_powerSeries {a r : ℝ} (hr : 0 < r) (f : ↑(Set.Ioo (a - r) (a + r)) → ℝ) (hseries : ∃ (c : ℕ → ℝ), ∀ (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) : ∃ (c : ℕ → ℝ), (∀ (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) ∧ ∀ (k : ℕ), IsKTimesDifferentiableSub (Set.Ioo (a - r) (a + r)) f k ∧ ∀ (x : ℝ) (hx : x ∈ Set.Ioo (a - r) (a + r)), (Summable fun (n : ℕ) => c (n + k) * (↑(n + k).factorial / ↑n.factorial) * (x - a) ^ n) ∧ IteratedDerivativeSub (Set.Ioo (a - r) (a + r)) f k ⟨x, hx⟩ = ∑' (n : ℕ), c (n + k) * (↑(n + k).factorial / ↑n.factorial) * (x - a) ^ n

Proposition 4.2.2 (Real analytic functions are k-times differentiable): if f : (a-r, a+r) → ℝ has a convergent power-series representation f(x) = ∑' n, c n * (x-a)^n on (a-r, a+r), then for every k : ℕ, f is k-times differentiable on (a-r, a+r), and the k-th iterated derivative has the termwise differentiated series ∑' n, c (n+k) * ((n+k)! / n!) * (x-a)^n (equivalently using (n+1)(n+2)...(n+k), with empty product 1 when k = 0).