Infinite sum and products that converge uniformly

Main definitions

• HasProdUniformlyOn f g s : ∏ i, f i b converges uniformly on s to g.
• HasProdLocallyUniformlyOn f g s : ∏ i, f i b converges locally uniformly on s to g.
• HasProdUniformly f g : ∏ i, f i b converges uniformly to g.
• HasProdLocallyUniformly f g : ∏ i, f i b converges locally uniformly to g.

Uniform convergence of sums and products

def HasProdUniformlyOn {α : Type u_1} {β : Type u_2} {ι : Type u_3} [CommMonoid α] (f : ι → β → α) (g : β → α) (s : Set β) [UniformSpace α] : Prop

HasProdUniformlyOn f g s means that the (potentially infinite) product ∏' i, f i b for b : β converges uniformly on s to g.

Equations

• HasProdUniformlyOn f g s = HasProd (⇑(UniformOnFun.ofFun {s}) ∘ f) ((UniformOnFun.ofFun {s}) g)

def HasSumUniformlyOn {α : Type u_1} {β : Type u_2} {ι : Type u_3} [AddCommMonoid α] (f : ι → β → α) (g : β → α) (s : Set β) [UniformSpace α] : Prop

HasSumUniformlyOn f g s means that the (potentially infinite) sum ∑' i, f i b for b : β converges uniformly on s to g.

Equations

• HasSumUniformlyOn f g s = HasSum (⇑(UniformOnFun.ofFun {s}) ∘ f) ((UniformOnFun.ofFun {s}) g)

def MultipliableUniformlyOn {α : Type u_1} {β : Type u_2} {ι : Type u_3} [CommMonoid α] (f : ι → β → α) (s : Set β) [UniformSpace α] : Prop

MultipliableUniformlyOn f s means that there is some infinite product to which f converges uniformly on s. Use fun x ↦ ∏' i, f i x to get the product function.

Equations

• MultipliableUniformlyOn f s = Multipliable (⇑(UniformOnFun.ofFun {s}) ∘ f)

def SummableUniformlyOn {α : Type u_1} {β : Type u_2} {ι : Type u_3} [AddCommMonoid α] (f : ι → β → α) (s : Set β) [UniformSpace α] : Prop

SummableUniformlyOn f s means that there is some infinite sum to which f converges uniformly on s. Use fun x ↦ ∑' i, f i x to get the sum function.

Equations

• SummableUniformlyOn f s = Summable (⇑(UniformOnFun.ofFun {s}) ∘ f)

theorem MultipliableUniformlyOn.exists {α : Type u_1} {β : Type u_2} {ι : Type u_3} [CommMonoid α] {f : ι → β → α} {s : Set β} [UniformSpace α] (h : MultipliableUniformlyOn f s) : ∃ (g : β → α), HasProdUniformlyOn f g s

theorem SummableUniformlyOn.exists {α : Type u_1} {β : Type u_2} {ι : Type u_3} [AddCommMonoid α] {f : ι → β → α} {s : Set β} [UniformSpace α] (h : SummableUniformlyOn f s) : ∃ (g : β → α), HasSumUniformlyOn f g s

theorem HasProdUniformlyOn.multipliableUniformlyOn {α : Type u_1} {β : Type u_2} {ι : Type u_3} [CommMonoid α] {f : ι → β → α} {g : β → α} {s : Set β} [UniformSpace α] (h : HasProdUniformlyOn f g s) : MultipliableUniformlyOn f s

theorem HasSumUniformlyOn.summableUniformlyOn {α : Type u_1} {β : Type u_2} {ι : Type u_3} [AddCommMonoid α] {f : ι → β → α} {g : β → α} {s : Set β} [UniformSpace α] (h : HasSumUniformlyOn f g s) : SummableUniformlyOn f s

theorem hasProdUniformlyOn_iff_tendstoUniformlyOn {α : Type u_1} {β : Type u_2} {ι : Type u_3} [CommMonoid α] {f : ι → β → α} {g : β → α} {s : Set β} [UniformSpace α] : HasProdUniformlyOn f g s ↔ TendstoUniformlyOn (fun (x1 : Finset ι) (x2 : β) => ∏ i ∈ x1, f i x2) g Filter.atTop s

theorem hasSumUniformlyOn_iff_tendstoUniformlyOn {α : Type u_1} {β : Type u_2} {ι : Type u_3} [AddCommMonoid α] {f : ι → β → α} {g : β → α} {s : Set β} [UniformSpace α] : HasSumUniformlyOn f g s ↔ TendstoUniformlyOn (fun (x1 : Finset ι) (x2 : β) => ∑ i ∈ x1, f i x2) g Filter.atTop s

theorem HasProdUniformlyOn.tendstoUniformlyOn {α : Type u_1} {β : Type u_2} {ι : Type u_3} [CommMonoid α] {f : ι → β → α} {g : β → α} {s : Set β} [UniformSpace α] : HasProdUniformlyOn f g s → TendstoUniformlyOn (fun (x1 : Finset ι) (x2 : β) => ∏ i ∈ x1, f i x2) g Filter.atTop s

Alias of the forward direction of hasProdUniformlyOn_iff_tendstoUniformlyOn.

theorem HasSumUniformlyOn.tendstoUniformlyOn {α : Type u_1} {β : Type u_2} {ι : Type u_3} [AddCommMonoid α] {f : ι → β → α} {g : β → α} {s : Set β} [UniformSpace α] : HasSumUniformlyOn f g s → TendstoUniformlyOn (fun (x1 : Finset ι) (x2 : β) => ∑ i ∈ x1, f i x2) g Filter.atTop s

theorem HasProdUniformlyOn.congr {α : Type u_1} {β : Type u_2} {ι : Type u_3} [CommMonoid α] {f : ι → β → α} {g : β → α} {s : Set β} [UniformSpace α] {f' : ι → β → α} (h : HasProdUniformlyOn f g s) (hff' : ∀ᶠ (n : Finset ι) in Filter.atTop, Set.EqOn (fun (x : β) => ∏ i ∈ n, f i x) (fun (x : β) => ∏ i ∈ n, f' i x) s) : HasProdUniformlyOn f' g s

theorem HasSumUniformlyOn.congr {α : Type u_1} {β : Type u_2} {ι : Type u_3} [AddCommMonoid α] {f : ι → β → α} {g : β → α} {s : Set β} [UniformSpace α] {f' : ι → β → α} (h : HasSumUniformlyOn f g s) (hff' : ∀ᶠ (n : Finset ι) in Filter.atTop, Set.EqOn (fun (x : β) => ∑ i ∈ n, f i x) (fun (x : β) => ∑ i ∈ n, f' i x) s) : HasSumUniformlyOn f' g s

theorem HasProdUniformlyOn.congr_right {α : Type u_1} {β : Type u_2} {ι : Type u_3} [CommMonoid α] {f : ι → β → α} {g : β → α} {s : Set β} [UniformSpace α] {g' : β → α} (h : HasProdUniformlyOn f g s) (hgg' : Set.EqOn g g' s) : HasProdUniformlyOn f g' s

theorem HasSumUniformlyOn.congr_right {α : Type u_1} {β : Type u_2} {ι : Type u_3} [AddCommMonoid α] {f : ι → β → α} {g : β → α} {s : Set β} [UniformSpace α] {g' : β → α} (h : HasSumUniformlyOn f g s) (hgg' : Set.EqOn g g' s) : HasSumUniformlyOn f g' s

theorem HasProdUniformlyOn.tendstoUniformlyOn_finsetRange {α : Type u_1} {β : Type u_2} [CommMonoid α] {g : β → α} {s : Set β} [UniformSpace α] {f : ℕ → β → α} (h : HasProdUniformlyOn f g s) : TendstoUniformlyOn (fun (x1 : ℕ) (x2 : β) => ∏ i ∈ Finset.range x1, f i x2) g Filter.atTop s

theorem HasSumUniformlyOn.tendstoUniformlyOn_finsetRange {α : Type u_1} {β : Type u_2} [AddCommMonoid α] {g : β → α} {s : Set β} [UniformSpace α] {f : ℕ → β → α} (h : HasSumUniformlyOn f g s) : TendstoUniformlyOn (fun (x1 : ℕ) (x2 : β) => ∑ i ∈ Finset.range x1, f i x2) g Filter.atTop s

theorem HasProdUniformlyOn.hasProd {α : Type u_1} {β : Type u_2} {ι : Type u_3} [CommMonoid α] {f : ι → β → α} {g : β → α} {x : β} {s : Set β} [UniformSpace α] (h : HasProdUniformlyOn f g 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 : β → α} {x : β} {s : Set β} [UniformSpace α] (h : HasSumUniformlyOn f g 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 : β → α} {s : Set β} [UniformSpace α] [T2Space α] (h : HasProdUniformlyOn f g s) : Set.EqOn (fun (x : β) => ∏' (b : ι), f b x) g s

theorem HasSumUniformlyOn.tsum_eqOn {α : Type u_1} {β : Type u_2} {ι : Type u_3} [AddCommMonoid α] {f : ι → β → α} {g : β → α} {s : Set β} [UniformSpace α] [T2Space α] (h : HasSumUniformlyOn f g s) : Set.EqOn (fun (x : β) => ∑' (b : ι), f b x) g s

@[deprecated HasProdUniformlyOn.tprod_eqOn (since := "2025-11-23")]

theorem HasProdUniformlyOn.tprod_eq {α : Type u_1} {β : Type u_2} {ι : Type u_3} [CommMonoid α] {f : ι → β → α} {g : β → α} {s : Set β} [UniformSpace α] [T2Space α] (h : HasProdUniformlyOn f g s) : Set.EqOn (fun (x : β) => ∏' (b : ι), f b x) g s

Alias of HasProdUniformlyOn.tprod_eqOn.

@[deprecated HasSumUniformlyOn.tsum_eqOn (since := "2025-11-23")]

theorem HasSumUniformlyOn.tsum_eq {α : Type u_1} {β : Type u_2} {ι : Type u_3} [AddCommMonoid α] {f : ι → β → α} {g : β → α} {s : Set β} [UniformSpace α] [T2Space α] (h : HasSumUniformlyOn f g s) : Set.EqOn (fun (x : β) => ∑' (b : ι), f b x) g s

Alias of HasSumUniformlyOn.tsum_eqOn.

theorem MultipliableUniformlyOn.multipliable {α : Type u_1} {β : Type u_2} {ι : Type u_3} [CommMonoid α] {f : ι → β → α} {x : β} {s : Set β} [UniformSpace α] (h : MultipliableUniformlyOn f 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 : ι → β → α} {x : β} {s : Set β} [UniformSpace α] (h : SummableUniformlyOn f 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 : ι → β → α} {s : Set β} [UniformSpace α] (h : MultipliableUniformlyOn f s) : HasProdUniformlyOn f (fun (x : β) => ∏' (i : ι), f i x) s

theorem SummableUniformlyOn.hasSumUniformlyOn {α : Type u_1} {β : Type u_2} {ι : Type u_3} [AddCommMonoid α] {f : ι → β → α} {s : Set β} [UniformSpace α] (h : SummableUniformlyOn f s) : HasSumUniformlyOn f (fun (x : β) => ∑' (i : ι), f i x) s

theorem multipliableUniformlyOn_iff_hasProdUniformlyOn {α : Type u_1} {β : Type u_2} {ι : Type u_3} [CommMonoid α] {f : ι → β → α} {s : Set β} [UniformSpace α] : MultipliableUniformlyOn f s ↔ HasProdUniformlyOn f (fun (x : β) => ∏' (i : ι), f i x) s

theorem summableUniformlyOn_iff_hasSumUniformlyOn {α : Type u_1} {β : Type u_2} {ι : Type u_3} [AddCommMonoid α] {f : ι → β → α} {s : Set β} [UniformSpace α] : SummableUniformlyOn f s ↔ HasSumUniformlyOn f (fun (x : β) => ∑' (i : ι), f i x) s

theorem HasProdUniformlyOn.mono {α : Type u_1} {β : Type u_2} {ι : Type u_3} [CommMonoid α] {f : ι → β → α} {g : β → α} {s : Set β} [UniformSpace α] {t : Set β} (h : HasProdUniformlyOn f g t) (hst : s ⊆ t) : HasProdUniformlyOn f g s

theorem HasSumUniformlyOn.mono {α : Type u_1} {β : Type u_2} {ι : Type u_3} [AddCommMonoid α] {f : ι → β → α} {g : β → α} {s : Set β} [UniformSpace α] {t : Set β} (h : HasSumUniformlyOn f g t) (hst : s ⊆ t) : HasSumUniformlyOn f g s

theorem MultipliableUniformlyOn.mono {α : Type u_1} {β : Type u_2} {ι : Type u_3} [CommMonoid α] {f : ι → β → α} {s : Set β} [UniformSpace α] {t : Set β} (h : MultipliableUniformlyOn f t) (hst : s ⊆ t) : MultipliableUniformlyOn f s

theorem SummableUniformlyOn.mono {α : Type u_1} {β : Type u_2} {ι : Type u_3} [AddCommMonoid α] {f : ι → β → α} {s : Set β} [UniformSpace α] {t : Set β} (h : SummableUniformlyOn f t) (hst : s ⊆ t) : SummableUniformlyOn f s

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 β] : Prop

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 (x1 : Finset ι) (x2 : β) => ∏ i ∈ x1, f i x2) g Filter.atTop s

def HasSumLocallyUniformlyOn {α : Type u_1} {β : Type u_2} {ι : Type u_3} [AddCommMonoid α] (f : ι → β → α) (g : β → α) (s : Set β) [UniformSpace α] [TopologicalSpace β] : Prop

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 (x1 : Finset ι) (x2 : β) => ∑ i ∈ x1, f i x2) g Filter.atTop s

def MultipliableLocallyUniformlyOn {α : Type u_1} {β : Type u_2} {ι : Type u_3} [CommMonoid α] (f : ι → β → α) (s : Set β) [UniformSpace α] [TopologicalSpace β] : Prop

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

def SummableLocallyUniformlyOn {α : Type u_1} {β : Type u_2} {ι : Type u_3} [AddCommMonoid α] (f : ι → β → α) (s : Set β) [UniformSpace α] [TopologicalSpace β] : Prop

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

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 (x1 : Finset ι) (x2 : β) => ∏ i ∈ x1, f i x2) 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 (x1 : Finset ι) (x2 : β) => ∑ i ∈ x1, f i x2) 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) : HasProdLocallyUniformlyOn 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 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.

theorem HasProdLocallyUniformlyOn.hasProdUniformlyOn_of_isCompact {α : Type u_1} {β : Type u_2} {ι : Type u_3} [CommMonoid α] {f : ι → β → α} {g : β → α} {s : Set β} [UniformSpace α] [TopologicalSpace β] (h : HasProdLocallyUniformlyOn f g s) (hs : IsCompact s) : HasProdUniformlyOn f g s

theorem HasProdLocallyUniformlyOn.exists_hasProdUniformlyOn {α : Type u_1} {β : Type u_2} {ι : Type u_3} [CommMonoid α] {f : ι → β → α} {g : β → α} {x : β} {s : Set β} [UniformSpace α] [TopologicalSpace β] [LocallyCompactSpace β] (h : HasProdLocallyUniformlyOn f g s) (hx : s ∈ nhds x) : ∃ t ∈ nhdsWithin x s, HasProdUniformlyOn f g t

@[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) : HasProdLocallyUniformlyOn f g s

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) : HasProdLocallyUniformlyOn 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) : HasProdLocallyUniformlyOn f g s

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) : MultipliableLocallyUniformlyOn f 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) : SummableLocallyUniformlyOn f s

theorem HasProdLocallyUniformlyOn.mono {α : Type u_1} {β : Type u_2} {ι : Type u_3} [CommMonoid α] {f : ι → β → α} {g : β → α} {s : Set β} [UniformSpace α] [TopologicalSpace β] {t : Set β} (h : HasProdLocallyUniformlyOn f g t) (hst : s ⊆ t) : HasProdLocallyUniformlyOn f g s

theorem HasSumLocallyUniformlyOn.mono {α : Type u_1} {β : Type u_2} {ι : Type u_3} [AddCommMonoid α] {f : ι → β → α} {g : β → α} {s : Set β} [UniformSpace α] [TopologicalSpace β] {t : Set β} (h : HasSumLocallyUniformlyOn f g t) (hst : s ⊆ t) : HasSumLocallyUniformlyOn f g s

theorem MultipliableLocallyUniformlyOn.mono {α : Type u_1} {β : Type u_2} {ι : Type u_3} [CommMonoid α] {f : ι → β → α} {s : Set β} [UniformSpace α] [TopologicalSpace β] {t : Set β} (h : MultipliableLocallyUniformlyOn f t) (hst : s ⊆ t) : MultipliableLocallyUniformlyOn f s

theorem SummableLocallyUniformlyOn.mono {α : Type u_1} {β : Type u_2} {ι : Type u_3} [AddCommMonoid α] {f : ι → β → α} {s : Set β} [UniformSpace α] [TopologicalSpace β] {t : Set β} (h : SummableLocallyUniformlyOn f t) (hst : s ⊆ t) : SummableLocallyUniformlyOn f s

theorem multipliableLocallyUniformlyOn_of_of_forall_exists_nhds {α : Type u_1} {β : Type u_2} {ι : Type u_3} [CommMonoid α] {f : ι → β → α} {s : Set β} [UniformSpace α] [TopologicalSpace β] (h : ∀ x ∈ s, ∃ t ∈ nhdsWithin x s, MultipliableUniformlyOn f t) : MultipliableLocallyUniformlyOn f s

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 β] (h : ∀ x ∈ s, ∃ t ∈ nhdsWithin x s, SummableUniformlyOn f t) : SummableLocallyUniformlyOn f s

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 β] (h : ∀ x ∈ s, ∃ t ∈ nhdsWithin x s, MultipliableUniformlyOn f t) : MultipliableLocallyUniformlyOn f s

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 β] (h : ∀ x ∈ s, ∃ t ∈ nhdsWithin x s, SummableUniformlyOn f t) : SummableLocallyUniformlyOn f s

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 MultipliableLocallyUniformlyOn.multipliableUniformlyOn_of_isCompact {α : Type u_1} {β : Type u_2} {ι : Type u_3} [CommMonoid α] {f : ι → β → α} {s : Set β} [UniformSpace α] [TopologicalSpace β] (h : MultipliableLocallyUniformlyOn f s) (hs : IsCompact s) : MultipliableUniformlyOn f s

theorem MultipliableLocallyUniformlyOn.exists_multipliableUniformlyOn {α : Type u_1} {β : Type u_2} {ι : Type u_3} [CommMonoid α] {f : ι → β → α} {x : β} {s : Set β} [UniformSpace α] [TopologicalSpace β] [LocallyCompactSpace β] (h : MultipliableLocallyUniformlyOn f s) (hx : s ∈ nhds x) : ∃ t ∈ nhdsWithin x s, MultipliableUniformlyOn f t

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 β] (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 β] (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) : Set.EqOn (fun (x : β) => ∏' (i : ι), f i x) 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) : Set.EqOn (fun (x : β) => ∑' (i : ι), f i x) g s

theorem MultipliableLocallyUniformlyOn_congr {α : Type u_1} {β : Type u_2} {ι : Type u_3} [CommMonoid α] {s : Set β} [UniformSpace α] [TopologicalSpace β] {f f' : ι → β → α} (h : ∀ (i : ι), Set.EqOn (f i) (f' i) s) (h2 : MultipliableLocallyUniformlyOn f s) : MultipliableLocallyUniformlyOn f' s

theorem SummableLocallyUniformlyOn_congr {α : Type u_1} {β : Type u_2} {ι : Type u_3} [AddCommMonoid α] {s : Set β} [UniformSpace α] [TopologicalSpace β] {f f' : ι → β → α} (h : ∀ (i : ι), Set.EqOn (f i) (f' i) s) (h2 : SummableLocallyUniformlyOn f s) : 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

theorem multipliableLocallyUniformlyOn_iff_hasProdLocallyUniformlyOn {α : Type u_1} {β : Type u_2} {ι : Type u_3} [CommMonoid α] {f : ι → β → α} {s : Set β} [UniformSpace α] [TopologicalSpace β] : MultipliableLocallyUniformlyOn f s ↔ HasProdLocallyUniformlyOn f (fun (x : β) => ∏' (i : ι), f i x) s

theorem summableLocallyUniformlyOn_iff_hasSumLocallyUniformlyOn {α : Type u_1} {β : Type u_2} {ι : Type u_3} [AddCommMonoid α] {f : ι → β → α} {s : Set β} [UniformSpace α] [TopologicalSpace β] : SummableLocallyUniformlyOn f s ↔ HasSumLocallyUniformlyOn f (fun (x : β) => ∑' (i : ι), f i x) s

def HasProdUniformly {α : Type u_1} {β : Type u_2} {ι : Type u_3} [CommMonoid α] (f : ι → β → α) (g : β → α) [UniformSpace α] : Prop

HasProdUniformly f g means that the product ∏ i, f i b converges uniformly (wrt b) to g.

Equations

• HasProdUniformly f g = HasProd (⇑UniformFun.ofFun ∘ f) (UniformFun.ofFun g)

def HasSumUniformly {α : Type u_1} {β : Type u_2} {ι : Type u_3} [AddCommMonoid α] (f : ι → β → α) (g : β → α) [UniformSpace α] : Prop

HasSumUniformly f g means that the sum ∑ i, f i b converges uniformly (wrt b) to g.

Equations

• HasSumUniformly f g = HasSum (⇑UniformFun.ofFun ∘ f) (UniformFun.ofFun g)

def MultipliableUniformly {α : Type u_1} {β : Type u_2} {ι : Type u_3} [CommMonoid α] (f : ι → β → α) [UniformSpace α] : Prop

MultipliableUniformly f means that there is some infinite product to which f converges uniformly. Use fun x ↦ ∏' i, f i x to get the product function.

Equations

• MultipliableUniformly f = Multipliable (⇑UniformFun.ofFun ∘ f)

def SummableUniformly {α : Type u_1} {β : Type u_2} {ι : Type u_3} [AddCommMonoid α] (f : ι → β → α) [UniformSpace α] : Prop

SummableUniformly f means that there is some infinite sum to which f converges uniformly. Use fun x ↦ ∑' i, f i x to get the product function.

Equations

• SummableUniformly f = Summable (⇑UniformFun.ofFun ∘ f)

theorem MultipliableUniformly.exists {α : Type u_1} {β : Type u_2} {ι : Type u_3} [CommMonoid α] {f : ι → β → α} [UniformSpace α] (h : MultipliableUniformly f) : ∃ (g : β → α), HasProdUniformly f g

theorem SummableUniformly.exists {α : Type u_1} {β : Type u_2} {ι : Type u_3} [AddCommMonoid α] {f : ι → β → α} [UniformSpace α] (h : SummableUniformly f) : ∃ (g : β → α), HasSumUniformly f g

theorem HasProdUniformly.multipliableUniformly {α : Type u_1} {β : Type u_2} {ι : Type u_3} [CommMonoid α] {f : ι → β → α} {g : β → α} [UniformSpace α] (h : HasProdUniformly f g) : MultipliableUniformly f

theorem HasSumUniformly.summableUniformly {α : Type u_1} {β : Type u_2} {ι : Type u_3} [AddCommMonoid α] {f : ι → β → α} {g : β → α} [UniformSpace α] (h : HasSumUniformly f g) : SummableUniformly f

theorem hasProdUniformly_iff_tendstoUniformly {α : Type u_1} {β : Type u_2} {ι : Type u_3} [CommMonoid α] {f : ι → β → α} {g : β → α} [UniformSpace α] : HasProdUniformly f g ↔ TendstoUniformly (fun (x1 : Finset ι) (x2 : β) => ∏ i ∈ x1, f i x2) g Filter.atTop

theorem hasSumUniformly_iff_tendstoUniformly {α : Type u_1} {β : Type u_2} {ι : Type u_3} [AddCommMonoid α] {f : ι → β → α} {g : β → α} [UniformSpace α] : HasSumUniformly f g ↔ TendstoUniformly (fun (x1 : Finset ι) (x2 : β) => ∑ i ∈ x1, f i x2) g Filter.atTop

theorem HasProdUniformly.tendstoUniformly {α : Type u_1} {β : Type u_2} {ι : Type u_3} [CommMonoid α] {f : ι → β → α} {g : β → α} [UniformSpace α] : HasProdUniformly f g → TendstoUniformly (fun (x1 : Finset ι) (x2 : β) => ∏ i ∈ x1, f i x2) g Filter.atTop

Alias of the forward direction of hasProdUniformly_iff_tendstoUniformly.

theorem HasSumUniformly.tendstoUniformly {α : Type u_1} {β : Type u_2} {ι : Type u_3} [AddCommMonoid α] {f : ι → β → α} {g : β → α} [UniformSpace α] : HasSumUniformly f g → TendstoUniformly (fun (x1 : Finset ι) (x2 : β) => ∑ i ∈ x1, f i x2) g Filter.atTop

theorem HasProdUniformly.hasProdUniformlyOn {α : Type u_1} {β : Type u_2} {ι : Type u_3} [CommMonoid α] {f : ι → β → α} {g : β → α} {s : Set β} [UniformSpace α] (h : HasProdUniformly f g) : HasProdUniformlyOn f g s

theorem HasSumUniformly.hasSumUniformlyOn {α : Type u_1} {β : Type u_2} {ι : Type u_3} [AddCommMonoid α] {f : ι → β → α} {g : β → α} {s : Set β} [UniformSpace α] (h : HasSumUniformly f g) : HasSumUniformlyOn f g s

theorem hasProdUniformlyOn_univ_iff {α : Type u_1} {β : Type u_2} {ι : Type u_3} [CommMonoid α] {f : ι → β → α} {g : β → α} [UniformSpace α] : HasProdUniformlyOn f g Set.univ ↔ HasProdUniformly f g

theorem hasSumUniformlyOn_univ_iff {α : Type u_1} {β : Type u_2} {ι : Type u_3} [AddCommMonoid α] {f : ι → β → α} {g : β → α} [UniformSpace α] : HasSumUniformlyOn f g Set.univ ↔ HasSumUniformly f g

theorem MultipliableUniformly.multipliableUniformlyOn {α : Type u_1} {β : Type u_2} {ι : Type u_3} [CommMonoid α] {f : ι → β → α} {s : Set β} [UniformSpace α] (h : MultipliableUniformly f) : MultipliableUniformlyOn f s

theorem SummableUniformly.summableUniformlyOn {α : Type u_1} {β : Type u_2} {ι : Type u_3} [AddCommMonoid α] {f : ι → β → α} {s : Set β} [UniformSpace α] (h : SummableUniformly f) : SummableUniformlyOn f s

theorem multipliableUniformlyOn_univ_iff {α : Type u_1} {β : Type u_2} {ι : Type u_3} [CommMonoid α] {f : ι → β → α} [UniformSpace α] : MultipliableUniformlyOn f Set.univ ↔ MultipliableUniformly f

theorem summableUniformlyOn_univ_iff {α : Type u_1} {β : Type u_2} {ι : Type u_3} [AddCommMonoid α] {f : ι → β → α} [UniformSpace α] : SummableUniformlyOn f Set.univ ↔ SummableUniformly f

theorem HasProdUniformly.congr {α : Type u_1} {β : Type u_2} {ι : Type u_3} [CommMonoid α] {f : ι → β → α} {g : β → α} [UniformSpace α] {f' : ι → β → α} (h : HasProdUniformly f g) (hff' : ∀ᶠ (n : Finset ι) in Filter.atTop, ∀ (b : β), ∏ i ∈ n, f i b = ∏ i ∈ n, f' i b) : HasProdUniformly f' g

theorem HasSumUniformly.congr {α : Type u_1} {β : Type u_2} {ι : Type u_3} [AddCommMonoid α] {f : ι → β → α} {g : β → α} [UniformSpace α] {f' : ι → β → α} (h : HasSumUniformly f g) (hff' : ∀ᶠ (n : Finset ι) in Filter.atTop, ∀ (b : β), ∑ i ∈ n, f i b = ∑ i ∈ n, f' i b) : HasSumUniformly f' g

theorem HasProdUniformly.tendstoUniformlyOn_finsetRange {α : Type u_1} {β : Type u_2} [CommMonoid α] {g : β → α} [UniformSpace α] {f : ℕ → β → α} (h : HasProdUniformly f g) : TendstoUniformly (fun (x1 : ℕ) (x2 : β) => ∏ i ∈ Finset.range x1, f i x2) g Filter.atTop

theorem HasSumUniformly.tendstoUniformlyOn_finsetRange {α : Type u_1} {β : Type u_2} [AddCommMonoid α] {g : β → α} [UniformSpace α] {f : ℕ → β → α} (h : HasSumUniformly f g) : TendstoUniformly (fun (x1 : ℕ) (x2 : β) => ∑ i ∈ Finset.range x1, f i x2) g Filter.atTop

theorem HasProdUniformly.hasProd {α : Type u_1} {β : Type u_2} {ι : Type u_3} [CommMonoid α] {f : ι → β → α} {g : β → α} {x : β} [UniformSpace α] (h : HasProdUniformly f g) : HasProd (fun (x_1 : ι) => f x_1 x) (g x)

theorem HasSumUniformly.hasSum {α : Type u_1} {β : Type u_2} {ι : Type u_3} [AddCommMonoid α] {f : ι → β → α} {g : β → α} {x : β} [UniformSpace α] (h : HasSumUniformly f g) : HasSum (fun (x_1 : ι) => f x_1 x) (g x)

theorem MultipliableUniformly.multipliable {α : Type u_1} {β : Type u_2} {ι : Type u_3} [CommMonoid α] {f : ι → β → α} {x : β} [UniformSpace α] (h : MultipliableUniformly f) : Multipliable fun (x_1 : ι) => f x_1 x

theorem SummableUniformly.summable {α : Type u_1} {β : Type u_2} {ι : Type u_3} [AddCommMonoid α] {f : ι → β → α} {x : β} [UniformSpace α] (h : SummableUniformly f) : Summable fun (x_1 : ι) => f x_1 x

theorem MultipliableUniformly.hasProdUniformly {α : Type u_1} {β : Type u_2} {ι : Type u_3} [CommMonoid α] {f : ι → β → α} [UniformSpace α] (h : MultipliableUniformly f) : HasProdUniformly f fun (x : β) => ∏' (i : ι), f i x

theorem SummableUniformly.hasSumUniformly {α : Type u_1} {β : Type u_2} {ι : Type u_3} [AddCommMonoid α] {f : ι → β → α} [UniformSpace α] (h : SummableUniformly f) : HasSumUniformly f fun (x : β) => ∑' (i : ι), f i x

theorem multipliableUniformly_iff_hasProdUniformly {α : Type u_1} {β : Type u_2} {ι : Type u_3} [CommMonoid α] {f : ι → β → α} [UniformSpace α] : MultipliableUniformly f ↔ HasProdUniformly f fun (x : β) => ∏' (i : ι), f i x

theorem summableUniformly_iff_hasSumUniformly {α : Type u_1} {β : Type u_2} {ι : Type u_3} [AddCommMonoid α] {f : ι → β → α} [UniformSpace α] : SummableUniformly f ↔ HasSumUniformly f fun (x : β) => ∑' (i : ι), f i x

Locally uniform convergence of sums and products

def HasProdLocallyUniformly {α : Type u_1} {β : Type u_2} {ι : Type u_3} [CommMonoid α] (f : ι → β → α) (g : β → α) [UniformSpace α] [TopologicalSpace β] : Prop

HasProdLocallyUniformly f g means that the (potentially infinite) product ∏' i, f i b for b : β converges locally uniformly to g b (in the sense of TendstoLocallyUniformly).

Equations

• HasProdLocallyUniformly f g = TendstoLocallyUniformly (fun (x1 : Finset ι) (x2 : β) => ∏ i ∈ x1, f i x2) g Filter.atTop

def HasSumLocallyUniformly {α : Type u_1} {β : Type u_2} {ι : Type u_3} [AddCommMonoid α] (f : ι → β → α) (g : β → α) [UniformSpace α] [TopologicalSpace β] : Prop

HasSumLocallyUniformly f g means that the (potentially infinite) sum ∑' i, f i b for b : β converges locally uniformly to g b (in the sense of TendstoLocallyUniformly).

Equations

• HasSumLocallyUniformly f g = TendstoLocallyUniformly (fun (x1 : Finset ι) (x2 : β) => ∑ i ∈ x1, f i x2) g Filter.atTop

def MultipliableLocallyUniformly {α : Type u_1} {β : Type u_2} {ι : Type u_3} [CommMonoid α] (f : ι → β → α) [UniformSpace α] [TopologicalSpace β] : Prop

MultipliableLocallyUniformly f means that the product ∏' i, f i b converges locally uniformly to something.

Equations

• MultipliableLocallyUniformly f = ∃ (g : β → α), HasProdLocallyUniformly f g

def SummableLocallyUniformly {α : Type u_1} {β : Type u_2} {ι : Type u_3} [AddCommMonoid α] (f : ι → β → α) [UniformSpace α] [TopologicalSpace β] : Prop

SummableLocallyUniformly f means that ∑' i, f i b converges locally uniformly to something.

Equations

• SummableLocallyUniformly f = ∃ (g : β → α), HasSumLocallyUniformly f g

theorem MultipliableLocallyUniformly.exists {α : Type u_1} {β : Type u_2} {ι : Type u_3} [CommMonoid α] {f : ι → β → α} [UniformSpace α] [TopologicalSpace β] (h : MultipliableLocallyUniformly f) : ∃ (g : β → α), HasProdLocallyUniformly f g

theorem SummableLocallyUniformly.exists {α : Type u_1} {β : Type u_2} {ι : Type u_3} [AddCommMonoid α] {f : ι → β → α} [UniformSpace α] [TopologicalSpace β] (h : SummableLocallyUniformly f) : ∃ (g : β → α), HasSumLocallyUniformly f g

theorem HasProdLocallyUniformly.multipliableLocallyUniformly {α : Type u_1} {β : Type u_2} {ι : Type u_3} [CommMonoid α] {f : ι → β → α} {g : β → α} [UniformSpace α] [TopologicalSpace β] (h : HasProdLocallyUniformly f g) : MultipliableLocallyUniformly f

theorem HasSumLocallyUniformly.summableLocallyUniformly {α : Type u_1} {β : Type u_2} {ι : Type u_3} [AddCommMonoid α] {f : ι → β → α} {g : β → α} [UniformSpace α] [TopologicalSpace β] (h : HasSumLocallyUniformly f g) : SummableLocallyUniformly f

theorem hasProdLocallyUniformly_iff_tendstoLocallyUniformly {α : Type u_1} {β : Type u_2} {ι : Type u_3} [CommMonoid α] {f : ι → β → α} {g : β → α} [UniformSpace α] [TopologicalSpace β] : HasProdLocallyUniformly f g ↔ TendstoLocallyUniformly (fun (x1 : Finset ι) (x2 : β) => ∏ i ∈ x1, f i x2) g Filter.atTop

theorem hasSumLocallyUniformly_iff_tendstoLocallyUniformly {α : Type u_1} {β : Type u_2} {ι : Type u_3} [AddCommMonoid α] {f : ι → β → α} {g : β → α} [UniformSpace α] [TopologicalSpace β] : HasSumLocallyUniformly f g ↔ TendstoLocallyUniformly (fun (x1 : Finset ι) (x2 : β) => ∑ i ∈ x1, f i x2) g Filter.atTop

theorem HasProdLocallyUniformly.hasProdLocallyUniformlyOn {α : Type u_1} {β : Type u_2} {ι : Type u_3} [CommMonoid α] {f : ι → β → α} {g : β → α} {s : Set β} [UniformSpace α] [TopologicalSpace β] (h : HasProdLocallyUniformly f g) : HasProdLocallyUniformlyOn f g s

theorem HasSumLocallyUniformly.hasSumLocallyUniformlyOn {α : Type u_1} {β : Type u_2} {ι : Type u_3} [AddCommMonoid α] {f : ι → β → α} {g : β → α} {s : Set β} [UniformSpace α] [TopologicalSpace β] (h : HasSumLocallyUniformly f g) : HasSumLocallyUniformlyOn f g s

theorem MultipliableLocallyUniformly.multipliableLocallyUniformlyOn {α : Type u_1} {β : Type u_2} {ι : Type u_3} [CommMonoid α] {f : ι → β → α} {s : Set β} [UniformSpace α] [TopologicalSpace β] (h : MultipliableLocallyUniformly f) : MultipliableLocallyUniformlyOn f s

theorem SummableLocallyUniformly.summableLocallyUniformlyOn {α : Type u_1} {β : Type u_2} {ι : Type u_3} [AddCommMonoid α] {f : ι → β → α} {s : Set β} [UniformSpace α] [TopologicalSpace β] (h : SummableLocallyUniformly f) : SummableLocallyUniformlyOn f s

theorem hasProdLocallyUniformly_of_of_forall_exists_nhds {α : Type u_1} {β : Type u_2} {ι : Type u_3} [CommMonoid α] {f : ι → β → α} {g : β → α} [UniformSpace α] [TopologicalSpace β] (h : ∀ (x : β), ∃ t ∈ nhds x, HasProdUniformlyOn f g t) : HasProdLocallyUniformly f g

If every x has a neighbourhood on which b ↦ ∏' i, f i b converges uniformly to g, then the product converges locally uniformly to g. Note that this is not a tautology, and the converse is only true if the domain is locally compact.

theorem hasSumLocallyUniformly_of_of_forall_exists_nhds {α : Type u_1} {β : Type u_2} {ι : Type u_3} [AddCommMonoid α] {f : ι → β → α} {g : β → α} [UniformSpace α] [TopologicalSpace β] (h : ∀ (x : β), ∃ t ∈ nhds x, HasSumUniformlyOn f g t) : HasSumLocallyUniformly f g

If every x has a neighbourhood 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 HasProdUniformly.hasProdLocallyUniformly {α : Type u_1} {β : Type u_2} {ι : Type u_3} [CommMonoid α] {f : ι → β → α} {g : β → α} [UniformSpace α] [TopologicalSpace β] (h : HasProdUniformly f g) : HasProdLocallyUniformly f g

theorem HasSumUniformly.hasSumLocallyUniformly {α : Type u_1} {β : Type u_2} {ι : Type u_3} [AddCommMonoid α] {f : ι → β → α} {g : β → α} [UniformSpace α] [TopologicalSpace β] (h : HasSumUniformly f g) : HasSumLocallyUniformly f g

theorem hasProdLocallyUniformly_of_forall_compact {α : Type u_1} {β : Type u_2} {ι : Type u_3} [CommMonoid α] {f : ι → β → α} {g : β → α} [UniformSpace α] [TopologicalSpace β] [LocallyCompactSpace β] (h : ∀ (K : Set β), IsCompact K → HasProdUniformlyOn f g K) : HasProdLocallyUniformly f g

theorem hasSumLocallyUniformly_of_forall_compact {α : Type u_1} {β : Type u_2} {ι : Type u_3} [AddCommMonoid α] {f : ι → β → α} {g : β → α} [UniformSpace α] [TopologicalSpace β] [LocallyCompactSpace β] (h : ∀ (K : Set β), IsCompact K → HasSumUniformlyOn f g K) : HasSumLocallyUniformly f g

theorem multipliableLocallyUniformly_of_of_forall_exists_nhds {α : Type u_1} {β : Type u_2} {ι : Type u_3} [CommMonoid α] {f : ι → β → α} [UniformSpace α] [TopologicalSpace β] (h : ∀ (x : β), ∃ t ∈ nhds x, MultipliableUniformlyOn f t) : MultipliableLocallyUniformly f

theorem summableLocallyUniformly_of_of_forall_exists_nhds {α : Type u_1} {β : Type u_2} {ι : Type u_3} [AddCommMonoid α] {f : ι → β → α} [UniformSpace α] [TopologicalSpace β] (h : ∀ (x : β), ∃ t ∈ nhds x, SummableUniformlyOn f t) : SummableLocallyUniformly f

theorem HasProdLocallyUniformly.hasProd {α : Type u_1} {β : Type u_2} {ι : Type u_3} [CommMonoid α] {f : ι → β → α} {g : β → α} {x : β} [UniformSpace α] [TopologicalSpace β] (h : HasProdLocallyUniformly f g) : HasProd (fun (x_1 : ι) => f x_1 x) (g x)

theorem HasSumLocallyUniformly.hasSum {α : Type u_1} {β : Type u_2} {ι : Type u_3} [AddCommMonoid α] {f : ι → β → α} {g : β → α} {x : β} [UniformSpace α] [TopologicalSpace β] (h : HasSumLocallyUniformly f g) : HasSum (fun (x_1 : ι) => f x_1 x) (g x)

theorem MultipliableLocallyUniformly.multipliable {α : Type u_1} {β : Type u_2} {ι : Type u_3} [CommMonoid α] {f : ι → β → α} {x : β} [UniformSpace α] [TopologicalSpace β] (h : MultipliableLocallyUniformly f) : Multipliable fun (x_1 : ι) => f x_1 x

theorem SummableLocallyUniformly.summable {α : Type u_1} {β : Type u_2} {ι : Type u_3} [AddCommMonoid α] {f : ι → β → α} {x : β} [UniformSpace α] [TopologicalSpace β] (h : SummableLocallyUniformly f) : Summable fun (x_1 : ι) => f x_1 x

theorem MultipliableLocallyUniformly.hasProdLocallyUniformly {α : Type u_1} {β : Type u_2} {ι : Type u_3} [CommMonoid α] {f : ι → β → α} [UniformSpace α] [TopologicalSpace β] (h : MultipliableLocallyUniformly f) : HasProdLocallyUniformly f fun (x : β) => ∏' (i : ι), f i x

theorem SummableLocallyUniformly.hasSumLocallyUniformly {α : Type u_1} {β : Type u_2} {ι : Type u_3} [AddCommMonoid α] {f : ι → β → α} [UniformSpace α] [TopologicalSpace β] (h : SummableLocallyUniformly f) : HasSumLocallyUniformly f fun (x : β) => ∑' (i : ι), f i x

theorem multipliableLocallyUniformly_iff_hasProdLocallyUniformly {α : Type u_1} {β : Type u_2} {ι : Type u_3} [CommMonoid α] {f : ι → β → α} [UniformSpace α] [TopologicalSpace β] : MultipliableLocallyUniformly f ↔ HasProdLocallyUniformly f fun (x : β) => ∏' (i : ι), f i x

theorem summableLocallyUniformly_iff_hasSumLocallyUniformly {α : Type u_1} {β : Type u_2} {ι : Type u_3} [AddCommMonoid α] {f : ι → β → α} [UniformSpace α] [TopologicalSpace β] : SummableLocallyUniformly f ↔ HasSumLocallyUniformly f fun (x : β) => ∑' (i : ι), f i x

theorem HasProdLocallyUniformly.tendstoLocallyUniformly_finsetRange {α : Type u_1} {β : Type u_2} [CommMonoid α] {g : β → α} [UniformSpace α] [TopologicalSpace β] {f : ℕ → β → α} (h : HasProdLocallyUniformly f g) : TendstoLocallyUniformly (fun (x1 : ℕ) (x2 : β) => ∏ i ∈ Finset.range x1, f i x2) g Filter.atTop

theorem HasSumLocallyUniformly.tendstoLocallyUniformly_finsetRange {α : Type u_1} {β : Type u_2} [AddCommMonoid α] {g : β → α} [UniformSpace α] [TopologicalSpace β] {f : ℕ → β → α} (h : HasSumLocallyUniformly f g) : TendstoLocallyUniformly (fun (x1 : ℕ) (x2 : β) => ∑ i ∈ Finset.range x1, f i x2) g Filter.atTop