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.congr
{α : Type u_1}
{β : Type u_2}
{ι : Type u_3}
[CommMonoid α]
{f : ι → β → α}
{g : β → α}
{𝔖 : Set (Set β)}
[UniformSpace α]
{f' : ι → β → α}
(h : HasProdUniformlyOn f g 𝔖)
(hff' :
∀ s ∈ 𝔖,
∀ᶠ (n : Finset ι) in Filter.atTop, Set.EqOn (fun (b : β) => ∏ i ∈ n, f i b) (fun (b : β) => ∏ i ∈ n, f' i b) s)
:
HasProdUniformlyOn f' g 𝔖
theorem
HasSumUniformlyOn.congr
{α : Type u_1}
{β : Type u_2}
{ι : Type u_3}
[AddCommMonoid α]
{f : ι → β → α}
{g : β → α}
{𝔖 : Set (Set β)}
[UniformSpace α]
{f' : ι → β → α}
(h : HasSumUniformlyOn f g 𝔖)
(hff' :
∀ s ∈ 𝔖,
∀ᶠ (n : Finset ι) in Filter.atTop, Set.EqOn (fun (b : β) => ∑ i ∈ n, f i b) (fun (b : β) => ∑ i ∈ n, f' i b) s)
:
HasSumUniformlyOn f' g 𝔖
theorem
HasProdUniformlyOn.congr_right
{α : Type u_1}
{β : Type u_2}
{ι : Type u_3}
[CommMonoid α]
{f : ι → β → α}
{g : β → α}
{𝔖 : Set (Set β)}
[UniformSpace α]
{g' : β → α}
(h : HasProdUniformlyOn f g 𝔖)
(hgg' : ∀ s ∈ 𝔖, Set.EqOn g g' s)
:
HasProdUniformlyOn f g' 𝔖
theorem
HasSumUniformlyOn.congr_right
{α : Type u_1}
{β : Type u_2}
{ι : Type u_3}
[AddCommMonoid α]
{f : ι → β → α}
{g : β → α}
{𝔖 : Set (Set β)}
[UniformSpace α]
{g' : β → α}
(h : HasSumUniformlyOn f g 𝔖)
(hgg' : ∀ s ∈ 𝔖, Set.EqOn g g' s)
:
HasSumUniformlyOn f g' 𝔖
theorem
HasProdUniformlyOn.tendstoUniformlyOn_finsetRange
{α : Type u_1}
{β : Type u_2}
[CommMonoid α]
{g : β → α}
{𝔖 : Set (Set β)}
{s : Set β}
[UniformSpace α]
{f : ℕ → β → α}
(h : HasProdUniformlyOn f g 𝔖)
(hs : s ∈ 𝔖)
:
TendstoUniformlyOn (fun (N : ℕ) (b : β) => ∏ i ∈ Finset.range N, f i b) g Filter.atTop s
theorem
HasSumUniformlyOn.tendstoUniformlyOn_finsetRange
{α : Type u_1}
{β : Type u_2}
[AddCommMonoid α]
{g : β → α}
{𝔖 : Set (Set β)}
{s : Set β}
[UniformSpace α]
{f : ℕ → β → α}
(h : HasSumUniformlyOn f g 𝔖)
(hs : s ∈ 𝔖)
:
TendstoUniformlyOn (fun (N : ℕ) (b : β) => ∑ i ∈ Finset.range N, 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_nhds
{α : 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_nhds
{α : 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.
@[deprecated hasProdLocallyUniformlyOn_of_of_forall_exists_nhds (since := "2025-05-22")]
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})
:
Alias of hasProdLocallyUniformlyOn_of_of_forall_exists_nhds.
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.
@[deprecated hasSumLocallyUniformlyOn_of_of_forall_exists_nhds (since := "2025-05-22")]
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
Alias of hasSumLocallyUniformlyOn_of_of_forall_exists_nhds.
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
HasProdUniformlyOn.hasProdLocallyUniformlyOn
{α : Type u_1}
{β : Type u_2}
{ι : Type u_3}
[CommMonoid α]
{f : ι → β → α}
{g : β → α}
{s : Set β}
[UniformSpace α]
[TopologicalSpace β]
(h : HasProdUniformlyOn f g {s})
:
theorem
HasSumUniformlyOn.hasSumLocallyUniformlyOn
{α : Type u_1}
{β : Type u_2}
{ι : Type u_3}
[AddCommMonoid α]
{f : ι → β → α}
{g : β → α}
{s : Set β}
[UniformSpace α]
[TopologicalSpace β]
(h : HasSumUniformlyOn f g {s})
:
HasSumLocallyUniformlyOn f g s
theorem
hasProdLocallyUniformlyOn_of_forall_compact
{α : Type u_1}
{β : Type u_2}
{ι : Type u_3}
[CommMonoid α]
{f : ι → β → α}
{g : β → α}
{s : Set β}
[UniformSpace α]
[TopologicalSpace β]
(hs : IsOpen s)
[LocallyCompactSpace β]
(h : ∀ K ⊆ s, IsCompact K → HasProdUniformlyOn f g {K})
:
theorem
hasSumLocallyUniformlyOn_of_forall_compact
{α : Type u_1}
{β : Type u_2}
{ι : Type u_3}
[AddCommMonoid α]
{f : ι → β → α}
{g : β → α}
{s : Set β}
[UniformSpace α]
[TopologicalSpace β]
(hs : IsOpen s)
[LocallyCompactSpace β]
(h : ∀ K ⊆ s, IsCompact K → HasSumUniformlyOn f g {K})
:
HasSumLocallyUniformlyOn f g s
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_nhds
{α : 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_nhds
{α : 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.
@[deprecated multipliableLocallyUniformlyOn_of_of_forall_exists_nhds (since := "2025-05-22")]
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})
:
Alias of multipliableLocallyUniformlyOn_of_of_forall_exists_nhds.
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.
@[deprecated summableLocallyUniformlyOn_of_of_forall_exists_nhds (since := "2025-05-22")]
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})
:
Alias of summableLocallyUniformlyOn_of_of_forall_exists_nhds.
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)
:
theorem
MultipliableLocallyUniformlyOn_congr
{α : Type u_1}
{β : Type u_2}
{ι : Type u_3}
[CommMonoid α]
{s : Set β}
[UniformSpace α]
[TopologicalSpace β]
[T2Space α]
{f f' : ι → β → α}
(h : ∀ (i : ι), Set.EqOn (f i) (f' i) s)
(h2 : MultipliableLocallyUniformlyOn f s)
:
theorem
SummableLocallyUniformlyOn_congr
{α : Type u_1}
{β : Type u_2}
{ι : Type u_3}
[AddCommMonoid α]
{s : Set β}
[UniformSpace α]
[TopologicalSpace β]
[T2Space α]
{f f' : ι → β → α}
(h : ∀ (i : ι), Set.EqOn (f i) (f' i) s)
(h2 : SummableLocallyUniformlyOn f s)
:
theorem
HasProdLocallyUniformlyOn.tendstoLocallyUniformlyOn_finsetRange
{α : Type u_1}
{β : Type u_2}
[CommMonoid α]
{g : β → α}
{s : Set β}
[UniformSpace α]
[TopologicalSpace β]
{f : ℕ → β → α}
(h : HasProdLocallyUniformlyOn f g s)
:
TendstoLocallyUniformlyOn (fun (N : ℕ) (b : β) => ∏ i ∈ Finset.range N, f i b) g Filter.atTop s
theorem
HasSumLocallyUniformlyOn.tendstoLocallyUniformlyOn_finsetRange
{α : Type u_1}
{β : Type u_2}
[AddCommMonoid α]
{g : β → α}
{s : Set β}
[UniformSpace α]
[TopologicalSpace β]
{f : ℕ → β → α}
(h : HasSumLocallyUniformlyOn f g s)
:
TendstoLocallyUniformlyOn (fun (N : ℕ) (b : β) => ∑ i ∈ Finset.range N, f i b) g Filter.atTop s