Interchange of limits and derivatives

TheoremInterchange of limits and derivatives on a closed interval#✓fully proved

Let \(a < b\) be real numbers, and let \(f_n, f_n' : \mathbb{R} \to \mathbb{R}\) for \(n \in \mathbb{N}\) and \(g, g' : \mathbb{R} \to \mathbb{R}\) be functions. Suppose that for every \(n\) and every \(x \in [a, b]\), \(f_n\) is differentiable at \(x\) (two-sided, also at the endpoints) with derivative \(f_n'(x)\); that each \(f_n'\) is continuous on \([a, b]\); that \(f_n' \to g'\) uniformly on \([a, b]\); and that \(f_n(x) \to g(x)\) for every \(x \in [a, b]\). Then for every \(x \in [a, b]\), \(g\) has derivative \(g'(x)\) at \(x\) within \([a, b]\) (a one-sided derivative at the endpoints), and \(g'\) is continuous on \([a, b]\).

theorem hasDerivWithinAt_of_tendstoUniformlyOn_Icc
    {f : ℕ → ℝ → ℝ} {g : ℝ → ℝ} {f' : ℕ → ℝ → ℝ} {g' : ℝ → ℝ}
    {a b : ℝ} (hab : a < b)
    (hderiv : ∀ n, ∀ x ∈ Icc a b, HasDerivAt (f n) (f' n x) x)
    (hf'_cont : ∀ n, ContinuousOn (f' n) (Icc a b))
    (hf'_unif : TendstoUniformlyOn f' g' atTop (Icc a b))
    (hfg : ∀ x ∈ Icc a b, Tendsto (fun n => f n x) atTop (nhds (g x))) :
    (∀ x ∈ Icc a b, HasDerivWithinAt g (g' x) (Icc a b) x) ∧
      ContinuousOn g' (Icc a b)

Used by 1

Used byInterchange of limits and derivatives at interior points

TheoremInterchange of limits and derivatives at interior points#✓fully proved

Let \(a < b\) be real numbers, and let \(f_n, f_n' : \mathbb{R} \to \mathbb{R}\) for \(n \in \mathbb{N}\) and \(g, g' : \mathbb{R} \to \mathbb{R}\) be functions. Suppose that for every \(n\) and every \(x \in [a, b]\), \(f_n\) is differentiable at \(x\) (two-sided, also at the endpoints) with derivative \(f_n'(x)\); that each \(f_n'\) is continuous on \([a, b]\); that \(f_n' \to g'\) uniformly on \([a, b]\); and that \(f_n(x) \to g(x)\) for every \(x \in [a, b]\). Then \(g\) is differentiable at every \(x \in (a, b)\) with derivative \(g'(x)\).

theorem hasDerivAt_of_tendstoUniformlyOn_Icc
    {f : ℕ → ℝ → ℝ} {g : ℝ → ℝ} {f' : ℕ → ℝ → ℝ} {g' : ℝ → ℝ}
    {a b : ℝ} (hab : a < b)
    (hderiv : ∀ n, ∀ x ∈ Icc a b, HasDerivAt (f n) (f' n x) x)
    (hf'_cont : ∀ n, ContinuousOn (f' n) (Icc a b))
    (hf'_unif : TendstoUniformlyOn f' g' atTop (Icc a b))
    (hfg : ∀ x ∈ Icc a b, Tendsto (fun n => f n x) atTop (nhds (g x))) :
    ∀ x ∈ Ioo a b, HasDerivAt g (g' x) x

Uses 1

Proof usesInterchange of limits and derivatives on a closed interval

2 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.