InfiniteProducts.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

Uniform estimates and limits for infinite products

theorem OAI.Nagata.W03.tendstoLocallyUniformlyOn_const_one line 27
Source documentation
A constant family of functions with value one converges locally uniformly.
```
theorem tendstoLocallyUniformlyOn_const_one :
    TendstoLocallyUniformlyOn (fun _ : α => fun _ : β => (1 : R))
      (fun _ => 1) l s :=
…
```
theorem OAI.Nagata.W03.tendstoLocallyUniformlyOn_pow_one line 34
Source documentation
A fixed natural power of a family converging locally uniformly to one has the same limit. No pointwise differentiability premise is needed.
```
theorem tendstoLocallyUniformlyOn_pow_one {F : α → β → R}
    (hF : TendstoLocallyUniformlyOn F (fun _ => 1) l s) (c : ℕ) :
    TendstoLocallyUniformlyOn (fun a x => F a x ^ c) (fun _ => 1) l s := by
…
```

theorem OAI.Nagata.W03.tendstoLocallyUniformlyOn_finset_prod_one line 45

Source documentation

Every finite product of families tending locally uniformly to one tends locally uniformly to one, including the empty product.

theorem tendstoLocallyUniformlyOn_finset_prod_one {ι : Type*}
    (T : Finset ι) {F : ι → α → β → R}
    (hF : ∀ i ∈ T, TendstoLocallyUniformlyOn (F i) (fun _ => 1) l s) :
    TendstoLocallyUniformlyOn (fun a x => ∏ i ∈ T, F i a x) (fun _ => 1) l s := by
…

theorem OAI.Nagata.W03.tendstoLocallyUniformlyOn_fintype_prod_one line 60

Source documentation

Fintype form, convenient for the nine marked-point factors.

theorem tendstoLocallyUniformlyOn_fintype_prod_one {ι : Type*} [Fintype ι]
    {F : ι → α → β → R}
    (hF : ∀ i, TendstoLocallyUniformlyOn (F i) (fun _ => 1) l s) :
    TendstoLocallyUniformlyOn (fun a x => ∏ i, F i a x) (fun _ => 1) l s :=
…

theorem OAI.Nagata.W03.norm_tprod_one_add_sub_one_le line 82

Source documentation

Infinite-product version of the finite product estimate.

theorem norm_tprod_one_add_sub_one_le {ι R : Type*}
    [NormedCommRing R] [NormOneClass R] [CompleteSpace R]
    {u : ι → R} (hu : Summable (fun i => ‖u i‖)) :
    ‖(∏' i, (1 + u i)) - 1‖ ≤ Real.exp (∑' i, ‖u i‖) - 1 := by
…

theorem OAI.Nagata.W03.norm_tprod_one_add_sub_one_le_of_tsum_norm_le line 95

Source documentation

A scalar upper bound on the norm sum bounds the infinite product's error.

theorem norm_tprod_one_add_sub_one_le_of_tsum_norm_le {ι R : Type*}
    [NormedCommRing R] [NormOneClass R] [CompleteSpace R]
    {u : ι → R} {B : ℝ} (hu : Summable (fun i => ‖u i‖))
    (hB : (∑' i, ‖u i‖) ≤ B) :
    ‖(∏' i, (1 + u i)) - 1‖ ≤ Real.exp B - 1 :=
…

theorem OAI.Nagata.W03.tendstoUniformlyOn_tprod_one_add_of_tsum_norm_le line 105

Source documentation

Uniform vanishing of a scalar bound on total norms makes the actual products converge uniformly to one. Summability and bounds need hold only eventually.

theorem tendstoUniformlyOn_tprod_one_add_of_tsum_norm_le
    {α β ι R : Type*} [NormedCommRing R] [NormOneClass R] [CompleteSpace R]
    {l : Filter α} {s : Set β} {u : α → ι → β → R} {B : α → ℝ}
    (hB : Tendsto B l (𝓝 0))
    (hsum : ∀ᶠ a in l, ∀ x ∈ s, Summable (fun i => ‖u a i x‖))
    (hbound : ∀ᶠ a in l, ∀ x ∈ s, (∑' i, ‖u a i x‖) ≤ B a) :
    TendstoUniformlyOn (fun a x => ∏' i, (1 + u a i x)) (fun _ => 1) l s := by
…

theorem OAI.Nagata.W03.tendstoLocallyUniformlyOn_tprod_one_add_of_local_tsum_norm_le line 125

Source documentation

Local bounds may use a different scalar majorant on each neighbourhood.

theorem tendstoLocallyUniformlyOn_tprod_one_add_of_local_tsum_norm_le
    {α β ι R : Type*} [TopologicalSpace β]
    [NormedCommRing R] [NormOneClass R] [CompleteSpace R]
    {l : Filter α} {s : Set β} {u : α → ι → β → R}
    (hlocal : ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, ∃ B : α → ℝ,
      Tendsto B l (𝓝 0) ∧
      (∀ᶠ a in l, ∀ y ∈ t, Summable (fun i => ‖u a i y‖)) ∧
      (∀ᶠ a in l, ∀ y ∈ t, (∑' i, ‖u a i y‖) ≤ B a)) :
    TendstoLocallyUniformlyOn (fun a x => ∏' i, (1 + u a i x))
      (fun _ => 1) l s := by
…

theorem OAI.Nagata.W03.tendstoLocallyUniformlyOn_tprod_one_add_of_compact_tsum_norm_le line 142

Source documentation

On an open locally compact domain it suffices to give vanishing majorants on every compact subset; this is the usual analytic local-uniform formulation.

theorem tendstoLocallyUniformlyOn_tprod_one_add_of_compact_tsum_norm_le
    {α β ι R : Type*} [TopologicalSpace β] [LocallyCompactSpace β]
    [NormedCommRing R] [NormOneClass R] [CompleteSpace R]
    {l : Filter α} {s : Set β} {u : α → ι → β → R} (hs : IsOpen s)
    (hcompact : ∀ K : Set β, K ⊆ s → IsCompact K → ∃ B : α → ℝ,
      Tendsto B l (𝓝 0) ∧
      (∀ᶠ a in l, ∀ x ∈ K, Summable (fun i => ‖u a i x‖)) ∧
      (∀ᶠ a in l, ∀ x ∈ K, (∑' i, ‖u a i x‖) ≤ B a)) :
    TendstoLocallyUniformlyOn (fun a x => ∏' i, (1 + u a i x))
      (fun _ => 1) l s := by
…