Uniform convergence of products of functions #
We gather some results about the uniform convergence of infinite products, in particular those of
the form ∏' i, (1 + f i x) for a sequence f of complex valued functions.
theorem
TendstoUniformlyOn.comp_cexp
{α : Type u_1}
{ι : Type u_2}
{K : Set α}
{f : ι → α → ℂ}
{p : Filter ι}
{g : α → ℂ}
(hf : TendstoUniformlyOn f g p K)
(hg : BddAbove ((fun (x : α) => (g x).re) '' K))
:
TendstoUniformlyOn (fun (x : ι) => Complex.exp ∘ f x) (Complex.exp ∘ g) p K
theorem
Summable.hasSumUniformlyOn_log_one_add
{α : Type u_1}
{ι : Type u_2}
{K : Set α}
{u : ι → ℝ}
{f : ι → α → ℂ}
(hu : Summable u)
(h : ∀ᶠ (i : ι) in Filter.cofinite, ∀ x ∈ K, ‖f i x‖ ≤ u i)
:
HasSumUniformlyOn (fun (i : ι) (x : α) => Complex.log (1 + f i x)) (fun (x : α) => ∑' (i : ι), Complex.log (1 + f i x))
{K}
theorem
Summable.tendstoUniformlyOn_tsum_nat_log_one_add
{α : Type u_1}
{K : Set α}
{f : ℕ → α → ℂ}
{u : ℕ → ℝ}
(hu : Summable u)
(h : ∀ᶠ (n : ℕ) in Filter.atTop, ∀ x ∈ K, ‖f n x‖ ≤ u n)
:
TendstoUniformlyOn (fun (n : ℕ) (x : α) => ∑ m ∈ Finset.range n, Complex.log (1 + f m x))
(fun (x : α) => ∑' (n : ℕ), Complex.log (1 + f n x)) Filter.atTop K
theorem
hasProdUniformlyOn_of_clog
{α : Type u_1}
{ι : Type u_2}
{𝔖 : Set (Set α)}
{f : ι → α → ℂ}
(hf : SummableUniformlyOn (fun (i : ι) (x : α) => Complex.log (f i x)) 𝔖)
(hfn : ∀ K ∈ 𝔖, ∀ x ∈ K, ∀ (i : ι), f i x ≠ 0)
(hg : ∀ K ∈ 𝔖, BddAbove ((fun (x : α) => (∑' (i : ι), Complex.log (f i x)).re) '' K))
:
HasProdUniformlyOn f (fun (x : α) => ∏' (i : ι), f i x) 𝔖
If x ↦ ∑' i, log (f i x) is uniformly convergent on 𝔖, its sum has bounded-above real part
on each set in 𝔖, and the functions f i x have no zeroes, then ∏' i, f i x is uniformly
convergent on 𝔖.
Note that the non-vanishing assumption is really needed here: if this assumption is dropped then
one obtains a counterexample if ι = α = ℕ and f i x is 0 if i = x and 1 otherwise.
theorem
multipliableUniformlyOn_of_clog
{α : Type u_1}
{ι : Type u_2}
{𝔖 : Set (Set α)}
{f : ι → α → ℂ}
(hf : SummableUniformlyOn (fun (i : ι) (x : α) => Complex.log (f i x)) 𝔖)
(hfn : ∀ K ∈ 𝔖, ∀ x ∈ K, ∀ (i : ι), f i x ≠ 0)
(hg : ∀ K ∈ 𝔖, BddAbove ((fun (x : α) => (∑' (i : ι), Complex.log (f i x)).re) '' K))
:
theorem
Summable.hasProdUniformlyOn_one_add
{α : Type u_1}
{ι : Type u_2}
{K : Set α}
{u : ι → ℝ}
{R : Type u_3}
[NormedCommRing R]
[NormOneClass R]
[CompleteSpace R]
[TopologicalSpace α]
{f : ι → α → R}
(hK : IsCompact K)
(hu : Summable u)
(h : ∀ᶠ (i : ι) in Filter.cofinite, ∀ x ∈ K, ‖f i x‖ ≤ u i)
(hcts : ∀ (i : ι), ContinuousOn (f i) K)
:
If a sequence of continuous functions f i x on an open compact K have norms eventually
bounded by a summable function, then ∏' i, (1 + f i x) is uniformly convergent on K.
theorem
Summable.multipliableUniformlyOn_one_add
{α : Type u_1}
{ι : Type u_2}
{K : Set α}
{u : ι → ℝ}
{R : Type u_3}
[NormedCommRing R]
[NormOneClass R]
[CompleteSpace R]
[TopologicalSpace α]
{f : ι → α → R}
(hK : IsCompact K)
(hu : Summable u)
(h : ∀ᶠ (i : ι) in Filter.cofinite, ∀ x ∈ K, ‖f i x‖ ≤ u i)
(hcts : ∀ (i : ι), ContinuousOn (f i) K)
:
MultipliableUniformlyOn (fun (i : ι) (x : α) => 1 + f i x) {K}
theorem
Summable.hasProdUniformlyOn_nat_one_add
{α : Type u_1}
{K : Set α}
{R : Type u_3}
[NormedCommRing R]
[NormOneClass R]
[CompleteSpace R]
[TopologicalSpace α]
{f : ℕ → α → R}
(hK : IsCompact K)
{u : ℕ → ℝ}
(hu : Summable u)
(h : ∀ᶠ (n : ℕ) in Filter.atTop, ∀ x ∈ K, ‖f n x‖ ≤ u n)
(hcts : ∀ (n : ℕ), ContinuousOn (f n) K)
:
This is a version of hasProdUniformlyOn_one_add for sequences indexed by ℕ.
theorem
Summable.multipliableUniformlyOn_nat_one_add
{α : Type u_1}
{K : Set α}
{R : Type u_3}
[NormedCommRing R]
[NormOneClass R]
[CompleteSpace R]
[TopologicalSpace α]
{f : ℕ → α → R}
(hK : IsCompact K)
{u : ℕ → ℝ}
(hu : Summable u)
(h : ∀ᶠ (n : ℕ) in Filter.atTop, ∀ x ∈ K, ‖f n x‖ ≤ u n)
(hcts : ∀ (n : ℕ), ContinuousOn (f n) K)
:
MultipliableUniformlyOn (fun (n : ℕ) (x : α) => 1 + f n x) {K}
theorem
Summable.hasProdLocallyUniformlyOn_one_add
{α : Type u_1}
{ι : Type u_2}
{K : Set α}
{u : ι → ℝ}
{R : Type u_3}
[NormedCommRing R]
[NormOneClass R]
[CompleteSpace R]
[TopologicalSpace α]
{f : ι → α → R}
[LocallyCompactSpace α]
(hK : IsOpen K)
(hu : Summable u)
(h : ∀ᶠ (i : ι) in Filter.cofinite, ∀ x ∈ K, ‖f i x‖ ≤ u i)
(hcts : ∀ (i : ι), ContinuousOn (f i) K)
:
HasProdLocallyUniformlyOn (fun (i : ι) (x : α) => 1 + f i x) (fun (x : α) => ∏' (i : ι), (1 + f i x)) K
If a sequence of continuous functions f i x on an open subset K have norms eventually
bounded by a summable function, then ∏' i, (1 + f i x) is locally uniformly convergent on K.
theorem
Summable.multipliableLocallyUniformlyOn_one_add
{α : Type u_1}
{ι : Type u_2}
{K : Set α}
{u : ι → ℝ}
{R : Type u_3}
[NormedCommRing R]
[NormOneClass R]
[CompleteSpace R]
[TopologicalSpace α]
{f : ι → α → R}
[LocallyCompactSpace α]
(hK : IsOpen K)
(hu : Summable u)
(h : ∀ᶠ (i : ι) in Filter.cofinite, ∀ x ∈ K, ‖f i x‖ ≤ u i)
(hcts : ∀ (i : ι), ContinuousOn (f i) K)
:
MultipliableLocallyUniformlyOn (fun (i : ι) (x : α) => 1 + f i x) K
theorem
Summable.hasProdLocallyUniformlyOn_nat_one_add
{α : Type u_1}
{K : Set α}
{R : Type u_3}
[NormedCommRing R]
[NormOneClass R]
[CompleteSpace R]
[TopologicalSpace α]
[LocallyCompactSpace α]
{f : ℕ → α → R}
(hK : IsOpen K)
{u : ℕ → ℝ}
(hu : Summable u)
(h : ∀ᶠ (n : ℕ) in Filter.atTop, ∀ x ∈ K, ‖f n x‖ ≤ u n)
(hcts : ∀ (n : ℕ), ContinuousOn (f n) K)
:
This is a version of hasProdLocallyUniformlyOn_one_add for sequences indexed by ℕ.
theorem
Summable.multipliableLocallyUniformlyOn_nat_one_add
{α : Type u_1}
{K : Set α}
{R : Type u_3}
[NormedCommRing R]
[NormOneClass R]
[CompleteSpace R]
[TopologicalSpace α]
[LocallyCompactSpace α]
{f : ℕ → α → R}
(hK : IsOpen K)
{u : ℕ → ℝ}
(hu : Summable u)
(h : ∀ᶠ (n : ℕ) in Filter.atTop, ∀ x ∈ K, ‖f n x‖ ≤ u n)
(hcts : ∀ (n : ℕ), ContinuousOn (f n) K)
:
MultipliableLocallyUniformlyOn (fun (n : ℕ) (x : α) => 1 + f n x) K