Normal convergence of series of functions

DefinitionExtended supremum norm on a set#✓fully proved

Let \(X\) be a type and \(E\) a seminormed additive commutative group. For a function \(g : X \to E\) and a set \(S \subseteq X\), the supremum norm of \(g\) on \(S\) is \(\sup_{x \in S} \|g(x)\|\), taken in the extended nonnegative reals \([0, \infty]\); in particular it is \(0\) when \(S\) is empty and \(\infty\) when \(\|g\|\) is unbounded on \(S\).

noncomputable def supNormOn (g : X → E) (S : Set X) : ℝ≥0∞ :=
  ⨆ x : S, ENNReal.ofReal ‖g x‖

Used by 11

Used byNormal convergence of a series of functions on a set · Normal convergence on the empty set · Normal convergence of the zero series · Derivative series of a locally normally convergent holomorphic series · Normal convergence passes to subsets · Normal convergence implies pointwise absolute convergence · Normal convergence gives summable real sup norms · Supremum norm over the empty set · Monotonicity of the supremum norm in the domain · Supremum norm of the zero function · Weierstrass M-test: normal convergence implies uniform convergence

DefinitionNormal convergence of a series of functions on a set#✓fully proved

Let \(X\) be a type and \(E\) a seminormed additive commutative group. A series of functions \(f_n \colon X \to E\) (\(n \in \mathbb{N}\)) converges normally on a set \(S \subseteq X\) when the sum \(\sum_{n} \sup_{x \in S} \|f_n(x)\|\) is finite, where each supremum norm and the sum are taken in the extended nonnegative reals \([0, \infty]\).

def ConvergesNormallyOn (f : ℕ → X → E) (S : Set X) : Prop :=
  ∑' n, supNormOn (f n) S ≠ ∞

Uses 1 · Used by 14

Statement usesExtended supremum norm on a set

Used byLocal normal convergence of a series of functions on a set · Local normal convergence on the empty set · Local normal convergence of the zero series · Normal convergence on the empty set · Normal convergence of the zero series · Derivative series of a locally normally convergent holomorphic series · Local normal convergence gives a neighbourhood of each point of the set · Normal convergence passes to subsets · Local normal convergence passes to subsets · Normal convergence implies pointwise absolute convergence · Local normal convergence implies pointwise absolute convergence · Normal convergence gives summable real sup norms · Local normal convergence implies locally uniform convergence · Weierstrass M-test: normal convergence implies uniform convergence

TheoremSupremum norm over the empty set#✓fully proved

For every function \(g \colon X \to E\) into a seminormed additive commutative group \(E\), the supremum norm of \(g\) on the empty set, valued in \([0, \infty]\), is \(0\).

@[simp]
theorem supNormOn_empty (g : X → E) : supNormOn g ∅ = 0

Uses 1 · Used by 1

Statement usesExtended supremum norm on a set

Used byNormal convergence on the empty set

TheoremSupremum norm of the zero function#✓fully proved

For every set \(S \subseteq X\), the supremum norm on \(S\) of the zero function from \(X\) to a seminormed additive commutative group \(E\) is \(0\).

@[simp]
theorem supNormOn_zero (S : Set X) : supNormOn (0 : X → E) S = 0

Uses 1 · Used by 1

Statement usesExtended supremum norm on a set

Used byNormal convergence of the zero series

TheoremMonotonicity of the supremum norm in the domain#✓fully proved

If \(T \subseteq S \subseteq X\), then for every function \(g \colon X \to E\) into a seminormed additive commutative group \(E\), the supremum norm of \(g\) on \(T\) is at most the supremum norm of \(g\) on \(S\).

theorem supNormOn_mono {S T : Set X} (h : T ⊆ S) (g : X → E) :
    supNormOn g T ≤ supNormOn g S

Uses 1 · Used by 2

Statement usesExtended supremum norm on a set

Used byDerivative series of a locally normally convergent holomorphic series · Normal convergence passes to subsets

TheoremNormal convergence on the empty set#✓fully proved

Every series of functions \(f_n \colon X \to E\) (\(n \in \mathbb{N}\)) with values in a seminormed additive commutative group \(E\) converges normally on the empty set.

@[simp]
theorem convergesNormallyOn_empty (f : ℕ → X → E) : ConvergesNormallyOn f ∅

Uses 3

Statement usesNormal convergence of a series of functions on a set

Proof usesExtended supremum norm on a set · Supremum norm over the empty set

TheoremNormal convergence of the zero series#✓fully proved

For every set \(S \subseteq X\) and every seminormed additive commutative group \(E\), the series of functions \(X \to E\) whose terms are all zero converges normally on \(S\).

@[simp]
theorem convergesNormallyOn_zero (S : Set X) :
    ConvergesNormallyOn (0 : ℕ → X → E) S

Uses 3 · Used by 1

Statement usesNormal convergence of a series of functions on a set

Proof usesExtended supremum norm on a set · Supremum norm of the zero function

Used byLocal normal convergence of the zero series

TheoremNormal convergence passes to subsets#✓fully proved

Let \(f_n \colon X \to E\) (\(n \in \mathbb{N}\)) be functions into a seminormed additive commutative group \(E\) and let \(T \subseteq S \subseteq X\). If the series \(\sum_n f_n\) converges normally on \(S\), then it converges normally on \(T\).

theorem ConvergesNormallyOn.mono {f : ℕ → X → E} {S T : Set X}
    (h : ConvergesNormallyOn f S) (hTS : T ⊆ S) : ConvergesNormallyOn f T

Uses 3 · Used by 1

Statement usesNormal convergence of a series of functions on a set

Proof usesExtended supremum norm on a set · Monotonicity of the supremum norm in the domain

Used byLocal normal convergence passes to subsets

DefinitionLocal normal convergence of a series of functions on a set#✓fully proved

Let \(X\) be a topological space and \(E\) a seminormed additive commutative group. A series of functions \(f_n \colon X \to E\) (\(n \in \mathbb{N}\)) converges locally normally on a set \(S \subseteq X\) when every \(x \in S\) has a neighbourhood \(U\) such that the series converges normally on \(U \cap S\).

def ConvergesLocallyNormallyOn (f : ℕ → X → E) (S : Set X) : Prop :=
  ∀ x ∈ S, ∃ U ∈ 𝓝 x, ConvergesNormallyOn f (U ∩ S)

Uses 1 · Used by 8

Statement usesNormal convergence of a series of functions on a set

Used byLocal normal convergence on the empty set · Local normal convergence of the zero series · Derivative series of a locally normally convergent holomorphic series · Local normal convergence gives a neighbourhood of each point of the set · Termwise differentiation of locally normally convergent holomorphic series · Local normal convergence passes to subsets · Local normal convergence implies pointwise absolute convergence · Local normal convergence implies locally uniform convergence

TheoremLocal normal convergence gives a neighbourhood of each point of the set#✓fully proved

Let \(X\) be a topological space, \(E\) a seminormed additive commutative group, \(f_n \colon X \to E\) (\(n \in \mathbb{N}\)) functions and \(S \subseteq X\). If the series \(\sum_n f_n\) converges locally normally on \(S\), then every \(x \in S\) has a neighbourhood \(U\) such that the series converges normally on \(U \cap S\).

theorem ConvergesLocallyNormallyOn.exists_nhds_inter {f : ℕ → X → E} {S : Set X}
    {x : X} (h : ConvergesLocallyNormallyOn f S) (hx : x ∈ S) :
    ∃ U ∈ 𝓝 x, ConvergesNormallyOn f (U ∩ S)

Uses 2

Statement usesLocal normal convergence of a series of functions on a set · Normal convergence of a series of functions on a set

TheoremLocal normal convergence on the empty set#✓fully proved

Let \(X\) be a topological space. Every series of functions \(f_n \colon X \to E\) (\(n \in \mathbb{N}\)) with values in a seminormed additive commutative group \(E\) converges locally normally on the empty set.

@[simp]
theorem convergesLocallyNormallyOn_empty (f : ℕ → X → E) :
    ConvergesLocallyNormallyOn f ∅

Uses 2

Statement usesLocal normal convergence of a series of functions on a set

Proof usesNormal convergence of a series of functions on a set

TheoremLocal normal convergence of the zero series#✓fully proved

Let \(X\) be a topological space and \(E\) a seminormed additive commutative group. For every set \(S \subseteq X\), the series of functions \(X \to E\) whose terms are all zero converges locally normally on \(S\).

@[simp]
theorem convergesLocallyNormallyOn_zero (S : Set X) :
    ConvergesLocallyNormallyOn (0 : ℕ → X → E) S

Uses 3

Statement usesLocal normal convergence of a series of functions on a set

Proof usesNormal convergence of a series of functions on a set · Normal convergence of the zero series

TheoremLocal normal convergence passes to subsets#✓fully proved

Let \(X\) be a topological space, let \(f_n \colon X \to E\) (\(n \in \mathbb{N}\)) be functions into a seminormed additive commutative group \(E\) and let \(T \subseteq S \subseteq X\). If the series \(\sum_n f_n\) converges locally normally on \(S\), then it converges locally normally on \(T\).

theorem ConvergesLocallyNormallyOn.mono {f : ℕ → X → E} {S T : Set X}
    (h : ConvergesLocallyNormallyOn f S) (hTS : T ⊆ S) :
    ConvergesLocallyNormallyOn f T

Uses 3

Statement usesLocal normal convergence of a series of functions on a set

Proof usesNormal convergence of a series of functions on a set · Normal convergence passes to subsets

TheoremNormal convergence gives summable real sup norms#✓fully proved

Let \(E\) be a seminormed additive commutative group, \(S\) a subset of a type \(X\) and \(f_n \colon X \to E\) for \(n \in \mathbb{N}\). If the series \(\sum_n f_n\) converges normally on \(S\), that is \(\sum_n \sup_{x \in S} \|f_n(x)\| < \infty\) with the suprema taken in \([0, \infty]\), then the sequence of sup norms \(\left(\sup_{x \in S} \|f_n(x)\|\right)_n\), viewed as real numbers, is summable.

theorem ConvergesNormallyOn.summable_toReal_supNormOn
    {X E : Type*} [SeminormedAddCommGroup E]
    {f : ℕ → X → E} {S : Set X}
    (hf : ConvergesNormallyOn f S) :
    Summable (fun n => (supNormOn (f n) S).toReal)

Uses 2 · Used by 2

Statement usesNormal convergence of a series of functions on a set · Extended supremum norm on a set

Used byNormal convergence implies pointwise absolute convergence · Weierstrass M-test: normal convergence implies uniform convergence

TheoremNormal convergence implies pointwise absolute convergence#✓fully proved

Let \(E\) be a seminormed additive commutative group, \(S\) a subset of a type \(X\) and \(f_n \colon X \to E\) for \(n \in \mathbb{N}\). If the series \(\sum_n f_n\) converges normally on \(S\), that is \(\sum_n \sup_{x \in S} \|f_n(x)\| < \infty\) with the suprema taken in \([0, \infty]\), then for every \(x \in S\) the series \(\sum_n \|f_n(x)\|\) is summable.

theorem ConvergesNormallyOn.summable_norm
    {X E : Type*} [SeminormedAddCommGroup E]
    {f : Nat → X → E} {S : Set X} (hf : ConvergesNormallyOn f S)
    {x : X} (hx : x ∈ S) : Summable (fun n => norm (f n x))

Uses 3 · Used by 1

Statement usesNormal convergence of a series of functions on a set

Proof usesNormal convergence gives summable real sup norms · Extended supremum norm on a set

Used byLocal normal convergence implies pointwise absolute convergence

TheoremLocal normal convergence implies pointwise absolute convergence#✓fully proved

Let \(E\) be a seminormed additive commutative group, \(S\) a subset of a topological space \(X\) and \(f_n \colon X \to E\) for \(n \in \mathbb{N}\). If the series \(\sum_n f_n\) converges locally normally on \(S\), that is every \(x \in S\) has a neighbourhood \(U\) with \(\sum_n \sup_{y \in U \cap S} \|f_n(y)\| < \infty\) (suprema taken in \([0, \infty]\)), then for every \(x \in S\) the series \(\sum_n \|f_n(x)\|\) is summable.

theorem ConvergesLocallyNormallyOn.summable_norm
    {X E : Type*} [TopologicalSpace X] [SeminormedAddCommGroup E]
    {f : Nat → X → E} {S : Set X} (hf : ConvergesLocallyNormallyOn f S)
    {x : X} (hx : x ∈ S) : Summable (fun n => norm (f n x))

Uses 3

Statement usesLocal normal convergence of a series of functions on a set

Proof usesNormal convergence of a series of functions on a set · Normal convergence implies pointwise absolute convergence

TheoremWeierstrass M-test: normal convergence implies uniform convergence#✓fully proved

Let \(E\) be a complete normed additive commutative group, \(S\) a subset of a type \(X\) and \(f_n \colon X \to E\) for \(n \in \mathbb{N}\). If the series \(\sum_n f_n\) converges normally on \(S\), that is \(\sum_n \sup_{x \in S} \|f_n(x)\| < \infty\) with the suprema taken in \([0, \infty]\), then the partial sums \(x \mapsto \sum_{n < N} f_n(x)\) converge uniformly on \(S\), as \(N \to \infty\), to the pointwise sum \(x \mapsto \sum_{n=0}^{\infty} f_n(x)\).

theorem ConvergesNormallyOn.tendstoUniformlyOn_tsum_nat
    {X E : Type*} [NormedAddCommGroup E] [CompleteSpace E]
    {f : ℕ → X → E} {S : Set X}
    (hf : ConvergesNormallyOn f S) :
    TendstoUniformlyOn (fun N z => ∑ n ∈ Finset.range N, f n z)
      (fun z => ∑' n, f n z) atTop S

Uses 3 · Used by 1

Statement usesNormal convergence of a series of functions on a set

Proof usesNormal convergence gives summable real sup norms · Extended supremum norm on a set

Used byLocal normal convergence implies locally uniform convergence

TheoremDerivative series of a locally normally convergent holomorphic series#✓fully proved

Let \(E\) be a normed space over \(\mathbb{C}\), \(S \subseteq \mathbb{C}\) an open set and \(f_n \colon \mathbb{C} \to E\) for \(n \in \mathbb{N}\) functions that are complex differentiable on \(S\). If the series \(\sum_n f_n\) converges locally normally on \(S\), that is every \(z \in S\) has a neighbourhood \(U\) with \(\sum_n \sup_{w \in U \cap S} \|f_n(w)\| < \infty\) (suprema taken in \([0, \infty]\)), then the series of derivatives \(\sum_n f_n'\) also converges locally normally on \(S\).

theorem ConvergesLocallyNormallyOn.deriv
    {E : Type*} [NormedAddCommGroup E] [NormedSpace ℂ E]
    {f : ℕ → ℂ → E} {S : Set ℂ}
    (hf : ConvergesLocallyNormallyOn f S)
    (hS : IsOpen S) (holo : ∀ n, DifferentiableOn ℂ (f n) S) :
    ConvergesLocallyNormallyOn (fun n z => _root_.deriv (f n) z) S

Uses 4 · Used by 1

Statement usesLocal normal convergence of a series of functions on a set

Proof usesNormal convergence of a series of functions on a set · Extended supremum norm on a set · Monotonicity of the supremum norm in the domain

Used byTermwise differentiation of locally normally convergent holomorphic series

TheoremLocal normal convergence implies locally uniform convergence#✓fully proved

Let \(E\) be a complete normed additive commutative group, \(S\) a subset of a topological space \(X\) and \(f_n \colon X \to E\) for \(n \in \mathbb{N}\). If the series \(\sum_n f_n\) converges locally normally on \(S\), that is every \(x \in S\) has a neighbourhood \(U\) with \(\sum_n \sup_{y \in U \cap S} \|f_n(y)\| < \infty\) (suprema taken in \([0, \infty]\)), then the partial sums \(x \mapsto \sum_{n < N} f_n(x)\) converge locally uniformly on \(S\), as \(N \to \infty\), to the pointwise sum \(x \mapsto \sum_{n=0}^{\infty} f_n(x)\).

theorem ConvergesLocallyNormallyOn.tendstoLocallyUniformlyOn_tsum_nat
    {X E : Type*} [TopologicalSpace X] [NormedAddCommGroup E] [CompleteSpace E]
    {f : Nat → X → E} {S : Set X} (hf : ConvergesLocallyNormallyOn f S) :
    TendstoLocallyUniformlyOn
      (fun N x => Finset.sum (Finset.range N) fun n => f n x)
      (fun x => ∑' n, f n x) atTop S

Uses 3 · Used by 1

Statement usesLocal normal convergence of a series of functions on a set

Proof usesNormal convergence of a series of functions on a set · Weierstrass M-test: normal convergence implies uniform convergence

Used byTermwise differentiation of locally normally convergent holomorphic series

TheoremTermwise differentiation of locally normally convergent holomorphic series#✓fully proved

Let \(E\) be a complete normed space over \(\mathbb{C}\), \(S \subseteq \mathbb{C}\) an open set and \(f_n \colon \mathbb{C} \to E\) for \(n \in \mathbb{N}\) functions that are complex differentiable on \(S\). If the series \(\sum_n f_n\) converges locally normally on \(S\), that is every \(z \in S\) has a neighbourhood \(U\) with \(\sum_n \sup_{w \in U \cap S} \|f_n(w)\| < \infty\) (suprema taken in \([0, \infty]\)), then for every \(z \in S\) the function \(w \mapsto \sum_{n=0}^{\infty} f_n(w)\) has derivative \(\sum_{n=0}^{\infty} f_n'(z)\) at \(z\).

theorem ConvergesLocallyNormallyOn.hasDerivAt_tsum
    {E : Type*} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E]
    {f : Nat → Complex → E} {S : Set Complex} {z : Complex}
    (hf : ConvergesLocallyNormallyOn f S)
    (hS : IsOpen S) (holo : ∀ n, DifferentiableOn Complex (f n) S)
    (hz : z ∈ S) :
    HasDerivAt (fun w => ∑' n, f n w) (∑' n, _root_.deriv (f n) z) z

Uses 3

Statement usesLocal normal convergence of a series of functions on a set

Proof usesDerivative series of a locally normally convergent holomorphic series · Local normal convergence implies locally uniform convergence

20 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.