Sequences and series of functions

TheoremPointwise convergence#

Mathlib states this as tendsto_pi_nhds.

tendsto_pi_nhds.{v, u_2, u_3} {Y : Type v} {ι : Type u_2} {A : ι → Type u_3}
  [T : (i : ι) → TopologicalSpace (A i)] {f : Y → (i : ι) → A i} {g : (i : ι) → A i}
  {u : Filter Y} :
  Filter.Tendsto f u (nhds g) ↔ ∀ (x : ι), Filter.Tendsto (fun i => f i x) u (nhds (g x))

Sources

• Mathlib documentation: tendsto_pi_nhds
• Source of tendsto_pi_nhds in Mathlib/Topology/Constructions.lean
• Mathlib undergraduate list: Single Variable Real Analysis › Sequences and series of functions

Mathlibtendsto_pi_nhds

Uses 3 · Used by 11

Statement usesLimit of a map with respect to filters · Topological space

Proof usesInduced topology

Used byJensen's inequality (integral version) · Change of variables formula · Divergence theorem · Fubini's theorem · Strong law of large numbers · Egorov's theorem · Lévy continuity theorem · Riemann-Lebesgue lemma (Measures and integral calculus) · Borel-Cantelli lemma (difficult direction) · Completeness of \(l^2\) · Completeness of \(L^2\)

• Uniform convergence

TheoremContinuity of the limit of a sequence of functions#

A function which can be uniformly approximated by continuous functions is continuous.

continuous_of_uniform_approx_of_continuous.{u_1, u_2} {α : Type u_1} {β : Type u_2}
  [TopologicalSpace α] [UniformSpace β] {f : α → β}
  (L : ∀ u ∈ uniformity β, ∃ F, Continuous F ∧ ∀ (y : α), (f y, F y) ∈ u) : Continuous f

Sources

• Mathlib documentation: continuous_of_uniform_approx_of_continuous
• Source of continuous_of_uniform_approx_of_continuous in Mathlib/Topology/UniformSpace/UniformApproximation.lean
• Mathlib undergraduate list: Single Variable Real Analysis › Sequences and series of functions

Mathlibcontinuous_of_uniform_approx_of_continuous

Uses 2

Statement usesContinuous function · Uniform space

TheoremContinuity of the sum of a series of functions#

An infinite sum of functions with summable sup norm is continuous if each individual function is.

continuous_tsum.{u_1, u_2, u_3} {α : Type u_1} {β : Type u_2} {F : Type u_3} [NormedAddCommGroup F]
  [CompleteSpace F] {u : α → ℝ} [TopologicalSpace β] {f : α → β → F}
  (hf : ∀ (i : α), Continuous (f i)) (hu : Summable u) (hfu : ∀ (n : α) (x : β), ‖f n x‖ ≤ u n) :
  Continuous fun x => ∑' (n : α), f n x

Sources

• Mathlib documentation: continuous_tsum
• Source of continuous_tsum in Mathlib/Analysis/Normed/Group/FunctionSeries.lean
• Mathlib undergraduate list: Single Variable Real Analysis › Sequences and series of functions

Mathlibcontinuous_tsum

Uses 8

Statement usesCompleteness · Continuous function · Infinite sum · Metric space

Proof usesAbsolutely convergent series in Banach spaces · Hausdorff space · Order topology · Uniformly continuous function

TheoremDifferentiability of the limit of a sequence of functions#

(d/dx) lim_{n → ∞} f n x = lim_{n → ∞} f' n x when the f' n converge uniformly to their limit.

hasFDerivAt_of_tendstoUniformly.{u_1, u_2, u_3, u_4} {ι : Type u_1} {l : Filter ι} {E : Type u_2}
  [NormedAddCommGroup E] {𝕜 : Type u_3} [NontriviallyNormedField 𝕜] [IsRCLikeNormedField 𝕜]
  [NormedSpace 𝕜 E] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {f : ι → E → G}
  {g : E → G} {f' : ι → E → E →L[𝕜] G} {g' : E → E →L[𝕜] G} [l.NeBot]
  (hf' : TendstoUniformly f' g' l) (hf : ∀ (n : ι) (x : E), HasFDerivAt (f n) (f' n x) x)
  (hfg : ∀ (x : E), Filter.Tendsto (fun n => f n x) l (nhds (g x))) (x : E) : HasFDerivAt g (g' x) x

Sources

• Mathlib documentation: hasFDerivAt_of_tendstoUniformly
• Source of hasFDerivAt_of_tendstoUniformly in Mathlib/Analysis/Calculus/UniformLimitsDeriv.lean
• Mathlib undergraduate list: Single Variable Real Analysis › Sequences and series of functions

MathlibhasFDerivAt_of_tendstoUniformly

Uses 14

Statement usesAssociative algebra over a commutative ring · Completeness · Differentiable function between normed vector spaces · Normed vector space over a normed field · Uniform convergence

Proof usesBall · Characteristic zero · Convex subsets · Euclidean affine space · Field \(\R\) of real numbers · List · Ring structure \(\Z\) · The Triangle Inequality · Topology on a normed vector space

TheoremDifferentiability of the sum of a series of functions#

Consider a series of functions ∑' n, f n x. If all functions in the series are differentiable with a summable bound on the derivatives, then the series is differentiable. Note that our assumptions do not ensure the pointwise convergence, but if there is no pointwise convergence then the series is zero everywhere so the result still holds.

differentiable_tsum.{u_1, u_2, u_3, u_4} {α : Type u_1} {𝕜 : Type u_2} {E : Type u_3} {F : Type u_4}
  [NontriviallyNormedField 𝕜] [IsRCLikeNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E]
  [NormedAddCommGroup F] [CompleteSpace F] {u : α → ℝ} [NormedSpace 𝕜 F] {f : α → E → F}
  {f' : α → E → E →L[𝕜] F} (hu : Summable u) (hf : ∀ (n : α) (x : E), HasFDerivAt (f n) (f' n x) x)
  (hf' : ∀ (n : α) (x : E), ‖f' n x‖ ≤ u n) : Differentiable 𝕜 fun y => ∑' (n : α), f n y

Sources

• Mathlib documentation: differentiable_tsum
• Source of differentiable_tsum in Mathlib/Analysis/Calculus/SmoothSeries.lean
• Mathlib undergraduate list: Single Variable Real Analysis › Sequences and series of functions

Mathlibdifferentiable_tsum

Uses 11

Statement usesAssociative algebra over a commutative ring · Completeness · Differentiable functions · Infinite sum · Normed vector space over a normed field

Proof usesAbsolutely convergent series in Banach spaces · Closure · Connectedness · Sequential space · Topological module · Topology of a metric space

TheoremWeierstrass polynomial approximation theorem#

The Weierstrass Approximation Theorem: polynomials functions on [a, b] ⊆ ℝ are dense in C([a,b],ℝ)

(While we could deduce this as an application of the Stone-Weierstrass theorem, our proof of that relies on the fact that abs is in the closure of polynomials on [-M, M], so we may as well get this done first.)

polynomialFunctions_closure_eq_top (a b : ℝ) :
  (polynomialFunctions (Set.Icc a b)).topologicalClosure = ⊤

Sources

• Mathlib documentation: polynomialFunctions_closure_eq_top
• Source of polynomialFunctions_closure_eq_top in Mathlib/Topology/ContinuousMap/Weierstrass.lean
• Mathlib undergraduate list: Single Variable Real Analysis › Sequences and series of functions

MathlibpolynomialFunctions_closure_eq_top

Uses 16 · Used by 1

Statement usesAssociative algebra over a commutative ring · Bornology · Closure · Compact open topology · Order · Order topology · Polynomial functions · Topological ring

Proof usesField \(\R\) of real numbers · Heine-Cantor theorem · Homeomorphisms · Linear map · Local convexity · Normed vector space over a normed field · Ordered ring · Topological module

Used byStone-Weierstrass theorem

TheoremWeierstrass trigonometric approximation theorem#

The linear span of the monomials fourier n is dense in C(AddCircle T, ℂ).

span_fourier_closure_eq_top {T : ℝ} [hT : Fact (0 < T)] :
  (Submodule.span ℂ (Set.range fourier)).topologicalClosure = ⊤

Sources

• Mathlib documentation: span_fourier_closure_eq_top
• Source of span_fourier_closure_eq_top in Mathlib/Analysis/Fourier/AddCircle.lean
• Mathlib undergraduate list: Single Variable Real Analysis › Sequences and series of functions

Mathlibspan_fourier_closure_eq_top

Uses 9 · Used by 1

Statement usesClosure · Compact open topology · Cos (extension of trigonometric functions to the complex plane) · Field \(\C\) of complex numbers · Generating sets · Metric space · Topological ring

Proof usesCompleteness · Stone-Weierstrass theorem

Used byFourier Series

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.