Infinite sum and products that converge uniformly on a set #
This file defines the notion of uniform convergence of infinite sums and products of functions, on a given family of subsets of their domain.
It also defines the notion of local uniform convergence of infinite sums and products of functions on a set.
Uniform convergence of sums and products #
def
HasProdUniformlyOn
{α : Type u_1}
{β : Type u_2}
{ι : Type u_3}
[CommMonoid α]
(f : ι → β → α)
(g : β → α)
(𝔖 : Set (Set β))
[UniformSpace α]
:
HasProdUniformlyOn f g 𝔖 means that the (potentially infinite) product ∏' i, f i b
for b : β converges uniformly on each s ∈ 𝔖 to g.
Equations
- HasProdUniformlyOn f g 𝔖 = HasProd (fun (i : ι) => (UniformOnFun.ofFun 𝔖) (f i)) ((UniformOnFun.ofFun 𝔖) g)
Instances For
def
HasSumUniformlyOn
{α : Type u_1}
{β : Type u_2}
{ι : Type u_3}
[AddCommMonoid α]
(f : ι → β → α)
(g : β → α)
(𝔖 : Set (Set β))
[UniformSpace α]
:
HasSumUniformlyOn f g 𝔖 means that the (potentially infinite) sum ∑' i, f i b
for b : β converges uniformly on each s ∈ 𝔖 to g.
Equations
- HasSumUniformlyOn f g 𝔖 = HasSum (fun (i : ι) => (UniformOnFun.ofFun 𝔖) (f i)) ((UniformOnFun.ofFun 𝔖) g)
Instances For
def
MultipliableUniformlyOn
{α : Type u_1}
{β : Type u_2}
{ι : Type u_3}
[CommMonoid α]
(f : ι → β → α)
(𝔖 : Set (Set β))
[UniformSpace α]
:
MultipliableUniformlyOn f 𝔖 means that there is some infinite product to which
f converges uniformly on every s ∈ 𝔖. Use fun x ↦ ∏' i, f i x to get the product function.
Equations
- MultipliableUniformlyOn f 𝔖 = Multipliable fun (i : ι) => (UniformOnFun.ofFun 𝔖) (f i)
Instances For
def
SummableUniformlyOn
{α : Type u_1}
{β : Type u_2}
{ι : Type u_3}
[AddCommMonoid α]
(f : ι → β → α)
(𝔖 : Set (Set β))
[UniformSpace α]
:
SummableUniformlyOn f s means that there is some infinite sum to
which f converges uniformly on every s ∈ 𝔖. Use fun x ↦ ∑' i, f i x to get the sum function.
Equations
- SummableUniformlyOn f 𝔖 = Summable fun (i : ι) => (UniformOnFun.ofFun 𝔖) (f i)
Instances For
theorem
MultipliableUniformlyOn.exists
{α : Type u_1}
{β : Type u_2}
{ι : Type u_3}
[CommMonoid α]
{f : ι → β → α}
{𝔖 : Set (Set β)}
[UniformSpace α]
(h : MultipliableUniformlyOn f 𝔖)
:
∃ (g : β → α), HasProdUniformlyOn f g 𝔖
theorem
SummableUniformlyOn.exists
{α : Type u_1}
{β : Type u_2}
{ι : Type u_3}
[AddCommMonoid α]
{f : ι → β → α}
{𝔖 : Set (Set β)}
[UniformSpace α]
(h : SummableUniformlyOn f 𝔖)
:
∃ (g : β → α), HasSumUniformlyOn f g 𝔖
theorem
HasProdUniformlyOn.multipliableUniformlyOn
{α : Type u_1}
{β : Type u_2}
{ι : Type u_3}
[CommMonoid α]
{f : ι → β → α}
{g : β → α}
{𝔖 : Set (Set β)}
[UniformSpace α]
(h : HasProdUniformlyOn f g 𝔖)
:
theorem
HasSumUniformlyOn.summableUniformlyOn
{α : Type u_1}
{β : Type u_2}
{ι : Type u_3}
[AddCommMonoid α]
{f : ι → β → α}
{g : β → α}
{𝔖 : Set (Set β)}
[UniformSpace α]
(h : HasSumUniformlyOn f g 𝔖)
:
theorem
hasProdUniformlyOn_iff_tendstoUniformlyOn
{α : Type u_1}
{β : Type u_2}
{ι : Type u_3}
[CommMonoid α]
{f : ι → β → α}
{g : β → α}
{𝔖 : Set (Set β)}
[UniformSpace α]
:
HasProdUniformlyOn f g 𝔖 ↔ ∀ s ∈ 𝔖, TendstoUniformlyOn (fun (I : Finset ι) (b : β) => ∏ i ∈ I, f i b) g Filter.atTop s
theorem
hasSumUniformlyOn_iff_tendstoUniformlyOn
{α : Type u_1}
{β : Type u_2}
{ι : Type u_3}
[AddCommMonoid α]
{f : ι → β → α}
{g : β → α}
{𝔖 : Set (Set β)}
[UniformSpace α]
:
HasSumUniformlyOn f g 𝔖 ↔ ∀ s ∈ 𝔖, TendstoUniformlyOn (fun (I : Finset ι) (b : β) => ∑ i ∈ I, f i b) g Filter.atTop s
theorem
HasProdUniformlyOn.hasProd
{α : Type u_1}
{β : Type u_2}
{ι : Type u_3}
[CommMonoid α]
{f : ι → β → α}
{g : β → α}
{𝔖 : Set (Set β)}
{x : β}
{s : Set β}
[UniformSpace α]
(h : HasProdUniformlyOn f g 𝔖)
(hs : s ∈ 𝔖)
(hx : x ∈ s)
:
HasProd (fun (x_1 : ι) => f x_1 x) (g x)
theorem
HasSumUniformlyOn.hasSum
{α : Type u_1}
{β : Type u_2}
{ι : Type u_3}
[AddCommMonoid α]
{f : ι → β → α}
{g : β → α}
{𝔖 : Set (Set β)}
{x : β}
{s : Set β}
[UniformSpace α]
(h : HasSumUniformlyOn f g 𝔖)
(hs : s ∈ 𝔖)
(hx : x ∈ s)
:
HasSum (fun (x_1 : ι) => f x_1 x) (g x)
theorem
HasProdUniformlyOn.tprod_eqOn
{α : Type u_1}
{β : Type u_2}
{ι : Type u_3}
[CommMonoid α]
{f : ι → β → α}
{g : β → α}
{𝔖 : Set (Set β)}
{s : Set β}
[UniformSpace α]
[T2Space α]
(h : HasProdUniformlyOn f g 𝔖)
(hs : s ∈ 𝔖)
:
theorem
HasSumUniformlyOn.tsum_eqOn
{α : Type u_1}
{β : Type u_2}
{ι : Type u_3}
[AddCommMonoid α]
{f : ι → β → α}
{g : β → α}
{𝔖 : Set (Set β)}
{s : Set β}
[UniformSpace α]
[T2Space α]
(h : HasSumUniformlyOn f g 𝔖)
(hs : s ∈ 𝔖)
:
theorem
HasProdUniformlyOn.tprod_eq
{α : Type u_1}
{β : Type u_2}
{ι : Type u_3}
[CommMonoid α]
{f : ι → β → α}
{g : β → α}
{𝔖 : Set (Set β)}
[UniformSpace α]
[T2Space α]
(h : HasProdUniformlyOn f g 𝔖)
(hs : ⋃₀ 𝔖 = Set.univ)
:
theorem
HasSumUniformlyOn.tsum_eq
{α : Type u_1}
{β : Type u_2}
{ι : Type u_3}
[AddCommMonoid α]
{f : ι → β → α}
{g : β → α}
{𝔖 : Set (Set β)}
[UniformSpace α]
[T2Space α]
(h : HasSumUniformlyOn f g 𝔖)
(hs : ⋃₀ 𝔖 = Set.univ)
:
theorem
MultipliableUniformlyOn.multipliable
{α : Type u_1}
{β : Type u_2}
{ι : Type u_3}
[CommMonoid α]
{f : ι → β → α}
{𝔖 : Set (Set β)}
{x : β}
{s : Set β}
[UniformSpace α]
(h : MultipliableUniformlyOn f 𝔖)
(hs : s ∈ 𝔖)
(hx : x ∈ s)
:
Multipliable fun (x_1 : ι) => f x_1 x
theorem
SummableUniformlyOn.summable
{α : Type u_1}
{β : Type u_2}
{ι : Type u_3}
[AddCommMonoid α]
{f : ι → β → α}
{𝔖 : Set (Set β)}
{x : β}
{s : Set β}
[UniformSpace α]
(h : SummableUniformlyOn f 𝔖)
(hs : s ∈ 𝔖)
(hx : x ∈ s)
:
Summable fun (x_1 : ι) => f x_1 x
theorem
MultipliableUniformlyOn.hasProdUniformlyOn
{α : Type u_1}
{β : Type u_2}
{ι : Type u_3}
[CommMonoid α]
{f : ι → β → α}
{𝔖 : Set (Set β)}
[UniformSpace α]
[T2Space α]
(h : MultipliableUniformlyOn f 𝔖)
:
HasProdUniformlyOn f (fun (x : β) => ∏' (i : ι), f i x) 𝔖
theorem
SummableUniformlyOn.hasSumUniformlyOn
{α : Type u_1}
{β : Type u_2}
{ι : Type u_3}
[AddCommMonoid α]
{f : ι → β → α}
{𝔖 : Set (Set β)}
[UniformSpace α]
[T2Space α]
(h : SummableUniformlyOn f 𝔖)
:
HasSumUniformlyOn f (fun (x : β) => ∑' (i : ι), f i x) 𝔖
## Locally uniform convergence of sums and products
def
HasProdLocallyUniformlyOn
{α : Type u_1}
{β : Type u_2}
{ι : Type u_3}
[CommMonoid α]
(f : ι → β → α)
(g : β → α)
(s : Set β)
[UniformSpace α]
[TopologicalSpace β]
:
HasProdLocallyUniformlyOn f g s means that the (potentially infinite) product ∏' i, f i b
for b : β converges locally uniformly on s to g b (in the sense of
TendstoLocallyUniformlyOn).
Equations
- HasProdLocallyUniformlyOn f g s = TendstoLocallyUniformlyOn (fun (I : Finset ι) (b : β) => ∏ i ∈ I, f i b) g Filter.atTop s
Instances For
def
HasSumLocallyUniformlyOn
{α : Type u_1}
{β : Type u_2}
{ι : Type u_3}
[AddCommMonoid α]
(f : ι → β → α)
(g : β → α)
(s : Set β)
[UniformSpace α]
[TopologicalSpace β]
:
HasSumLocallyUniformlyOn f g s means that the (potentially infinite) sum
∑' i, f i b for b : β converges locally uniformly on s to g b (in the sense of
TendstoLocallyUniformlyOn).
Equations
- HasSumLocallyUniformlyOn f g s = TendstoLocallyUniformlyOn (fun (I : Finset ι) (b : β) => ∑ i ∈ I, f i b) g Filter.atTop s
Instances For
def
MultipliableLocallyUniformlyOn
{α : Type u_1}
{β : Type u_2}
{ι : Type u_3}
[CommMonoid α]
(f : ι → β → α)
(s : Set β)
[UniformSpace α]
[TopologicalSpace β]
:
MultipliableLocallyUniformlyOn f s means that the product ∏' i, f i b converges locally
uniformly on s to something.
Equations
- MultipliableLocallyUniformlyOn f s = ∃ (g : β → α), HasProdLocallyUniformlyOn f g s
Instances For
def
SummableLocallyUniformlyOn
{α : Type u_1}
{β : Type u_2}
{ι : Type u_3}
[AddCommMonoid α]
(f : ι → β → α)
(s : Set β)
[UniformSpace α]
[TopologicalSpace β]
:
SummableLocallyUniformlyOn f s means that ∑' i, f i b converges locally
uniformly on s to something.
Equations
- SummableLocallyUniformlyOn f s = ∃ (g : β → α), HasSumLocallyUniformlyOn f g s
Instances For
theorem
hasProdLocallyUniformlyOn_iff_tendstoLocallyUniformlyOn
{α : Type u_1}
{β : Type u_2}
{ι : Type u_3}
[CommMonoid α]
{f : ι → β → α}
{g : β → α}
{s : Set β}
[UniformSpace α]
[TopologicalSpace β]
:
HasProdLocallyUniformlyOn f g s ↔ TendstoLocallyUniformlyOn (fun (I : Finset ι) (b : β) => ∏ i ∈ I, f i b) g Filter.atTop s
theorem
hasSumLocallyUniformlyOn_iff_tendstoLocallyUniformlyOn
{α : Type u_1}
{β : Type u_2}
{ι : Type u_3}
[AddCommMonoid α]
{f : ι → β → α}
{g : β → α}
{s : Set β}
[UniformSpace α]
[TopologicalSpace β]
:
HasSumLocallyUniformlyOn f g s ↔ TendstoLocallyUniformlyOn (fun (I : Finset ι) (b : β) => ∑ i ∈ I, f i b) g Filter.atTop s
theorem
hasProdLocallyUniformlyOn_of_of_forall_exists_nhd
{α : Type u_1}
{β : Type u_2}
{ι : Type u_3}
[CommMonoid α]
{f : ι → β → α}
{g : β → α}
{s : Set β}
[UniformSpace α]
[TopologicalSpace β]
(h : ∀ x ∈ s, ∃ t ∈ nhdsWithin x s, HasProdUniformlyOn f g {t})
:
If every x ∈ s has a neighbourhood within s on which b ↦ ∏' i, f i b converges uniformly
to g, then the product converges locally uniformly on s to g. Note that this is not a
tautology, and the converse is only true if the domain is locally compact.
theorem
hasSumLocallyUniformlyOn_of_of_forall_exists_nhd
{α : Type u_1}
{β : Type u_2}
{ι : Type u_3}
[AddCommMonoid α]
{f : ι → β → α}
{g : β → α}
{s : Set β}
[UniformSpace α]
[TopologicalSpace β]
(h : ∀ x ∈ s, ∃ t ∈ nhdsWithin x s, HasSumUniformlyOn f g {t})
:
HasSumLocallyUniformlyOn f g s
If every x ∈ s has a neighbourhood within s on which b ↦ ∑' i, f i b converges
uniformly to g, then the sum converges locally uniformly. Note that this is not a tautology,
and the converse is only true if the domain is locally compact.
theorem
HasProdLocallyUniformlyOn.multipliableLocallyUniformlyOn
{α : Type u_1}
{β : Type u_2}
{ι : Type u_3}
[CommMonoid α]
{f : ι → β → α}
{g : β → α}
{s : Set β}
[UniformSpace α]
[TopologicalSpace β]
(h : HasProdLocallyUniformlyOn f g s)
:
theorem
HasSumLocallyUniformlyOn.summableLocallyUniformlyOn
{α : Type u_1}
{β : Type u_2}
{ι : Type u_3}
[AddCommMonoid α]
{f : ι → β → α}
{g : β → α}
{s : Set β}
[UniformSpace α]
[TopologicalSpace β]
(h : HasSumLocallyUniformlyOn f g s)
:
theorem
multipliableLocallyUniformlyOn_of_of_forall_exists_nhd
{α : Type u_1}
{β : Type u_2}
{ι : Type u_3}
[CommMonoid α]
{f : ι → β → α}
{s : Set β}
[UniformSpace α]
[TopologicalSpace β]
[T2Space α]
(h : ∀ x ∈ s, ∃ t ∈ nhdsWithin x s, MultipliableUniformlyOn f {t})
:
If every x ∈ s has a neighbourhood within s on which b ↦ ∏' i, f i b converges uniformly,
then the product converges locally uniformly on s. Note that this is not a tautology, and the
converse is only true if the domain is locally compact.
theorem
summableLocallyUniformlyOn_of_of_forall_exists_nhd
{α : Type u_1}
{β : Type u_2}
{ι : Type u_3}
[AddCommMonoid α]
{f : ι → β → α}
{s : Set β}
[UniformSpace α]
[TopologicalSpace β]
[T2Space α]
(h : ∀ x ∈ s, ∃ t ∈ nhdsWithin x s, SummableUniformlyOn f {t})
:
If every x ∈ s has a neighbourhood within s on which b ↦ ∑' i, f i b converges
uniformly, then the sum converges locally uniformly. Note that this is not a tautology, and the
converse is only true if the domain is locally compact.
theorem
HasProdLocallyUniformlyOn.hasProd
{α : Type u_1}
{β : Type u_2}
{ι : Type u_3}
[CommMonoid α]
{f : ι → β → α}
{g : β → α}
{x : β}
{s : Set β}
[UniformSpace α]
[TopologicalSpace β]
(h : HasProdLocallyUniformlyOn f g s)
(hx : x ∈ s)
:
HasProd (fun (x_1 : ι) => f x_1 x) (g x)
theorem
HasSumLocallyUniformlyOn.hasSum
{α : Type u_1}
{β : Type u_2}
{ι : Type u_3}
[AddCommMonoid α]
{f : ι → β → α}
{g : β → α}
{x : β}
{s : Set β}
[UniformSpace α]
[TopologicalSpace β]
(h : HasSumLocallyUniformlyOn f g s)
(hx : x ∈ s)
:
HasSum (fun (x_1 : ι) => f x_1 x) (g x)
theorem
MultipliableLocallyUniformlyOn.multipliable
{α : Type u_1}
{β : Type u_2}
{ι : Type u_3}
[CommMonoid α]
{f : ι → β → α}
{x : β}
{s : Set β}
[UniformSpace α]
[TopologicalSpace β]
(h : MultipliableLocallyUniformlyOn f s)
(hx : x ∈ s)
:
Multipliable fun (x_1 : ι) => f x_1 x
theorem
SummableLocallyUniformlyOn.summable
{α : Type u_1}
{β : Type u_2}
{ι : Type u_3}
[AddCommMonoid α]
{f : ι → β → α}
{x : β}
{s : Set β}
[UniformSpace α]
[TopologicalSpace β]
(h : SummableLocallyUniformlyOn f s)
(hx : x ∈ s)
:
Summable fun (x_1 : ι) => f x_1 x
theorem
MultipliableLocallyUniformlyOn.hasProdLocallyUniformlyOn
{α : Type u_1}
{β : Type u_2}
{ι : Type u_3}
[CommMonoid α]
{f : ι → β → α}
{s : Set β}
[UniformSpace α]
[TopologicalSpace β]
[T2Space α]
(h : MultipliableLocallyUniformlyOn f s)
:
HasProdLocallyUniformlyOn f (fun (x : β) => ∏' (i : ι), f i x) s
theorem
SummableLocallyUniformlyOn.hasSumLocallyUniformlyOn
{α : Type u_1}
{β : Type u_2}
{ι : Type u_3}
[AddCommMonoid α]
{f : ι → β → α}
{s : Set β}
[UniformSpace α]
[TopologicalSpace β]
[T2Space α]
(h : SummableLocallyUniformlyOn f s)
:
HasSumLocallyUniformlyOn f (fun (x : β) => ∑' (i : ι), f i x) s
theorem
HasProdLocallyUniformlyOn.tprod_eqOn
{α : Type u_1}
{β : Type u_2}
{ι : Type u_3}
[CommMonoid α]
{f : ι → β → α}
{g : β → α}
{s : Set β}
[UniformSpace α]
[TopologicalSpace β]
[T2Space α]
(h : HasProdLocallyUniformlyOn f g s)
:
theorem
HasSumLocallyUniformlyOn.tsum_eqOn
{α : Type u_1}
{β : Type u_2}
{ι : Type u_3}
[AddCommMonoid α]
{f : ι → β → α}
{g : β → α}
{s : Set β}
[UniformSpace α]
[TopologicalSpace β]
[T2Space α]
(h : HasSumLocallyUniformlyOn f g s)
: