diff --git a/Mathlib/Analysis/Normed/Group/InfiniteSum.lean b/Mathlib/Analysis/Normed/Group/InfiniteSum.lean index 6693b108874d3c..457c5bde0e8f68 100644 --- a/Mathlib/Analysis/Normed/Group/InfiniteSum.lean +++ b/Mathlib/Analysis/Normed/Group/InfiniteSum.lean @@ -40,7 +40,7 @@ variable {ι α E F : Type*} [SeminormedAddCommGroup E] [SeminormedAddCommGroup theorem cauchySeq_finset_iff_vanishing_norm {f : ι → E} : (CauchySeq fun s : Finset ι => ∑ i in s, f i) ↔ ∀ ε > (0 : ℝ), ∃ s : Finset ι, ∀ t, Disjoint t s → ‖∑ i in t, f i‖ < ε := by - rw [cauchySeq_finset_iff_vanishing, nhds_basis_ball.forall_iff] + rw [cauchySeq_finset_iff_sum_vanishing, nhds_basis_ball.forall_iff] · simp only [ball_zero_eq, Set.mem_setOf_eq] · rintro s t hst ⟨s', hs'⟩ exact ⟨s', fun t' ht' => hst <| hs' _ ht'⟩ diff --git a/Mathlib/Tactic/ToAdditive.lean b/Mathlib/Tactic/ToAdditive.lean index c6133d37169c0f..a27d551d7dbf23 100644 --- a/Mathlib/Tactic/ToAdditive.lean +++ b/Mathlib/Tactic/ToAdditive.lean @@ -925,6 +925,7 @@ def nameDict : String → List String | "hdiv" => ["hsub"] | "hpow" => ["hsmul"] | "finprod" => ["finsum"] + | "tprod" => ["tsum"] | "pow" => ["nsmul"] | "npow" => ["nsmul"] | "zpow" => ["zsmul"] @@ -945,6 +946,7 @@ def nameDict : String → List String | "semiconj" => ["add", "Semiconj"] | "zpowers" => ["zmultiples"] | "powers" => ["multiples"] + | "multipliable"=> ["summable"] | x => [x] /-- diff --git a/Mathlib/Topology/Algebra/InfiniteSum/Basic.lean b/Mathlib/Topology/Algebra/InfiniteSum/Basic.lean index 653d4a2f3351ea..7c89212d35f55f 100644 --- a/Mathlib/Topology/Algebra/InfiniteSum/Basic.lean +++ b/Mathlib/Topology/Algebra/InfiniteSum/Basic.lean @@ -8,7 +8,7 @@ import Mathlib.Data.Fintype.BigOperators import Mathlib.Topology.Algebra.Monoid /-! -# Lemmas on infinite sums in topological monoids +# Lemmas on infinite sums and products in topological monoids This file contains many simple lemmas on `tsum`, `HasSum` etc, which are placed here in order to keep the basic file of definitions as short as possible. @@ -25,526 +25,613 @@ open scoped BigOperators Topology variable {α β γ δ : Type*} -section HasSum +section HasProd -variable [AddCommMonoid α] [TopologicalSpace α] +variable [CommMonoid α] [TopologicalSpace α] variable {f g : β → α} {a b : α} {s : Finset β} -/-- Constant zero function has sum `0` -/ -theorem hasSum_zero : HasSum (fun _ ↦ 0 : β → α) 0 := by simp [HasSum, tendsto_const_nhds] +/-- Constant one function has product `1` -/ +@[to_additive "Constant zero function has sum `0`"] +theorem hasProd_one : HasProd (fun _ ↦ 1 : β → α) 1 := by simp [HasProd, tendsto_const_nhds] #align has_sum_zero hasSum_zero -theorem hasSum_empty [IsEmpty β] : HasSum f 0 := by - convert @hasSum_zero α β _ _ +@[to_additive] +theorem hasProd_empty [IsEmpty β] : HasProd f 1 := by + convert @hasProd_one α β _ _ #align has_sum_empty hasSum_empty -theorem summable_zero : Summable (fun _ ↦ 0 : β → α) := - hasSum_zero.summable +@[to_additive] +theorem multipliable_one : Multipliable (fun _ ↦ 1 : β → α) := + hasProd_one.multipliable #align summable_zero summable_zero -theorem summable_empty [IsEmpty β] : Summable f := - hasSum_empty.summable +@[to_additive] +theorem multipliable_empty [IsEmpty β] : Multipliable f := + hasProd_empty.multipliable #align summable_empty summable_empty -theorem summable_congr (hfg : ∀ b, f b = g b) : Summable f ↔ Summable g := - iff_of_eq (congr_arg Summable <| funext hfg) +@[to_additive] +theorem multipliable_congr (hfg : ∀ b, f b = g b) : Multipliable f ↔ Multipliable g := + iff_of_eq (congr_arg Multipliable <| funext hfg) #align summable_congr summable_congr -theorem Summable.congr (hf : Summable f) (hfg : ∀ b, f b = g b) : Summable g := - (summable_congr hfg).mp hf +@[to_additive] +theorem Multipliable.congr (hf : Multipliable f) (hfg : ∀ b, f b = g b) : Multipliable g := + (multipliable_congr hfg).mp hf #align summable.congr Summable.congr -theorem HasSum.hasSum_of_sum_eq {g : γ → α} +@[to_additive] +theorem HasProd.hasProd_of_prod_eq {g : γ → α} (h_eq : ∀ u : Finset γ, ∃ v : Finset β, ∀ v', v ⊆ v' → - ∃ u', u ⊆ u' ∧ ∑ x in u', g x = ∑ b in v', f b) - (hf : HasSum g a) : HasSum f a := - le_trans (map_atTop_finset_sum_le_of_sum_eq h_eq) hf + ∃ u', u ⊆ u' ∧ ∏ x in u', g x = ∏ b in v', f b) + (hf : HasProd g a) : HasProd f a := + le_trans (map_atTop_finset_prod_le_of_prod_eq h_eq) hf #align has_sum.has_sum_of_sum_eq HasSum.hasSum_of_sum_eq -theorem hasSum_iff_hasSum {g : γ → α} +@[to_additive] +theorem hasProd_iff_hasProd {g : γ → α} (h₁ : ∀ u : Finset γ, ∃ v : Finset β, ∀ v', v ⊆ v' → - ∃ u', u ⊆ u' ∧ ∑ x in u', g x = ∑ b in v', f b) + ∃ u', u ⊆ u' ∧ ∏ x in u', g x = ∏ b in v', f b) (h₂ : ∀ v : Finset β, ∃ u : Finset γ, ∀ u', u ⊆ u' → - ∃ v', v ⊆ v' ∧ ∑ b in v', f b = ∑ x in u', g x) : - HasSum f a ↔ HasSum g a := - ⟨HasSum.hasSum_of_sum_eq h₂, HasSum.hasSum_of_sum_eq h₁⟩ + ∃ v', v ⊆ v' ∧ ∏ b in v', f b = ∏ x in u', g x) : + HasProd f a ↔ HasProd g a := + ⟨HasProd.hasProd_of_prod_eq h₂, HasProd.hasProd_of_prod_eq h₁⟩ #align has_sum_iff_has_sum hasSum_iff_hasSum -theorem Function.Injective.summable_iff {g : γ → β} (hg : Injective g) - (hf : ∀ x ∉ Set.range g, f x = 0) : Summable (f ∘ g) ↔ Summable f := - exists_congr fun _ ↦ hg.hasSum_iff hf +@[to_additive] +theorem Function.Injective.multipliable_iff {g : γ → β} (hg : Injective g) + (hf : ∀ x ∉ Set.range g, f x = 1) : Multipliable (f ∘ g) ↔ Multipliable f := + exists_congr fun _ ↦ hg.hasProd_iff hf #align function.injective.summable_iff Function.Injective.summable_iff -@[simp] theorem hasSum_extend_zero {g : β → γ} (hg : Injective g) : - HasSum (extend g f 0) a ↔ HasSum f a := by - rw [← hg.hasSum_iff, extend_comp hg] +@[to_additive (attr := simp)] theorem hasProd_extend_one {g : β → γ} (hg : Injective g) : + HasProd (extend g f 1) a ↔ HasProd f a := by + rw [← hg.hasProd_iff, extend_comp hg] exact extend_apply' _ _ -@[simp] theorem summable_extend_zero {g : β → γ} (hg : Injective g) : - Summable (extend g f 0) ↔ Summable f := - exists_congr fun _ ↦ hasSum_extend_zero hg +@[to_additive (attr := simp)] theorem multipliable_extend_one {g : β → γ} (hg : Injective g) : + Multipliable (extend g f 1) ↔ Multipliable f := + exists_congr fun _ ↦ hasProd_extend_one hg -theorem hasSum_subtype_iff_indicator {s : Set β} : - HasSum (f ∘ (↑) : s → α) a ↔ HasSum (s.indicator f) a := by - rw [← Set.indicator_range_comp, Subtype.range_coe, - hasSum_subtype_iff_of_support_subset Set.support_indicator_subset] +@[to_additive] +theorem hasProd_subtype_iff_mulIndicator {s : Set β} : + HasProd (f ∘ (↑) : s → α) a ↔ HasProd (s.mulIndicator f) a := by + rw [← Set.mulIndicator_range_comp, Subtype.range_coe, + hasProd_subtype_iff_of_mulSupport_subset Set.mulSupport_mulIndicator_subset] #align has_sum_subtype_iff_indicator hasSum_subtype_iff_indicator -theorem summable_subtype_iff_indicator {s : Set β} : - Summable (f ∘ (↑) : s → α) ↔ Summable (s.indicator f) := - exists_congr fun _ ↦ hasSum_subtype_iff_indicator +@[to_additive] +theorem multipliable_subtype_iff_mulIndicator {s : Set β} : + Multipliable (f ∘ (↑) : s → α) ↔ Multipliable (s.mulIndicator f) := + exists_congr fun _ ↦ hasProd_subtype_iff_mulIndicator #align summable_subtype_iff_indicator summable_subtype_iff_indicator -@[simp] -theorem hasSum_subtype_support : HasSum (f ∘ (↑) : support f → α) a ↔ HasSum f a := - hasSum_subtype_iff_of_support_subset <| Set.Subset.refl _ +@[to_additive (attr := simp)] +theorem hasProd_subtype_mulSupport : HasProd (f ∘ (↑) : mulSupport f → α) a ↔ HasProd f a := + hasProd_subtype_iff_of_mulSupport_subset <| Set.Subset.refl _ #align has_sum_subtype_support hasSum_subtype_support -protected theorem Finset.summable (s : Finset β) (f : β → α) : - Summable (f ∘ (↑) : (↑s : Set β) → α) := - (s.hasSum f).summable +@[to_additive] +protected theorem Finset.multipliable (s : Finset β) (f : β → α) : + Multipliable (f ∘ (↑) : (↑s : Set β) → α) := + (s.hasProd f).multipliable #align finset.summable Finset.summable -protected theorem Set.Finite.summable {s : Set β} (hs : s.Finite) (f : β → α) : - Summable (f ∘ (↑) : s → α) := by - have := hs.toFinset.summable f +@[to_additive] +protected theorem Set.Finite.multipliable {s : Set β} (hs : s.Finite) (f : β → α) : + Multipliable (f ∘ (↑) : s → α) := by + have := hs.toFinset.multipliable f rwa [hs.coe_toFinset] at this #align set.finite.summable Set.Finite.summable -theorem summable_of_finite_support (h : (support f).Finite) : Summable f := by - apply summable_of_ne_finset_zero (s := h.toFinset); simp +@[to_additive] +theorem multipliable_of_finite_mulSupport (h : (mulSupport f).Finite) : Multipliable f := by + apply multipliable_of_ne_finset_one (s := h.toFinset); simp -theorem hasSum_single {f : β → α} (b : β) (hf : ∀ (b') (_ : b' ≠ b), f b' = 0) : HasSum f (f b) := - suffices HasSum f (∑ b' in {b}, f b') by simpa using this - hasSum_sum_of_ne_finset_zero <| by simpa [hf] +@[to_additive] +theorem hasProd_single {f : β → α} (b : β) (hf : ∀ (b') (_ : b' ≠ b), f b' = 1) : HasProd f (f b) := + suffices HasProd f (∏ b' in {b}, f b') by simpa using this + hasProd_prod_of_ne_finset_one <| by simpa [hf] #align has_sum_single hasSum_single -@[simp] lemma hasSum_unique [Unique β] (f : β → α) : HasSum f (f default) := - hasSum_single default (fun _ hb ↦ False.elim <| hb <| Unique.uniq ..) +@[to_additive (attr := simp)] lemma hasProd_unique [Unique β] (f : β → α) : HasProd f (f default) := + hasProd_single default (fun _ hb ↦ False.elim <| hb <| Unique.uniq ..) -@[simp] lemma hasSum_singleton (m : β) (f : β → α) : HasSum (({m} : Set β).restrict f) (f m) := - hasSum_unique (Set.restrict {m} f) +@[to_additive (attr := simp)] +lemma hasProd_singleton (m : β) (f : β → α) : HasProd (({m} : Set β).restrict f) (f m) := + hasProd_unique (Set.restrict {m} f) -theorem hasSum_ite_eq (b : β) [DecidablePred (· = b)] (a : α) : - HasSum (fun b' ↦ if b' = b then a else 0) a := by - convert @hasSum_single _ _ _ _ (fun b' ↦ if b' = b then a else 0) b (fun b' hb' ↦ if_neg hb') +@[to_additive] +theorem hasProd_ite_eq (b : β) [DecidablePred (· = b)] (a : α) : + HasProd (fun b' ↦ if b' = b then a else 1) a := by + convert @hasProd_single _ _ _ _ (fun b' ↦ if b' = b then a else 1) b (fun b' hb' ↦ if_neg hb') exact (if_pos rfl).symm #align has_sum_ite_eq hasSum_ite_eq -theorem Equiv.hasSum_iff (e : γ ≃ β) : HasSum (f ∘ e) a ↔ HasSum f a := - e.injective.hasSum_iff <| by simp +@[to_additive] +theorem Equiv.hasProd_iff (e : γ ≃ β) : HasProd (f ∘ e) a ↔ HasProd f a := + e.injective.hasProd_iff <| by simp #align equiv.has_sum_iff Equiv.hasSum_iff -theorem Function.Injective.hasSum_range_iff {g : γ → β} (hg : Injective g) : - HasSum (fun x : Set.range g ↦ f x) a ↔ HasSum (f ∘ g) a := - (Equiv.ofInjective g hg).hasSum_iff.symm +@[to_additive] +theorem Function.Injective.hasProd_range_iff {g : γ → β} (hg : Injective g) : + HasProd (fun x : Set.range g ↦ f x) a ↔ HasProd (f ∘ g) a := + (Equiv.ofInjective g hg).hasProd_iff.symm #align function.injective.has_sum_range_iff Function.Injective.hasSum_range_iff -theorem Equiv.summable_iff (e : γ ≃ β) : Summable (f ∘ e) ↔ Summable f := - exists_congr fun _ ↦ e.hasSum_iff +@[to_additive] +theorem Equiv.multipliable_iff (e : γ ≃ β) : Multipliable (f ∘ e) ↔ Multipliable f := + exists_congr fun _ ↦ e.hasProd_iff #align equiv.summable_iff Equiv.summable_iff -theorem Equiv.hasSum_iff_of_support {g : γ → α} (e : support f ≃ support g) - (he : ∀ x : support f, g (e x) = f x) : HasSum f a ↔ HasSum g a := by +@[to_additive] +theorem Equiv.hasProd_iff_of_mulSupport {g : γ → α} (e : mulSupport f ≃ mulSupport g) + (he : ∀ x : mulSupport f, g (e x) = f x) : HasProd f a ↔ HasProd g a := by have : (g ∘ (↑)) ∘ e = f ∘ (↑) := funext he - rw [← hasSum_subtype_support, ← this, e.hasSum_iff, hasSum_subtype_support] + rw [← hasProd_subtype_mulSupport, ← this, e.hasProd_iff, hasProd_subtype_mulSupport] #align equiv.has_sum_iff_of_support Equiv.hasSum_iff_of_support -theorem hasSum_iff_hasSum_of_ne_zero_bij {g : γ → α} (i : support g → β) - (hi : Injective i) (hf : support f ⊆ Set.range i) - (hfg : ∀ x, f (i x) = g x) : HasSum f a ↔ HasSum g a := +@[to_additive] +theorem hasProd_iff_hasProd_of_ne_one_bij {g : γ → α} (i : mulSupport g → β) + (hi : Injective i) (hf : mulSupport f ⊆ Set.range i) + (hfg : ∀ x, f (i x) = g x) : HasProd f a ↔ HasProd g a := Iff.symm <| - Equiv.hasSum_iff_of_support + Equiv.hasProd_iff_of_mulSupport (Equiv.ofBijective (fun x ↦ ⟨i x, fun hx ↦ x.coe_prop <| hfg x ▸ hx⟩) ⟨fun _ _ h ↦ hi <| Subtype.ext_iff.1 h, fun y ↦ (hf y.coe_prop).imp fun _ hx ↦ Subtype.ext hx⟩) hfg #align has_sum_iff_has_sum_of_ne_zero_bij hasSum_iff_hasSum_of_ne_zero_bij -theorem Equiv.summable_iff_of_support {g : γ → α} (e : support f ≃ support g) - (he : ∀ x : support f, g (e x) = f x) : Summable f ↔ Summable g := - exists_congr fun _ ↦ e.hasSum_iff_of_support he +@[to_additive] +theorem Equiv.multipliable_iff_of_mulSupport {g : γ → α} (e : mulSupport f ≃ mulSupport g) + (he : ∀ x : mulSupport f, g (e x) = f x) : Multipliable f ↔ Multipliable g := + exists_congr fun _ ↦ e.hasProd_iff_of_mulSupport he #align equiv.summable_iff_of_support Equiv.summable_iff_of_support -protected theorem HasSum.map [AddCommMonoid γ] [TopologicalSpace γ] (hf : HasSum f a) {G} - [FunLike G α γ] [AddMonoidHomClass G α γ] (g : G) (hg : Continuous g) : - HasSum (g ∘ f) (g a) := - have : (g ∘ fun s : Finset β ↦ ∑ b in s, f b) = fun s : Finset β ↦ ∑ b in s, g (f b) := - funext <| map_sum g _ - show Tendsto (fun s : Finset β ↦ ∑ b in s, g (f b)) atTop (𝓝 (g a)) from +@[to_additive] +protected theorem HasProd.map [CommMonoid γ] [TopologicalSpace γ] (hf : HasProd f a) {G} + [FunLike G α γ] [MonoidHomClass G α γ] (g : G) (hg : Continuous g) : + HasProd (g ∘ f) (g a) := + have : (g ∘ fun s : Finset β ↦ ∏ b in s, f b) = fun s : Finset β ↦ ∏ b in s, g (f b) := + funext <| map_prod g _ + show Tendsto (fun s : Finset β ↦ ∏ b in s, g (f b)) atTop (𝓝 (g a)) from this ▸ (hg.tendsto a).comp hf #align has_sum.map HasSum.map -protected theorem Summable.map [AddCommMonoid γ] [TopologicalSpace γ] (hf : Summable f) {G} - [FunLike G α γ] [AddMonoidHomClass G α γ] (g : G) (hg : Continuous g) : Summable (g ∘ f) := - (hf.hasSum.map g hg).summable +@[to_additive] +protected theorem Multipliable.map [CommMonoid γ] [TopologicalSpace γ] (hf : Multipliable f) {G} + [FunLike G α γ] [MonoidHomClass G α γ] (g : G) (hg : Continuous g) : Multipliable (g ∘ f) := + (hf.hasProd.map g hg).multipliable #align summable.map Summable.map -protected theorem Summable.map_iff_of_leftInverse [AddCommMonoid γ] [TopologicalSpace γ] {G G'} - [FunLike G α γ] [AddMonoidHomClass G α γ] [FunLike G' γ α] [AddMonoidHomClass G' γ α] - (g : G) (g' : G') (hg : Continuous g) - (hg' : Continuous g') (hinv : Function.LeftInverse g' g) : Summable (g ∘ f) ↔ Summable f := +@[to_additive] +protected theorem Multipliable.map_iff_of_leftInverse [CommMonoid γ] [TopologicalSpace γ] {G G'} + [FunLike G α γ] [MonoidHomClass G α γ] [FunLike G' γ α] [MonoidHomClass G' γ α] + (g : G) (g' : G') (hg : Continuous g) (hg' : Continuous g') (hinv : Function.LeftInverse g' g) : + Multipliable (g ∘ f) ↔ Multipliable f := ⟨fun h ↦ by have := h.map _ hg' rwa [← Function.comp.assoc, hinv.id] at this, fun h ↦ h.map _ hg⟩ #align summable.map_iff_of_left_inverse Summable.map_iff_of_leftInverse -/-- A special case of `Summable.map_iff_of_leftInverse` for convenience -/ -protected theorem Summable.map_iff_of_equiv [AddCommMonoid γ] [TopologicalSpace γ] {G} - [EquivLike G α γ] [AddEquivClass G α γ] (g : G) (hg : Continuous g) - (hg' : Continuous (EquivLike.inv g : γ → α)) : Summable (g ∘ f) ↔ Summable f := - Summable.map_iff_of_leftInverse g (g : α ≃+ γ).symm hg hg' (EquivLike.left_inv g) +/-- "A special case of `Multipliable.map_iff_of_leftInverse` for convenience" -/ +@[to_additive "A special case of `Summable.map_iff_of_leftInverse` for convenience"] +protected theorem Multipliable.map_iff_of_equiv [CommMonoid γ] [TopologicalSpace γ] {G} + [EquivLike G α γ] [MulEquivClass G α γ] (g : G) (hg : Continuous g) + (hg' : Continuous (EquivLike.inv g : γ → α)) : Multipliable (g ∘ f) ↔ Multipliable f := + Multipliable.map_iff_of_leftInverse g (g : α ≃* γ).symm hg hg' (EquivLike.left_inv g) #align summable.map_iff_of_equiv Summable.map_iff_of_equiv -theorem Function.Surjective.summable_iff_of_hasSum_iff {α' : Type*} [AddCommMonoid α'] +@[to_additive] +theorem Function.Surjective.multipliable_iff_of_hasProd_iff {α' : Type*} [CommMonoid α'] [TopologicalSpace α'] {e : α' → α} (hes : Function.Surjective e) {f : β → α} {g : γ → α'} - (he : ∀ {a}, HasSum f (e a) ↔ HasSum g a) : Summable f ↔ Summable g := + (he : ∀ {a}, HasProd f (e a) ↔ HasProd g a) : Multipliable f ↔ Multipliable g := hes.exists.trans <| exists_congr <| @he #align function.surjective.summable_iff_of_has_sum_iff Function.Surjective.summable_iff_of_hasSum_iff -variable [ContinuousAdd α] +variable [ContinuousMul α] -theorem HasSum.add (hf : HasSum f a) (hg : HasSum g b) : HasSum (fun b ↦ f b + g b) (a + b) := by - dsimp only [HasSum] at hf hg ⊢ - simp_rw [sum_add_distrib] - exact hf.add hg +@[to_additive] +theorem HasProd.mul (hf : HasProd f a) (hg : HasProd g b) : + HasProd (fun b ↦ f b * g b) (a * b) := by + dsimp only [HasProd] at hf hg ⊢ + simp_rw [prod_mul_distrib] + exact hf.mul hg #align has_sum.add HasSum.add -theorem Summable.add (hf : Summable f) (hg : Summable g) : Summable fun b ↦ f b + g b := - (hf.hasSum.add hg.hasSum).summable +@[to_additive] +theorem Multipliable.mul (hf : Multipliable f) (hg : Multipliable g) : + Multipliable fun b ↦ f b * g b := + (hf.hasProd.mul hg.hasProd).multipliable #align summable.add Summable.add -theorem hasSum_sum {f : γ → β → α} {a : γ → α} {s : Finset γ} : - (∀ i ∈ s, HasSum (f i) (a i)) → HasSum (fun b ↦ ∑ i in s, f i b) (∑ i in s, a i) := by +@[to_additive] +theorem hasProd_prod {f : γ → β → α} {a : γ → α} {s : Finset γ} : + (∀ i ∈ s, HasProd (f i) (a i)) → HasProd (fun b ↦ ∏ i in s, f i b) (∏ i in s, a i) := by classical - exact Finset.induction_on s (by simp only [hasSum_zero, sum_empty, forall_true_iff]) <| by + exact Finset.induction_on s (by simp only [hasProd_one, prod_empty, forall_true_iff]) <| by -- Porting note: with some help, `simp` used to be able to close the goal simp (config := { contextual := true }) only [mem_insert, forall_eq_or_imp, not_false_iff, - sum_insert, and_imp] - exact fun x s _ IH hx h ↦ hx.add (IH h) + prod_insert, and_imp] + exact fun x s _ IH hx h ↦ hx.mul (IH h) #align has_sum_sum hasSum_sum -theorem summable_sum {f : γ → β → α} {s : Finset γ} (hf : ∀ i ∈ s, Summable (f i)) : - Summable fun b ↦ ∑ i in s, f i b := - (hasSum_sum fun i hi ↦ (hf i hi).hasSum).summable +@[to_additive] +theorem multipliable_prod {f : γ → β → α} {s : Finset γ} (hf : ∀ i ∈ s, Multipliable (f i)) : + Multipliable fun b ↦ ∏ i in s, f i b := + (hasProd_prod fun i hi ↦ (hf i hi).hasProd).multipliable #align summable_sum summable_sum -theorem HasSum.add_disjoint {s t : Set β} (hs : Disjoint s t) (ha : HasSum (f ∘ (↑) : s → α) a) - (hb : HasSum (f ∘ (↑) : t → α) b) : HasSum (f ∘ (↑) : (s ∪ t : Set β) → α) (a + b) := by - rw [hasSum_subtype_iff_indicator] at * - rw [Set.indicator_union_of_disjoint hs] - exact ha.add hb +@[to_additive] +theorem HasProd.mul_disjoint {s t : Set β} (hs : Disjoint s t) (ha : HasProd (f ∘ (↑) : s → α) a) + (hb : HasProd (f ∘ (↑) : t → α) b) : HasProd (f ∘ (↑) : (s ∪ t : Set β) → α) (a * b) := by + rw [hasProd_subtype_iff_mulIndicator] at * + rw [Set.mulIndicator_union_of_disjoint hs] + exact ha.mul hb #align has_sum.add_disjoint HasSum.add_disjoint -theorem hasSum_sum_disjoint {ι} (s : Finset ι) {t : ι → Set β} {a : ι → α} - (hs : (s : Set ι).Pairwise (Disjoint on t)) (hf : ∀ i ∈ s, HasSum (f ∘ (↑) : t i → α) (a i)) : - HasSum (f ∘ (↑) : (⋃ i ∈ s, t i) → α) (∑ i in s, a i) := by - simp_rw [hasSum_subtype_iff_indicator] at * - rw [Finset.indicator_biUnion _ _ hs] - exact hasSum_sum hf +@[to_additive] +theorem hasProd_prod_disjoint {ι} (s : Finset ι) {t : ι → Set β} {a : ι → α} + (hs : (s : Set ι).Pairwise (Disjoint on t)) (hf : ∀ i ∈ s, HasProd (f ∘ (↑) : t i → α) (a i)) : + HasProd (f ∘ (↑) : (⋃ i ∈ s, t i) → α) (∏ i in s, a i) := by + simp_rw [hasProd_subtype_iff_mulIndicator] at * + rw [Finset.mulIndicator_biUnion _ _ hs] + exact hasProd_prod hf #align has_sum_sum_disjoint hasSum_sum_disjoint -theorem HasSum.add_isCompl {s t : Set β} (hs : IsCompl s t) (ha : HasSum (f ∘ (↑) : s → α) a) - (hb : HasSum (f ∘ (↑) : t → α) b) : HasSum f (a + b) := by +@[to_additive] +theorem HasProd.mul_isCompl {s t : Set β} (hs : IsCompl s t) (ha : HasProd (f ∘ (↑) : s → α) a) + (hb : HasProd (f ∘ (↑) : t → α) b) : HasProd f (a * b) := by simpa [← hs.compl_eq] using - (hasSum_subtype_iff_indicator.1 ha).add (hasSum_subtype_iff_indicator.1 hb) + (hasProd_subtype_iff_mulIndicator.1 ha).mul (hasProd_subtype_iff_mulIndicator.1 hb) #align has_sum.add_is_compl HasSum.add_isCompl -theorem HasSum.add_compl {s : Set β} (ha : HasSum (f ∘ (↑) : s → α) a) - (hb : HasSum (f ∘ (↑) : (sᶜ : Set β) → α) b) : HasSum f (a + b) := - ha.add_isCompl isCompl_compl hb +@[to_additive] +theorem HasProd.mul_compl {s : Set β} (ha : HasProd (f ∘ (↑) : s → α) a) + (hb : HasProd (f ∘ (↑) : (sᶜ : Set β) → α) b) : HasProd f (a * b) := + ha.mul_isCompl isCompl_compl hb #align has_sum.add_compl HasSum.add_compl -theorem Summable.add_compl {s : Set β} (hs : Summable (f ∘ (↑) : s → α)) - (hsc : Summable (f ∘ (↑) : (sᶜ : Set β) → α)) : Summable f := - (hs.hasSum.add_compl hsc.hasSum).summable +@[to_additive] +theorem Multipliable.mul_compl {s : Set β} (hs : Multipliable (f ∘ (↑) : s → α)) + (hsc : Multipliable (f ∘ (↑) : (sᶜ : Set β) → α)) : Multipliable f := + (hs.hasProd.mul_compl hsc.hasProd).multipliable #align summable.add_compl Summable.add_compl -theorem HasSum.compl_add {s : Set β} (ha : HasSum (f ∘ (↑) : (sᶜ : Set β) → α) a) - (hb : HasSum (f ∘ (↑) : s → α) b) : HasSum f (a + b) := - ha.add_isCompl isCompl_compl.symm hb +@[to_additive] +theorem HasProd.compl_mul {s : Set β} (ha : HasProd (f ∘ (↑) : (sᶜ : Set β) → α) a) + (hb : HasProd (f ∘ (↑) : s → α) b) : HasProd f (a * b) := + ha.mul_isCompl isCompl_compl.symm hb #align has_sum.compl_add HasSum.compl_add -theorem Summable.compl_add {s : Set β} (hs : Summable (f ∘ (↑) : (sᶜ : Set β) → α)) - (hsc : Summable (f ∘ (↑) : s → α)) : Summable f := - (hs.hasSum.compl_add hsc.hasSum).summable +@[to_additive] +theorem Multipliable.compl_add {s : Set β} (hs : Multipliable (f ∘ (↑) : (sᶜ : Set β) → α)) + (hsc : Multipliable (f ∘ (↑) : s → α)) : Multipliable f := + (hs.hasProd.compl_mul hsc.hasProd).multipliable #align summable.compl_add Summable.compl_add -/-- Version of `HasSum.update` for `AddCommMonoid` rather than `AddCommGroup`. +/-- Version of `HasProd.update` for `CommMonoid` rather than `CommGroup`. +Rather than showing that `f.update` has a specific product in terms of `HasProd`, +it gives a relationship between the products of `f` and `f.update` given that both exist. -/ +@[to_additive "Version of `HasSum.update` for `AddCommMonoid` rather than `AddCommGroup`. Rather than showing that `f.update` has a specific sum in terms of `HasSum`, -it gives a relationship between the sums of `f` and `f.update` given that both exist. -/ -theorem HasSum.update' {α β : Type*} [TopologicalSpace α] [AddCommMonoid α] [T2Space α] - [ContinuousAdd α] [DecidableEq β] {f : β → α} {a a' : α} (hf : HasSum f a) (b : β) (x : α) - (hf' : HasSum (update f b x) a') : a + x = a' + f b := by - have : ∀ b', f b' + ite (b' = b) x 0 = update f b x b' + ite (b' = b) (f b) 0 := by +it gives a relationship between the sums of `f` and `f.update` given that both exist."] +theorem HasProd.update' {α β : Type*} [TopologicalSpace α] [CommMonoid α] [T2Space α] + [ContinuousMul α] [DecidableEq β] {f : β → α} {a a' : α} (hf : HasProd f a) (b : β) (x : α) + (hf' : HasProd (update f b x) a') : a * x = a' * f b := by + have : ∀ b', f b' * ite (b' = b) x 1 = update f b x b' * ite (b' = b) (f b) 1 := by intro b' split_ifs with hb' - · simpa only [Function.update_apply, hb', eq_self_iff_true] using add_comm (f b) x + · simpa only [Function.update_apply, hb', eq_self_iff_true] using mul_comm (f b) x · simp only [Function.update_apply, hb', if_false] - have h := hf.add (hasSum_ite_eq b x) + have h := hf.mul (hasProd_ite_eq b x) simp_rw [this] at h - exact HasSum.unique h (hf'.add (hasSum_ite_eq b (f b))) + exact HasProd.unique h (hf'.mul (hasProd_ite_eq b (f b))) #align has_sum.update' HasSum.update' -/-- Version of `hasSum_ite_sub_hasSum` for `AddCommMonoid` rather than `AddCommGroup`. +/-- Version of `hasProd_ite_div_hasProd` for `CommMonoid` rather than `CommGroup`. +Rather than showing that the `ite` expression has a specific product in terms of `HasProd`, it gives +a relationship between the products of `f` and `ite (n = b) 0 (f n)` given that both exist. -/ +@[to_additive "Version of `hasSum_ite_sub_hasSum` for `AddCommMonoid` rather than `AddCommGroup`. Rather than showing that the `ite` expression has a specific sum in terms of `HasSum`, -it gives a relationship between the sums of `f` and `ite (n = b) 0 (f n)` given that both exist. -/ -theorem eq_add_of_hasSum_ite {α β : Type*} [TopologicalSpace α] [AddCommMonoid α] [T2Space α] - [ContinuousAdd α] [DecidableEq β] {f : β → α} {a : α} (hf : HasSum f a) (b : β) (a' : α) - (hf' : HasSum (fun n ↦ ite (n = b) 0 (f n)) a') : a = a' + f b := by - refine' (add_zero a).symm.trans (hf.update' b 0 _) +it gives a relationship between the sums of `f` and `ite (n = b) 0 (f n)` given that both exist."] +theorem eq_mul_of_hasProd_ite {α β : Type*} [TopologicalSpace α] [CommMonoid α] [T2Space α] + [ContinuousMul α] [DecidableEq β] {f : β → α} {a : α} (hf : HasProd f a) (b : β) (a' : α) + (hf' : HasProd (fun n ↦ ite (n = b) 1 (f n)) a') : a = a' * f b := by + refine' (mul_one a).symm.trans (hf.update' b 1 _) convert hf' apply update_apply #align eq_add_of_has_sum_ite eq_add_of_hasSum_ite -end HasSum +end HasProd -section tsum +section tprod -variable [AddCommMonoid α] [TopologicalSpace α] {f g : β → α} {a a₁ a₂ : α} +variable [CommMonoid α] [TopologicalSpace α] {f g : β → α} {a a₁ a₂ : α} -theorem tsum_congr_set_coe (f : β → α) {s t : Set β} (h : s = t) : - ∑' x : s, f x = ∑' x : t, f x := by rw [h] +@[to_additive] +theorem tprod_congr_set_coe (f : β → α) {s t : Set β} (h : s = t) : + ∏' x : s, f x = ∏' x : t, f x := by rw [h] #align tsum_congr_subtype tsum_congr_set_coe -theorem tsum_congr_subtype (f : β → α) {P Q : β → Prop} (h : ∀ x, P x ↔ Q x): - ∑' x : {x // P x}, f x = ∑' x : {x // Q x}, f x := - tsum_congr_set_coe f <| Set.ext h +@[to_additive] +theorem tprod_congr_subtype (f : β → α) {P Q : β → Prop} (h : ∀ x, P x ↔ Q x): + ∏' x : {x // P x}, f x = ∏' x : {x // Q x}, f x := + tprod_congr_set_coe f <| Set.ext h -theorem tsum_eq_finsum (hf : (support f).Finite) : - ∑' b, f b = ∑ᶠ b, f b := by simp [tsum_def, summable_of_finite_support hf, hf] +@[to_additive] +theorem tprod_eq_finprod (hf : (mulSupport f).Finite) : + ∏' b, f b = ∏ᶠ b, f b := by simp [tprod_def, multipliable_of_finite_mulSupport hf, hf] -theorem tsum_eq_sum' {s : Finset β} (hf : support f ⊆ s) : - ∑' b, f b = ∑ b in s, f b := by - rw [tsum_eq_finsum (s.finite_toSet.subset hf), finsum_eq_sum_of_support_subset _ hf] +@[to_additive] +theorem tprod_eq_prod' {s : Finset β} (hf : mulSupport f ⊆ s) : + ∏' b, f b = ∏ b in s, f b := by + rw [tprod_eq_finprod (s.finite_toSet.subset hf), finprod_eq_prod_of_mulSupport_subset _ hf] -theorem tsum_eq_sum {s : Finset β} (hf : ∀ b ∉ s, f b = 0) : - ∑' b, f b = ∑ b in s, f b := - tsum_eq_sum' <| support_subset_iff'.2 hf +@[to_additive] +theorem tprod_eq_prod {s : Finset β} (hf : ∀ b ∉ s, f b = 1) : + ∏' b, f b = ∏ b in s, f b := + tprod_eq_prod' <| mulSupport_subset_iff'.2 hf #align tsum_eq_sum tsum_eq_sum -@[simp] -theorem tsum_zero : ∑' _ : β, (0 : α) = 0 := by rw [tsum_eq_finsum] <;> simp +@[to_additive (attr := simp)] +theorem tprod_one : ∏' _ : β, (1 : α) = 1 := by rw [tprod_eq_finprod] <;> simp #align tsum_zero tsum_zero #align tsum_zero' tsum_zero -@[simp] -theorem tsum_empty [IsEmpty β] : ∑' b, f b = 0 := by - rw [tsum_eq_sum (s := (∅ : Finset β))] <;> simp +@[to_additive (attr := simp)] +theorem tprod_empty [IsEmpty β] : ∏' b, f b = 1 := by + rw [tprod_eq_prod (s := (∅ : Finset β))] <;> simp #align tsum_empty tsum_empty -theorem tsum_congr {f g : β → α} - (hfg : ∀ b, f b = g b) : ∑' b, f b = ∑' b, g b := - congr_arg tsum (funext hfg) +@[to_additive] +theorem tprod_congr {f g : β → α} + (hfg : ∀ b, f b = g b) : ∏' b, f b = ∏' b, g b := + congr_arg tprod (funext hfg) #align tsum_congr tsum_congr -theorem tsum_fintype [Fintype β] (f : β → α) : ∑' b, f b = ∑ b, f b := by - apply tsum_eq_sum; simp +@[to_additive] +theorem tprod_fintype [Fintype β] (f : β → α) : ∏' b, f b = ∏ b, f b := by + apply tprod_eq_prod; simp #align tsum_fintype tsum_fintype -theorem sum_eq_tsum_indicator (f : β → α) (s : Finset β) : - ∑ x in s, f x = ∑' x, Set.indicator (↑s) f x := by - rw [tsum_eq_sum' (Set.support_indicator_subset), Finset.sum_indicator_subset _ Finset.Subset.rfl] +@[to_additive] +theorem prod_eq_tprod_mulIndicator (f : β → α) (s : Finset β) : + ∏ x in s, f x = ∏' x, Set.mulIndicator (↑s) f x := by + rw [tprod_eq_prod' (Set.mulSupport_mulIndicator_subset), + Finset.prod_mulIndicator_subset _ Finset.Subset.rfl] #align sum_eq_tsum_indicator sum_eq_tsum_indicator -theorem tsum_bool (f : Bool → α) : ∑' i : Bool, f i = f false + f true := by - rw [tsum_fintype, Fintype.sum_bool, add_comm] +@[to_additive] +theorem tprod_bool (f : Bool → α) : ∏' i : Bool, f i = f false * f true := by + rw [tprod_fintype, Fintype.prod_bool, mul_comm] #align tsum_bool tsum_bool -theorem tsum_eq_single {f : β → α} (b : β) (hf : ∀ b' ≠ b, f b' = 0) : - ∑' b, f b = f b := by - rw [tsum_eq_sum (s := {b}), sum_singleton] +@[to_additive] +theorem tprod_eq_mulSingle {f : β → α} (b : β) (hf : ∀ b' ≠ b, f b' = 1) : + ∏' b, f b = f b := by + rw [tprod_eq_prod (s := {b}), prod_singleton] exact fun b' hb' ↦ hf b' (by simpa using hb') #align tsum_eq_single tsum_eq_single -theorem tsum_tsum_eq_single (f : β → γ → α) (b : β) (c : γ) (hfb : ∀ b' ≠ b, f b' c = 0) - (hfc : ∀ b', ∀ c' ≠ c, f b' c' = 0) : ∑' (b') (c'), f b' c' = f b c := +@[to_additive] +theorem tprod_tprod_eq_mulSingle (f : β → γ → α) (b : β) (c : γ) (hfb : ∀ b' ≠ b, f b' c = 1) + (hfc : ∀ b', ∀ c' ≠ c, f b' c' = 1) : ∏' (b') (c'), f b' c' = f b c := calc - ∑' (b') (c'), f b' c' = ∑' b', f b' c := tsum_congr fun b' ↦ tsum_eq_single _ (hfc b') - _ = f b c := tsum_eq_single _ hfb + ∏' (b') (c'), f b' c' = ∏' b', f b' c := tprod_congr fun b' ↦ tprod_eq_mulSingle _ (hfc b') + _ = f b c := tprod_eq_mulSingle _ hfb #align tsum_tsum_eq_single tsum_tsum_eq_single -@[simp] -theorem tsum_ite_eq (b : β) [DecidablePred (· = b)] (a : α) : - ∑' b', (if b' = b then a else 0) = a := by - rw [tsum_eq_single b] +@[to_additive (attr := simp)] +theorem tprod_ite_eq (b : β) [DecidablePred (· = b)] (a : α) : + ∏' b', (if b' = b then a else 1) = a := by + rw [tprod_eq_mulSingle b] · simp · intro b' hb'; simp [hb'] #align tsum_ite_eq tsum_ite_eq -- Porting note: Added nolint simpNF, simpNF falsely claims that lhs does not simplify under simp -@[simp, nolint simpNF] -theorem Finset.tsum_subtype (s : Finset β) (f : β → α) : - ∑' x : { x // x ∈ s }, f x = ∑ x in s, f x := by - rw [← sum_attach]; exact tsum_fintype _ +@[to_additive (attr := simp, nolint simpNF)] +theorem Finset.tprod_subtype (s : Finset β) (f : β → α) : + ∏' x : { x // x ∈ s }, f x = ∏ x in s, f x := by + rw [← prod_attach]; exact tprod_fintype _ #align finset.tsum_subtype Finset.tsum_subtype -theorem Finset.tsum_subtype' (s : Finset β) (f : β → α) : - ∑' x : (s : Set β), f x = ∑ x in s, f x := by simp +@[to_additive] +theorem Finset.tprod_subtype' (s : Finset β) (f : β → α) : + ∏' x : (s : Set β), f x = ∏ x in s, f x := by simp #align finset.tsum_subtype' Finset.tsum_subtype' -- Porting note: Added nolint simpNF, simpNF falsely claims that lhs does not simplify under simp -@[simp, nolint simpNF] -theorem tsum_singleton (b : β) (f : β → α) : ∑' x : ({b} : Set β), f x = f b := by - rw [← coe_singleton, Finset.tsum_subtype', sum_singleton] +@[to_additive (attr := simp, nolint simpNF)] +theorem tprod_singleton (b : β) (f : β → α) : ∏' x : ({b} : Set β), f x = f b := by + rw [← coe_singleton, Finset.tprod_subtype', prod_singleton] #align tsum_singleton tsum_singleton open scoped Classical in -theorem Function.Injective.tsum_eq {g : γ → β} (hg : Injective g) {f : β → α} - (hf : support f ⊆ Set.range g) : ∑' c, f (g c) = ∑' b, f b := by - have : support f = g '' support (f ∘ g) := by - rw [support_comp_eq_preimage, Set.image_preimage_eq_iff.2 hf] +@[to_additive] +theorem Function.Injective.tprod_eq {g : γ → β} (hg : Injective g) {f : β → α} + (hf : mulSupport f ⊆ Set.range g) : ∏' c, f (g c) = ∏' b, f b := by + have : mulSupport f = g '' mulSupport (f ∘ g) := by + rw [mulSupport_comp_eq_preimage, Set.image_preimage_eq_iff.2 hf] rw [← Function.comp_def] - by_cases hf_fin : (support f).Finite - · have hfg_fin : (support (f ∘ g)).Finite := hf_fin.preimage (hg.injOn _) + by_cases hf_fin : (mulSupport f).Finite + · have hfg_fin : (mulSupport (f ∘ g)).Finite := hf_fin.preimage (hg.injOn _) lift g to γ ↪ β using hg - simp_rw [tsum_eq_sum' hf_fin.coe_toFinset.ge, tsum_eq_sum' hfg_fin.coe_toFinset.ge, - comp_apply, ← Finset.sum_map] - refine Finset.sum_congr (Finset.coe_injective ?_) fun _ _ ↦ rfl + simp_rw [tprod_eq_prod' hf_fin.coe_toFinset.ge, tprod_eq_prod' hfg_fin.coe_toFinset.ge, + comp_apply, ← Finset.prod_map] + refine Finset.prod_congr (Finset.coe_injective ?_) fun _ _ ↦ rfl simp [this] - · have hf_fin' : ¬ Set.Finite (support (f ∘ g)) := by + · have hf_fin' : ¬ Set.Finite (mulSupport (f ∘ g)) := by rwa [this, Set.finite_image_iff (hg.injOn _)] at hf_fin - simp_rw [tsum_def, if_neg hf_fin, if_neg hf_fin', Summable, - hg.hasSum_iff (support_subset_iff'.1 hf)] + simp_rw [tprod_def, if_neg hf_fin, if_neg hf_fin', Multipliable, + hg.hasProd_iff (mulSupport_subset_iff'.1 hf)] -theorem Equiv.tsum_eq (e : γ ≃ β) (f : β → α) : ∑' c, f (e c) = ∑' b, f b := - e.injective.tsum_eq <| by simp +@[to_additive] +theorem Equiv.tprod_eq (e : γ ≃ β) (f : β → α) : ∏' c, f (e c) = ∏' b, f b := + e.injective.tprod_eq <| by simp #align equiv.tsum_eq Equiv.tsum_eq -/-! ### `tsum` on subsets - part 1 -/ +/-! ### `tprod` on subsets - part 1 -/ -theorem tsum_subtype_eq_of_support_subset {f : β → α} {s : Set β} (hs : support f ⊆ s) : - ∑' x : s, f x = ∑' x, f x := - Subtype.val_injective.tsum_eq <| by simpa +@[to_additive] +theorem tprod_subtype_eq_of_mulSupport_subset {f : β → α} {s : Set β} (hs : mulSupport f ⊆ s) : + ∏' x : s, f x = ∏' x, f x := + Subtype.val_injective.tprod_eq <| by simpa #align tsum_subtype_eq_of_support_subset tsum_subtype_eq_of_support_subset -theorem tsum_subtype_support (f : β → α) : ∑' x : support f, f x = ∑' x, f x := - tsum_subtype_eq_of_support_subset Set.Subset.rfl +@[to_additive] +theorem tprod_subtype_mulSupport (f : β → α) : ∏' x : mulSupport f, f x = ∏' x, f x := + tprod_subtype_eq_of_mulSupport_subset Set.Subset.rfl -theorem tsum_subtype (s : Set β) (f : β → α) : ∑' x : s, f x = ∑' x, s.indicator f x := by - rw [← tsum_subtype_eq_of_support_subset Set.support_indicator_subset, tsum_congr] +@[to_additive] +theorem tprod_subtype (s : Set β) (f : β → α) : ∏' x : s, f x = ∏' x, s.mulIndicator f x := by + rw [← tprod_subtype_eq_of_mulSupport_subset Set.mulSupport_mulIndicator_subset, tprod_congr] simp #align tsum_subtype tsum_subtype -- Porting note: Added nolint simpNF, simpNF falsely claims that lhs does not simplify under simp -@[simp, nolint simpNF] -theorem tsum_univ (f : β → α) : ∑' x : (Set.univ : Set β), f x = ∑' x, f x := - tsum_subtype_eq_of_support_subset <| Set.subset_univ _ +@[to_additive (attr := simp, nolint simpNF)] +theorem tprod_univ (f : β → α) : ∏' x : (Set.univ : Set β), f x = ∏' x, f x := + tprod_subtype_eq_of_mulSupport_subset <| Set.subset_univ _ #align tsum_univ tsum_univ -theorem tsum_image {g : γ → β} (f : β → α) {s : Set γ} (hg : Set.InjOn g s) : - ∑' x : g '' s, f x = ∑' x : s, f (g x) := - ((Equiv.Set.imageOfInjOn _ _ hg).tsum_eq fun x ↦ f x).symm +@[to_additive] +theorem tprod_image {g : γ → β} (f : β → α) {s : Set γ} (hg : Set.InjOn g s) : + ∏' x : g '' s, f x = ∏' x : s, f (g x) := + ((Equiv.Set.imageOfInjOn _ _ hg).tprod_eq fun x ↦ f x).symm #align tsum_image tsum_image -theorem tsum_range {g : γ → β} (f : β → α) (hg : Injective g) : - ∑' x : Set.range g, f x = ∑' x, f (g x) := by - rw [← Set.image_univ, tsum_image f (hg.injOn _)] - simp_rw [← comp_apply (g := g), tsum_univ (f ∘ g)] +@[to_additive] +theorem tprod_range {g : γ → β} (f : β → α) (hg : Injective g) : + ∏' x : Set.range g, f x = ∏' x, f (g x) := by + rw [← Set.image_univ, tprod_image f (hg.injOn _)] + simp_rw [← comp_apply (g := g), tprod_univ (f ∘ g)] #align tsum_range tsum_range -/-- If `f b = 0` for all `b ∈ t`, then the sum over `f a` with `a ∈ s` is the same as the -sum over `f a` with `a ∈ s ∖ t`. -/ -lemma tsum_setElem_eq_tsum_setElem_diff {f : β → α} (s t : Set β) - (hf₀ : ∀ b ∈ t, f b = 0) : - ∑' a : s, f a = ∑' a : (s \ t : Set β), f a := - .symm <| (Set.inclusion_injective (Set.diff_subset s t)).tsum_eq (f := f ∘ (↑)) <| - support_subset_iff'.2 fun b hb ↦ hf₀ b <| by simpa using hb - -/-- If `f b = 0`, then the sum over `f a` with `a ∈ s` is the same as the sum over `f a` for +/-- If `f b = 1` for all `b ∈ t`, then the product of `f a` with `a ∈ s` is the same as the +product of `f a` with `a ∈ s ∖ t`. -/ +@[to_additive "If `f b = 0` for all `b ∈ t`, then the sum of `f a` with `a ∈ s` is the same as the +sum of `f a` with `a ∈ s ∖ t`."] +lemma tprod_setElem_eq_tprod_setElem_diff {f : β → α} (s t : Set β) + (hf₀ : ∀ b ∈ t, f b = 1) : + ∏' a : s, f a = ∏' a : (s \ t : Set β), f a := + .symm <| (Set.inclusion_injective (Set.diff_subset s t)).tprod_eq (f := f ∘ (↑)) <| + mulSupport_subset_iff'.2 fun b hb ↦ hf₀ b <| by simpa using hb + +/-- If `f b = 1`, then the product of `f a` with `a ∈ s` is the same as the product of `f a` for `a ∈ s ∖ {b}`. -/ -lemma tsum_eq_tsum_diff_singleton {f : β → α} (s : Set β) {b : β} (hf₀ : f b = 0) : - ∑' a : s, f a = ∑' a : (s \ {b} : Set β), f a := - tsum_setElem_eq_tsum_setElem_diff s {b} fun _ ha ↦ ha ▸ hf₀ - -theorem tsum_eq_tsum_of_ne_zero_bij {g : γ → α} (i : support g → β) (hi : Injective i) - (hf : support f ⊆ Set.range i) (hfg : ∀ x, f (i x) = g x) : ∑' x, f x = ∑' y, g y := by - rw [← tsum_subtype_support g, ← hi.tsum_eq hf] +@[to_additive "If `f b = 0`, then the sum of `f a` with `a ∈ s` is the same as the sum of `f a` +for `a ∈ s ∖ {b}`."] +lemma tprod_eq_tprod_diff_singleton {f : β → α} (s : Set β) {b : β} (hf₀ : f b = 1) : + ∏' a : s, f a = ∏' a : (s \ {b} : Set β), f a := + tprod_setElem_eq_tprod_setElem_diff s {b} fun _ ha ↦ ha ▸ hf₀ + +@[to_additive] +theorem tprod_eq_tprod_of_ne_one_bij {g : γ → α} (i : mulSupport g → β) (hi : Injective i) + (hf : mulSupport f ⊆ Set.range i) (hfg : ∀ x, f (i x) = g x) : ∏' x, f x = ∏' y, g y := by + rw [← tprod_subtype_mulSupport g, ← hi.tprod_eq hf] simp only [hfg] #align tsum_eq_tsum_of_ne_zero_bij tsum_eq_tsum_of_ne_zero_bij -theorem Equiv.tsum_eq_tsum_of_support {f : β → α} {g : γ → α} (e : support f ≃ support g) - (he : ∀ x, g (e x) = f x) : ∑' x, f x = ∑' y, g y := - .symm <| tsum_eq_tsum_of_ne_zero_bij _ (Subtype.val_injective.comp e.injective) (by simp) he +@[to_additive] +theorem Equiv.tprod_eq_tprod_of_mulSupport {f : β → α} {g : γ → α} + (e : mulSupport f ≃ mulSupport g) (he : ∀ x, g (e x) = f x) : + ∏' x, f x = ∏' y, g y := + .symm <| tprod_eq_tprod_of_ne_one_bij _ (Subtype.val_injective.comp e.injective) (by simp) he #align equiv.tsum_eq_tsum_of_support Equiv.tsum_eq_tsum_of_support -theorem tsum_dite_right (P : Prop) [Decidable P] (x : β → ¬P → α) : - ∑' b : β, (if h : P then (0 : α) else x b h) = if h : P then (0 : α) else ∑' b : β, x b h := by +@[to_additive] +theorem tprod_dite_right (P : Prop) [Decidable P] (x : β → ¬P → α) : + ∏' b : β, (if h : P then (1 : α) else x b h) = if h : P then (1 : α) else ∏' b : β, x b h := by by_cases hP : P <;> simp [hP] #align tsum_dite_right tsum_dite_right -theorem tsum_dite_left (P : Prop) [Decidable P] (x : β → P → α) : - ∑' b : β, (if h : P then x b h else 0) = if h : P then ∑' b : β, x b h else 0 := by +@[to_additive] +theorem tprod_dite_left (P : Prop) [Decidable P] (x : β → P → α) : + ∏' b : β, (if h : P then x b h else 1) = if h : P then ∏' b : β, x b h else 1 := by by_cases hP : P <;> simp [hP] #align tsum_dite_left tsum_dite_left -@[simp] -lemma tsum_extend_zero {γ : Type*} {g : γ → β} (hg : Injective g) (f : γ → α) : - ∑' y, extend g f 0 y = ∑' x, f x := by - have : support (extend g f 0) ⊆ Set.range g := support_subset_iff'.2 <| extend_apply' _ _ - simp_rw [← hg.tsum_eq this, hg.extend_apply] +@[to_additive (attr := simp)] +lemma tprod_extend_one {γ : Type*} {g : γ → β} (hg : Injective g) (f : γ → α) : + ∏' y, extend g f 1 y = ∏' x, f x := by + have : mulSupport (extend g f 1) ⊆ Set.range g := mulSupport_subset_iff'.2 <| extend_apply' _ _ + simp_rw [← hg.tprod_eq this, hg.extend_apply] variable [T2Space α] -theorem Function.Surjective.tsum_eq_tsum_of_hasSum_iff_hasSum {α' : Type*} [AddCommMonoid α'] - [TopologicalSpace α'] {e : α' → α} (hes : Function.Surjective e) (h0 : e 0 = 0) {f : β → α} - {g : γ → α'} (h : ∀ {a}, HasSum f (e a) ↔ HasSum g a) : ∑' b, f b = e (∑' c, g c) := - by_cases (fun x ↦ (h.mpr x.hasSum).tsum_eq) fun hg : ¬Summable g ↦ by - have hf : ¬Summable f := mt (hes.summable_iff_of_hasSum_iff @h).1 hg - simp [tsum_def, hf, hg, h0] +@[to_additive] +theorem Function.Surjective.tprod_eq_tprod_of_hasProd_iff_hasProd {α' : Type*} [CommMonoid α'] + [TopologicalSpace α'] {e : α' → α} (hes : Function.Surjective e) (h1 : e 1 = 1) {f : β → α} + {g : γ → α'} (h : ∀ {a}, HasProd f (e a) ↔ HasProd g a) : ∏' b, f b = e (∏' c, g c) := + by_cases (fun x ↦ (h.mpr x.hasProd).tprod_eq) fun hg : ¬Multipliable g ↦ by + have hf : ¬Multipliable f := mt (hes.multipliable_iff_of_hasProd_iff @h).1 hg + simp [tprod_def, hf, hg, h1] #align function.surjective.tsum_eq_tsum_of_has_sum_iff_has_sum Function.Surjective.tsum_eq_tsum_of_hasSum_iff_hasSum -theorem tsum_eq_tsum_of_hasSum_iff_hasSum {f : β → α} {g : γ → α} - (h : ∀ {a}, HasSum f a ↔ HasSum g a) : ∑' b, f b = ∑' c, g c := - surjective_id.tsum_eq_tsum_of_hasSum_iff_hasSum rfl @h +@[to_additive] +theorem tprod_eq_tprod_of_hasProd_iff_hasProd {f : β → α} {g : γ → α} + (h : ∀ {a}, HasProd f a ↔ HasProd g a) : ∏' b, f b = ∏' c, g c := + surjective_id.tprod_eq_tprod_of_hasProd_iff_hasProd rfl @h #align tsum_eq_tsum_of_has_sum_iff_has_sum tsum_eq_tsum_of_hasSum_iff_hasSum -section ContinuousAdd +section ContinuousMul -variable [ContinuousAdd α] +variable [ContinuousMul α] -theorem tsum_add (hf : Summable f) (hg : Summable g) : - ∑' b, (f b + g b) = ∑' b, f b + ∑' b, g b := - (hf.hasSum.add hg.hasSum).tsum_eq +@[to_additive] +theorem tprod_mul (hf : Multipliable f) (hg : Multipliable g) : + ∏' b, (f b * g b) = (∏' b, f b) * ∏' b, g b := + (hf.hasProd.mul hg.hasProd).tprod_eq #align tsum_add tsum_add -theorem tsum_sum {f : γ → β → α} {s : Finset γ} (hf : ∀ i ∈ s, Summable (f i)) : - ∑' b, ∑ i in s, f i b = ∑ i in s, ∑' b, f i b := - (hasSum_sum fun i hi ↦ (hf i hi).hasSum).tsum_eq +@[to_additive tsum_sum] +theorem tprod_of_prod {f : γ → β → α} {s : Finset γ} (hf : ∀ i ∈ s, Multipliable (f i)) : + ∏' b, ∏ i in s, f i b = ∏ i in s, ∏' b, f i b := + (hasProd_prod fun i hi ↦ (hf i hi).hasProd).tprod_eq #align tsum_sum tsum_sum -/-- Version of `tsum_eq_add_tsum_ite` for `AddCommMonoid` rather than `AddCommGroup`. +/-- Version of `tprod_eq_mul_tprod_ite` for `CommMonoid` rather than `CommGroup`. Requires a different convergence assumption involving `Function.update`. -/ -theorem tsum_eq_add_tsum_ite' [DecidableEq β] {f : β → α} (b : β) (hf : Summable (update f b 0)) : - ∑' x, f x = f b + ∑' x, ite (x = b) 0 (f x) := +@[to_additive "Version of `tsum_eq_add_tsum_ite` for `AddCommMonoid` rather than `AddCommGroup`. +Requires a different convergence assumption involving `Function.update`."] +theorem tprod_eq_mul_tprod_ite' [DecidableEq β] {f : β → α} (b : β) + (hf : Multipliable (update f b 1)) : + ∏' x, f x = f b * ∏' x, ite (x = b) 1 (f x) := calc - ∑' x, f x = ∑' x, (ite (x = b) (f x) 0 + update f b 0 x) := - tsum_congr fun n ↦ by split_ifs with h <;> simp [update_apply, h] - _ = ∑' x, ite (x = b) (f x) 0 + ∑' x, update f b 0 x := - tsum_add ⟨ite (b = b) (f b) 0, hasSum_single b fun b hb ↦ if_neg hb⟩ hf - _ = ite (b = b) (f b) 0 + ∑' x, update f b 0 x := by + ∏' x, f x = ∏' x, (ite (x = b) (f x) 1 * update f b 1 x) := + tprod_congr fun n ↦ by split_ifs with h <;> simp [update_apply, h] + _ = (∏' x, ite (x = b) (f x) 1) * ∏' x, update f b 1 x := + tprod_mul ⟨ite (b = b) (f b) 1, hasProd_single b fun b hb ↦ if_neg hb⟩ hf + _ = ite (b = b) (f b) 1 * ∏' x, update f b 1 x := by congr - exact tsum_eq_single b fun b' hb' ↦ if_neg hb' - _ = f b + ∑' x, ite (x = b) 0 (f x) := by + exact tprod_eq_mulSingle b fun b' hb' ↦ if_neg hb' + _ = f b * ∏' x, ite (x = b) 1 (f x) := by simp only [update, eq_self_iff_true, if_true, eq_rec_constant, dite_eq_ite] #align tsum_eq_add_tsum_ite' tsum_eq_add_tsum_ite' -theorem tsum_add_tsum_compl {s : Set β} (hs : Summable (f ∘ (↑) : s → α)) - (hsc : Summable (f ∘ (↑) : ↑sᶜ → α)) : ∑' x : s, f x + ∑' x : ↑sᶜ, f x = ∑' x, f x := - (hs.hasSum.add_compl hsc.hasSum).tsum_eq.symm +@[to_additive] +theorem tprod_mul_tprod_compl {s : Set β} (hs : Multipliable (f ∘ (↑) : s → α)) + (hsc : Multipliable (f ∘ (↑) : ↑sᶜ → α)) : (∏' x : s, f x) * ∏' x : ↑sᶜ, f x = ∏' x, f x := + (hs.hasProd.mul_compl hsc.hasProd).tprod_eq.symm #align tsum_add_tsum_compl tsum_add_tsum_compl -theorem tsum_union_disjoint {s t : Set β} (hd : Disjoint s t) (hs : Summable (f ∘ (↑) : s → α)) - (ht : Summable (f ∘ (↑) : t → α)) : ∑' x : ↑(s ∪ t), f x = ∑' x : s, f x + ∑' x : t, f x := - (hs.hasSum.add_disjoint hd ht.hasSum).tsum_eq +@[to_additive] +theorem tprod_union_disjoint {s t : Set β} (hd : Disjoint s t) (hs : Multipliable (f ∘ (↑) : s → α)) + (ht : Multipliable (f ∘ (↑) : t → α)) : + ∏' x : ↑(s ∪ t), f x = (∏' x : s, f x) * ∏' x : t, f x := + (hs.hasProd.mul_disjoint hd ht.hasProd).tprod_eq #align tsum_union_disjoint tsum_union_disjoint -theorem tsum_finset_bUnion_disjoint {ι} {s : Finset ι} {t : ι → Set β} - (hd : (s : Set ι).Pairwise (Disjoint on t)) (hf : ∀ i ∈ s, Summable (f ∘ (↑) : t i → α)) : - ∑' x : ⋃ i ∈ s, t i, f x = ∑ i in s, ∑' x : t i, f x := - (hasSum_sum_disjoint _ hd fun i hi ↦ (hf i hi).hasSum).tsum_eq +@[to_additive] +theorem tprod_finset_bUnion_disjoint {ι} {s : Finset ι} {t : ι → Set β} + (hd : (s : Set ι).Pairwise (Disjoint on t)) (hf : ∀ i ∈ s, Multipliable (f ∘ (↑) : t i → α)) : + ∏' x : ⋃ i ∈ s, t i, f x = ∏ i in s, ∏' x : t i, f x := + (hasProd_prod_disjoint _ hd fun i hi ↦ (hf i hi).hasProd).tprod_eq #align tsum_finset_bUnion_disjoint tsum_finset_bUnion_disjoint -end ContinuousAdd +end ContinuousMul -end tsum +end tprod diff --git a/Mathlib/Topology/Algebra/InfiniteSum/Constructions.lean b/Mathlib/Topology/Algebra/InfiniteSum/Constructions.lean index 64538ec837fc39..effddecdeee20c 100644 --- a/Mathlib/Topology/Algebra/InfiniteSum/Constructions.lean +++ b/Mathlib/Topology/Algebra/InfiniteSum/Constructions.lean @@ -9,8 +9,8 @@ import Mathlib.Topology.Algebra.Star /-! # Topological sums and functorial constructions -Lemmas on the interaction of `tsum`, `HasSum` etc with products, Sigma and Pi types, -`MulOpposite`, etc. +Lemmas on the interaction of `tprod`, `tsum`, `HasProd`, `HasSum` etc with products, Sigma and Pi +types, `MulOpposite`, etc. -/ @@ -27,55 +27,62 @@ variable {α β γ δ : Type*} section ProdDomain -variable [AddCommMonoid α] [TopologicalSpace α] +variable [CommMonoid α] [TopologicalSpace α] -theorem hasSum_pi_single [DecidableEq β] (b : β) (a : α) : HasSum (Pi.single b a) a := by - convert hasSum_ite_eq b a - simp [Pi.single_apply] +@[to_additive] +theorem hasProd_pi_single [DecidableEq β] (b : β) (a : α) : HasProd (Pi.mulSingle b a) a := by + convert hasProd_ite_eq b a + simp [Pi.mulSingle_apply] #align has_sum_pi_single hasSum_pi_single -@[simp] -theorem tsum_pi_single [DecidableEq β] (b : β) (a : α) : ∑' b', Pi.single b a b' = a := by - rw [tsum_eq_single b] +@[to_additive (attr := simp)] +theorem tprod_pi_single [DecidableEq β] (b : β) (a : α) : ∏' b', Pi.mulSingle b a b' = a := by + rw [tprod_eq_mulSingle b] · simp · intro b' hb'; simp [hb'] #align tsum_pi_single tsum_pi_single -lemma tsum_setProd_singleton_left (b : β) (t : Set γ) (f : β × γ → α) : - (∑' x : {b} ×ˢ t, f x) = ∑' c : t, f (b, c) := by - rw [tsum_congr_set_coe _ Set.singleton_prod, tsum_image _ ((Prod.mk.inj_left b).injOn _)] +@[to_additive tsum_setProd_singleton_left] +lemma tprod_setProd_singleton_left (b : β) (t : Set γ) (f : β × γ → α) : + (∏' x : {b} ×ˢ t, f x) = ∏' c : t, f (b, c) := by + rw [tprod_congr_set_coe _ Set.singleton_prod, tprod_image _ ((Prod.mk.inj_left b).injOn _)] -lemma tsum_setProd_singleton_right (s : Set β) (c : γ) (f : β × γ → α) : - (∑' x : s ×ˢ {c}, f x) = ∑' b : s, f (b, c) := by - rw [tsum_congr_set_coe _ Set.prod_singleton, tsum_image _ ((Prod.mk.inj_right c).injOn _)] +@[to_additive tsum_setProd_singleton_right] +lemma tprod_setProd_singleton_right (s : Set β) (c : γ) (f : β × γ → α) : + (∏' x : s ×ˢ {c}, f x) = ∏' b : s, f (b, c) := by + rw [tprod_congr_set_coe _ Set.prod_singleton, tprod_image _ ((Prod.mk.inj_right c).injOn _)] -theorem Summable.prod_symm {f : β × γ → α} (hf : Summable f) : Summable fun p : γ × β ↦ f p.swap := - (Equiv.prodComm γ β).summable_iff.2 hf +@[to_additive Summable.prod_symm] +theorem Multipliable.prod_symm {f : β × γ → α} (hf : Multipliable f) : + Multipliable fun p : γ × β ↦ f p.swap := + (Equiv.prodComm γ β).multipliable_iff.2 hf #align summable.prod_symm Summable.prod_symm end ProdDomain section ProdCodomain -variable [AddCommMonoid α] [TopologicalSpace α] [AddCommMonoid γ] [TopologicalSpace γ] +variable [CommMonoid α] [TopologicalSpace α] [CommMonoid γ] [TopologicalSpace γ] -theorem HasSum.prod_mk {f : β → α} {g : β → γ} {a : α} {b : γ} (hf : HasSum f a) (hg : HasSum g b) : - HasSum (fun x ↦ (⟨f x, g x⟩ : α × γ)) ⟨a, b⟩ := by - simp [HasSum, ← prod_mk_sum, Filter.Tendsto.prod_mk_nhds hf hg] +@[to_additive HasSum.prod_mk] +theorem HasProd.prod_mk {f : β → α} {g : β → γ} {a : α} {b : γ} + (hf : HasProd f a) (hg : HasProd g b) : HasProd (fun x ↦ (⟨f x, g x⟩ : α × γ)) ⟨a, b⟩ := by + simp [HasProd, ← prod_mk_prod, Filter.Tendsto.prod_mk_nhds hf hg] #align has_sum.prod_mk HasSum.prod_mk end ProdCodomain -section ContinuousAdd +section ContinuousMul -variable [AddCommMonoid α] [TopologicalSpace α] [ContinuousAdd α] +variable [CommMonoid α] [TopologicalSpace α] [ContinuousMul α] section RegularSpace variable [RegularSpace α] -theorem HasSum.sigma {γ : β → Type*} {f : (Σ b : β, γ b) → α} {g : β → α} {a : α} - (ha : HasSum f a) (hf : ∀ b, HasSum (fun c ↦ f ⟨b, c⟩) (g b)) : HasSum g a := by +@[to_additive] +theorem HasProd.sigma {γ : β → Type*} {f : (Σ b : β, γ b) → α} {g : β → α} {a : α} + (ha : HasProd f a) (hf : ∀ b, HasProd (fun c ↦ f ⟨b, c⟩) (g b)) : HasProd g a := by classical refine' (atTop_basis.tendsto_iff (closed_nhds_basis a)).mpr _ rintro s ⟨hs, hsc⟩ @@ -83,27 +90,30 @@ theorem HasSum.sigma {γ : β → Type*} {f : (Σ b : β, γ b) → α} {g : β use u.image Sigma.fst, trivial intro bs hbs simp only [Set.mem_preimage, ge_iff_le, Finset.le_iff_subset] at hu - have : Tendsto (fun t : Finset (Σb, γ b) ↦ ∑ p in t.filter fun p ↦ p.1 ∈ bs, f p) atTop - (𝓝 <| ∑ b in bs, g b) := by - simp only [← sigma_preimage_mk, sum_sigma] - refine' tendsto_finset_sum _ fun b _ ↦ _ + have : Tendsto (fun t : Finset (Σb, γ b) ↦ ∏ p in t.filter fun p ↦ p.1 ∈ bs, f p) atTop + (𝓝 <| ∏ b in bs, g b) := by + simp only [← sigma_preimage_mk, prod_sigma] + refine' tendsto_finset_prod _ fun b _ ↦ _ change - Tendsto (fun t ↦ (fun t ↦ ∑ s in t, f ⟨b, s⟩) (preimage t (Sigma.mk b) _)) atTop (𝓝 (g b)) + Tendsto (fun t ↦ (fun t ↦ ∏ s in t, f ⟨b, s⟩) (preimage t (Sigma.mk b) _)) atTop (𝓝 (g b)) exact (hf b).comp (tendsto_finset_preimage_atTop_atTop (sigma_mk_injective)) refine' hsc.mem_of_tendsto this (eventually_atTop.2 ⟨u, fun t ht ↦ hu _ fun x hx ↦ _⟩) exact mem_filter.2 ⟨ht hx, hbs <| mem_image_of_mem _ hx⟩ #align has_sum.sigma HasSum.sigma -/-- If a series `f` on `β × γ` has sum `a` and for each `b` the restriction of `f` to `{b} × γ` -has sum `g b`, then the series `g` has sum `a`. -/ -theorem HasSum.prod_fiberwise {f : β × γ → α} {g : β → α} {a : α} (ha : HasSum f a) - (hf : ∀ b, HasSum (fun c ↦ f (b, c)) (g b)) : HasSum g a := - HasSum.sigma ((Equiv.sigmaEquivProd β γ).hasSum_iff.2 ha) hf +/-- If a function `f` on `β × γ` has product `a` and for each `b` the restriction of `f` to +`{b} × γ` has product `g b`, then the function `g` has product `a`. -/ +@[to_additive HasSum.prod_fiberwise "If a series `f` on `β × γ` has sum `a` and for each `b` the +restriction of `f` to `{b} × γ` has sum `g b`, then the series `g` has sum `a`."] +theorem HasProd.prod_fiberwise {f : β × γ → α} {g : β → α} {a : α} (ha : HasProd f a) + (hf : ∀ b, HasProd (fun c ↦ f (b, c)) (g b)) : HasProd g a := + HasProd.sigma ((Equiv.sigmaEquivProd β γ).hasProd_iff.2 ha) hf #align has_sum.prod_fiberwise HasSum.prod_fiberwise -theorem Summable.sigma' {γ : β → Type*} {f : (Σb : β, γ b) → α} (ha : Summable f) - (hf : ∀ b, Summable fun c ↦ f ⟨b, c⟩) : Summable fun b ↦ ∑' c, f ⟨b, c⟩ := - (ha.hasSum.sigma fun b ↦ (hf b).hasSum).summable +@[to_additive] +theorem Multipliable.sigma' {γ : β → Type*} {f : (Σb : β, γ b) → α} (ha : Multipliable f) + (hf : ∀ b, Multipliable fun c ↦ f ⟨b, c⟩) : Multipliable fun b ↦ ∏' c, f ⟨b, c⟩ := + (ha.hasProd.sigma fun b ↦ (hf b).hasProd).multipliable #align summable.sigma' Summable.sigma' end RegularSpace @@ -112,72 +122,88 @@ section T3Space variable [T3Space α] -theorem HasSum.sigma_of_hasSum {γ : β → Type*} {f : (Σb : β, γ b) → α} {g : β → α} - {a : α} (ha : HasSum g a) (hf : ∀ b, HasSum (fun c ↦ f ⟨b, c⟩) (g b)) (hf' : Summable f) : - HasSum f a := by simpa [(hf'.hasSum.sigma hf).unique ha] using hf'.hasSum +@[to_additive] +theorem HasProd.sigma_of_hasProd {γ : β → Type*} {f : (Σb : β, γ b) → α} {g : β → α} + {a : α} (ha : HasProd g a) (hf : ∀ b, HasProd (fun c ↦ f ⟨b, c⟩) (g b)) (hf' : Multipliable f) : + HasProd f a := by simpa [(hf'.hasProd.sigma hf).unique ha] using hf'.hasProd #align has_sum.sigma_of_has_sum HasSum.sigma_of_hasSum -theorem tsum_sigma' {γ : β → Type*} {f : (Σb : β, γ b) → α} (h₁ : ∀ b, Summable fun c ↦ f ⟨b, c⟩) - (h₂ : Summable f) : ∑' p, f p = ∑' (b) (c), f ⟨b, c⟩ := - (h₂.hasSum.sigma fun b ↦ (h₁ b).hasSum).tsum_eq.symm +@[to_additive] +theorem tprod_sigma' {γ : β → Type*} {f : (Σb : β, γ b) → α} + (h₁ : ∀ b, Multipliable fun c ↦ f ⟨b, c⟩) (h₂ : Multipliable f) : + ∏' p, f p = ∏' (b) (c), f ⟨b, c⟩ := + (h₂.hasProd.sigma fun b ↦ (h₁ b).hasProd).tprod_eq.symm #align tsum_sigma' tsum_sigma' -theorem tsum_prod' {f : β × γ → α} (h : Summable f) (h₁ : ∀ b, Summable fun c ↦ f (b, c)) : - ∑' p, f p = ∑' (b) (c), f (b, c) := - (h.hasSum.prod_fiberwise fun b ↦ (h₁ b).hasSum).tsum_eq.symm +@[to_additive tsum_prod'] +theorem tprod_prod' {f : β × γ → α} (h : Multipliable f) + (h₁ : ∀ b, Multipliable fun c ↦ f (b, c)) : + ∏' p, f p = ∏' (b) (c), f (b, c) := + (h.hasProd.prod_fiberwise fun b ↦ (h₁ b).hasProd).tprod_eq.symm #align tsum_prod' tsum_prod' -theorem tsum_comm' {f : β → γ → α} (h : Summable (Function.uncurry f)) (h₁ : ∀ b, Summable (f b)) - (h₂ : ∀ c, Summable fun b ↦ f b c) : ∑' (c) (b), f b c = ∑' (b) (c), f b c := by - erw [← tsum_prod' h h₁, ← tsum_prod' h.prod_symm h₂, ← (Equiv.prodComm γ β).tsum_eq (uncurry f)] +@[to_additive] +theorem tprod_comm' {f : β → γ → α} (h : Multipliable (Function.uncurry f)) + (h₁ : ∀ b, Multipliable (f b)) (h₂ : ∀ c, Multipliable fun b ↦ f b c) : + ∏' (c) (b), f b c = ∏' (b) (c), f b c := by + erw [← tprod_prod' h h₁, ← tprod_prod' h.prod_symm h₂, + ← (Equiv.prodComm γ β).tprod_eq (uncurry f)] rfl #align tsum_comm' tsum_comm' end T3Space -end ContinuousAdd +end ContinuousMul section CompleteSpace -variable [AddCommGroup α] [UniformSpace α] [UniformAddGroup α] [CompleteSpace α] +variable [CommGroup α] [UniformSpace α] [UniformGroup α] [CompleteSpace α] -theorem Summable.sigma_factor {γ : β → Type*} {f : (Σb : β, γ b) → α} (ha : Summable f) (b : β) : - Summable fun c ↦ f ⟨b, c⟩ := +@[to_additive] +theorem Multipliable.sigma_factor {γ : β → Type*} {f : (Σb : β, γ b) → α} + (ha : Multipliable f) (b : β) : + Multipliable fun c ↦ f ⟨b, c⟩ := ha.comp_injective sigma_mk_injective #align summable.sigma_factor Summable.sigma_factor -theorem Summable.sigma {γ : β → Type*} {f : (Σb : β, γ b) → α} (ha : Summable f) : - Summable fun b ↦ ∑' c, f ⟨b, c⟩ := +@[to_additive] +theorem Multipliable.sigma {γ : β → Type*} {f : (Σb : β, γ b) → α} (ha : Multipliable f) : + Multipliable fun b ↦ ∏' c, f ⟨b, c⟩ := ha.sigma' fun b ↦ ha.sigma_factor b #align summable.sigma Summable.sigma -theorem Summable.prod_factor {f : β × γ → α} (h : Summable f) (b : β) : - Summable fun c ↦ f (b, c) := +@[to_additive Summable.prod_factor] +theorem Multipliable.prod_factor {f : β × γ → α} (h : Multipliable f) (b : β) : + Multipliable fun c ↦ f (b, c) := h.comp_injective fun _ _ h ↦ (Prod.ext_iff.1 h).2 #align summable.prod_factor Summable.prod_factor -lemma HasSum.tsum_fiberwise [T2Space α] {f : β → α} {a : α} (hf : HasSum f a) (g : β → γ) : - HasSum (fun c : γ ↦ ∑' b : g ⁻¹' {c}, f b) a := - (((Equiv.sigmaFiberEquiv g).hasSum_iff).mpr hf).sigma <| - fun _ ↦ ((hf.summable.subtype _).hasSum_iff).mpr rfl +@[to_additive] +lemma HasProd.tprod_fiberwise [T2Space α] {f : β → α} {a : α} (hf : HasProd f a) (g : β → γ) : + HasProd (fun c : γ ↦ ∏' b : g ⁻¹' {c}, f b) a := + (((Equiv.sigmaFiberEquiv g).hasProd_iff).mpr hf).sigma <| + fun _ ↦ ((hf.multipliable.subtype _).hasProd_iff).mpr rfl section CompleteT0Space variable [T0Space α] -theorem tsum_sigma {γ : β → Type*} {f : (Σb : β, γ b) → α} (ha : Summable f) : - ∑' p, f p = ∑' (b) (c), f ⟨b, c⟩ := - tsum_sigma' (fun b ↦ ha.sigma_factor b) ha +@[to_additive] +theorem tprod_sigma {γ : β → Type*} {f : (Σb : β, γ b) → α} (ha : Multipliable f) : + ∏' p, f p = ∏' (b) (c), f ⟨b, c⟩ := + tprod_sigma' (fun b ↦ ha.sigma_factor b) ha #align tsum_sigma tsum_sigma -theorem tsum_prod {f : β × γ → α} (h : Summable f) : - ∑' p, f p = ∑' (b) (c), f ⟨b, c⟩ := - tsum_prod' h h.prod_factor +@[to_additive tsum_prod] +theorem tprod_prod {f : β × γ → α} (h : Multipliable f) : + ∏' p, f p = ∏' (b) (c), f ⟨b, c⟩ := + tprod_prod' h h.prod_factor #align tsum_prod tsum_prod -theorem tsum_comm {f : β → γ → α} (h : Summable (Function.uncurry f)) : - ∑' (c) (b), f b c = ∑' (b) (c), f b c := - tsum_comm' h h.prod_factor h.prod_symm.prod_factor +@[to_additive] +theorem tprod_comm {f : β → γ → α} (h : Multipliable (Function.uncurry f)) : + ∏' (c) (b), f b c = ∏' (b) (c), f b c := + tprod_comm' h h.prod_factor h.prod_symm.prod_factor #align tsum_comm tsum_comm end CompleteT0Space @@ -186,20 +212,23 @@ end CompleteSpace section Pi -variable {ι : Type*} {π : α → Type*} [∀ x, AddCommMonoid (π x)] [∀ x, TopologicalSpace (π x)] +variable {ι : Type*} {π : α → Type*} [∀ x, CommMonoid (π x)] [∀ x, TopologicalSpace (π x)] -theorem Pi.hasSum {f : ι → ∀ x, π x} {g : ∀ x, π x} : - HasSum f g ↔ ∀ x, HasSum (fun i ↦ f i x) (g x) := by - simp only [HasSum, tendsto_pi_nhds, sum_apply] +@[to_additive] +theorem Pi.hasProd {f : ι → ∀ x, π x} {g : ∀ x, π x} : + HasProd f g ↔ ∀ x, HasProd (fun i ↦ f i x) (g x) := by + simp only [HasProd, tendsto_pi_nhds, prod_apply] #align pi.has_sum Pi.hasSum -theorem Pi.summable {f : ι → ∀ x, π x} : Summable f ↔ ∀ x, Summable fun i ↦ f i x := by - simp only [Summable, Pi.hasSum, Classical.skolem] +@[to_additive] +theorem Pi.multipliable {f : ι → ∀ x, π x} : Multipliable f ↔ ∀ x, Multipliable fun i ↦ f i x := by + simp only [Multipliable, Pi.hasProd, Classical.skolem] #align pi.summable Pi.summable -theorem tsum_apply [∀ x, T2Space (π x)] {f : ι → ∀ x, π x} {x : α} (hf : Summable f) : - (∑' i, f i) x = ∑' i, f i x := - (Pi.hasSum.mp hf.hasSum x).tsum_eq.symm +@[to_additive] +theorem tprod_apply [∀ x, T2Space (π x)] {f : ι → ∀ x, π x} {x : α} (hf : Multipliable f) : + (∏' i, f i) x = ∏' i, f i x := + (Pi.hasProd.mp hf.hasProd x).tprod_eq.symm #align tsum_apply tsum_apply end Pi diff --git a/Mathlib/Topology/Algebra/InfiniteSum/Defs.lean b/Mathlib/Topology/Algebra/InfiniteSum/Defs.lean index 28fa0779bdceed..496b7ba25e44bc 100644 --- a/Mathlib/Topology/Algebra/InfiniteSum/Defs.lean +++ b/Mathlib/Topology/Algebra/InfiniteSum/Defs.lean @@ -9,15 +9,32 @@ import Mathlib.Algebra.BigOperators.Finprod #align_import topology.algebra.infinite_sum.basic from "leanprover-community/mathlib"@"3b52265189f3fb43aa631edffce5d060fafaf82f" /-! -# Infinite sum over a topological monoid +# Infinite sum and product over a topological monoid -This sum is known as unconditionally convergent, as it sums to the same value under all possible -permutations. For Euclidean spaces (finite dimensional Banach spaces) this is equivalent to absolute +This file defines unconditionally convergent sums over a commutative topological additive monoid. +For Euclidean spaces (finite dimensional Banach spaces) this is equivalent to absolute convergence. +We also define unconditionally convergent products over a commutative topological multiplicative +monoid. + Note: There are summable sequences which are not unconditionally convergent! The other way holds generally, see `HasSum.tendsto_sum_nat`. +## Implementation notes + +We say that a function `f : β → α` has an unconditional product of `a` if the function +`fun s : Finset β ↦ ∏ b in s, f b` converges to `a` on the `atTop` filter on `Finset β`. In other +words, for every neighborhood `U` of `a`, there exists a finite set `s : Finset β` of indices such +that `∏ b in s', f b ∈ U` for any finite set `s'` which is a superset of `s`. + +This may yield some unexpected results. For example, according to this definition, the product +`∏' n : ℕ, (1 : ℝ) / 2` unconditionally exists and is equal to `0`. More strikingly, +the product `∏' n : ℕ, (n : ℝ)` unconditionally exists and is equal to `0`, because one +of its terms is `0` (even though the product of the remaining terms diverges). Users who would +prefer that these products be considered not to exist can carry them out in the unit group `ℝˣ` +rather than in `ℝ`. + ## References * Bourbaki: General Topology (1995), Chapter 3 §5 (Infinite sums in commutative groups) @@ -25,8 +42,8 @@ generally, see `HasSum.tendsto_sum_nat`. -/ /- **NOTE**. This file is intended to be kept short, just enough to state the basic definitions and -three key lemmas relating them together, namely `Summable.hasSum`, `HasSum.tsum_eq`, and -`Summable.hasSum_iff`. +six key lemmas relating them together, namely `Summable.hasSum`, `Multipliable.hasProd`, +`HasSum.tsum_eq`, `HasProd.tprod_eq`, `Summable.hasSum_iff`, and `Multipliable.hasProd_iff`. Do not add further lemmas here -- add them to `InfiniteSum.Basic` or (preferably) another, more specific file. -/ @@ -39,11 +56,22 @@ open scoped BigOperators Topology variable {α β γ : Type*} -section HasSum +section HasProd + +variable [CommMonoid α] [TopologicalSpace α] -variable [AddCommMonoid α] [TopologicalSpace α] +/-- Infinite product on a topological monoid -/-- Infinite sum on a topological monoid +The `atTop` filter on `Finset β` is the limit of all finite sets towards the entire type. So we take +the product over bigger and bigger sets. This product operation is invariant under reordering. + +For the definition and many statements, `α` does not need to be a topological monoid. We only add +this assumption later, for the lemmas where it is relevant. + +These are defined in an identical way to infinite sums (`HasSum`). For example, we say that +the function `ℕ → ℝ` sending `n` to `1 / 2` has a product of `0`, rather than saying that it does +not converge as some authors would. -/ +@[to_additive "Infinite sum on a topological monoid The `atTop` filter on `Finset β` is the limit of all finite sets towards the entire type. So we sum up bigger and bigger sets. This sum operation is invariant under reordering. In particular, @@ -53,91 +81,110 @@ sum for this definition, but a series which is absolutely convergent will have t This is based on Mario Carneiro's [infinite sum `df-tsms` in Metamath](http://us.metamath.org/mpeuni/df-tsms.html). -For the definition or many statements, `α` does not need to be a topological monoid. We only add -this assumption later, for the lemmas where it is relevant. --/ -def HasSum (f : β → α) (a : α) : Prop := - Tendsto (fun s : Finset β ↦ ∑ b in s, f b) atTop (𝓝 a) +For the definition and many statements, `α` does not need to be a topological monoid. We only add +this assumption later, for the lemmas where it is relevant."] +def HasProd (f : β → α) (a : α) : Prop := + Tendsto (fun s : Finset β ↦ ∏ b in s, f b) atTop (𝓝 a) #align has_sum HasSum -/-- `Summable f` means that `f` has some (infinite) sum. Use `tsum` to get the value. -/ -def Summable (f : β → α) : Prop := - ∃ a, HasSum f a +/-- `Multipliable f` means that `f` has some (infinite) product. Use `tprod` to get the value. -/ +@[to_additive "`Summable f` means that `f` has some (infinite) sum. Use `tsum` to get the value."] +def Multipliable (f : β → α) : Prop := + ∃ a, HasProd f a #align summable Summable open scoped Classical in -/-- `∑' i, f i` is the sum of `f` it exists, or 0 otherwise. -/ -irreducible_def tsum {β} (f : β → α) := - if h : Summable f then - /- Note that the sum might not be uniquely defined if the topology is not separated. - When the support of `f` is finite, we make the most reasonable choice to use the finite sum over - the support. Otherwise, we choose arbitrarily an `a` satisfying `HasSum f a`. -/ - if (support f).Finite then finsum f +/-- `∏' i, f i` is the product of `f` it exists, or 1 otherwise. -/ +@[to_additive "`∑' i, f i` is the sum of `f` it exists, or 0 otherwise."] +noncomputable irreducible_def tprod {β} (f : β → α) := + if h : Multipliable f then + /- Note that the product might not be uniquely defined if the topology is not separated. + When the multiplicative support of `f` is finite, we make the most reasonable choice to use the + product over the multiplicative support. Otherwise, we choose arbitrarily an `a` satisfying + `HasProd f a`. -/ + if (mulSupport f).Finite then finprod f else h.choose - else 0 + else 1 #align tsum tsum -- see Note [operator precedence of big operators] +@[inherit_doc tprod] +notation3 "∏' "(...)", "r:67:(scoped f => tprod f) => r @[inherit_doc tsum] notation3 "∑' "(...)", "r:67:(scoped f => tsum f) => r variable {f g : β → α} {a b : α} {s : Finset β} -theorem HasSum.summable (h : HasSum f a) : Summable f := +@[to_additive] +theorem HasProd.multipliable (h : HasProd f a) : Multipliable f := ⟨a, h⟩ #align has_sum.summable HasSum.summable -theorem tsum_eq_zero_of_not_summable (h : ¬Summable f) : ∑' b, f b = 0 := by simp [tsum_def, h] +@[to_additive] +theorem tprod_eq_one_of_not_multipliable (h : ¬Multipliable f) : ∏' b, f b = 1 := by + simp [tprod_def, h] #align tsum_eq_zero_of_not_summable tsum_eq_zero_of_not_summable -theorem Function.Injective.hasSum_iff {g : γ → β} (hg : Injective g) - (hf : ∀ x, x ∉ Set.range g → f x = 0) : HasSum (f ∘ g) a ↔ HasSum f a := by - simp only [HasSum, Tendsto, comp_apply, hg.map_atTop_finset_sum_eq hf] +@[to_additive] +theorem Function.Injective.hasProd_iff {g : γ → β} (hg : Injective g) + (hf : ∀ x, x ∉ Set.range g → f x = 1) : HasProd (f ∘ g) a ↔ HasProd f a := by + simp only [HasProd, Tendsto, comp_apply, hg.map_atTop_finset_prod_eq hf] #align function.injective.has_sum_iff Function.Injective.hasSum_iff -theorem hasSum_subtype_iff_of_support_subset {s : Set β} (hf : support f ⊆ s) : - HasSum (f ∘ (↑) : s → α) a ↔ HasSum f a := - Subtype.coe_injective.hasSum_iff <| by simpa using support_subset_iff'.1 hf +@[to_additive] +theorem hasProd_subtype_iff_of_mulSupport_subset {s : Set β} (hf : mulSupport f ⊆ s) : + HasProd (f ∘ (↑) : s → α) a ↔ HasProd f a := + Subtype.coe_injective.hasProd_iff <| by simpa using mulSupport_subset_iff'.1 hf #align has_sum_subtype_iff_of_support_subset hasSum_subtype_iff_of_support_subset -theorem hasSum_fintype [Fintype β] (f : β → α) : HasSum f (∑ b, f b) := +@[to_additive] +theorem hasProd_fintype [Fintype β] (f : β → α) : HasProd f (∏ b, f b) := OrderTop.tendsto_atTop_nhds _ #align has_sum_fintype hasSum_fintype -protected theorem Finset.hasSum (s : Finset β) (f : β → α) : - HasSum (f ∘ (↑) : (↑s : Set β) → α) (∑ b in s, f b) := by - rw [← sum_attach] - exact hasSum_fintype _ +@[to_additive] +protected theorem Finset.hasProd (s : Finset β) (f : β → α) : + HasProd (f ∘ (↑) : (↑s : Set β) → α) (∏ b in s, f b) := by + rw [← prod_attach] + exact hasProd_fintype _ #align finset.has_sum Finset.hasSum -/-- If a function `f` vanishes outside of a finite set `s`, then it `HasSum` `∑ b in s, f b`. -/ -theorem hasSum_sum_of_ne_finset_zero (hf : ∀ (b) (_ : b ∉ s), f b = 0) : HasSum f (∑ b in s, f b) := - (hasSum_subtype_iff_of_support_subset <| support_subset_iff'.2 hf).1 <| s.hasSum f +/-- If a function `f` is `1` outside of a finite set `s`, then it `HasProd` `∏ b in s, f b`. -/ +@[to_additive "If a function `f` vanishes outside of a finite set `s`, then it `HasSum` +`∑ b in s, f b`."] +theorem hasProd_prod_of_ne_finset_one (hf : ∀ (b) (_ : b ∉ s), f b = 1) : + HasProd f (∏ b in s, f b) := + (hasProd_subtype_iff_of_mulSupport_subset <| mulSupport_subset_iff'.2 hf).1 <| s.hasProd f #align has_sum_sum_of_ne_finset_zero hasSum_sum_of_ne_finset_zero -theorem summable_of_ne_finset_zero (hf : ∀ (b) (_ : b ∉ s), f b = 0) : Summable f := - (hasSum_sum_of_ne_finset_zero hf).summable +@[to_additive] +theorem multipliable_of_ne_finset_one (hf : ∀ (b) (_ : b ∉ s), f b = 1) : Multipliable f := + (hasProd_prod_of_ne_finset_one hf).multipliable #align summable_of_ne_finset_zero summable_of_ne_finset_zero -theorem Summable.hasSum (ha : Summable f) : HasSum f (∑' b, f b) := by - simp only [tsum_def, ha, dite_true] - by_cases H : (support f).Finite - · simp [H, hasSum_sum_of_ne_finset_zero, finsum_eq_sum] +@[to_additive] +theorem Multipliable.hasProd (ha : Multipliable f) : HasProd f (∏' b, f b) := by + simp only [tprod_def, ha, dite_true] + by_cases H : (mulSupport f).Finite + · simp [H, hasProd_prod_of_ne_finset_one, finprod_eq_prod] · simpa [H] using ha.choose_spec #align summable.has_sum Summable.hasSum -theorem HasSum.unique {a₁ a₂ : α} [T2Space α] : HasSum f a₁ → HasSum f a₂ → a₁ = a₂ := by +@[to_additive] +theorem HasProd.unique {a₁ a₂ : α} [T2Space α] : HasProd f a₁ → HasProd f a₂ → a₁ = a₂ := by classical exact tendsto_nhds_unique #align has_sum.unique HasSum.unique variable [T2Space α] -theorem HasSum.tsum_eq (ha : HasSum f a) : ∑' b, f b = a := - (Summable.hasSum ⟨a, ha⟩).unique ha +@[to_additive] +theorem HasProd.tprod_eq (ha : HasProd f a) : ∏' b, f b = a := + (Multipliable.hasProd ⟨a, ha⟩).unique ha #align has_sum.tsum_eq HasSum.tsum_eq -theorem Summable.hasSum_iff (h : Summable f) : HasSum f a ↔ ∑' b, f b = a := - Iff.intro HasSum.tsum_eq fun eq ↦ eq ▸ h.hasSum +@[to_additive] +theorem Multipliable.hasProd_iff (h : Multipliable f) : HasProd f a ↔ ∏' b, f b = a := + Iff.intro HasProd.tprod_eq fun eq ↦ eq ▸ h.hasProd #align summable.has_sum_iff Summable.hasSum_iff -end HasSum +end HasProd diff --git a/Mathlib/Topology/Algebra/InfiniteSum/Group.lean b/Mathlib/Topology/Algebra/InfiniteSum/Group.lean index 6ccabeb30d9dd2..c22457d9256a16 100644 --- a/Mathlib/Topology/Algebra/InfiniteSum/Group.lean +++ b/Mathlib/Topology/Algebra/InfiniteSum/Group.lean @@ -7,7 +7,7 @@ import Mathlib.Topology.Algebra.InfiniteSum.Basic import Mathlib.Topology.Algebra.UniformGroup /-! -# Infinite sums in topological groups +# Infinite sums and products in topological groups Lemmas on topological sums in groups (as opposed to monoids). -/ @@ -22,157 +22,187 @@ variable {α β γ δ : Type*} section TopologicalGroup -variable [AddCommGroup α] [TopologicalSpace α] [TopologicalAddGroup α] +variable [CommGroup α] [TopologicalSpace α] [TopologicalGroup α] variable {f g : β → α} {a a₁ a₂ : α} -- `by simpa using` speeds up elaboration. Why? -theorem HasSum.neg (h : HasSum f a) : HasSum (fun b ↦ -f b) (-a) := by - simpa only using h.map (-AddMonoidHom.id α) continuous_neg +@[to_additive] +theorem HasProd.inv (h : HasProd f a) : HasProd (fun b ↦ (f b)⁻¹) a⁻¹ := by + simpa only using h.map (MonoidHom.id α)⁻¹ continuous_inv #align has_sum.neg HasSum.neg -theorem Summable.neg (hf : Summable f) : Summable fun b ↦ -f b := - hf.hasSum.neg.summable +@[to_additive] +theorem Multipliable.inv (hf : Multipliable f) : Multipliable fun b ↦ (f b)⁻¹ := + hf.hasProd.inv.multipliable #align summable.neg Summable.neg -theorem Summable.of_neg (hf : Summable fun b ↦ -f b) : Summable f := by - simpa only [neg_neg] using hf.neg +@[to_additive] +theorem Multipliable.of_inv (hf : Multipliable fun b ↦ (f b)⁻¹) : Multipliable f := by + simpa only [inv_inv] using hf.inv #align summable.of_neg Summable.of_neg -theorem summable_neg_iff : (Summable fun b ↦ -f b) ↔ Summable f := - ⟨Summable.of_neg, Summable.neg⟩ +@[to_additive] +theorem multipliable_inv_iff : (Multipliable fun b ↦ (f b)⁻¹) ↔ Multipliable f := + ⟨Multipliable.of_inv, Multipliable.inv⟩ #align summable_neg_iff summable_neg_iff -theorem HasSum.sub (hf : HasSum f a₁) (hg : HasSum g a₂) : - HasSum (fun b ↦ f b - g b) (a₁ - a₂) := by - simp only [sub_eq_add_neg] - exact hf.add hg.neg +@[to_additive] +theorem HasProd.div (hf : HasProd f a₁) (hg : HasProd g a₂) : + HasProd (fun b ↦ f b / g b) (a₁ / a₂) := by + simp only [div_eq_mul_inv] + exact hf.mul hg.inv #align has_sum.sub HasSum.sub -theorem Summable.sub (hf : Summable f) (hg : Summable g) : Summable fun b ↦ f b - g b := - (hf.hasSum.sub hg.hasSum).summable +@[to_additive] +theorem Multipliable.div (hf : Multipliable f) (hg : Multipliable g) : + Multipliable fun b ↦ f b / g b := + (hf.hasProd.div hg.hasProd).multipliable #align summable.sub Summable.sub -theorem Summable.trans_sub (hg : Summable g) (hfg : Summable fun b ↦ f b - g b) : Summable f := by - simpa only [sub_add_cancel] using hfg.add hg +@[to_additive] +theorem Multipliable.trans_div (hg : Multipliable g) (hfg : Multipliable fun b ↦ f b / g b) : + Multipliable f := by + simpa only [div_mul_cancel] using hfg.mul hg #align summable.trans_sub Summable.trans_sub -theorem summable_iff_of_summable_sub (hfg : Summable fun b ↦ f b - g b) : - Summable f ↔ Summable g := - ⟨fun hf ↦ hf.trans_sub <| by simpa only [neg_sub] using hfg.neg, fun hg ↦ hg.trans_sub hfg⟩ +@[to_additive] +theorem multipliable_iff_of_multipliable_div (hfg : Multipliable fun b ↦ f b / g b) : + Multipliable f ↔ Multipliable g := + ⟨fun hf ↦ hf.trans_div <| by simpa only [inv_div] using hfg.inv, fun hg ↦ hg.trans_div hfg⟩ #align summable_iff_of_summable_sub summable_iff_of_summable_sub -theorem HasSum.update (hf : HasSum f a₁) (b : β) [DecidableEq β] (a : α) : - HasSum (update f b a) (a - f b + a₁) := by - convert (hasSum_ite_eq b (a - f b)).add hf with b' +@[to_additive] +theorem HasProd.update (hf : HasProd f a₁) (b : β) [DecidableEq β] (a : α) : + HasProd (update f b a) (a / f b * a₁) := by + convert (hasProd_ite_eq b (a / f b)).mul hf with b' by_cases h : b' = b · rw [h, update_same] simp [eq_self_iff_true, if_true, sub_add_cancel] - · simp only [h, update_noteq, if_false, Ne.def, zero_add, not_false_iff] + · simp only [h, update_noteq, if_false, Ne.def, one_mul, not_false_iff] #align has_sum.update HasSum.update -theorem Summable.update (hf : Summable f) (b : β) [DecidableEq β] (a : α) : - Summable (update f b a) := - (hf.hasSum.update b a).summable +@[to_additive] +theorem Multipliable.update (hf : Multipliable f) (b : β) [DecidableEq β] (a : α) : + Multipliable (update f b a) := + (hf.hasProd.update b a).multipliable #align summable.update Summable.update -theorem HasSum.hasSum_compl_iff {s : Set β} (hf : HasSum (f ∘ (↑) : s → α) a₁) : - HasSum (f ∘ (↑) : ↑sᶜ → α) a₂ ↔ HasSum f (a₁ + a₂) := by - refine' ⟨fun h ↦ hf.add_compl h, fun h ↦ _⟩ - rw [hasSum_subtype_iff_indicator] at hf ⊢ - rw [Set.indicator_compl] - simpa only [add_sub_cancel_left] using h.sub hf +@[to_additive] +theorem HasProd.hasProd_compl_iff {s : Set β} (hf : HasProd (f ∘ (↑) : s → α) a₁) : + HasProd (f ∘ (↑) : ↑sᶜ → α) a₂ ↔ HasProd f (a₁ * a₂) := by + refine' ⟨fun h ↦ hf.mul_compl h, fun h ↦ _⟩ + rw [hasProd_subtype_iff_mulIndicator] at hf ⊢ + rw [Set.mulIndicator_compl] + simpa only [div_eq_mul_inv, mul_inv_cancel_comm] using h.div hf #align has_sum.has_sum_compl_iff HasSum.hasSum_compl_iff -theorem HasSum.hasSum_iff_compl {s : Set β} (hf : HasSum (f ∘ (↑) : s → α) a₁) : - HasSum f a₂ ↔ HasSum (f ∘ (↑) : ↑sᶜ → α) (a₂ - a₁) := - Iff.symm <| hf.hasSum_compl_iff.trans <| by rw [add_sub_cancel] +@[to_additive] +theorem HasProd.hasProd_iff_compl {s : Set β} (hf : HasProd (f ∘ (↑) : s → α) a₁) : + HasProd f a₂ ↔ HasProd (f ∘ (↑) : ↑sᶜ → α) (a₂ / a₁) := + Iff.symm <| hf.hasProd_compl_iff.trans <| by rw [mul_div_cancel] #align has_sum.has_sum_iff_compl HasSum.hasSum_iff_compl -theorem Summable.summable_compl_iff {s : Set β} (hf : Summable (f ∘ (↑) : s → α)) : - Summable (f ∘ (↑) : ↑sᶜ → α) ↔ Summable f := - ⟨fun ⟨_, ha⟩ ↦ (hf.hasSum.hasSum_compl_iff.1 ha).summable, fun ⟨_, ha⟩ ↦ - (hf.hasSum.hasSum_iff_compl.1 ha).summable⟩ +@[to_additive] +theorem Multipliable.multipliable_compl_iff {s : Set β} (hf : Multipliable (f ∘ (↑) : s → α)) : + Multipliable (f ∘ (↑) : ↑sᶜ → α) ↔ Multipliable f := + ⟨fun ⟨_, ha⟩ ↦ (hf.hasProd.hasProd_compl_iff.1 ha).multipliable, fun ⟨_, ha⟩ ↦ + (hf.hasProd.hasProd_iff_compl.1 ha).multipliable⟩ #align summable.summable_compl_iff Summable.summable_compl_iff -protected theorem Finset.hasSum_compl_iff (s : Finset β) : - HasSum (fun x : { x // x ∉ s } ↦ f x) a ↔ HasSum f (a + ∑ i in s, f i) := - (s.hasSum f).hasSum_compl_iff.trans <| by rw [add_comm] +@[to_additive] +protected theorem Finset.hasProd_compl_iff (s : Finset β) : + HasProd (fun x : { x // x ∉ s } ↦ f x) a ↔ HasProd f (a * ∏ i in s, f i) := + (s.hasProd f).hasProd_compl_iff.trans <| by rw [mul_comm] #align finset.has_sum_compl_iff Finset.hasSum_compl_iff -protected theorem Finset.hasSum_iff_compl (s : Finset β) : - HasSum f a ↔ HasSum (fun x : { x // x ∉ s } ↦ f x) (a - ∑ i in s, f i) := - (s.hasSum f).hasSum_iff_compl +@[to_additive] +protected theorem Finset.hasProd_iff_compl (s : Finset β) : + HasProd f a ↔ HasProd (fun x : { x // x ∉ s } ↦ f x) (a / ∏ i in s, f i) := + (s.hasProd f).hasProd_iff_compl #align finset.has_sum_iff_compl Finset.hasSum_iff_compl -protected theorem Finset.summable_compl_iff (s : Finset β) : - (Summable fun x : { x // x ∉ s } ↦ f x) ↔ Summable f := - (s.summable f).summable_compl_iff +@[to_additive] +protected theorem Finset.multipliable_compl_iff (s : Finset β) : + (Multipliable fun x : { x // x ∉ s } ↦ f x) ↔ Multipliable f := + (s.multipliable f).multipliable_compl_iff #align finset.summable_compl_iff Finset.summable_compl_iff -theorem Set.Finite.summable_compl_iff {s : Set β} (hs : s.Finite) : - Summable (f ∘ (↑) : ↑sᶜ → α) ↔ Summable f := - (hs.summable f).summable_compl_iff +@[to_additive] +theorem Set.Finite.multipliable_compl_iff {s : Set β} (hs : s.Finite) : + Multipliable (f ∘ (↑) : ↑sᶜ → α) ↔ Multipliable f := + (hs.multipliable f).multipliable_compl_iff #align set.finite.summable_compl_iff Set.Finite.summable_compl_iff -theorem hasSum_ite_sub_hasSum [DecidableEq β] (hf : HasSum f a) (b : β) : - HasSum (fun n ↦ ite (n = b) 0 (f n)) (a - f b) := by - convert hf.update b 0 using 1 +@[to_additive] +theorem hasProd_ite_div_hasProd [DecidableEq β] (hf : HasProd f a) (b : β) : + HasProd (fun n ↦ ite (n = b) 1 (f n)) (a / f b) := by + convert hf.update b 1 using 1 · ext n rw [Function.update_apply] - · rw [sub_add_eq_add_sub, zero_add] + · rw [div_mul_eq_mul_div, one_mul] #align has_sum_ite_sub_has_sum hasSum_ite_sub_hasSum -section tsum +section tprod variable [T2Space α] -theorem tsum_neg : ∑' b, -f b = -∑' b, f b := by - by_cases hf : Summable f - · exact hf.hasSum.neg.tsum_eq - · simp [tsum_eq_zero_of_not_summable hf, tsum_eq_zero_of_not_summable (mt Summable.of_neg hf)] +@[to_additive] +theorem tprod_inv : ∏' b, (f b)⁻¹ = (∏' b, f b)⁻¹ := by + by_cases hf : Multipliable f + · exact hf.hasProd.inv.tprod_eq + · simp [tprod_eq_one_of_not_multipliable hf, + tprod_eq_one_of_not_multipliable (mt Multipliable.of_inv hf)] #align tsum_neg tsum_neg -theorem tsum_sub (hf : Summable f) (hg : Summable g) : - ∑' b, (f b - g b) = ∑' b, f b - ∑' b, g b := - (hf.hasSum.sub hg.hasSum).tsum_eq +@[to_additive] +theorem tprod_div (hf : Multipliable f) (hg : Multipliable g) : + ∏' b, (f b / g b) = (∏' b, f b) / ∏' b, g b := + (hf.hasProd.div hg.hasProd).tprod_eq #align tsum_sub tsum_sub -theorem sum_add_tsum_compl {s : Finset β} (hf : Summable f) : - ((∑ x in s, f x) + ∑' x : ↑(s : Set β)ᶜ, f x) = ∑' x, f x := - ((s.hasSum f).add_compl (s.summable_compl_iff.2 hf).hasSum).tsum_eq.symm +@[to_additive] +theorem prod_mul_tprod_compl {s : Finset β} (hf : Multipliable f) : + (∏ x in s, f x) * ∏' x : ↑(s : Set β)ᶜ, f x = ∏' x, f x := + ((s.hasProd f).mul_compl (s.multipliable_compl_iff.2 hf).hasProd).tprod_eq.symm #align sum_add_tsum_compl sum_add_tsum_compl -/-- Let `f : β → α` be a sequence with summable series and let `b ∈ β` be an index. -Lemma `tsum_eq_add_tsum_ite` writes `Σ f n` as the sum of `f b` plus the series of the +/-- Let `f : β → α` be a multipliable function and let `b ∈ β` be an index. +Lemma `tprod_eq_mul_tprod_ite` writes `∏ n, f n` as `f b` times the product of the remaining terms. -/ -theorem tsum_eq_add_tsum_ite [DecidableEq β] (hf : Summable f) (b : β) : - ∑' n, f n = f b + ∑' n, ite (n = b) 0 (f n) := by - rw [(hasSum_ite_sub_hasSum hf.hasSum b).tsum_eq] - exact (add_sub_cancel _ _).symm +@[to_additive "Let `f : β → α` be a summable function and let `b ∈ β` be an index. +Lemma `tsum_eq_add_tsum_ite` writes `Σ' n, f n` as `f b` plus the sum of the +remaining terms."] +theorem tprod_eq_mul_tprod_ite [DecidableEq β] (hf : Multipliable f) (b : β) : + ∏' n, f n = f b * ∏' n, ite (n = b) 1 (f n) := by + rw [(hasProd_ite_div_hasProd hf.hasProd b).tprod_eq] + exact (mul_div_cancel _ _).symm #align tsum_eq_add_tsum_ite tsum_eq_add_tsum_ite -end tsum +end tprod end TopologicalGroup section UniformGroup -variable [AddCommGroup α] [UniformSpace α] +variable [CommGroup α] [UniformSpace α] -/-- The **Cauchy criterion** for infinite sums, also known as the **Cauchy convergence test** -/ -theorem summable_iff_cauchySeq_finset [CompleteSpace α] {f : β → α} : - Summable f ↔ CauchySeq fun s : Finset β ↦ ∑ b in s, f b := by +/-- The **Cauchy criterion** for infinite products, also known as the **Cauchy convergence test** -/ +@[to_additive "The **Cauchy criterion** for infinite sums, also known as the +**Cauchy convergence test**"] +theorem multipliable_iff_cauchySeq_finset [CompleteSpace α] {f : β → α} : + Multipliable f ↔ CauchySeq fun s : Finset β ↦ ∏ b in s, f b := by classical exact cauchy_map_iff_exists_tendsto.symm #align summable_iff_cauchy_seq_finset summable_iff_cauchySeq_finset -variable [UniformAddGroup α] {f g : β → α} {a a₁ a₂ : α} +variable [UniformGroup α] {f g : β → α} {a a₁ a₂ : α} -theorem cauchySeq_finset_iff_vanishing : - (CauchySeq fun s : Finset β ↦ ∑ b in s, f b) ↔ - ∀ e ∈ 𝓝 (0 : α), ∃ s : Finset β, ∀ t, Disjoint t s → (∑ b in t, f b) ∈ e := by +@[to_additive] +theorem cauchySeq_finset_iff_prod_vanishing : + (CauchySeq fun s : Finset β ↦ ∏ b in s, f b) ↔ + ∀ e ∈ 𝓝 (1 : α), ∃ s : Finset β, ∀ t, Disjoint t s → (∏ b in t, f b) ∈ e := by classical simp only [CauchySeq, cauchy_map_iff, and_iff_right atTop_neBot, prod_atTop_atTop_eq, - uniformity_eq_comap_nhds_zero α, tendsto_comap_iff, (· ∘ ·), atTop_neBot, true_and] + uniformity_eq_comap_nhds_one α, tendsto_comap_iff, (· ∘ ·), atTop_neBot, true_and] rw [tendsto_atTop'] constructor · intro h e he @@ -180,96 +210,109 @@ theorem cauchySeq_finset_iff_vanishing : use s₁ ∪ s₂ intro t ht specialize h (s₁ ∪ s₂, s₁ ∪ s₂ ∪ t) ⟨le_sup_left, le_sup_of_le_left le_sup_right⟩ - simpa only [Finset.sum_union ht.symm, add_sub_cancel_left] using h + simpa only [Finset.prod_union ht.symm, mul_div_cancel_left] using h · rintro h e he - rcases exists_nhds_half_neg he with ⟨d, hd, hde⟩ + rcases exists_nhds_split_inv he with ⟨d, hd, hde⟩ rcases h d hd with ⟨s, h⟩ use (s, s) rintro ⟨t₁, t₂⟩ ⟨ht₁, ht₂⟩ - have : ((∑ b in t₂, f b) - ∑ b in t₁, f b) = (∑ b in t₂ \ s, f b) - ∑ b in t₁ \ s, f b := by - rw [← Finset.sum_sdiff ht₁, ← Finset.sum_sdiff ht₂, add_sub_add_right_eq_sub] + have : ((∏ b in t₂, f b) / ∏ b in t₁, f b) = (∏ b in t₂ \ s, f b) / ∏ b in t₁ \ s, f b := by + rw [← Finset.prod_sdiff ht₁, ← Finset.prod_sdiff ht₂, mul_div_mul_right_eq_div] simp only [this] exact hde _ (h _ Finset.sdiff_disjoint) _ (h _ Finset.sdiff_disjoint) -#align cauchy_seq_finset_iff_vanishing cauchySeq_finset_iff_vanishing +#align cauchy_seq_finset_iff_vanishing cauchySeq_finset_iff_sum_vanishing -theorem cauchySeq_finset_iff_tsum_vanishing : - (CauchySeq fun s : Finset β ↦ ∑ b in s, f b) ↔ - ∀ e ∈ 𝓝 (0 : α), ∃ s : Finset β, ∀ t : Set β, Disjoint t s → (∑' b : t, f b) ∈ e := by - simp_rw [cauchySeq_finset_iff_vanishing, Set.disjoint_left, disjoint_left] +@[to_additive] +theorem cauchySeq_finset_iff_tprod_vanishing : + (CauchySeq fun s : Finset β ↦ ∏ b in s, f b) ↔ + ∀ e ∈ 𝓝 (1 : α), ∃ s : Finset β, ∀ t : Set β, Disjoint t s → (∏' b : t, f b) ∈ e := by + simp_rw [cauchySeq_finset_iff_prod_vanishing, Set.disjoint_left, disjoint_left] refine ⟨fun vanish e he ↦ ?_, fun vanish e he ↦ ?_⟩ · obtain ⟨o, ho, o_closed, oe⟩ := exists_mem_nhds_isClosed_subset he obtain ⟨s, hs⟩ := vanish o ho refine ⟨s, fun t hts ↦ oe ?_⟩ - by_cases ht : Summable fun a : t ↦ f a + by_cases ht : Multipliable fun a : t ↦ f a · classical - refine o_closed.mem_of_tendsto ht.hasSum (eventually_of_forall fun t' ↦ ?_) - rw [← sum_subtype_map_embedding fun _ _ ↦ by rfl] + refine o_closed.mem_of_tendsto ht.hasProd (eventually_of_forall fun t' ↦ ?_) + rw [← prod_subtype_map_embedding fun _ _ ↦ by rfl] apply hs simp_rw [Finset.mem_map] rintro _ ⟨b, -, rfl⟩ exact hts b.prop - · exact tsum_eq_zero_of_not_summable ht ▸ mem_of_mem_nhds ho + · exact tprod_eq_one_of_not_multipliable ht ▸ mem_of_mem_nhds ho · obtain ⟨s, hs⟩ := vanish _ he - exact ⟨s, fun t hts ↦ (t.tsum_subtype f).symm ▸ hs _ hts⟩ + exact ⟨s, fun t hts ↦ (t.tprod_subtype f).symm ▸ hs _ hts⟩ variable [CompleteSpace α] -theorem summable_iff_vanishing : - Summable f ↔ ∀ e ∈ 𝓝 (0 : α), ∃ s : Finset β, ∀ t, Disjoint t s → (∑ b in t, f b) ∈ e := by - rw [summable_iff_cauchySeq_finset, cauchySeq_finset_iff_vanishing] +@[to_additive] +theorem multipliable_iff_vanishing : + Multipliable f ↔ + ∀ e ∈ 𝓝 (1 : α), ∃ s : Finset β, ∀ t, Disjoint t s → (∏ b in t, f b) ∈ e := by + rw [multipliable_iff_cauchySeq_finset, cauchySeq_finset_iff_prod_vanishing] #align summable_iff_vanishing summable_iff_vanishing -theorem summable_iff_tsum_vanishing : Summable f ↔ - ∀ e ∈ 𝓝 (0 : α), ∃ s : Finset β, ∀ t : Set β, Disjoint t s → (∑' b : t, f b) ∈ e := by - rw [summable_iff_cauchySeq_finset, cauchySeq_finset_iff_tsum_vanishing] +@[to_additive] +theorem multipliable_iff_tprod_vanishing : Multipliable f ↔ + ∀ e ∈ 𝓝 (1 : α), ∃ s : Finset β, ∀ t : Set β, Disjoint t s → (∏' b : t, f b) ∈ e := by + rw [multipliable_iff_cauchySeq_finset, cauchySeq_finset_iff_tprod_vanishing] -- TODO: generalize to monoid with a uniform continuous subtraction operator: `(a + b) - b = a` -theorem Summable.summable_of_eq_zero_or_self (hf : Summable f) (h : ∀ b, g b = 0 ∨ g b = f b) : - Summable g := by +@[to_additive] +theorem Multipliable.multipliable_of_eq_one_or_self (hf : Multipliable f) + (h : ∀ b, g b = 1 ∨ g b = f b) : Multipliable g := by classical - exact summable_iff_vanishing.2 fun e he ↦ - let ⟨s, hs⟩ := summable_iff_vanishing.1 hf e he + exact multipliable_iff_vanishing.2 fun e he ↦ + let ⟨s, hs⟩ := multipliable_iff_vanishing.1 hf e he ⟨s, fun t ht ↦ - have eq : ∑ b in t.filter fun b ↦ g b = f b, f b = ∑ b in t, g b := + have eq : ∏ b in t.filter fun b ↦ g b = f b, f b = ∏ b in t, g b := calc - ∑ b in t.filter fun b ↦ g b = f b, f b = ∑ b in t.filter fun b ↦ g b = f b, g b := - Finset.sum_congr rfl fun b hb ↦ (Finset.mem_filter.1 hb).2.symm - _ = ∑ b in t, g b := by - {refine' Finset.sum_subset (Finset.filter_subset _ _) _ + ∏ b in t.filter fun b ↦ g b = f b, f b = ∏ b in t.filter fun b ↦ g b = f b, g b := + Finset.prod_congr rfl fun b hb ↦ (Finset.mem_filter.1 hb).2.symm + _ = ∏ b in t, g b := by + {refine' Finset.prod_subset (Finset.filter_subset _ _) _ intro b hbt hb simp only [Finset.mem_filter, and_iff_right hbt] at hb exact (h b).resolve_right hb} eq ▸ hs _ <| Finset.disjoint_of_subset_left (Finset.filter_subset _ _) ht⟩ #align summable.summable_of_eq_zero_or_self Summable.summable_of_eq_zero_or_self -protected theorem Summable.indicator (hf : Summable f) (s : Set β) : Summable (s.indicator f) := - hf.summable_of_eq_zero_or_self <| Set.indicator_eq_zero_or_self _ _ +@[to_additive] +protected theorem Multipliable.mulIndicator (hf : Multipliable f) (s : Set β) : + Multipliable (s.mulIndicator f) := + hf.multipliable_of_eq_one_or_self <| Set.mulIndicator_eq_one_or_self _ _ #align summable.indicator Summable.indicator -theorem Summable.comp_injective {i : γ → β} (hf : Summable f) (hi : Injective i) : - Summable (f ∘ i) := by - simpa only [Set.indicator_range_comp] using - (hi.summable_iff (fun x hx ↦ Set.indicator_of_not_mem hx _)).2 (hf.indicator (Set.range i)) +@[to_additive] +theorem Multipliable.comp_injective {i : γ → β} (hf : Multipliable f) (hi : Injective i) : + Multipliable (f ∘ i) := by + simpa only [Set.mulIndicator_range_comp] using + (hi.multipliable_iff (fun x hx ↦ Set.mulIndicator_of_not_mem hx _)).2 + (hf.mulIndicator (Set.range i)) #align summable.comp_injective Summable.comp_injective -theorem Summable.subtype (hf : Summable f) (s : Set β) : Summable (f ∘ (↑) : s → α) := +@[to_additive] +theorem Multipliable.subtype (hf : Multipliable f) (s : Set β) : Multipliable (f ∘ (↑) : s → α) := hf.comp_injective Subtype.coe_injective #align summable.subtype Summable.subtype -theorem summable_subtype_and_compl {s : Set β} : - ((Summable fun x : s ↦ f x) ∧ Summable fun x : ↑sᶜ ↦ f x) ↔ Summable f := - ⟨and_imp.2 Summable.add_compl, fun h ↦ ⟨h.subtype s, h.subtype sᶜ⟩⟩ +@[to_additive] +theorem multipliable_subtype_and_compl {s : Set β} : + ((Multipliable fun x : s ↦ f x) ∧ Multipliable fun x : ↑sᶜ ↦ f x) ↔ Multipliable f := + ⟨and_imp.2 Multipliable.mul_compl, fun h ↦ ⟨h.subtype s, h.subtype sᶜ⟩⟩ #align summable_subtype_and_compl summable_subtype_and_compl -theorem tsum_subtype_add_tsum_subtype_compl [T2Space α] {f : β → α} (hf : Summable f) (s : Set β) : - ∑' x : s, f x + ∑' x : ↑sᶜ, f x = ∑' x, f x := - ((hf.subtype s).hasSum.add_compl (hf.subtype { x | x ∉ s }).hasSum).unique hf.hasSum +@[to_additive] +theorem tprod_subtype_mul_tprod_subtype_compl [T2Space α] {f : β → α} (hf : Multipliable f) + (s : Set β) : (∏' x : s, f x) * ∏' x : ↑sᶜ, f x = ∏' x, f x := + ((hf.subtype s).hasProd.mul_compl (hf.subtype { x | x ∉ s }).hasProd).unique hf.hasProd #align tsum_subtype_add_tsum_subtype_compl tsum_subtype_add_tsum_subtype_compl -theorem sum_add_tsum_subtype_compl [T2Space α] {f : β → α} (hf : Summable f) (s : Finset β) : - ∑ x in s, f x + ∑' x : { x // x ∉ s }, f x = ∑' x, f x := by - rw [← tsum_subtype_add_tsum_subtype_compl hf s] - simp only [Finset.tsum_subtype', add_right_inj] +@[to_additive] +theorem prod_mul_tprod_subtype_compl [T2Space α] {f : β → α} (hf : Multipliable f) (s : Finset β) : + (∏ x in s, f x) * ∏' x : { x // x ∉ s }, f x = ∏' x, f x := by + rw [← tprod_subtype_mul_tprod_subtype_compl hf s] + simp only [Finset.tprod_subtype', mul_right_inj] rfl #align sum_add_tsum_subtype_compl sum_add_tsum_subtype_compl @@ -277,40 +320,47 @@ end UniformGroup section TopologicalGroup -variable {G : Type*} [TopologicalSpace G] [AddCommGroup G] [TopologicalAddGroup G] {f : α → G} +variable {G : Type*} [TopologicalSpace G] [CommGroup G] [TopologicalGroup G] {f : α → G} -theorem Summable.vanishing (hf : Summable f) ⦃e : Set G⦄ (he : e ∈ 𝓝 (0 : G)) : - ∃ s : Finset α, ∀ t, Disjoint t s → (∑ k in t, f k) ∈ e := by +@[to_additive] +theorem Multipliable.vanishing (hf : Multipliable f) ⦃e : Set G⦄ (he : e ∈ 𝓝 (1 : G)) : + ∃ s : Finset α, ∀ t, Disjoint t s → (∏ k in t, f k) ∈ e := by classical - letI : UniformSpace G := TopologicalAddGroup.toUniformSpace G - have : UniformAddGroup G := comm_topologicalAddGroup_is_uniform - exact cauchySeq_finset_iff_vanishing.1 hf.hasSum.cauchySeq e he + letI : UniformSpace G := TopologicalGroup.toUniformSpace G + have : UniformGroup G := comm_topologicalGroup_is_uniform + exact cauchySeq_finset_iff_prod_vanishing.1 hf.hasProd.cauchySeq e he #align summable.vanishing Summable.vanishing -theorem Summable.tsum_vanishing (hf : Summable f) ⦃e : Set G⦄ (he : e ∈ 𝓝 0) : - ∃ s : Finset α, ∀ t : Set α, Disjoint t s → (∑' b : t, f b) ∈ e := by +@[to_additive] +theorem Multipliable.tprod_vanishing (hf : Multipliable f) ⦃e : Set G⦄ (he : e ∈ 𝓝 1) : + ∃ s : Finset α, ∀ t : Set α, Disjoint t s → (∏' b : t, f b) ∈ e := by classical - letI : UniformSpace G := TopologicalAddGroup.toUniformSpace G - have : UniformAddGroup G := comm_topologicalAddGroup_is_uniform - exact cauchySeq_finset_iff_tsum_vanishing.1 hf.hasSum.cauchySeq e he - -/-- The sum over the complement of a finset tends to `0` when the finset grows to cover the whole -space. This does not need a summability assumption, as otherwise all sums are zero. -/ -theorem tendsto_tsum_compl_atTop_zero (f : α → G) : - Tendsto (fun s : Finset α ↦ ∑' a : { x // x ∉ s }, f a) atTop (𝓝 0) := by + letI : UniformSpace G := TopologicalGroup.toUniformSpace G + have : UniformGroup G := comm_topologicalGroup_is_uniform + exact cauchySeq_finset_iff_tprod_vanishing.1 hf.hasProd.cauchySeq e he + +/-- The product over the complement of a finset tends to `1` when the finset grows to cover the +whole space. This does not need a multipliability assumption, as otherwise all such products are +one. -/ +@[to_additive "The sum over the complement of a finset tends to `0` when the finset grows to cover +the whole space. This does not need a summability assumption, as otherwise all such sums are zero."] +theorem tendsto_tprod_compl_atTop_one (f : α → G) : + Tendsto (fun s : Finset α ↦ ∏' a : { x // x ∉ s }, f a) atTop (𝓝 1) := by classical - by_cases H : Summable f + by_cases H : Multipliable f · intro e he - obtain ⟨s, hs⟩ := H.tsum_vanishing he + obtain ⟨s, hs⟩ := H.tprod_vanishing he rw [Filter.mem_map, mem_atTop_sets] exact ⟨s, fun t hts ↦ hs _ <| Set.disjoint_left.mpr fun a ha has ↦ ha (hts has)⟩ - · refine tendsto_const_nhds.congr fun _ ↦ (tsum_eq_zero_of_not_summable ?_).symm - rwa [Finset.summable_compl_iff] + · refine tendsto_const_nhds.congr fun _ ↦ (tprod_eq_one_of_not_multipliable ?_).symm + rwa [Finset.multipliable_compl_iff] #align tendsto_tsum_compl_at_top_zero tendsto_tsum_compl_atTop_zero -/-- Series divergence test: if `f` is a convergent series, then `f x` tends to zero along +/-- Product divergence test: if `f` is unconditionally multipliable, then `f x` tends to one along `cofinite`. -/ -theorem Summable.tendsto_cofinite_zero (hf : Summable f) : Tendsto f cofinite (𝓝 0) := by +@[to_additive "Series divergence test: if `f` is unconditionally summable, then `f x` tends to zero +along `cofinite`."] +theorem Multipliable.tendsto_cofinite_one (hf : Multipliable f) : Tendsto f cofinite (𝓝 1) := by intro e he rw [Filter.mem_map] rcases hf.vanishing he with ⟨s, hs⟩ @@ -318,31 +368,33 @@ theorem Summable.tendsto_cofinite_zero (hf : Summable f) : Tendsto f cofinite ( · simpa using hs {x} (disjoint_singleton_left.2 hx) #align summable.tendsto_cofinite_zero Summable.tendsto_cofinite_zero -theorem Summable.countable_support [FirstCountableTopology G] [T1Space G] - (hf : Summable f) : f.support.Countable := by - simpa only [ker_nhds] using hf.tendsto_cofinite_zero.countable_compl_preimage_ker +@[to_additive] +theorem Multipliable.countable_mulSupport [FirstCountableTopology G] [T1Space G] + (hf : Multipliable f) : f.mulSupport.Countable := by + simpa only [ker_nhds] using hf.tendsto_cofinite_one.countable_compl_preimage_ker -theorem summable_const_iff [Infinite β] [T2Space G] (a : G) : - Summable (fun _ : β ↦ a) ↔ a = 0 := by +@[to_additive] +theorem multipliable_const_iff [Infinite β] [T2Space G] (a : G) : + Multipliable (fun _ : β ↦ a) ↔ a = 1 := by refine ⟨fun h ↦ ?_, ?_⟩ · by_contra ha - have : {a}ᶜ ∈ 𝓝 0 := compl_singleton_mem_nhds (Ne.symm ha) + have : {a}ᶜ ∈ 𝓝 1 := compl_singleton_mem_nhds (Ne.symm ha) have : Finite β := by - simpa [← Set.finite_univ_iff] using h.tendsto_cofinite_zero this + simpa [← Set.finite_univ_iff] using h.tendsto_cofinite_one this exact not_finite β · rintro rfl - exact summable_zero + exact multipliable_one -@[simp] -theorem tsum_const [T2Space G] (a : G) : ∑' _ : β, a = Nat.card β • a := by +@[to_additive (attr := simp)] +theorem tprod_const [T2Space G] (a : G) : ∏' _ : β, a = a ^ (Nat.card β) := by rcases finite_or_infinite β with hβ|hβ · letI : Fintype β := Fintype.ofFinite β - rw [tsum_eq_sum (s := univ) (fun x hx ↦ (hx (mem_univ x)).elim)] - simp only [sum_const, Nat.card_eq_fintype_card, Fintype.card] - · simp only [Nat.card_eq_zero_of_infinite, zero_smul] - rcases eq_or_ne a 0 with rfl|ha + rw [tprod_eq_prod (s := univ) (fun x hx ↦ (hx (mem_univ x)).elim)] + simp only [prod_const, Nat.card_eq_fintype_card, Fintype.card] + · simp only [Nat.card_eq_zero_of_infinite, pow_zero] + rcases eq_or_ne a 1 with rfl|ha · simp - · apply tsum_eq_zero_of_not_summable - simpa [summable_const_iff] using ha + · apply tprod_eq_one_of_not_multipliable + simpa [multipliable_const_iff] using ha end TopologicalGroup diff --git a/Mathlib/Topology/Algebra/InfiniteSum/NatInt.lean b/Mathlib/Topology/Algebra/InfiniteSum/NatInt.lean index a679682776863a..5ea71b9fcca771 100644 --- a/Mathlib/Topology/Algebra/InfiniteSum/NatInt.lean +++ b/Mathlib/Topology/Algebra/InfiniteSum/NatInt.lean @@ -10,10 +10,10 @@ import Mathlib.Logic.Encodable.Lattice /-! # Infinite sums over `ℕ` and `ℤ` -This file contains lemmas about `HasSum`, `Summable`, and `tsum` applied to the important special -cases where the domain is `ℕ` or `ℤ`. For instance, we prove the formula -`∑ i in range k, f i + ∑' i, f (i + k) = ∑' i, f i`, in `sum_add_tsum_nat_add`, as well as several -results relating sums on `ℕ` and `ℤ`. +This file contains lemmas about `HasSum`, `Summable`, `tsum`, `HasProd`, `Multipliable`, `tprod` +applied to the important special cases where the domain is `ℕ` or `ℤ`. For instance, we prove the +formula `∑ i in range k, f i + ∑' i, f (i + k) = ∑' i, f i`, in `sum_add_tsum_nat_add`, as well as +several results relating sums on `ℕ` and `ℤ`. -/ noncomputable section @@ -22,9 +22,9 @@ open Filter Finset Function Encodable open scoped BigOperators Topology -variable {M : Type*} [AddCommMonoid M] [TopologicalSpace M] {m m' : M} +variable {M : Type*} [CommMonoid M] [TopologicalSpace M] {m m' : M} -variable {G : Type*} [AddCommGroup G] {g g' : G} +variable {G : Type*} [CommGroup G] {g g' : G} -- don't declare [TopologicalAddGroup G] here as some results require [UniformAddGroup G] instead /-! @@ -35,64 +35,73 @@ section Nat section Monoid -namespace HasSum +namespace HasProd -/-- If `f : ℕ → M` has sum `m`, then the partial sums `∑ i in range n, f i` converge to `m`. -/ -theorem tendsto_sum_nat {f : ℕ → M} (h : HasSum f m) : - Tendsto (fun n ↦ ∑ i in range n, f i) atTop (𝓝 m) := +/-- If `f : ℕ → M` has product `m`, then the partial products `∏ i in range n, f i` converge +to `m`. -/ +@[to_additive "If `f : ℕ → M` has sum `m`, then the partial sums `∑ i in range n, f i` converge +to `m`."] +theorem tendsto_prod_nat {f : ℕ → M} (h : HasProd f m) : + Tendsto (fun n ↦ ∏ i in range n, f i) atTop (𝓝 m) := h.comp tendsto_finset_range #align has_sum.tendsto_sum_nat HasSum.tendsto_sum_nat -section ContinuousAdd +section ContinuousMul -variable [ContinuousAdd M] +variable [ContinuousMul M] -theorem sum_range_add {f : ℕ → M} {k : ℕ} (h : HasSum (fun n ↦ f (n + k)) m) : - HasSum f ((∑ i in range k, f i) + m) := by - refine ((range k).hasSum f).add_compl ?_ - rwa [← (notMemRangeEquiv k).symm.hasSum_iff] +@[to_additive] +theorem prod_range_mul {f : ℕ → M} {k : ℕ} (h : HasProd (fun n ↦ f (n + k)) m) : + HasProd f ((∏ i in range k, f i) * m) := by + refine ((range k).hasProd f).mul_compl ?_ + rwa [← (notMemRangeEquiv k).symm.hasProd_iff] -theorem zero_add {f : ℕ → M} (h : HasSum (fun n ↦ f (n + 1)) m) : - HasSum f (f 0 + m) := by - simpa only [sum_range_one] using h.sum_range_add +@[to_additive] +theorem zero_mul {f : ℕ → M} (h : HasProd (fun n ↦ f (n + 1)) m) : + HasProd f (f 0 * m) := by + simpa only [prod_range_one] using h.prod_range_mul -theorem even_add_odd {f : ℕ → M} (he : HasSum (fun k ↦ f (2 * k)) m) - (ho : HasSum (fun k ↦ f (2 * k + 1)) m') : HasSum f (m + m') := by +@[to_additive] +theorem even_mul_odd {f : ℕ → M} (he : HasProd (fun k ↦ f (2 * k)) m) + (ho : HasProd (fun k ↦ f (2 * k + 1)) m') : HasProd f (m * m') := by have := mul_right_injective₀ (two_ne_zero' ℕ) - replace ho := ((add_left_injective 1).comp this).hasSum_range_iff.2 ho - refine (this.hasSum_range_iff.2 he).add_isCompl ?_ ho + replace ho := ((add_left_injective 1).comp this).hasProd_range_iff.2 ho + refine (this.hasProd_range_iff.2 he).mul_isCompl ?_ ho simpa [(· ∘ ·)] using Nat.isCompl_even_odd #align has_sum.even_add_odd HasSum.even_add_odd -end ContinuousAdd +end ContinuousMul -end HasSum +end HasProd -namespace Summable +namespace Multipliable -theorem hasSum_iff_tendsto_nat [T2Space M] {f : ℕ → M} (hf : Summable f) : - HasSum f m ↔ Tendsto (fun n : ℕ ↦ ∑ i in range n, f i) atTop (𝓝 m) := by - refine ⟨fun h ↦ h.tendsto_sum_nat, fun h ↦ ?_⟩ - rw [tendsto_nhds_unique h hf.hasSum.tendsto_sum_nat] - exact hf.hasSum +@[to_additive] +theorem hasProd_iff_tendsto_nat [T2Space M] {f : ℕ → M} (hf : Multipliable f) : + HasProd f m ↔ Tendsto (fun n : ℕ ↦ ∏ i in range n, f i) atTop (𝓝 m) := by + refine ⟨fun h ↦ h.tendsto_prod_nat, fun h ↦ ?_⟩ + rw [tendsto_nhds_unique h hf.hasProd.tendsto_prod_nat] + exact hf.hasProd #align summable.has_sum_iff_tendsto_nat Summable.hasSum_iff_tendsto_nat -section ContinuousAdd +section ContinuousMul -variable [ContinuousAdd M] +variable [ContinuousMul M] -theorem comp_nat_add {f : ℕ → M} {k : ℕ} (h : Summable fun n ↦ f (n + k)) : Summable f := - h.hasSum.sum_range_add.summable +@[to_additive] +theorem comp_nat_add {f : ℕ → M} {k : ℕ} (h : Multipliable fun n ↦ f (n + k)) : Multipliable f := + h.hasProd.prod_range_mul.multipliable -theorem even_add_odd {f : ℕ → M} (he : Summable fun k ↦ f (2 * k)) - (ho : Summable fun k ↦ f (2 * k + 1)) : Summable f := - (he.hasSum.even_add_odd ho.hasSum).summable +@[to_additive] +theorem even_mul_odd {f : ℕ → M} (he : Multipliable fun k ↦ f (2 * k)) + (ho : Multipliable fun k ↦ f (2 * k + 1)) : Multipliable f := + (he.hasProd.even_mul_odd ho.hasProd).multipliable -end ContinuousAdd +end ContinuousMul -end Summable +end Multipliable -section tsum +section tprod variable [T2Space M] {α β γ : Type*} @@ -100,12 +109,14 @@ section Encodable variable [Encodable β] -/-- You can compute a sum over an encodable type by summing over the natural numbers and - taking a supremum. This is useful for outer measures. -/ -theorem tsum_iSup_decode₂ [CompleteLattice α] (m : α → M) (m0 : m ⊥ = 0) (s : β → α) : - ∑' i : ℕ, m (⨆ b ∈ decode₂ β i, s b) = ∑' b : β, m (s b) := by - rw [← tsum_extend_zero (@encode_injective β _)] - refine tsum_congr fun n ↦ ?_ +/-- You can compute a product over an encodable type by multiplying over the natural numbers and +taking a supremum. -/ +@[to_additive "You can compute a sum over an encodable type by summing over the natural numbers and + taking a supremum. This is useful for outer measures."] +theorem tprod_iSup_decode₂ [CompleteLattice α] (m : α → M) (m0 : m ⊥ = 1) (s : β → α) : + ∏' i : ℕ, m (⨆ b ∈ decode₂ β i, s b) = ∏' b : β, m (s b) := by + rw [← tprod_extend_one (@encode_injective β _)] + refine tprod_congr fun n ↦ ?_ rcases em (n ∈ Set.range (encode : β → ℕ)) with ⟨a, rfl⟩ | hn · simp [encode_injective.extend_apply] · rw [extend_apply' _ _ _ hn] @@ -113,10 +124,11 @@ theorem tsum_iSup_decode₂ [CompleteLattice α] (m : α → M) (m0 : m ⊥ = 0) simp [hn, m0] #align tsum_supr_decode₂ tsum_iSup_decode₂ -/-- `tsum_iSup_decode₂` specialized to the complete lattice of sets. -/ -theorem tsum_iUnion_decode₂ (m : Set α → M) (m0 : m ∅ = 0) (s : β → Set α) : - ∑' i, m (⋃ b ∈ decode₂ β i, s b) = ∑' b, m (s b) := - tsum_iSup_decode₂ m m0 s +/-- `tprod_iSup_decode₂` specialized to the complete lattice of sets. -/ +@[to_additive "`tsum_iSup_decode₂` specialized to the complete lattice of sets."] +theorem tprod_iUnion_decode₂ (m : Set α → M) (m0 : m ∅ = 1) (s : β → Set α) : + ∏' i, m (⋃ b ∈ decode₂ β i, s b) = ∏' b, m (s b) := + tprod_iSup_decode₂ m m0 s #align tsum_Union_decode₂ tsum_iUnion_decode₂ end Encodable @@ -129,117 +141,134 @@ section Countable variable [Countable β] -/-- If a function is countably sub-additive then it is sub-additive on countable types -/ -theorem rel_iSup_tsum [CompleteLattice α] (m : α → M) (m0 : m ⊥ = 0) (R : M → M → Prop) - (m_iSup : ∀ s : ℕ → α, R (m (⨆ i, s i)) (∑' i, m (s i))) (s : β → α) : - R (m (⨆ b : β, s b)) (∑' b : β, m (s b)) := by +/-- If a function is countably sub-multiplicative then it is sub-multiplicative on countable +types -/ +@[to_additive "If a function is countably sub-additive then it is sub-additive on countable types"] +theorem rel_iSup_tprod [CompleteLattice α] (m : α → M) (m0 : m ⊥ = 1) (R : M → M → Prop) + (m_iSup : ∀ s : ℕ → α, R (m (⨆ i, s i)) (∏' i, m (s i))) (s : β → α) : + R (m (⨆ b : β, s b)) (∏' b : β, m (s b)) := by cases nonempty_encodable β - rw [← iSup_decode₂, ← tsum_iSup_decode₂ _ m0 s] + rw [← iSup_decode₂, ← tprod_iSup_decode₂ _ m0 s] exact m_iSup _ #align rel_supr_tsum rel_iSup_tsum -/-- If a function is countably sub-additive then it is sub-additive on finite sets -/ -theorem rel_iSup_sum [CompleteLattice α] (m : α → M) (m0 : m ⊥ = 0) (R : M → M → Prop) - (m_iSup : ∀ s : ℕ → α, R (m (⨆ i, s i)) (∑' i, m (s i))) (s : γ → α) (t : Finset γ) : - R (m (⨆ d ∈ t, s d)) (∑ d in t, m (s d)) := by - rw [iSup_subtype', ← Finset.tsum_subtype] - exact rel_iSup_tsum m m0 R m_iSup _ +/-- If a function is countably sub-multiplicative then it is sub-multiplicative on finite sets -/ +@[to_additive "If a function is countably sub-additive then it is sub-additive on finite sets"] +theorem rel_iSup_prod [CompleteLattice α] (m : α → M) (m0 : m ⊥ = 1) (R : M → M → Prop) + (m_iSup : ∀ s : ℕ → α, R (m (⨆ i, s i)) (∏' i, m (s i))) (s : γ → α) (t : Finset γ) : + R (m (⨆ d ∈ t, s d)) (∏ d in t, m (s d)) := by + rw [iSup_subtype', ← Finset.tprod_subtype] + exact rel_iSup_tprod m m0 R m_iSup _ #align rel_supr_sum rel_iSup_sum -/-- If a function is countably sub-additive then it is binary sub-additive -/ -theorem rel_sup_add [CompleteLattice α] (m : α → M) (m0 : m ⊥ = 0) (R : M → M → Prop) - (m_iSup : ∀ s : ℕ → α, R (m (⨆ i, s i)) (∑' i, m (s i))) (s₁ s₂ : α) : - R (m (s₁ ⊔ s₂)) (m s₁ + m s₂) := by - convert rel_iSup_tsum m m0 R m_iSup fun b ↦ cond b s₁ s₂ +/-- If a function is countably sub-multiplicative then it is binary sub-multiplicative -/ +@[to_additive "If a function is countably sub-additive then it is binary sub-additive"] +theorem rel_sup_mul [CompleteLattice α] (m : α → M) (m0 : m ⊥ = 1) (R : M → M → Prop) + (m_iSup : ∀ s : ℕ → α, R (m (⨆ i, s i)) (∏' i, m (s i))) (s₁ s₂ : α) : + R (m (s₁ ⊔ s₂)) (m s₁ * m s₂) := by + convert rel_iSup_tprod m m0 R m_iSup fun b ↦ cond b s₁ s₂ · simp only [iSup_bool_eq, cond] - · rw [tsum_fintype, Fintype.sum_bool, cond, cond] + · rw [tprod_fintype, Fintype.prod_bool, cond, cond] #align rel_sup_add rel_sup_add end Countable -section ContinuousAdd +section ContinuousMul -variable [ContinuousAdd M] +variable [ContinuousMul M] -theorem sum_add_tsum_nat_add' - {f : ℕ → M} {k : ℕ} (h : Summable (fun n ↦ f (n + k))) : - ((∑ i in range k, f i) + ∑' i, f (i + k)) = ∑' i, f i := - h.hasSum.sum_range_add.tsum_eq.symm +@[to_additive] +theorem prod_mul_tprod_nat_mul' + {f : ℕ → M} {k : ℕ} (h : Multipliable (fun n ↦ f (n + k))) : + ((∏ i in range k, f i) * ∏' i, f (i + k)) = ∏' i, f i := + h.hasProd.prod_range_mul.tprod_eq.symm -theorem tsum_eq_zero_add' - {f : ℕ → M} (hf : Summable (fun n ↦ f (n + 1))) : - ∑' b, f b = f 0 + ∑' b, f (b + 1) := by - simpa only [sum_range_one] using (sum_add_tsum_nat_add' hf).symm +@[to_additive] +theorem tprod_eq_zero_mul' + {f : ℕ → M} (hf : Multipliable (fun n ↦ f (n + 1))) : + ∏' b, f b = f 0 * ∏' b, f (b + 1) := by + simpa only [prod_range_one] using (prod_mul_tprod_nat_mul' hf).symm -theorem tsum_even_add_odd {f : ℕ → M} (he : Summable fun k ↦ f (2 * k)) - (ho : Summable fun k ↦ f (2 * k + 1)) : - ∑' k, f (2 * k) + ∑' k, f (2 * k + 1) = ∑' k, f k := - (he.hasSum.even_add_odd ho.hasSum).tsum_eq.symm +@[to_additive] +theorem tprod_even_mul_odd {f : ℕ → M} (he : Multipliable fun k ↦ f (2 * k)) + (ho : Multipliable fun k ↦ f (2 * k + 1)) : + (∏' k, f (2 * k)) * ∏' k, f (2 * k + 1) = ∏' k, f k := + (he.hasProd.even_mul_odd ho.hasProd).tprod_eq.symm #align tsum_even_add_odd tsum_even_add_odd -end ContinuousAdd +end ContinuousMul -end tsum +end tprod end Monoid section TopologicalGroup -variable [TopologicalSpace G] [TopologicalAddGroup G] +variable [TopologicalSpace G] [TopologicalGroup G] -theorem hasSum_nat_add_iff {f : ℕ → G} (k : ℕ) : - HasSum (fun n ↦ f (n + k)) g ↔ HasSum f (g + ∑ i in range k, f i) := by - refine Iff.trans ?_ (range k).hasSum_compl_iff - rw [← (notMemRangeEquiv k).symm.hasSum_iff, Function.comp_def, coe_notMemRangeEquiv_symm] +@[to_additive] +theorem hasProd_nat_add_iff {f : ℕ → G} (k : ℕ) : + HasProd (fun n ↦ f (n + k)) g ↔ HasProd f (g * ∏ i in range k, f i) := by + refine Iff.trans ?_ (range k).hasProd_compl_iff + rw [← (notMemRangeEquiv k).symm.hasProd_iff, Function.comp_def, coe_notMemRangeEquiv_symm] #align has_sum_nat_add_iff hasSum_nat_add_iff -theorem summable_nat_add_iff {f : ℕ → G} (k : ℕ) : (Summable fun n ↦ f (n + k)) ↔ Summable f := +@[to_additive] +theorem multipliable_nat_add_iff {f : ℕ → G} (k : ℕ) : + (Multipliable fun n ↦ f (n + k)) ↔ Multipliable f := Iff.symm <| - (Equiv.addRight (∑ i in range k, f i)).surjective.summable_iff_of_hasSum_iff - (hasSum_nat_add_iff k).symm + (Equiv.mulRight (∏ i in range k, f i)).surjective.multipliable_iff_of_hasProd_iff + (hasProd_nat_add_iff k).symm #align summable_nat_add_iff summable_nat_add_iff -theorem hasSum_nat_add_iff' {f : ℕ → G} (k : ℕ) : - HasSum (fun n ↦ f (n + k)) (g - ∑ i in range k, f i) ↔ HasSum f g := by - simp [hasSum_nat_add_iff] +@[to_additive] +theorem hasProd_nat_add_iff' {f : ℕ → G} (k : ℕ) : + HasProd (fun n ↦ f (n + k)) (g / ∏ i in range k, f i) ↔ HasProd f g := by + simp [hasProd_nat_add_iff] #align has_sum_nat_add_iff' hasSum_nat_add_iff' -theorem sum_add_tsum_nat_add [T2Space G] {f : ℕ → G} (k : ℕ) (h : Summable f) : - ((∑ i in range k, f i) + ∑' i, f (i + k)) = ∑' i, f i := - sum_add_tsum_nat_add' <| (summable_nat_add_iff k).2 h +@[to_additive] +theorem prod_mul_tprod_nat_add [T2Space G] {f : ℕ → G} (k : ℕ) (h : Multipliable f) : + ((∏ i in range k, f i) * ∏' i, f (i + k)) = ∏' i, f i := + prod_mul_tprod_nat_mul' <| (multipliable_nat_add_iff k).2 h #align sum_add_tsum_nat_add sum_add_tsum_nat_add -theorem tsum_eq_zero_add [T2Space G] {f : ℕ → G} (hf : Summable f) : - ∑' b, f b = f 0 + ∑' b, f (b + 1) := - tsum_eq_zero_add' <| (summable_nat_add_iff 1).2 hf +@[to_additive] +theorem tprod_eq_zero_mul [T2Space G] {f : ℕ → G} (hf : Multipliable f) : + ∏' b, f b = f 0 * ∏' b, f (b + 1) := + tprod_eq_zero_mul' <| (multipliable_nat_add_iff 1).2 hf #align tsum_eq_zero_add tsum_eq_zero_add -/-- For `f : ℕ → G`, then `∑' k, f (k + i)` tends to zero. This does not require a summability -assumption on `f`, as otherwise all sums are zero. -/ -theorem tendsto_sum_nat_add [T2Space G] (f : ℕ → G) : - Tendsto (fun i ↦ ∑' k, f (k + i)) atTop (𝓝 0) := by - by_cases hf : Summable f - · have h₀ : (fun i ↦ ∑' i, f i - ∑ j in range i, f j) = fun i ↦ ∑' k : ℕ, f (k + i) := by +/-- For `f : ℕ → G`, the product `∏' k, f (k + i)` tends to one. This does not require a +multipliability assumption on `f`, as otherwise all such products are one. -/ +@[to_additive "For `f : ℕ → G`, the sum `∑' k, f (k + i)` tends to zero. This does not require a +summability assumption on `f`, as otherwise all such sums are zero."] +theorem tendsto_prod_nat_add [T2Space G] (f : ℕ → G) : + Tendsto (fun i ↦ ∏' k, f (k + i)) atTop (𝓝 1) := by + by_cases hf : Multipliable f + · have h₀ : (fun i ↦ (∏' i, f i) / ∏ j in range i, f j) = fun i ↦ ∏' k : ℕ, f (k + i) := by ext1 i - rw [sub_eq_iff_eq_add, add_comm, sum_add_tsum_nat_add i hf] - have h₁ : Tendsto (fun _ : ℕ ↦ ∑' i, f i) atTop (𝓝 (∑' i, f i)) := tendsto_const_nhds - simpa only [h₀, sub_self] using Tendsto.sub h₁ hf.hasSum.tendsto_sum_nat - · refine tendsto_const_nhds.congr fun n ↦ (tsum_eq_zero_of_not_summable ?_).symm - rwa [summable_nat_add_iff n] + rw [div_eq_iff_eq_mul, mul_comm, prod_mul_tprod_nat_add i hf] + have h₁ : Tendsto (fun _ : ℕ ↦ ∏' i, f i) atTop (𝓝 (∏' i, f i)) := tendsto_const_nhds + simpa only [h₀, div_self'] using Tendsto.div' h₁ hf.hasProd.tendsto_prod_nat + · refine tendsto_const_nhds.congr fun n ↦ (tprod_eq_one_of_not_multipliable ?_).symm + rwa [multipliable_nat_add_iff n] #align tendsto_sum_nat_add tendsto_sum_nat_add end TopologicalGroup section UniformGroup -variable [UniformSpace G] [UniformAddGroup G] +variable [UniformSpace G] [UniformGroup G] -theorem cauchySeq_finset_iff_nat_tsum_vanishing {f : ℕ → G} : - (CauchySeq fun s : Finset ℕ ↦ ∑ n in s, f n) ↔ - ∀ e ∈ 𝓝 (0 : G), ∃ N : ℕ, ∀ t ⊆ {n | N ≤ n}, (∑' n : t, f n) ∈ e := by - refine cauchySeq_finset_iff_tsum_vanishing.trans ⟨fun vanish e he ↦ ?_, fun vanish e he ↦ ?_⟩ +@[to_additive] +theorem cauchySeq_finset_iff_nat_tprod_vanishing {f : ℕ → G} : + (CauchySeq fun s : Finset ℕ ↦ ∏ n in s, f n) ↔ + ∀ e ∈ 𝓝 (1 : G), ∃ N : ℕ, ∀ t ⊆ {n | N ≤ n}, (∏' n : t, f n) ∈ e := by + refine cauchySeq_finset_iff_tprod_vanishing.trans ⟨fun vanish e he ↦ ?_, fun vanish e he ↦ ?_⟩ · obtain ⟨s, hs⟩ := vanish e he - refine ⟨if h : s.Nonempty then s.max' h + 1 else 0, fun t ht ↦ hs _ <| Set.disjoint_left.mpr ?_⟩ + refine ⟨if h : s.Nonempty then s.max' h + 1 else 0, + fun t ht ↦ hs _ <| Set.disjoint_left.mpr ?_⟩ split_ifs at ht with h · exact fun m hmt hms ↦ (s.le_max' _ hms).not_lt (Nat.succ_le_iff.mp <| ht hmt) · exact fun _ _ hs ↦ h ⟨_, hs⟩ @@ -249,25 +278,29 @@ theorem cauchySeq_finset_iff_nat_tsum_vanishing {f : ℕ → G} : variable [CompleteSpace G] -theorem summable_iff_nat_tsum_vanishing {f : ℕ → G} : Summable f ↔ - ∀ e ∈ 𝓝 0, ∃ N : ℕ, ∀ t ⊆ {n | N ≤ n}, (∑' n : t, f n) ∈ e := by - rw [summable_iff_cauchySeq_finset, cauchySeq_finset_iff_nat_tsum_vanishing] +@[to_additive] +theorem multipliable_iff_nat_tprod_vanishing {f : ℕ → G} : Multipliable f ↔ + ∀ e ∈ 𝓝 1, ∃ N : ℕ, ∀ t ⊆ {n | N ≤ n}, (∏' n : t, f n) ∈ e := by + rw [multipliable_iff_cauchySeq_finset, cauchySeq_finset_iff_nat_tprod_vanishing] end UniformGroup section TopologicalGroup -variable [TopologicalSpace G] [TopologicalAddGroup G] +variable [TopologicalSpace G] [TopologicalGroup G] -theorem Summable.nat_tsum_vanishing {f : ℕ → G} (hf : Summable f) ⦃e : Set G⦄ (he : e ∈ 𝓝 0) : - ∃ N : ℕ, ∀ t ⊆ {n | N ≤ n}, (∑' n : t, f n) ∈ e := - letI : UniformSpace G := TopologicalAddGroup.toUniformSpace G - have : UniformAddGroup G := comm_topologicalAddGroup_is_uniform - cauchySeq_finset_iff_nat_tsum_vanishing.1 hf.hasSum.cauchySeq e he +@[to_additive] +theorem Multipliable.nat_tprod_vanishing {f : ℕ → G} (hf : Multipliable f) ⦃e : Set G⦄ + (he : e ∈ 𝓝 1) : ∃ N : ℕ, ∀ t ⊆ {n | N ≤ n}, (∏' n : t, f n) ∈ e := + letI : UniformSpace G := TopologicalGroup.toUniformSpace G + have : UniformGroup G := comm_topologicalGroup_is_uniform + cauchySeq_finset_iff_nat_tprod_vanishing.1 hf.hasProd.cauchySeq e he -theorem Summable.tendsto_atTop_zero {f : ℕ → G} (hf : Summable f) : Tendsto f atTop (𝓝 0) := by +@[to_additive] +theorem Multipliable.tendsto_atTop_one {f : ℕ → G} (hf : Multipliable f) : + Tendsto f atTop (𝓝 1) := by rw [← Nat.cofinite_eq_atTop] - exact hf.tendsto_cofinite_zero + exact hf.tendsto_cofinite_one #align summable.tendsto_at_top_zero Summable.tendsto_atTop_zero end TopologicalGroup @@ -284,37 +317,41 @@ section Int section Monoid -lemma HasSum.nat_add_neg_add_one {f : ℤ → M} (hf : HasSum f m) : - HasSum (fun n : ℕ ↦ f n + f (-(n + 1))) m := by - change HasSum (fun n : ℕ ↦ f n + f (Int.negSucc n)) m +@[to_additive HasSum.nat_add_neg_add_one] +lemma HasProd.nat_mul_neg_add_one {f : ℤ → M} (hf : HasProd f m) : + HasProd (fun n : ℕ ↦ f n * f (-(n + 1))) m := by + change HasProd (fun n : ℕ ↦ f n * f (Int.negSucc n)) m have : Injective Int.negSucc := @Int.negSucc.inj - refine hf.hasSum_of_sum_eq fun u ↦ ?_ + refine hf.hasProd_of_prod_eq fun u ↦ ?_ refine ⟨u.preimage _ (Nat.cast_injective.injOn _) ∪ u.preimage _ (this.injOn _), fun v' hv' ↦ ⟨v'.image Nat.cast ∪ v'.image Int.negSucc, fun x hx ↦ ?_, ?_⟩⟩ · simp only [mem_union, mem_image] cases x · exact Or.inl ⟨_, hv' (by simpa using Or.inl hx), rfl⟩ · exact Or.inr ⟨_, hv' (by simpa using Or.inr hx), rfl⟩ - · rw [sum_union, sum_image (Nat.cast_injective.injOn _), sum_image (this.injOn _), - sum_add_distrib] + · rw [prod_union, prod_image (Nat.cast_injective.injOn _), prod_image (this.injOn _), + prod_mul_distrib] simp only [disjoint_iff_ne, mem_image, ne_eq, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂, not_false_eq_true, implies_true, forall_const] -lemma Summable.nat_add_neg_add_one {f : ℤ → M} (hf : Summable f) : - Summable (fun n : ℕ ↦ f n + f (-(n + 1))) := - hf.hasSum.nat_add_neg_add_one.summable +@[to_additive Summable.nat_add_neg_add_one] +lemma Multipliable.nat_mul_neg_add_one {f : ℤ → M} (hf : Multipliable f) : + Multipliable (fun n : ℕ ↦ f n * f (-(n + 1))) := + hf.hasProd.nat_mul_neg_add_one.multipliable -lemma tsum_nat_add_neg_add_one [T2Space M] {f : ℤ → M} (hf : Summable f) : - ∑' (n : ℕ), (f n + f (-(n + 1))) = ∑' (n : ℤ), f n := - hf.hasSum.nat_add_neg_add_one.tsum_eq +@[to_additive tsum_nat_add_neg_add_one] +lemma tprod_nat_mul_neg_add_one [T2Space M] {f : ℤ → M} (hf : Multipliable f) : + ∏' (n : ℕ), (f n * f (-(n + 1))) = ∏' (n : ℤ), f n := + hf.hasProd.nat_mul_neg_add_one.tprod_eq -section ContinuousAdd +section ContinuousMul -variable [ContinuousAdd M] +variable [ContinuousMul M] -lemma HasSum.of_nat_of_neg_add_one {f : ℤ → M} - (hf₁ : HasSum (fun n : ℕ ↦ f n) m) (hf₂ : HasSum (fun n : ℕ ↦ f (-(n + 1))) m') : - HasSum f (m + m') := by +@[to_additive HasSum.of_nat_of_neg_add_one] +lemma HasProd.of_nat_of_neg_add_one {f : ℤ → M} + (hf₁ : HasProd (fun n : ℕ ↦ f n) m) (hf₂ : HasProd (fun n : ℕ ↦ f (-(n + 1))) m') : + HasProd f (m * m') := by have hi₁ : Injective ((↑) : ℕ → ℤ) := @Int.ofNat.inj have hi₂ : Injective Int.negSucc := @Int.negSucc.inj have : IsCompl (Set.range ((↑) : ℕ → ℤ)) (Set.range Int.negSucc) := by @@ -323,46 +360,59 @@ lemma HasSum.of_nat_of_neg_add_one {f : ℤ → M} rintro _ ⟨⟨i, rfl⟩, ⟨j, ⟨⟩⟩⟩ · rw [codisjoint_iff_le_sup] rintro (i | j) <;> simp - exact (hi₁.hasSum_range_iff.mpr hf₁).add_isCompl this (hi₂.hasSum_range_iff.mpr hf₂) + exact (hi₁.hasProd_range_iff.mpr hf₁).mul_isCompl this (hi₂.hasProd_range_iff.mpr hf₂) #align has_sum.nonneg_add_neg HasSum.of_nat_of_neg_add_one -- deprecated 2024-03-04 @[deprecated] alias HasSum.nonneg_add_neg := HasSum.of_nat_of_neg_add_one -lemma Summable.of_nat_of_neg_add_one {f : ℤ → M} - (hf₁ : Summable fun n : ℕ ↦ f n) (hf₂ : Summable fun n : ℕ ↦ f (-(n + 1))) : - Summable f := - (hf₁.hasSum.of_nat_of_neg_add_one hf₂.hasSum).summable - -lemma tsum_of_nat_of_neg_add_one [T2Space M] {f : ℤ → M} - (hf₁ : Summable fun n : ℕ ↦ f n) (hf₂ : Summable fun n : ℕ ↦ f (-(n + 1))) : - ∑' n : ℤ, f n = ∑' n : ℕ, f n + ∑' n : ℕ, f (-(n + 1)) := - (hf₁.hasSum.of_nat_of_neg_add_one hf₂.hasSum).tsum_eq - -/-- If `f₀, f₁, f₂, ...` and `g₀, g₁, g₂, ...` have sums `a`, `b` respectively, then the `ℤ`-indexed -sequence: `..., g₂, g₁, g₀, f₀, f₁, f₂, ...` (with `f₀` at the `0`-th position) has sum `a + b`. -/ -lemma HasSum.int_rec {f g : ℕ → M} (hf : HasSum f m) (hg : HasSum g m') : - HasSum (Int.rec f g) (m + m') := - HasSum.of_nat_of_neg_add_one hf hg +@[to_additive Summable.of_nat_of_neg_add_one] +lemma Multipliable.of_nat_of_neg_add_one {f : ℤ → M} + (hf₁ : Multipliable fun n : ℕ ↦ f n) (hf₂ : Multipliable fun n : ℕ ↦ f (-(n + 1))) : + Multipliable f := + (hf₁.hasProd.of_nat_of_neg_add_one hf₂.hasProd).multipliable + +@[to_additive tsum_of_nat_of_neg_add_one] +lemma tprod_of_nat_of_neg_add_one [T2Space M] {f : ℤ → M} + (hf₁ : Multipliable fun n : ℕ ↦ f n) (hf₂ : Multipliable fun n : ℕ ↦ f (-(n + 1))) : + ∏' n : ℤ, f n = (∏' n : ℕ, f n) * ∏' n : ℕ, f (-(n + 1)) := + (hf₁.hasProd.of_nat_of_neg_add_one hf₂.hasProd).tprod_eq + +/-- If `f₀, f₁, f₂, ...` and `g₀, g₁, g₂, ...` have products `a`, `b` respectively, then +the `ℤ`-indexed sequence: `..., g₂, g₁, g₀, f₀, f₁, f₂, ...` (with `f₀` at the `0`-th position) has +product `a + b`. -/ +@[to_additive "If `f₀, f₁, f₂, ...` and `g₀, g₁, g₂, ...` have sums `a`, `b` respectively, then +the `ℤ`-indexed sequence: `..., g₂, g₁, g₀, f₀, f₁, f₂, ...` (with `f₀` at the `0`-th position) has +sum `a + b`."] +lemma HasProd.int_rec {f g : ℕ → M} (hf : HasProd f m) (hg : HasProd g m') : + HasProd (Int.rec f g) (m * m') := + HasProd.of_nat_of_neg_add_one hf hg #align has_sum.int_rec HasSum.int_rec -/-- If `f₀, f₁, f₂, ...` and `g₀, g₁, g₂, ...` are both summable then so is the `ℤ`-indexed -sequence: `..., g₂, g₁, g₀, f₀, f₁, f₂, ...` (with `f₀` at the `0`-th position). -/ -lemma Summable.int_rec {f g : ℕ → M} (hf : Summable f) (hg : Summable g) : Summable (Int.rec f g) := +/-- If `f₀, f₁, f₂, ...` and `g₀, g₁, g₂, ...` are both multipliable then so is the +`ℤ`-indexed sequence: `..., g₂, g₁, g₀, f₀, f₁, f₂, ...` (with `f₀` at the `0`-th position). -/ +@[to_additive "If `f₀, f₁, f₂, ...` and `g₀, g₁, g₂, ...` are both summable then so is the +`ℤ`-indexed sequence: `..., g₂, g₁, g₀, f₀, f₁, f₂, ...` (with `f₀` at the `0`-th position)."] +lemma Multipliable.int_rec {f g : ℕ → M} (hf : Multipliable f) (hg : Multipliable g) : + Multipliable (Int.rec f g) := .of_nat_of_neg_add_one hf hg -/-- If `f₀, f₁, f₂, ...` and `g₀, g₁, g₂, ...` are both summable, then the sum of the `ℤ`-indexed -sequence: `..., g₂, g₁, g₀, f₀, f₁, f₂, ...` (with `f₀` at the `0`-th position) is -`∑' n, f n + ∑' n, g n`. -/ -lemma tsum_int_rec [T2Space M] {f g : ℕ → M} (hf : Summable f) (hg : Summable g) : - ∑' n : ℤ, Int.rec f g n = ∑' n : ℕ, f n + ∑' n : ℕ, g n := - (hf.hasSum.int_rec hg.hasSum).tsum_eq - -theorem HasSum.nat_add_neg {f : ℤ → M} (hf : HasSum f m) : - HasSum (fun n : ℕ ↦ f n + f (-n)) (m + f 0) := by +/-- If `f₀, f₁, f₂, ...` and `g₀, g₁, g₂, ...` are both multipliable, then the product of the +`ℤ`-indexed sequence: `..., g₂, g₁, g₀, f₀, f₁, f₂, ...` (with `f₀` at the `0`-th position) is +`(∏' n, f n) * ∏' n, g n`. -/ +@[to_additive "If `f₀, f₁, f₂, ...` and `g₀, g₁, g₂, ...` are both summable, then the sum of the +`ℤ`-indexed sequence: `..., g₂, g₁, g₀, f₀, f₁, f₂, ...` (with `f₀` at the `0`-th position) is +`∑' n, f n + ∑' n, g n`."] +lemma tprod_int_rec [T2Space M] {f g : ℕ → M} (hf : Multipliable f) (hg : Multipliable g) : + ∏' n : ℤ, Int.rec f g n = (∏' n : ℕ, f n) * ∏' n : ℕ, g n := + (hf.hasProd.int_rec hg.hasProd).tprod_eq + +@[to_additive] +theorem HasProd.nat_mul_neg {f : ℤ → M} (hf : HasProd f m) : + HasProd (fun n : ℕ ↦ f n * f (-n)) (m * f 0) := by -- Note this is much easier to prove if you assume more about the target space, but we have to -- work hard to prove it under the very minimal assumptions here. - apply (hf.add (hasSum_ite_eq (0 : ℤ) (f 0))).hasSum_of_sum_eq fun u ↦ ?_ + apply (hf.mul (hasProd_ite_eq (0 : ℤ) (f 0))).hasProd_of_prod_eq fun u ↦ ?_ refine ⟨u.image Int.natAbs, fun v' hv' ↦ ?_⟩ let u1 := v'.image fun x : ℕ ↦ (x : ℤ) let u2 := v'.image fun x : ℕ ↦ -(x : ℤ) @@ -375,11 +425,11 @@ theorem HasSum.nat_add_neg {f : ℤ → M} (hf : HasSum f m) : · refine Or.inr ⟨_, hv' <| mem_image.mpr ⟨x, hx, rfl⟩, ?_⟩ simp only [abs_of_nonpos h'x, Int.coe_natAbs, neg_neg] exact ⟨_, A, calc - (∑ x in u1 ∪ u2, (f x + if x = 0 then f 0 else 0)) = - (∑ x in u1 ∪ u2, f x) + ∑ x in u1 ∩ u2, f x := by - rw [sum_add_distrib] + (∏ x in u1 ∪ u2, (f x * if x = 0 then f 0 else 1)) = + (∏ x in u1 ∪ u2, f x) * ∏ x in u1 ∩ u2, f x := by + rw [prod_mul_distrib] congr 1 - refine (sum_subset_zero_on_sdiff inter_subset_union ?_ ?_).symm + refine (prod_subset_one_on_sdiff inter_subset_union ?_ ?_).symm · intro x hx suffices x ≠ 0 by simp only [this, if_false] rintro rfl @@ -393,88 +443,98 @@ theorem HasSum.nat_add_neg {f : ℤ → M} (hf : HasSum f m) : simp only [Right.neg_nonpos_iff, Nat.cast_nonneg] · rcases hx.1 with ⟨a, _, rfl⟩ simp only [Nat.cast_nonneg] - _ = (∑ x in u1, f x) + ∑ x in u2, f x := sum_union_inter - _ = (∑ b in v', f b) + ∑ b in v', f (-b) := by - simp only [u1, u2, Nat.cast_inj, imp_self, implies_true, forall_const, sum_image, neg_inj] - _ = ∑ b in v', (f b + f (-b)) := sum_add_distrib.symm⟩ + _ = (∏ x in u1, f x) * ∏ x in u2, f x := prod_union_inter + _ = (∏ b in v', f b) * ∏ b in v', f (-b) := by + simp only [u1, u2, Nat.cast_inj, imp_self, implies_true, forall_const, prod_image, neg_inj] + _ = ∏ b in v', (f b * f (-b)) := prod_mul_distrib.symm⟩ #align has_sum.sum_nat_of_sum_int HasSum.nat_add_neg -- deprecated 2024-03-04 @[deprecated HasSum.nat_add_neg] alias HasSum.sum_nat_of_sum_int := HasSum.nat_add_neg -theorem Summable.nat_add_neg {f : ℤ → M} (hf : Summable f) : - Summable fun n : ℕ ↦ f n + f (-n) := - hf.hasSum.nat_add_neg.summable - -lemma tsum_nat_add_neg [T2Space M] {f : ℤ → M} (hf : Summable f) : - ∑' n : ℕ, (f n + f (-n)) = (∑' n : ℤ, f n) + f 0 := - hf.hasSum.nat_add_neg.tsum_eq - -theorem HasSum.of_add_one_of_neg_add_one {f : ℤ → M} - (hf₁ : HasSum (fun n : ℕ ↦ f (n + 1)) m) (hf₂ : HasSum (fun n : ℕ ↦ f (-(n + 1))) m') : - HasSum f (m + f 0 + m') := - HasSum.of_nat_of_neg_add_one (add_comm _ m ▸ HasSum.zero_add hf₁) hf₂ +@[to_additive] +theorem Multipliable.nat_mul_neg {f : ℤ → M} (hf : Multipliable f) : + Multipliable fun n : ℕ ↦ f n * f (-n) := + hf.hasProd.nat_mul_neg.multipliable + +@[to_additive] +lemma tprod_nat_mul_neg [T2Space M] {f : ℤ → M} (hf : Multipliable f) : + ∏' n : ℕ, (f n * f (-n)) = (∏' n : ℤ, f n) * f 0 := + hf.hasProd.nat_mul_neg.tprod_eq + +@[to_additive HasSum.of_add_one_of_neg_add_one] +theorem HasProd.of_add_one_of_neg_add_one {f : ℤ → M} + (hf₁ : HasProd (fun n : ℕ ↦ f (n + 1)) m) (hf₂ : HasProd (fun n : ℕ ↦ f (-(n + 1))) m') : + HasProd f (m * f 0 * m') := + HasProd.of_nat_of_neg_add_one (mul_comm _ m ▸ HasProd.zero_mul hf₁) hf₂ #align has_sum.pos_add_zero_add_neg HasSum.of_add_one_of_neg_add_one -- deprecated 2024-03-04 @[deprecated HasSum.of_add_one_of_neg_add_one] alias HasSum.pos_add_zero_add_neg := HasSum.of_add_one_of_neg_add_one -lemma Summable.of_add_one_of_neg_add_one {f : ℤ → M} - (hf₁ : Summable fun n : ℕ ↦ f (n + 1)) (hf₂ : Summable fun n : ℕ ↦ f (-(n + 1))) : - Summable f := - (hf₁.hasSum.of_add_one_of_neg_add_one hf₂.hasSum).summable +@[to_additive Summable.of_add_one_of_neg_add_one] +lemma Multipliable.of_add_one_of_neg_add_one {f : ℤ → M} + (hf₁ : Multipliable fun n : ℕ ↦ f (n + 1)) (hf₂ : Multipliable fun n : ℕ ↦ f (-(n + 1))) : + Multipliable f := + (hf₁.hasProd.of_add_one_of_neg_add_one hf₂.hasProd).multipliable -lemma tsum_of_add_one_of_neg_add_one [T2Space M] {f : ℤ → M} - (hf₁ : Summable fun n : ℕ ↦ f (n + 1)) (hf₂ : Summable fun n : ℕ ↦ f (-(n + 1))) : - ∑' n : ℤ, f n = ∑' n : ℕ, f (n + 1) + f 0 + ∑' n : ℕ, f (-(n + 1)) := - (hf₁.hasSum.of_add_one_of_neg_add_one hf₂.hasSum).tsum_eq +@[to_additive tsum_of_add_one_of_neg_add_one] +lemma tprod_of_add_one_of_neg_add_one [T2Space M] {f : ℤ → M} + (hf₁ : Multipliable fun n : ℕ ↦ f (n + 1)) (hf₂ : Multipliable fun n : ℕ ↦ f (-(n + 1))) : + ∏' n : ℤ, f n = (∏' n : ℕ, f (n + 1)) * f 0 * ∏' n : ℕ, f (-(n + 1)) := + (hf₁.hasProd.of_add_one_of_neg_add_one hf₂.hasProd).tprod_eq -end ContinuousAdd +end ContinuousMul end Monoid section TopologicalGroup -variable [TopologicalSpace G] [TopologicalAddGroup G] +variable [TopologicalSpace G] [TopologicalGroup G] -lemma HasSum.of_nat_of_neg {f : ℤ → G} (hf₁ : HasSum (fun n : ℕ ↦ f n) g) - (hf₂ : HasSum (fun n : ℕ ↦ f (-n)) g') : HasSum f (g + g' - f 0) := by - refine add_sub_assoc' g .. ▸ hf₁.nonneg_add_neg (m' := g' - f 0) ?_ - rwa [← hasSum_nat_add_iff' 1, sum_range_one, Nat.cast_zero, neg_zero] at hf₂ +@[to_additive] +lemma HasProd.of_nat_of_neg {f : ℤ → G} (hf₁ : HasProd (fun n : ℕ ↦ f n) g) + (hf₂ : HasProd (fun n : ℕ ↦ f (-n)) g') : HasProd f (g * g' / f 0) := by + refine mul_div_assoc' g .. ▸ hf₁.of_nat_of_neg_add_one (m' := g' / f 0) ?_ + rwa [← hasProd_nat_add_iff' 1, prod_range_one, Nat.cast_zero, neg_zero] at hf₂ -lemma Summable.of_nat_of_neg {f : ℤ → G} (hf₁ : Summable fun n : ℕ ↦ f n) - (hf₂ : Summable fun n : ℕ ↦ f (-n)) : Summable f := - (hf₁.hasSum.of_nat_of_neg hf₂.hasSum).summable +@[to_additive] +lemma Multipliable.of_nat_of_neg {f : ℤ → G} (hf₁ : Multipliable fun n : ℕ ↦ f n) + (hf₂ : Multipliable fun n : ℕ ↦ f (-n)) : Multipliable f := + (hf₁.hasProd.of_nat_of_neg hf₂.hasProd).multipliable #align summable_int_of_summable_nat Summable.of_nat_of_neg -- deprecated 2024-03-04 @[deprecated Summable.of_nat_of_neg] alias summable_int_of_summable_nat := Summable.of_nat_of_neg -lemma tsum_of_nat_of_neg [T2Space G] {f : ℤ → G} - (hf₁ : Summable fun n : ℕ ↦ f n) (hf₂ : Summable fun n : ℕ ↦ f (-n)) : - ∑' n : ℤ, f n = ∑' n : ℕ, f n + ∑' n : ℕ, f (-n) - f 0 := - (hf₁.hasSum.of_nat_of_neg hf₂.hasSum).tsum_eq +@[to_additive] +lemma tprod_of_nat_of_neg [T2Space G] {f : ℤ → G} + (hf₁ : Multipliable fun n : ℕ ↦ f n) (hf₂ : Multipliable fun n : ℕ ↦ f (-n)) : + ∏' n : ℤ, f n = (∏' n : ℕ, f n) * (∏' n : ℕ, f (-n)) / f 0 := + (hf₁.hasProd.of_nat_of_neg hf₂.hasProd).tprod_eq end TopologicalGroup section UniformGroup -- results which depend on completeness -variable [UniformSpace G] [UniformAddGroup G] [CompleteSpace G] +variable [UniformSpace G] [UniformGroup G] [CompleteSpace G] -/-- "iff" version of `Summable.of_nat_of_neg_add_one`. -/ -lemma summable_int_iff_summable_nat_and_neg_add_one {f : ℤ → G} : - Summable f ↔ (Summable fun n : ℕ ↦ f n) ∧ (Summable fun n : ℕ ↦ f (-(n + 1))) := by - refine ⟨fun p ↦ ⟨?_, ?_⟩, fun ⟨hf₁, hf₂⟩ ↦ Summable.of_nat_of_neg_add_one hf₁ hf₂⟩ <;> +/-- "iff" version of `Multipliable.of_nat_of_neg_add_one`. -/ +@[to_additive "\"iff\" version of `Summable.of_nat_of_neg_add_one`."] +lemma multipliable_int_iff_multipliable_nat_and_neg_add_one {f : ℤ → G} : Multipliable f ↔ + (Multipliable fun n : ℕ ↦ f n) ∧ (Multipliable fun n : ℕ ↦ f (-(n + 1))) := by + refine ⟨fun p ↦ ⟨?_, ?_⟩, fun ⟨hf₁, hf₂⟩ ↦ Multipliable.of_nat_of_neg_add_one hf₁ hf₂⟩ <;> apply p.comp_injective exacts [Nat.cast_injective, @Int.negSucc.inj] -/-- "iff" version of `Summable.of_natCast_neg_natCast`. -/ -lemma summable_int_iff_summable_nat_and_neg {f : ℤ → G} : - Summable f ↔ (Summable fun n : ℕ ↦ f n) ∧ (Summable fun n : ℕ ↦ f (-n)) := by - refine ⟨fun p ↦ ⟨?_, ?_⟩, fun ⟨hf₁, hf₂⟩ ↦ Summable.of_nat_of_neg hf₁ hf₂⟩ <;> +/-- "iff" version of `Multipliable.of_nat_of_neg`. -/ +@[to_additive "\"iff\" version of `Summable.of_nat_of_neg`."] +lemma multipliable_int_iff_multipliable_nat_and_neg {f : ℤ → G} : + Multipliable f ↔ (Multipliable fun n : ℕ ↦ f n) ∧ (Multipliable fun n : ℕ ↦ f (-n)) := by + refine ⟨fun p ↦ ⟨?_, ?_⟩, fun ⟨hf₁, hf₂⟩ ↦ Multipliable.of_nat_of_neg hf₁ hf₂⟩ <;> apply p.comp_injective exacts [Nat.cast_injective, neg_injective.comp Nat.cast_injective] diff --git a/Mathlib/Topology/Algebra/InfiniteSum/Order.lean b/Mathlib/Topology/Algebra/InfiniteSum/Order.lean index b9e6dc4eb25e9a..8b3bda3b3f9e6a 100644 --- a/Mathlib/Topology/Algebra/InfiniteSum/Order.lean +++ b/Mathlib/Topology/Algebra/InfiniteSum/Order.lean @@ -11,9 +11,9 @@ import Mathlib.Topology.Order.MonotoneConvergence #align_import topology.algebra.infinite_sum.order from "leanprover-community/mathlib"@"32253a1a1071173b33dc7d6a218cf722c6feb514" /-! -# Infinite sum in an order +# Infinite sum or product in an order -This file provides lemmas about the interaction of infinite sums and order operations. +This file provides lemmas about the interaction of infinite sums and products and order operations. -/ @@ -24,44 +24,49 @@ variable {ι κ α : Type*} section Preorder -variable [Preorder α] [AddCommMonoid α] [TopologicalSpace α] [OrderClosedTopology α] [T2Space α] +variable [Preorder α] [CommMonoid α] [TopologicalSpace α] [OrderClosedTopology α] [T2Space α] {f : ℕ → α} {c : α} -theorem tsum_le_of_sum_range_le (hf : Summable f) (h : ∀ n, ∑ i in range n, f i ≤ c) : - ∑' n, f n ≤ c := +@[to_additive] +theorem tprod_le_of_prod_range_le (hf : Multipliable f) (h : ∀ n, ∏ i in range n, f i ≤ c) : + ∏' n, f n ≤ c := let ⟨_l, hl⟩ := hf - hl.tsum_eq.symm ▸ le_of_tendsto' hl.tendsto_sum_nat h + hl.tprod_eq.symm ▸ le_of_tendsto' hl.tendsto_prod_nat h #align tsum_le_of_sum_range_le tsum_le_of_sum_range_le end Preorder -section OrderedAddCommMonoid +section OrderedCommMonoid -variable [OrderedAddCommMonoid α] [TopologicalSpace α] [OrderClosedTopology α] {f g : ι → α} +variable [OrderedCommMonoid α] [TopologicalSpace α] [OrderClosedTopology α] {f g : ι → α} {a a₁ a₂ : α} -theorem hasSum_le (h : ∀ i, f i ≤ g i) (hf : HasSum f a₁) (hg : HasSum g a₂) : a₁ ≤ a₂ := - le_of_tendsto_of_tendsto' hf hg fun _ ↦ sum_le_sum fun i _ ↦ h i +@[to_additive] +theorem hasProd_le (h : ∀ i, f i ≤ g i) (hf : HasProd f a₁) (hg : HasProd g a₂) : a₁ ≤ a₂ := + le_of_tendsto_of_tendsto' hf hg fun _ ↦ prod_le_prod' fun i _ ↦ h i #align has_sum_le hasSum_le -@[mono] -theorem hasSum_mono (hf : HasSum f a₁) (hg : HasSum g a₂) (h : f ≤ g) : a₁ ≤ a₂ := - hasSum_le h hf hg +@[to_additive (attr := mono)] +theorem hasProd_mono (hf : HasProd f a₁) (hg : HasProd g a₂) (h : f ≤ g) : a₁ ≤ a₂ := + hasProd_le h hf hg #align has_sum_mono hasSum_mono -theorem hasSum_le_of_sum_le (hf : HasSum f a) (h : ∀ s, ∑ i in s, f i ≤ a₂) : a ≤ a₂ := +@[to_additive] +theorem hasProd_le_of_prod_le (hf : HasProd f a) (h : ∀ s, ∏ i in s, f i ≤ a₂) : a ≤ a₂ := le_of_tendsto' hf h #align has_sum_le_of_sum_le hasSum_le_of_sum_le -theorem le_hasSum_of_le_sum (hf : HasSum f a) (h : ∀ s, a₂ ≤ ∑ i in s, f i) : a₂ ≤ a := +@[to_additive] +theorem le_hasProd_of_le_prod (hf : HasProd f a) (h : ∀ s, a₂ ≤ ∏ i in s, f i) : a₂ ≤ a := ge_of_tendsto' hf h #align le_has_sum_of_le_sum le_hasSum_of_le_sum -theorem hasSum_le_inj {g : κ → α} (e : ι → κ) (he : Injective e) - (hs : ∀ c, c ∉ Set.range e → 0 ≤ g c) (h : ∀ i, f i ≤ g (e i)) (hf : HasSum f a₁) - (hg : HasSum g a₂) : a₁ ≤ a₂ := by - rw [← hasSum_extend_zero he] at hf - refine hasSum_le (fun c ↦ ?_) hf hg +@[to_additive] +theorem hasProd_le_inj {g : κ → α} (e : ι → κ) (he : Injective e) + (hs : ∀ c, c ∉ Set.range e → 1 ≤ g c) (h : ∀ i, f i ≤ g (e i)) (hf : HasProd f a₁) + (hg : HasProd g a₂) : a₁ ≤ a₂ := by + rw [← hasProd_extend_one he] at hf + refine hasProd_le (fun c ↦ ?_) hf hg obtain ⟨i, rfl⟩ | h := em (c ∈ Set.range e) · rw [he.extend_apply] exact h _ @@ -69,157 +74,182 @@ theorem hasSum_le_inj {g : κ → α} (e : ι → κ) (he : Injective e) exact hs _ h #align has_sum_le_inj hasSum_le_inj -theorem tsum_le_tsum_of_inj {g : κ → α} (e : ι → κ) (he : Injective e) - (hs : ∀ c, c ∉ Set.range e → 0 ≤ g c) (h : ∀ i, f i ≤ g (e i)) (hf : Summable f) - (hg : Summable g) : tsum f ≤ tsum g := - hasSum_le_inj _ he hs h hf.hasSum hg.hasSum +@[to_additive] +theorem tprod_le_tprod_of_inj {g : κ → α} (e : ι → κ) (he : Injective e) + (hs : ∀ c, c ∉ Set.range e → 1 ≤ g c) (h : ∀ i, f i ≤ g (e i)) (hf : Multipliable f) + (hg : Multipliable g) : tprod f ≤ tprod g := + hasProd_le_inj _ he hs h hf.hasProd hg.hasProd #align tsum_le_tsum_of_inj tsum_le_tsum_of_inj -theorem sum_le_hasSum (s : Finset ι) (hs : ∀ i, i ∉ s → 0 ≤ f i) (hf : HasSum f a) : - ∑ i in s, f i ≤ a := +@[to_additive] +theorem prod_le_hasProd (s : Finset ι) (hs : ∀ i, i ∉ s → 1 ≤ f i) (hf : HasProd f a) : + ∏ i in s, f i ≤ a := ge_of_tendsto hf (eventually_atTop.2 - ⟨s, fun _t hst ↦ sum_le_sum_of_subset_of_nonneg hst fun i _ hbs ↦ hs i hbs⟩) + ⟨s, fun _t hst ↦ prod_le_prod_of_subset_of_one_le' hst fun i _ hbs ↦ hs i hbs⟩) #align sum_le_has_sum sum_le_hasSum -theorem isLUB_hasSum (h : ∀ i, 0 ≤ f i) (hf : HasSum f a) : - IsLUB (Set.range fun s ↦ ∑ i in s, f i) a := - isLUB_of_tendsto_atTop (Finset.sum_mono_set_of_nonneg h) hf +@[to_additive] +theorem isLUB_hasProd (h : ∀ i, 1 ≤ f i) (hf : HasProd f a) : + IsLUB (Set.range fun s ↦ ∏ i in s, f i) a := + isLUB_of_tendsto_atTop (Finset.prod_mono_set_of_one_le' h) hf #align is_lub_has_sum isLUB_hasSum -theorem le_hasSum (hf : HasSum f a) (i : ι) (hb : ∀ j, j ≠ i → 0 ≤ f j) : f i ≤ a := +@[to_additive] +theorem le_hasProd (hf : HasProd f a) (i : ι) (hb : ∀ j, j ≠ i → 1 ≤ f j) : f i ≤ a := calc - f i = ∑ i in {i}, f i := by rw [sum_singleton] - _ ≤ a := sum_le_hasSum _ (by simpa) hf + f i = ∏ i in {i}, f i := by rw [prod_singleton] + _ ≤ a := prod_le_hasProd _ (by simpa) hf #align le_has_sum le_hasSum -theorem sum_le_tsum {f : ι → α} (s : Finset ι) (hs : ∀ i, i ∉ s → 0 ≤ f i) (hf : Summable f) : - ∑ i in s, f i ≤ ∑' i, f i := - sum_le_hasSum s hs hf.hasSum +@[to_additive] +theorem prod_le_tprod {f : ι → α} (s : Finset ι) (hs : ∀ i, i ∉ s → 1 ≤ f i) (hf : Multipliable f) : + ∏ i in s, f i ≤ ∏' i, f i := + prod_le_hasProd s hs hf.hasProd #align sum_le_tsum sum_le_tsum -theorem le_tsum (hf : Summable f) (i : ι) (hb : ∀ j, j ≠ i → 0 ≤ f j) : f i ≤ ∑' i, f i := - le_hasSum hf.hasSum i hb +@[to_additive] +theorem le_tprod (hf : Multipliable f) (i : ι) (hb : ∀ j, j ≠ i → 1 ≤ f j) : f i ≤ ∏' i, f i := + le_hasProd hf.hasProd i hb #align le_tsum le_tsum -theorem tsum_le_tsum (h : ∀ i, f i ≤ g i) (hf : Summable f) (hg : Summable g) : - ∑' i, f i ≤ ∑' i, g i := - hasSum_le h hf.hasSum hg.hasSum +@[to_additive] +theorem tprod_le_tprod (h : ∀ i, f i ≤ g i) (hf : Multipliable f) (hg : Multipliable g) : + ∏' i, f i ≤ ∏' i, g i := + hasProd_le h hf.hasProd hg.hasProd #align tsum_le_tsum tsum_le_tsum -@[mono] -theorem tsum_mono (hf : Summable f) (hg : Summable g) (h : f ≤ g) : ∑' n, f n ≤ ∑' n, g n := - tsum_le_tsum h hf hg +@[to_additive (attr := mono)] +theorem tprod_mono (hf : Multipliable f) (hg : Multipliable g) (h : f ≤ g) : + ∏' n, f n ≤ ∏' n, g n := + tprod_le_tprod h hf hg #align tsum_mono tsum_mono -theorem tsum_le_of_sum_le (hf : Summable f) (h : ∀ s, ∑ i in s, f i ≤ a₂) : ∑' i, f i ≤ a₂ := - hasSum_le_of_sum_le hf.hasSum h +@[to_additive] +theorem tprod_le_of_prod_le (hf : Multipliable f) (h : ∀ s, ∏ i in s, f i ≤ a₂) : ∏' i, f i ≤ a₂ := + hasProd_le_of_prod_le hf.hasProd h #align tsum_le_of_sum_le tsum_le_of_sum_le -theorem tsum_le_of_sum_le' (ha₂ : 0 ≤ a₂) (h : ∀ s, ∑ i in s, f i ≤ a₂) : ∑' i, f i ≤ a₂ := by - by_cases hf : Summable f - · exact tsum_le_of_sum_le hf h - · rw [tsum_eq_zero_of_not_summable hf] +@[to_additive] +theorem tprod_le_of_prod_le' (ha₂ : 1 ≤ a₂) (h : ∀ s, ∏ i in s, f i ≤ a₂) : ∏' i, f i ≤ a₂ := by + by_cases hf : Multipliable f + · exact tprod_le_of_prod_le hf h + · rw [tprod_eq_one_of_not_multipliable hf] exact ha₂ #align tsum_le_of_sum_le' tsum_le_of_sum_le' -theorem HasSum.nonneg (h : ∀ i, 0 ≤ g i) (ha : HasSum g a) : 0 ≤ a := - hasSum_le h hasSum_zero ha +@[to_additive] +theorem HasProd.one_le (h : ∀ i, 1 ≤ g i) (ha : HasProd g a) : 1 ≤ a := + hasProd_le h hasProd_one ha #align has_sum.nonneg HasSum.nonneg -theorem HasSum.nonpos (h : ∀ i, g i ≤ 0) (ha : HasSum g a) : a ≤ 0 := - hasSum_le h ha hasSum_zero +@[to_additive] +theorem HasProd.le_one (h : ∀ i, g i ≤ 1) (ha : HasProd g a) : a ≤ 1 := + hasProd_le h ha hasProd_one #align has_sum.nonpos HasSum.nonpos -theorem tsum_nonneg (h : ∀ i, 0 ≤ g i) : 0 ≤ ∑' i, g i := by - by_cases hg : Summable g - · exact hg.hasSum.nonneg h - · rw [tsum_eq_zero_of_not_summable hg] +@[to_additive tsum_nonneg] +theorem one_le_tprod (h : ∀ i, 1 ≤ g i) : 1 ≤ ∏' i, g i := by + by_cases hg : Multipliable g + · exact hg.hasProd.one_le h + · rw [tprod_eq_one_of_not_multipliable hg] #align tsum_nonneg tsum_nonneg -theorem tsum_nonpos (h : ∀ i, f i ≤ 0) : ∑' i, f i ≤ 0 := by - by_cases hf : Summable f - · exact hf.hasSum.nonpos h - · rw [tsum_eq_zero_of_not_summable hf] +@[to_additive] +theorem tprod_le_one (h : ∀ i, f i ≤ 1) : ∏' i, f i ≤ 1 := by + by_cases hf : Multipliable f + · exact hf.hasProd.le_one h + · rw [tprod_eq_one_of_not_multipliable hf] #align tsum_nonpos tsum_nonpos -- Porting note: generalized from `OrderedAddCommGroup` to `OrderedAddCommMonoid` -theorem hasSum_zero_iff_of_nonneg (hf : ∀ i, 0 ≤ f i) : HasSum f 0 ↔ f = 0 := by +@[to_additive] +theorem hasProd_one_iff_of_one_le (hf : ∀ i, 1 ≤ f i) : HasProd f 1 ↔ f = 1 := by refine' ⟨fun hf' ↦ _, _⟩ · ext i - exact (hf i).antisymm' (le_hasSum hf' _ fun j _ ↦ hf j) + exact (hf i).antisymm' (le_hasProd hf' _ fun j _ ↦ hf j) · rintro rfl - exact hasSum_zero + exact hasProd_one #align has_sum_zero_iff_of_nonneg hasSum_zero_iff_of_nonneg -end OrderedAddCommMonoid +end OrderedCommMonoid -section OrderedAddCommGroup +section OrderedCommGroup -variable [OrderedAddCommGroup α] [TopologicalSpace α] [TopologicalAddGroup α] +variable [OrderedCommGroup α] [TopologicalSpace α] [TopologicalGroup α] [OrderClosedTopology α] {f g : ι → α} {a₁ a₂ : α} {i : ι} -theorem hasSum_lt (h : f ≤ g) (hi : f i < g i) (hf : HasSum f a₁) (hg : HasSum g a₂) : a₁ < a₂ := by - have : update f i 0 ≤ update g i 0 := update_le_update_iff.mpr ⟨rfl.le, fun i _ ↦ h i⟩ - have : 0 - f i + a₁ ≤ 0 - g i + a₂ := hasSum_le this (hf.update i 0) (hg.update i 0) - simpa only [zero_sub, add_neg_cancel_left] using add_lt_add_of_lt_of_le hi this +@[to_additive] +theorem hasProd_lt (h : f ≤ g) (hi : f i < g i) (hf : HasProd f a₁) (hg : HasProd g a₂) : + a₁ < a₂ := by + have : update f i 1 ≤ update g i 1 := update_le_update_iff.mpr ⟨rfl.le, fun i _ ↦ h i⟩ + have : 1 / f i * a₁ ≤ 1 / g i * a₂ := hasProd_le this (hf.update i 1) (hg.update i 1) + simpa only [one_div, mul_inv_cancel_left] using mul_lt_mul_of_lt_of_le hi this #align has_sum_lt hasSum_lt -@[mono] -theorem hasSum_strict_mono (hf : HasSum f a₁) (hg : HasSum g a₂) (h : f < g) : a₁ < a₂ := +@[to_additive (attr := mono)] +theorem hasProd_strict_mono (hf : HasProd f a₁) (hg : HasProd g a₂) (h : f < g) : a₁ < a₂ := let ⟨hle, _i, hi⟩ := Pi.lt_def.mp h - hasSum_lt hle hi hf hg + hasProd_lt hle hi hf hg #align has_sum_strict_mono hasSum_strict_mono -theorem tsum_lt_tsum (h : f ≤ g) (hi : f i < g i) (hf : Summable f) (hg : Summable g) : - ∑' n, f n < ∑' n, g n := - hasSum_lt h hi hf.hasSum hg.hasSum +@[to_additive] +theorem tprod_lt_tprod (h : f ≤ g) (hi : f i < g i) (hf : Multipliable f) (hg : Multipliable g) : + ∏' n, f n < ∏' n, g n := + hasProd_lt h hi hf.hasProd hg.hasProd #align tsum_lt_tsum tsum_lt_tsum -@[mono] -theorem tsum_strict_mono (hf : Summable f) (hg : Summable g) (h : f < g) : - ∑' n, f n < ∑' n, g n := +@[to_additive (attr := mono)] +theorem tprod_strict_mono (hf : Multipliable f) (hg : Multipliable g) (h : f < g) : + ∏' n, f n < ∏' n, g n := let ⟨hle, _i, hi⟩ := Pi.lt_def.mp h - tsum_lt_tsum hle hi hf hg + tprod_lt_tprod hle hi hf hg #align tsum_strict_mono tsum_strict_mono -theorem tsum_pos (hsum : Summable g) (hg : ∀ i, 0 ≤ g i) (i : ι) (hi : 0 < g i) : - 0 < ∑' i, g i := by - rw [← tsum_zero] - exact tsum_lt_tsum hg hi summable_zero hsum +@[to_additive tsum_pos] +theorem one_lt_tprod (hsum : Multipliable g) (hg : ∀ i, 1 ≤ g i) (i : ι) (hi : 1 < g i) : + 1 < ∏' i, g i := by + rw [← tprod_one] + exact tprod_lt_tprod hg hi multipliable_one hsum #align tsum_pos tsum_pos -end OrderedAddCommGroup +end OrderedCommGroup -section CanonicallyOrderedAddCommMonoid +section CanonicallyOrderedCommMonoid -variable [CanonicallyOrderedAddCommMonoid α] [TopologicalSpace α] [OrderClosedTopology α] +variable [CanonicallyOrderedCommMonoid α] [TopologicalSpace α] [OrderClosedTopology α] {f : ι → α} {a : α} -theorem le_hasSum' (hf : HasSum f a) (i : ι) : f i ≤ a := - le_hasSum hf i fun _ _ ↦ zero_le _ +@[to_additive] +theorem le_hasProd' (hf : HasProd f a) (i : ι) : f i ≤ a := + le_hasProd hf i fun _ _ ↦ one_le _ #align le_has_sum' le_hasSum' -theorem le_tsum' (hf : Summable f) (i : ι) : f i ≤ ∑' i, f i := - le_tsum hf i fun _ _ ↦ zero_le _ +@[to_additive] +theorem le_tprod' (hf : Multipliable f) (i : ι) : f i ≤ ∏' i, f i := + le_tprod hf i fun _ _ ↦ one_le _ #align le_tsum' le_tsum' -theorem hasSum_zero_iff : HasSum f 0 ↔ ∀ x, f x = 0 := - (hasSum_zero_iff_of_nonneg fun _ ↦ zero_le _).trans funext_iff +@[to_additive] +theorem hasProd_one_iff : HasProd f 1 ↔ ∀ x, f x = 1 := + (hasProd_one_iff_of_one_le fun _ ↦ one_le _).trans funext_iff #align has_sum_zero_iff hasSum_zero_iff -theorem tsum_eq_zero_iff (hf : Summable f) : ∑' i, f i = 0 ↔ ∀ x, f x = 0 := by - rw [← hasSum_zero_iff, hf.hasSum_iff] +@[to_additive] +theorem tprod_eq_one_iff (hf : Multipliable f) : ∏' i, f i = 1 ↔ ∀ x, f x = 1 := by + rw [← hasProd_one_iff, hf.hasProd_iff] #align tsum_eq_zero_iff tsum_eq_zero_iff -theorem tsum_ne_zero_iff (hf : Summable f) : ∑' i, f i ≠ 0 ↔ ∃ x, f x ≠ 0 := by - rw [Ne.def, tsum_eq_zero_iff hf, not_forall] +@[to_additive] +theorem tprod_ne_one_iff (hf : Multipliable f) : ∏' i, f i ≠ 1 ↔ ∃ x, f x ≠ 1 := by + rw [Ne.def, tprod_eq_one_iff hf, not_forall] #align tsum_ne_zero_iff tsum_ne_zero_iff -theorem isLUB_hasSum' (hf : HasSum f a) : IsLUB (Set.range fun s ↦ ∑ i in s, f i) a := - isLUB_of_tendsto_atTop (Finset.sum_mono_set f) hf +@[to_additive] +theorem isLUB_hasProd' (hf : HasProd f a) : IsLUB (Set.range fun s ↦ ∏ i in s, f i) a := + isLUB_of_tendsto_atTop (Finset.prod_mono_set' f) hf #align is_lub_has_sum' isLUB_hasSum' -end CanonicallyOrderedAddCommMonoid +end CanonicallyOrderedCommMonoid section LinearOrder @@ -232,28 +262,31 @@ conditionally complete linear order, such as `ℝ`, `ℝ≥0`, `ℝ≥0∞`, bec the existence of a least upper bound. -/ -theorem hasSum_of_isLUB_of_nonneg [LinearOrderedAddCommMonoid α] [TopologicalSpace α] - [OrderTopology α] {f : ι → α} (i : α) (h : ∀ i, 0 ≤ f i) - (hf : IsLUB (Set.range fun s ↦ ∑ i in s, f i) i) : HasSum f i := - tendsto_atTop_isLUB (Finset.sum_mono_set_of_nonneg h) hf +@[to_additive] +theorem hasProd_of_isLUB_of_one_le [LinearOrderedCommMonoid α] [TopologicalSpace α] + [OrderTopology α] {f : ι → α} (i : α) (h : ∀ i, 1 ≤ f i) + (hf : IsLUB (Set.range fun s ↦ ∏ i in s, f i) i) : HasProd f i := + tendsto_atTop_isLUB (Finset.prod_mono_set_of_one_le' h) hf #align has_sum_of_is_lub_of_nonneg hasSum_of_isLUB_of_nonneg -theorem hasSum_of_isLUB [CanonicallyLinearOrderedAddCommMonoid α] [TopologicalSpace α] - [OrderTopology α] {f : ι → α} (b : α) (hf : IsLUB (Set.range fun s ↦ ∑ i in s, f i) b) : - HasSum f b := - tendsto_atTop_isLUB (Finset.sum_mono_set f) hf +@[to_additive] +theorem hasProd_of_isLUB [CanonicallyLinearOrderedCommMonoid α] [TopologicalSpace α] + [OrderTopology α] {f : ι → α} (b : α) (hf : IsLUB (Set.range fun s ↦ ∏ i in s, f i) b) : + HasProd f b := + tendsto_atTop_isLUB (Finset.prod_mono_set' f) hf #align has_sum_of_is_lub hasSum_of_isLUB -theorem summable_abs_iff [LinearOrderedAddCommGroup α] [UniformSpace α] [UniformAddGroup α] - [CompleteSpace α] {f : ι → α} : (Summable fun x ↦ |f x|) ↔ Summable f := - let s := { x | 0 ≤ f x } - have h1 : ∀ x : s, |f x| = f x := fun x ↦ abs_of_nonneg x.2 - have h2 : ∀ x : ↑sᶜ, |f x| = -f x := fun x ↦ abs_of_neg (not_le.1 x.2) - calc (Summable fun x ↦ |f x|) ↔ - (Summable fun x : s ↦ |f x|) ∧ Summable fun x : ↑sᶜ ↦ |f x| := - summable_subtype_and_compl.symm - _ ↔ (Summable fun x : s ↦ f x) ∧ Summable fun x : ↑sᶜ ↦ -f x := by simp only [h1, h2] - _ ↔ Summable f := by simp only [summable_neg_iff, summable_subtype_and_compl] +@[to_additive] +theorem multipliable_mabs_iff [LinearOrderedCommGroup α] [UniformSpace α] [UniformGroup α] + [CompleteSpace α] {f : ι → α} : (Multipliable fun x ↦ mabs (f x)) ↔ Multipliable f := + let s := { x | 1 ≤ f x } + have h1 : ∀ x : s, mabs (f x) = f x := fun x ↦ mabs_of_one_le x.2 + have h2 : ∀ x : ↑sᶜ, mabs (f x) = (f x)⁻¹ := fun x ↦ mabs_of_lt_one (not_le.1 x.2) + calc (Multipliable fun x ↦ mabs (f x)) ↔ + (Multipliable fun x : s ↦ mabs (f x)) ∧ Multipliable fun x : ↑sᶜ ↦ mabs (f x) := + multipliable_subtype_and_compl.symm + _ ↔ (Multipliable fun x : s ↦ f x) ∧ Multipliable fun x : ↑sᶜ ↦ (f x)⁻¹ := by simp only [h1, h2] + _ ↔ Multipliable f := by simp only [multipliable_inv_iff, multipliable_subtype_and_compl] #align summable_abs_iff summable_abs_iff alias ⟨Summable.of_abs, Summable.abs⟩ := summable_abs_iff