diff --git a/src/analysis/analytic/composition.lean b/src/analysis/analytic/composition.lean index 72c45ccf16d31..dbd30ee712e5d 100644 --- a/src/analysis/analytic/composition.lean +++ b/src/analysis/analytic/composition.lean @@ -517,7 +517,7 @@ begin exact mul_le_mul' (nnnorm_sum_le _ _) le_rfl end ... ≤ ∑' (i : Σ (n : ℕ), composition n), ‖comp_along_composition q p i.snd‖₊ * r ^ i.fst : - nnreal.tsum_comp_le_tsum_of_inj hr sigma_mk_injective + (nnreal.tsum_comp_le_tsum_of_inj hr sigma_mk_injective : _) end /-! diff --git a/src/analysis/normed/group/infinite_sum.lean b/src/analysis/normed/group/infinite_sum.lean index 84b2afbcb9395..8d51432b20b3d 100644 --- a/src/analysis/normed/group/infinite_sum.lean +++ b/src/analysis/normed/group/infinite_sum.lean @@ -36,11 +36,11 @@ open finset filter metric variables {ι α E F : Type*} [seminormed_add_comm_group E] [seminormed_add_comm_group F] -lemma cauchy_seq_finset_iff_vanishing_norm {f : ι → E} : +lemma cauchy_seq_finset_sum_iff_vanishing_norm {f : ι → E} : cauchy_seq (λ s : finset ι, ∑ i in s, f i) ↔ ∀ε > (0 : ℝ), ∃s:finset ι, ∀t, disjoint t s → ‖ ∑ i in t, f i ‖ < ε := begin - rw [cauchy_seq_finset_iff_vanishing, nhds_basis_ball.forall_iff], + rw [cauchy_seq_finset_sum_iff_vanishing, nhds_basis_ball.forall_iff], { simp only [ball_zero_eq, set.mem_set_of_eq] }, { rintros s t hst ⟨s', hs'⟩, exact ⟨s', λ t' ht', hst $ hs' _ ht'⟩ } @@ -48,12 +48,12 @@ end lemma summable_iff_vanishing_norm [complete_space E] {f : ι → E} : summable f ↔ ∀ε > (0 : ℝ), ∃s:finset ι, ∀t, disjoint t s → ‖ ∑ i in t, f i ‖ < ε := -by rw [summable_iff_cauchy_seq_finset, cauchy_seq_finset_iff_vanishing_norm] +by rw [summable_iff_cauchy_seq_finset, cauchy_seq_finset_sum_iff_vanishing_norm] lemma cauchy_seq_finset_of_norm_bounded_eventually {f : ι → E} {g : ι → ℝ} (hg : summable g) (h : ∀ᶠ i in cofinite, ‖f i‖ ≤ g i) : cauchy_seq (λ s, ∑ i in s, f i) := begin - refine cauchy_seq_finset_iff_vanishing_norm.2 (λ ε hε, _), + refine cauchy_seq_finset_sum_iff_vanishing_norm.2 (λ ε hε, _), rcases summable_iff_vanishing_norm.1 hg ε hε with ⟨s, hs⟩, refine ⟨s ∪ h.to_finset, λ t ht, _⟩, have : ∀ i ∈ t, ‖f i‖ ≤ g i, diff --git a/src/analysis/normed_space/exponential.lean b/src/analysis/normed_space/exponential.lean index c75855885cbb5..9c0d86da7c854 100644 --- a/src/analysis/normed_space/exponential.lean +++ b/src/analysis/normed_space/exponential.lean @@ -498,7 +498,7 @@ lemma exp_smul {G} [monoid G] [mul_semiring_action G 𝔸] [has_continuous_const lemma exp_units_conj (y : 𝔸ˣ) (x : 𝔸) : exp 𝕂 (y * x * ↑(y⁻¹) : 𝔸) = y * exp 𝕂 x * ↑(y⁻¹) := -exp_smul _ (conj_act.to_conj_act y) x +(exp_smul _ (conj_act.to_conj_act y) x : _) lemma exp_units_conj' (y : 𝔸ˣ) (x : 𝔸) : exp 𝕂 (↑(y⁻¹) * x * y) = ↑(y⁻¹) * exp 𝕂 x * y := @@ -578,11 +578,11 @@ end lemma exp_conj (y : 𝔸) (x : 𝔸) (hy : y ≠ 0) : exp 𝕂 (y * x * y⁻¹) = y * exp 𝕂 x * y⁻¹ := -exp_units_conj _ (units.mk0 y hy) x +(exp_units_conj _ (units.mk0 y hy) x : _) lemma exp_conj' (y : 𝔸) (x : 𝔸) (hy : y ≠ 0) : exp 𝕂 (y⁻¹ * x * y) = y⁻¹ * exp 𝕂 x * y := -exp_units_conj' _ (units.mk0 y hy) x +(exp_units_conj' _ (units.mk0 y hy) x : _) end division_algebra diff --git a/src/analysis/normed_space/matrix_exponential.lean b/src/analysis/normed_space/matrix_exponential.lean index 529ec5ab24174..48ec626b787db 100644 --- a/src/analysis/normed_space/matrix_exponential.lean +++ b/src/analysis/normed_space/matrix_exponential.lean @@ -118,7 +118,7 @@ by simp_rw [exp_eq_tsum, ←block_diagonal'_pow, ←block_diagonal'_smul, ←blo lemma exp_conj_transpose [star_ring 𝔸] [has_continuous_star 𝔸] (A : matrix m m 𝔸) : exp 𝕂 Aᴴ = (exp 𝕂 A)ᴴ := -(star_exp A).symm +((star_exp A).symm : _) lemma is_hermitian.exp [star_ring 𝔸] [has_continuous_star 𝔸] {A : matrix m m 𝔸} (h : A.is_hermitian) : (exp 𝕂 A).is_hermitian := diff --git a/src/measure_theory/measure/measure_space.lean b/src/measure_theory/measure/measure_space.lean index 9089d791ce8e2..254b4953b5f27 100644 --- a/src/measure_theory/measure/measure_space.lean +++ b/src/measure_theory/measure/measure_space.lean @@ -1844,7 +1844,7 @@ lemma sum_add_sum_compl (s : set ι) (μ : ι → measure α) : begin ext1 t ht, simp only [add_apply, sum_apply _ ht], - exact @tsum_add_tsum_compl ℝ≥0∞ ι _ _ _ (λ i, μ i t) _ s ennreal.summable ennreal.summable + exact @tsum_add_tsum_compl ℝ≥0∞ ι _ _ (λ i, μ i t) _ _ s ennreal.summable ennreal.summable, end lemma sum_congr {μ ν : ℕ → measure α} (h : ∀ n, μ n = ν n) : sum μ = sum ν := @@ -1912,7 +1912,7 @@ variable [measurable_space α] def count : measure α := sum dirac lemma le_count_apply : (∑' i : s, 1 : ℝ≥0∞) ≤ count s := -calc (∑' i : s, 1 : ℝ≥0∞) = ∑' i, indicator s 1 i : tsum_subtype s 1 +calc (∑' i : s, 1 : ℝ≥0∞) = ∑' i, indicator s 1 i : by simp_rw [←tsum_subtype, pi.one_apply] ... ≤ ∑' i, dirac i s : ennreal.tsum_le_tsum $ λ x, le_dirac_apply ... ≤ count s : le_sum_apply _ _ @@ -1925,7 +1925,7 @@ by rw [count_apply measurable_set.empty, tsum_empty] @[simp] lemma count_apply_finset' {s : finset α} (s_mble : measurable_set (s : set α)) : count (↑s : set α) = s.card := calc count (↑s : set α) = ∑' i : (↑s : set α), 1 : count_apply s_mble - ... = ∑ i in s, 1 : s.tsum_subtype 1 + ... = ∑ i in s, 1 : by rw [←finset.tsum_subtype]; refl ... = s.card : by simp @[simp] lemma count_apply_finset [measurable_singleton_class α] (s : finset α) : diff --git a/src/measure_theory/measure/outer_measure.lean b/src/measure_theory/measure/outer_measure.lean index d4f4103e49130..7e38d2bb7bbc1 100644 --- a/src/measure_theory/measure/outer_measure.lean +++ b/src/measure_theory/measure/outer_measure.lean @@ -604,7 +604,7 @@ begin calc μ s + μ t ≤ (∑' i : I s, μ (f i)) + (∑' i : I t, μ (f i)) : add_le_add (hI _ $ subset_union_left _ _) (hI _ $ subset_union_right _ _) ... = ∑' i : I s ∪ I t, μ (f i) : - (@tsum_union_disjoint _ _ _ _ _ (λ i, μ (f i)) _ _ _ hd ennreal.summable ennreal.summable).symm + (@tsum_union_disjoint _ _ _ _ (λ i, μ (f i)) _ _ _ _ hd ennreal.summable ennreal.summable).symm ... ≤ ∑' i, μ (f i) : tsum_le_tsum_of_inj coe subtype.coe_injective (λ _ _, zero_le _) (λ _, le_rfl) ennreal.summable ennreal.summable diff --git a/src/tactic/to_additive.lean b/src/tactic/to_additive.lean index c0aa488aa028c..aeedc9a55db17 100644 --- a/src/tactic/to_additive.lean +++ b/src/tactic/to_additive.lean @@ -244,6 +244,8 @@ meta def tr : bool → list string → list string | is_comm ("root" :: s) := add_comm_prefix is_comm "div" :: tr ff s | is_comm ("rootable" :: s) := add_comm_prefix is_comm "divisible" :: tr ff s | is_comm ("prods" :: s) := add_comm_prefix is_comm "sums" :: tr ff s +| is_comm ("tprod" :: s) := add_comm_prefix is_comm "tsum" :: tr ff s +| is_comm ("prodable" :: s) := add_comm_prefix is_comm "summable" :: tr ff s | is_comm (x :: s) := (add_comm_prefix is_comm x :: tr ff s) | tt [] := ["comm"] | ff [] := [] diff --git a/src/topology/algebra/infinite_sum/basic.lean b/src/topology/algebra/infinite_sum/basic.lean index 9d0486d2144d3..344b0ba618d35 100644 --- a/src/topology/algebra/infinite_sum/basic.lean +++ b/src/topology/algebra/infinite_sum/basic.lean @@ -9,7 +9,7 @@ import topology.algebra.uniform_group import topology.algebra.star /-! -# Infinite sum over a topological monoid +# Infinite sum/product over a topological monoid > THIS FILE IS SYNCHRONIZED WITH MATHLIB4. > Any changes to this file require a corresponding PR to mathlib4. @@ -21,6 +21,15 @@ convergence. Note: There are summable sequences which are not unconditionally convergent! The other way holds generally, see `has_sum.tendsto_sum_nat`. +## Main declarations + +* `has_prod`: Predicate for an infinite product to unconditionally converge to a given value. +* `has_sum`: Predicate for an infinite series to unconditionally converge to a given value. +* `prodable`: Predicate for an infinite product to unconditionally converge to some value. +* `summable`: Predicate for an infinite series to unconditionally converge to some value. +* `tprod`: The value an infinite product converges to, if such value exists. Else, defaults to `1`. +* `tsum`: The value an infinite series converges to, if such value exists. Else, defaults to `0`. + ## References * Bourbaki: General Topology (1995), Chapter 3 §5 (Infinite sums in commutative groups) @@ -31,12 +40,24 @@ noncomputable theory open classical filter finset function open_locale big_operators classical topology -variables {α : Type*} {β : Type*} {γ : Type*} {δ : Type*} +variables {α α' β γ δ G G' : Type*} + +section has_prod +variables [comm_monoid α] [topological_space α] + +/-- Infinite product on a topological monoid -section has_sum -variables [add_comm_monoid α] [topological_space α] +The `at_top` filter on `finset β` is the limit of all finite sets towards the entire type. So we +take the product of bigger and bigger sets. This product operation is invariant under reordering. In +particular, the function `ℕ → ℝ` sending `n` to `e ^ ((-1)^n / (n + 1))` does not have a product for +this definition, but a series which is absolutely convergent will have the correct product. + +This is based on Mario Carneiro's +[infinite sum `df-tsms` in Metamath](http://us.metamath.org/mpeuni/df-tsms.html). -/-- Infinite sum on a topological monoid +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. -/ +@[to_additive "Infinite sum on a topological monoid The `at_top` 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, @@ -47,295 +68,296 @@ 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 has_sum (f : β → α) (a : α) : Prop := tendsto (λs:finset β, ∑ b in s, f b) at_top (𝓝 a) +this assumption later, for the lemmas where it is relevant."] +def has_prod (f : β → α) (a : α) : Prop := tendsto (λ s, ∏ b in s, f b) at_top (𝓝 a) -/-- `summable f` means that `f` has some (infinite) sum. Use `tsum` to get the value. -/ -def summable (f : β → α) : Prop := ∃a, has_sum f a +/-- `prodable f` means that `f` has some (infinite) sum. Use `tsum` to get the value. -/ +@[to_additive "`summable f` means that `f` has some (infinite) sum. Use `tsum` to get the value."] +def prodable (f : β → α) : Prop := ∃ a, has_prod f a -/-- `∑' i, f i` is the sum of `f` it exists, or 0 otherwise -/ -@[irreducible] def tsum {β} (f : β → α) := if h : summable f then classical.some h else 0 +/-- `∏' 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.", irreducible] +def tprod (f : β → α) := if h : prodable f then classical.some h else 1 -- see Note [operator precedence of big operators] notation `∑'` binders `, ` r:(scoped:67 f, tsum f) := r +notation `∏'` binders `, ` r:(scoped:67 f, tprod f) := r -variables {f g : β → α} {a b : α} {s : finset β} +variables {f g : β → α} {a a' a₁ a₂ b : α} {s : finset β} -lemma summable.has_sum (ha : summable f) : has_sum f (∑'b, f b) := -by simp [ha, tsum]; exact some_spec ha +@[to_additive] lemma prodable.has_prod (ha : prodable f) : has_prod f (∏' b, f b) := +by simp [ha, tprod]; exact some_spec ha -lemma has_sum.summable (h : has_sum f a) : summable f := ⟨a, h⟩ +@[to_additive] protected lemma has_prod.prodable (h : has_prod f a) : prodable f := ⟨a, h⟩ -/-- Constant zero function has sum `0` -/ -lemma has_sum_zero : has_sum (λb, 0 : β → α) 0 := -by simp [has_sum, tendsto_const_nhds] +/-- The constant one function has product `1`. -/ +@[to_additive "The constant zero function has sum `0`."] +lemma has_prod_one : has_prod (λ b, 1 : β → α) 1 := by simp [has_prod, tendsto_const_nhds] -lemma has_sum_empty [is_empty β] : has_sum f 0 := -by convert has_sum_zero +@[to_additive] lemma has_prod_empty [is_empty β] : has_prod f 1 := by convert has_prod_one -lemma summable_zero : summable (λb, 0 : β → α) := has_sum_zero.summable +@[to_additive] lemma prodable_one : prodable (λ b, 1 : β → α) := has_prod_one.prodable -lemma summable_empty [is_empty β] : summable f := has_sum_empty.summable +@[to_additive] lemma prodable_empty [is_empty β] : prodable f := has_prod_empty.prodable -lemma tsum_eq_zero_of_not_summable (h : ¬ summable f) : ∑'b, f b = 0 := -by simp [tsum, h] +@[to_additive] lemma tprod_eq_one_of_not_prodable (h : ¬ prodable f) : ∏' b, f b = 1 := +by simp [tprod, h] -lemma summable_congr (hfg : ∀b, f b = g b) : - summable f ↔ summable g := -iff_of_eq (congr_arg summable $ funext hfg) +@[to_additive] lemma prodable_congr (hfg : ∀ b, f b = g b) : prodable f ↔ prodable g := +iff_of_eq (congr_arg prodable $ funext hfg) -lemma summable.congr (hf : summable f) (hfg : ∀b, f b = g b) : - summable g := -(summable_congr hfg).mp hf +@[to_additive] lemma prodable.congr (hf : prodable f) (hfg : ∀ b, f b = g b) : prodable g := +(prodable_congr hfg).mp hf -lemma has_sum.has_sum_of_sum_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 : has_sum g a) : - has_sum f a := -le_trans (map_at_top_finset_sum_le_of_sum_eq h_eq) hf +@[to_additive] lemma has_prod.has_prod_of_prod_eq {g : γ → α} + (h_eq : ∀ u, ∃ v, ∀ v', v ⊆ v' → ∃ u', u ⊆ u' ∧ ∏ x in u', g x = ∏ b in v', f b) + (hf : has_prod g a) : + has_prod f a := +le_trans (map_at_top_finset_prod_le_of_prod_eq h_eq) hf -lemma has_sum_iff_has_sum {g : γ → α} - (h₁ : ∀u:finset γ, ∃v:finset β, ∀v', v ⊆ v' → ∃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) : - has_sum f a ↔ has_sum g a := -⟨has_sum.has_sum_of_sum_eq h₂, has_sum.has_sum_of_sum_eq h₁⟩ +@[to_additive] lemma has_prod_iff_has_prod {g : γ → α} + (h₁ : ∀ u, ∃ v, ∀ v', v ⊆ v' → ∃ u', u ⊆ u' ∧ ∏ x in u', g x = ∏ b in v', f b) + (h₂ : ∀ v, ∃ u, ∀ u', u ⊆ u' → ∃ v', v ⊆ v' ∧ ∏ b in v', f b = ∏ x in u', g x) : + has_prod f a ↔ has_prod g a := +⟨has_prod.has_prod_of_prod_eq h₂, has_prod.has_prod_of_prod_eq h₁⟩ -lemma function.injective.has_sum_iff {g : γ → β} (hg : injective g) - (hf : ∀ x ∉ set.range g, f x = 0) : - has_sum (f ∘ g) a ↔ has_sum f a := -by simp only [has_sum, tendsto, hg.map_at_top_finset_sum_eq hf] +@[to_additive] lemma function.injective.has_prod_iff {g : γ → β} (hg : injective g) + (hf : ∀ x ∉ set.range g, f x = 1) : + has_prod (f ∘ g) a ↔ has_prod f a := +by simp only [has_prod, tendsto, hg.map_at_top_finset_prod_eq hf] -lemma function.injective.summable_iff {g : γ → β} (hg : injective g) - (hf : ∀ x ∉ set.range g, f x = 0) : - summable (f ∘ g) ↔ summable f := -exists_congr $ λ _, hg.has_sum_iff hf +@[to_additive] lemma function.injective.prodable_iff {g : γ → β} (hg : injective g) + (hf : ∀ x ∉ set.range g, f x = 1) : + prodable (f ∘ g) ↔ prodable f := +exists_congr $ λ _, hg.has_prod_iff hf -lemma has_sum_subtype_iff_of_support_subset {s : set β} (hf : support f ⊆ s) : - has_sum (f ∘ coe : s → α) a ↔ has_sum f a := -subtype.coe_injective.has_sum_iff $ by simpa using support_subset_iff'.1 hf +@[to_additive] +lemma has_prod_subtype_iff_of_mul_support_subset {s : set β} (hf : mul_support f ⊆ s) : + has_prod (f ∘ coe : s → α) a ↔ has_prod f a := +subtype.coe_injective.has_prod_iff $ by simpa using mul_support_subset_iff'.1 hf -lemma has_sum_subtype_iff_indicator {s : set β} : - has_sum (f ∘ coe : s → α) a ↔ has_sum (s.indicator f) a := -by rw [← set.indicator_range_comp, subtype.range_coe, - has_sum_subtype_iff_of_support_subset set.support_indicator_subset] +@[to_additive] lemma has_prod_subtype_iff_mul_indicator {s : set β} : + has_prod (f ∘ coe : s → α) a ↔ has_prod (s.mul_indicator f) a := +by rw [← set.mul_indicator_range_comp, subtype.range_coe, + has_prod_subtype_iff_of_mul_support_subset set.mul_support_mul_indicator_subset] -lemma summable_subtype_iff_indicator {s : set β} : - summable (f ∘ coe : s → α) ↔ summable (s.indicator f) := -exists_congr (λ _, has_sum_subtype_iff_indicator) +@[to_additive] lemma prodable_subtype_iff_mul_indicator {s : set β} : + prodable (f ∘ coe : s → α) ↔ prodable (s.mul_indicator f) := +exists_congr $ λ _, has_prod_subtype_iff_mul_indicator -@[simp] lemma has_sum_subtype_support : has_sum (f ∘ coe : support f → α) a ↔ has_sum f a := -has_sum_subtype_iff_of_support_subset $ set.subset.refl _ +@[simp, to_additive] +lemma has_prod_subtype_support : has_prod (f ∘ coe : mul_support f → α) a ↔ has_prod f a := +has_prod_subtype_iff_of_mul_support_subset $ set.subset.refl _ -lemma has_sum_fintype [fintype β] (f : β → α) : has_sum f (∑ b, f b) := +@[to_additive] lemma has_prod_fintype [fintype β] (f : β → α) : has_prod f (∏ b, f b) := order_top.tendsto_at_top_nhds _ -protected lemma finset.has_sum (s : finset β) (f : β → α) : - has_sum (f ∘ coe : (↑s : set β) → α) (∑ b in s, f b) := -by { rw ← sum_attach, exact has_sum_fintype _ } +@[to_additive] protected lemma finset.has_prod (s : finset β) (f : β → α) : + has_prod (f ∘ coe : (↑s : set β) → α) (∏ b in s, f b) := +by { rw ← prod_attach, exact has_prod_fintype _ } -protected lemma finset.summable (s : finset β) (f : β → α) : - summable (f ∘ coe : (↑s : set β) → α) := -(s.has_sum f).summable +@[to_additive] protected lemma finset.prodable (s : finset β) (f : β → α) : + prodable (f ∘ coe : (↑s : set β) → α) := +(s.has_prod f).prodable -protected lemma set.finite.summable {s : set β} (hs : s.finite) (f : β → α) : - summable (f ∘ coe : s → α) := -by convert hs.to_finset.summable f; simp only [hs.coe_to_finset] +@[to_additive] protected lemma set.finite.prodable {s : set β} (hs : s.finite) (f : β → α) : + prodable (f ∘ coe : s → α) := +by convert hs.to_finset.prodable f; simp only [hs.coe_to_finset] -/-- If a function `f` vanishes outside of a finite set `s`, then it `has_sum` `∑ b in s, f b`. -/ -lemma has_sum_sum_of_ne_finset_zero (hf : ∀b∉s, f b = 0) : has_sum f (∑ b in s, f b) := -(has_sum_subtype_iff_of_support_subset $ support_subset_iff'.2 hf).1 $ s.has_sum f +/-- If a function `f` vanishes outside of a finite set `s`, then it `has_prod` `∏ b in s, f b`. -/ +@[to_additive +"If a function `f` vanishes outside of a finite set `s`, then it `has_sum` `∑ b in s, f b`."] +lemma has_prod_prod_of_ne_finset_one (hf : ∀ b ∉ s, f b = 1) : has_prod f (∏ b in s, f b) := +(has_prod_subtype_iff_of_mul_support_subset $ mul_support_subset_iff'.2 hf).1 $ s.has_prod f -lemma summable_of_ne_finset_zero (hf : ∀b∉s, f b = 0) : summable f := -(has_sum_sum_of_ne_finset_zero hf).summable +@[to_additive] lemma prodable_of_ne_finset_one (hf : ∀ b ∉ s, f b = 1) : prodable f := +(has_prod_prod_of_ne_finset_one hf).prodable -lemma has_sum_single {f : β → α} (b : β) (hf : ∀b' ≠ b, f b' = 0) : - has_sum f (f b) := -suffices has_sum f (∑ b' in {b}, f b'), +@[to_additive] lemma has_prod_single (b : β) (hf : ∀ b' ≠ b, f b' = 1) : has_prod f (f b) := +suffices has_prod f (∏ b' in {b}, f b'), by simpa using this, -has_sum_sum_of_ne_finset_zero $ by simpa [hf] +has_prod_prod_of_ne_finset_one $ by simpa [hf] -lemma has_sum_ite_eq (b : β) [decidable_pred (= b)] (a : α) : - has_sum (λb', if b' = b then a else 0) a := +@[to_additive] lemma has_prod_ite_eq (b : β) [decidable_pred (= b)] (a : α) : + has_prod (λ b', if b' = b then a else 1) a := begin - convert has_sum_single b _, + convert has_prod_single b _, { exact (if_pos rfl).symm }, - assume b' hb', - exact if_neg hb' + { exact λ b' hb', if_neg hb' } end -lemma has_sum_pi_single [decidable_eq β] (b : β) (a : α) : - has_sum (pi.single b a) a := -show has_sum (λ x, pi.single b a x) a, by simpa only [pi.single_apply] using has_sum_ite_eq b a +@[to_additive] lemma has_prod_pi_mul_single [decidable_eq β] (b : β) (a : α) : + has_prod (pi.mul_single b a) a := +show has_prod (λ x, pi.mul_single b a x) a, + by simpa only [pi.mul_single_apply] using has_prod_ite_eq b a -lemma equiv.has_sum_iff (e : γ ≃ β) : - has_sum (f ∘ e) a ↔ has_sum f a := -e.injective.has_sum_iff $ by simp +@[to_additive] lemma equiv.has_prod_iff (e : γ ≃ β) : has_prod (f ∘ e) a ↔ has_prod f a := +e.injective.has_prod_iff $ by simp -lemma function.injective.has_sum_range_iff {g : γ → β} (hg : injective g) : - has_sum (λ x : set.range g, f x) a ↔ has_sum (f ∘ g) a := -(equiv.of_injective g hg).has_sum_iff.symm +@[to_additive] lemma function.injective.has_prod_range_iff {g : γ → β} (hg : injective g) : + has_prod (λ x : set.range g, f x) a ↔ has_prod (f ∘ g) a := +(equiv.of_injective g hg).has_prod_iff.symm -lemma equiv.summable_iff (e : γ ≃ β) : - summable (f ∘ e) ↔ summable f := -exists_congr $ λ a, e.has_sum_iff +@[to_additive] lemma equiv.prodable_iff (e : γ ≃ β) : prodable (f ∘ e) ↔ prodable f := +exists_congr $ λ a, e.has_prod_iff -lemma summable.prod_symm {f : β × γ → α} (hf : summable f) : summable (λ p : γ × β, f p.swap) := -(equiv.prod_comm γ β).summable_iff.2 hf +@[to_additive summable.prod_symm] +lemma prodable.prod_symm {f : β × γ → α} (hf : prodable f) : prodable (λ p : γ × β, f p.swap) := +(equiv.prod_comm γ β).prodable_iff.2 hf -lemma equiv.has_sum_iff_of_support {g : γ → α} (e : support f ≃ support g) - (he : ∀ x : support f, g (e x) = f x) : - has_sum f a ↔ has_sum g a := +@[to_additive] lemma equiv.has_prod_iff_of_mul_support {g : γ → α} + (e : mul_support f ≃ mul_support g) (he : ∀ x : mul_support f, g (e x) = f x) : + has_prod f a ↔ has_prod g a := have (g ∘ coe) ∘ e = f ∘ coe, from funext he, -by rw [← has_sum_subtype_support, ← this, e.has_sum_iff, has_sum_subtype_support] +by rw [← has_prod_subtype_support, ← this, e.has_prod_iff, has_prod_subtype_support] -lemma has_sum_iff_has_sum_of_ne_zero_bij {g : γ → α} (i : support g → β) +@[to_additive] lemma has_prod_iff_has_prod_of_ne_one_bij {g : γ → α} (i : mul_support g → β) (hi : ∀ ⦃x y⦄, i x = i y → (x : γ) = y) - (hf : support f ⊆ set.range i) (hfg : ∀ x, f (i x) = g x) : - has_sum f a ↔ has_sum g a := -iff.symm $ equiv.has_sum_iff_of_support + (hf : mul_support f ⊆ set.range i) (hfg : ∀ x, f (i x) = g x) : + has_prod f a ↔ has_prod g a := +iff.symm $ equiv.has_prod_iff_of_mul_support (equiv.of_bijective (λ x, ⟨i x, λ hx, x.coe_prop $ hfg x ▸ hx⟩) ⟨λ x y h, subtype.ext $ hi $ subtype.ext_iff.1 h, λ y, (hf y.coe_prop).imp $ λ x hx, subtype.ext hx⟩) hfg -lemma 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 $ λ _, e.has_sum_iff_of_support he - -protected lemma has_sum.map [add_comm_monoid γ] [topological_space γ] (hf : has_sum f a) - {G} [add_monoid_hom_class G α γ] (g : G) (hg : continuous g) : - has_sum (g ∘ f) (g a) := -have g ∘ (λs:finset β, ∑ b in s, f b) = (λs:finset β, ∑ b in s, g (f b)), - from funext $ map_sum g _, -show tendsto (λs:finset β, ∑ b in s, g (f b)) at_top (𝓝 (g a)), +@[to_additive] lemma equiv.prodable_iff_of_mul_support {g : γ → α} + (e : mul_support f ≃ mul_support g) (he : ∀ x : mul_support f, g (e x) = f x) : + prodable f ↔ prodable g := +exists_congr $ λ _, e.has_prod_iff_of_mul_support he + +@[to_additive] protected lemma has_prod.map [comm_monoid γ] [topological_space γ] + (hf : has_prod f a) [monoid_hom_class G α γ] (g : G) (hg : continuous g) : + has_prod (g ∘ f) (g a) := +have g ∘ (λ s, ∏ b in s, f b) = (λ s, ∏ b in s, g (f b)), + from funext $ map_prod g _, +show tendsto (λ s, ∏ b in s, g (f b)) at_top (𝓝 (g a)), from this ▸ (hg.tendsto a).comp hf -protected lemma summable.map [add_comm_monoid γ] [topological_space γ] (hf : summable f) - {G} [add_monoid_hom_class G α γ] (g : G) (hg : continuous g) : - summable (g ∘ f) := -(hf.has_sum.map g hg).summable +@[to_additive] protected lemma prodable.map [comm_monoid γ] [topological_space γ] + (hf : prodable f) [monoid_hom_class G α γ] (g : G) (hg : continuous g) : + prodable (g ∘ f) := +(hf.has_prod.map g hg).prodable -protected lemma summable.map_iff_of_left_inverse [add_comm_monoid γ] [topological_space γ] - {G G'} [add_monoid_hom_class G α γ] [add_monoid_hom_class G' γ α] (g : G) (g' : G') +@[to_additive] protected lemma prodable.map_iff_of_left_inverse [comm_monoid γ] + [topological_space γ] [monoid_hom_class G α γ] [monoid_hom_class G' γ α] (g : G) (g' : G') (hg : continuous g) (hg' : continuous g') (hinv : function.left_inverse g' g) : - summable (g ∘ f) ↔ summable f := -⟨λ h, begin - have := h.map _ hg', - rwa [←function.comp.assoc, hinv.id] at this, -end, λ h, h.map _ hg⟩ - -/-- A special case of `summable.map_iff_of_left_inverse` for convenience -/ -protected lemma summable.map_iff_of_equiv [add_comm_monoid γ] [topological_space γ] - {G} [add_equiv_class G α γ] (g : G) - (hg : continuous g) (hg' : continuous (add_equiv_class.inv g : γ → α)) : - summable (g ∘ f) ↔ summable f := -summable.map_iff_of_left_inverse g (g : α ≃+ γ).symm hg hg' (add_equiv_class.left_inv g) - -/-- If `f : ℕ → α` has sum `a`, then the partial sums `∑_{i=0}^{n-1} f i` converge to `a`. -/ -lemma has_sum.tendsto_sum_nat {f : ℕ → α} (h : has_sum f a) : - tendsto (λn:ℕ, ∑ i in range n, f i) at_top (𝓝 a) := + prodable (g ∘ f) ↔ prodable f := +⟨λ h, by simpa only [←function.comp.assoc g', hinv.id] using h.map _ hg', λ h, h.map _ hg⟩ + +/-- A special case of `prodable.map_iff_of_left_inverse` for convenience -/ +@[to_additive "A special case of `summable.map_iff_of_left_inverse` for convenience"] +protected lemma prodable.map_iff_of_equiv [comm_monoid γ] [topological_space γ] + [mul_equiv_class G α γ] (g : G) (hg : continuous g) + (hg' : continuous (mul_equiv_class.inv g : γ → α)) : + prodable (g ∘ f) ↔ prodable f := +prodable.map_iff_of_left_inverse g (g : α ≃* γ).symm hg hg' (mul_equiv_class.left_inv g) + +/-- If `f : ℕ → α` has product `a`, then the partial prods `∏_{i=1}^{n-1} f i` converge to `a`. -/ +@[to_additive +"If `f : ℕ → α` has sum `a`, then the partial sums `∑_{i=1}^{n-1} f i` converge to `a`."] +lemma has_prod.tendsto_prod_nat {f : ℕ → α} (h : has_prod f a) : + tendsto (λ n, ∏ i in range n, f i) at_top (𝓝 a) := h.comp tendsto_finset_range -lemma has_sum.unique {a₁ a₂ : α} [t2_space α] : has_sum f a₁ → has_sum f a₂ → a₁ = a₂ := +@[to_additive] lemma has_prod.unique [t2_space α] : has_prod f a₁ → has_prod f a₂ → a₁ = a₂ := tendsto_nhds_unique -lemma summable.has_sum_iff_tendsto_nat [t2_space α] {f : ℕ → α} {a : α} (hf : summable f) : - has_sum f a ↔ tendsto (λn:ℕ, ∑ i in range n, f i) at_top (𝓝 a) := +@[to_additive] lemma prodable.has_prod_iff_tendsto_nat [t2_space α] {f : ℕ → α} (hf : prodable f) : + has_prod f a ↔ tendsto (λ n, ∏ i in range n, f i) at_top (𝓝 a) := begin - refine ⟨λ h, h.tendsto_sum_nat, λ h, _⟩, - rw tendsto_nhds_unique h hf.has_sum.tendsto_sum_nat, - exact hf.has_sum + refine ⟨λ h, h.tendsto_prod_nat, λ h, _⟩, + rw tendsto_nhds_unique h hf.has_prod.tendsto_prod_nat, + exact hf.has_prod end -lemma function.surjective.summable_iff_of_has_sum_iff {α' : Type*} [add_comm_monoid α'] - [topological_space α'] {e : α' → α} (hes : function.surjective e) {f : β → α} {g : γ → α'} - (he : ∀ {a}, has_sum f (e a) ↔ has_sum g a) : - summable f ↔ summable g := +@[to_additive] lemma function.surjective.prodable_iff_of_has_prod_iff [comm_monoid α'] + [topological_space α'] {e : α' → α} (hes : surjective e) {g : γ → α'} + (he : ∀ {a}, has_prod f (e a) ↔ has_prod g a) : + prodable f ↔ prodable g := hes.exists.trans $ exists_congr $ @he -variable [has_continuous_add α] +variables [has_continuous_mul α] -lemma has_sum.add (hf : has_sum f a) (hg : has_sum g b) : has_sum (λb, f b + g b) (a + b) := -by simp only [has_sum, sum_add_distrib]; exact hf.add hg +@[to_additive] lemma has_prod.mul (hf : has_prod f a) (hg : has_prod g b) : + has_prod (λ b, f b * g b) (a * b) := +by simp only [has_prod, prod_mul_distrib]; exact hf.mul hg -lemma summable.add (hf : summable f) (hg : summable g) : summable (λb, f b + g b) := -(hf.has_sum.add hg.has_sum).summable +@[to_additive] lemma prodable.mul (hf : prodable f) (hg : prodable g) : + prodable (λ b, f b * g b) := +(hf.has_prod.mul hg.has_prod).prodable -lemma has_sum_sum {f : γ → β → α} {a : γ → α} {s : finset γ} : - (∀i∈s, has_sum (f i) (a i)) → has_sum (λb, ∑ i in s, f i b) (∑ i in s, a i) := -finset.induction_on s (by simp only [has_sum_zero, sum_empty, forall_true_iff]) - (by simp only [has_sum.add, sum_insert, mem_insert, forall_eq_or_imp, +@[to_additive] lemma has_prod_prod {f : γ → β → α} {a : γ → α} {s : finset γ} : + (∀ i ∈ s, has_prod (f i) (a i)) → has_prod (λ b, ∏ i in s, f i b) (∏ i in s, a i) := +finset.induction_on s (by simp only [has_prod_one, prod_empty, forall_true_iff]) + (by simp only [has_prod.mul, prod_insert, mem_insert, forall_eq_or_imp, forall_2_true_iff, not_false_iff, forall_true_iff] {contextual := tt}) -lemma summable_sum {f : γ → β → α} {s : finset γ} (hf : ∀i∈s, summable (f i)) : - summable (λb, ∑ i in s, f i b) := -(has_sum_sum $ assume i hi, (hf i hi).has_sum).summable +@[to_additive] lemma prodable_prod {f : γ → β → α} {s : finset γ} (hf : ∀ i ∈ s, prodable (f i)) : + prodable (λ b, ∏ i in s, f i b) := +(has_prod_prod $ assume i hi, (hf i hi).has_prod).prodable -lemma has_sum.add_disjoint {s t : set β} (hs : disjoint s t) - (ha : has_sum (f ∘ coe : s → α) a) (hb : has_sum (f ∘ coe : t → α) b) : - has_sum (f ∘ coe : s ∪ t → α) (a + b) := +@[to_additive] lemma has_prod.mul_disjoint {s t : set β} (hs : disjoint s t) + (ha : has_prod (f ∘ coe : s → α) a) (hb : has_prod (f ∘ coe : t → α) b) : + has_prod (f ∘ coe : s ∪ t → α) (a * b) := begin - rw has_sum_subtype_iff_indicator at *, - rw set.indicator_union_of_disjoint hs, - exact ha.add hb + rw has_prod_subtype_iff_mul_indicator at *, + rw set.mul_indicator_union_of_disjoint hs, + exact ha.mul hb, end -lemma has_sum_sum_disjoint {ι} (s : finset ι) {t : ι → set β} {a : ι → α} +@[to_additive] lemma has_prod_prod_disjoint {ι} (s : finset ι) {t : ι → set β} {a : ι → α} (hs : (s : set ι).pairwise (disjoint on t)) - (hf : ∀ i ∈ s, has_sum (f ∘ coe : t i → α) (a i)) : - has_sum (f ∘ coe : (⋃ i ∈ s, t i) → α) (∑ i in s, a i) := + (hf : ∀ i ∈ s, has_prod (f ∘ coe : t i → α) (a i)) : + has_prod (f ∘ coe : (⋃ i ∈ s, t i) → α) (∏ i in s, a i) := begin - simp_rw has_sum_subtype_iff_indicator at *, - rw set.indicator_finset_bUnion _ _ hs, - exact has_sum_sum hf, + simp_rw has_prod_subtype_iff_mul_indicator at *, + rw set.mul_indicator_finset_bUnion _ _ hs, + exact has_prod_prod hf, end -lemma has_sum.add_is_compl {s t : set β} (hs : is_compl s t) - (ha : has_sum (f ∘ coe : s → α) a) (hb : has_sum (f ∘ coe : t → α) b) : - has_sum f (a + b) := +@[to_additive] lemma has_prod.mul_is_compl {s t : set β} (hs : is_compl s t) + (ha : has_prod (f ∘ coe : s → α) a) (hb : has_prod (f ∘ coe : t → α) b) : + has_prod f (a * b) := by simpa [← hs.compl_eq] - using (has_sum_subtype_iff_indicator.1 ha).add (has_sum_subtype_iff_indicator.1 hb) - -lemma has_sum.add_compl {s : set β} (ha : has_sum (f ∘ coe : s → α) a) - (hb : has_sum (f ∘ coe : sᶜ → α) b) : - has_sum f (a + b) := -ha.add_is_compl is_compl_compl hb - -lemma summable.add_compl {s : set β} (hs : summable (f ∘ coe : s → α)) - (hsc : summable (f ∘ coe : sᶜ → α)) : - summable f := -(hs.has_sum.add_compl hsc.has_sum).summable - -lemma has_sum.compl_add {s : set β} (ha : has_sum (f ∘ coe : sᶜ → α) a) - (hb : has_sum (f ∘ coe : s → α) b) : - has_sum f (a + b) := -ha.add_is_compl is_compl_compl.symm hb - -lemma has_sum.even_add_odd {f : ℕ → α} (he : has_sum (λ k, f (2 * k)) a) - (ho : has_sum (λ k, f (2 * k + 1)) b) : - has_sum f (a + b) := + using (has_prod_subtype_iff_mul_indicator.1 ha).mul (has_prod_subtype_iff_mul_indicator.1 hb) + +@[to_additive] lemma has_prod.mul_compl {s : set β} (ha : has_prod (f ∘ coe : s → α) a) + (hb : has_prod (f ∘ coe : sᶜ → α) b) : + has_prod f (a * b) := +ha.mul_is_compl is_compl_compl hb + +@[to_additive] lemma prodable.mul_compl {s : set β} (hs : prodable (f ∘ coe : s → α)) + (hsc : prodable (f ∘ coe : sᶜ → α)) : + prodable f := +(hs.has_prod.mul_compl hsc.has_prod).prodable + +@[to_additive] lemma has_prod.compl_mul {s : set β} (ha : has_prod (f ∘ coe : sᶜ → α) a) + (hb : has_prod (f ∘ coe : s → α) b) : + has_prod f (a * b) := +ha.mul_is_compl is_compl_compl.symm hb + +@[to_additive] lemma has_prod.even_mul_odd {f : ℕ → α} (he : has_prod (λ k, f (2 * k)) a) + (ho : has_prod (λ k, f (2 * k + 1)) b) : + has_prod f (a * b) := begin have := mul_right_injective₀ (two_ne_zero' ℕ), - replace he := this.has_sum_range_iff.2 he, - replace ho := ((add_left_injective 1).comp this).has_sum_range_iff.2 ho, - refine he.add_is_compl _ ho, + replace he := this.has_prod_range_iff.2 he, + replace ho := ((add_left_injective 1).comp this).has_prod_range_iff.2 ho, + refine he.mul_is_compl _ ho, simpa [(∘)] using nat.is_compl_even_odd end -lemma summable.compl_add {s : set β} (hs : summable (f ∘ coe : sᶜ → α)) - (hsc : summable (f ∘ coe : s → α)) : - summable f := -(hs.has_sum.compl_add hsc.has_sum).summable +@[to_additive] lemma prodable.compl_mul {s : set β} (hs : prodable (f ∘ coe : sᶜ → α)) + (hsc : prodable (f ∘ coe : s → α)) : prodable f := +(hs.has_prod.compl_mul hsc.has_prod).prodable -lemma summable.even_add_odd {f : ℕ → α} (he : summable (λ k, f (2 * k))) - (ho : summable (λ k, f (2 * k + 1))) : - summable f := -(he.has_sum.even_add_odd ho.has_sum).summable +@[to_additive] lemma prodable.even_mul_odd {f : ℕ → α} (he : prodable (λ k, f (2 * k))) + (ho : prodable (λ k, f (2 * k + 1))) : prodable f := +(he.has_prod.even_mul_odd ho.has_prod).prodable -lemma has_sum.sigma [regular_space α] {γ : β → Type*} {f : (Σ b:β, γ b) → α} {g : β → α} {a : α} - (ha : has_sum f a) (hf : ∀b, has_sum (λc, f ⟨b, c⟩) (g b)) : has_sum g a := +@[to_additive] protected lemma has_prod.sigma [regular_space α] {γ : β → Type*} {f : (Σ b, γ b) → α} + {g : β → α} (ha : has_prod f a) (hf : ∀ b, has_prod (λ c, f ⟨b, c⟩) (g b)) : has_prod g a := begin refine (at_top_basis.tendsto_iff (closed_nhds_basis a)).mpr _, rintros s ⟨hs, hsc⟩, @@ -343,281 +365,294 @@ begin use [u.image sigma.fst, trivial], intros bs hbs, simp only [set.mem_preimage, ge_iff_le, finset.le_iff_subset] at hu, - have : tendsto (λ t : finset (Σ b, γ b), ∑ p in t.filter (λ p, p.1 ∈ bs), f p) - at_top (𝓝 $ ∑ b in bs, g b), - { simp only [← sigma_preimage_mk, sum_sigma], - refine tendsto_finset_sum _ (λ b hb, _), - change tendsto (λ t, (λ t, ∑ s in t, f ⟨b, s⟩) (preimage t (sigma.mk b) _)) at_top (𝓝 (g b)), + have : tendsto (λ t : finset (Σ b, γ b), ∏ p in t.filter (λ p, p.1 ∈ bs), f p) + at_top (𝓝 $ ∏ b in bs, g b), + { simp only [← sigma_preimage_mk, prod_sigma], + refine tendsto_finset_prod _ (λ b hb, _), + change tendsto (λ t, (λ t, ∏ s in t, f ⟨b, s⟩) (preimage t (sigma.mk b) _)) at_top (𝓝 (g b)), exact tendsto.comp (hf b) (tendsto_finset_preimage_at_top_at_top _) }, refine hsc.mem_of_tendsto this (eventually_at_top.2 ⟨u, λ t ht, hu _ (λ x hx, _)⟩), exact mem_filter.2 ⟨ht hx, hbs $ mem_image_of_mem _ hx⟩ end -/-- 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`. -/ -lemma has_sum.prod_fiberwise [regular_space α] {f : β × γ → α} {g : β → α} {a : α} - (ha : has_sum f a) (hf : ∀b, has_sum (λc, f (b, c)) (g b)) : - has_sum g a := -has_sum.sigma ((equiv.sigma_equiv_prod β γ).has_sum_iff.2 ha) hf - -lemma summable.sigma' [regular_space α] {γ : β → Type*} {f : (Σb:β, γ b) → α} - (ha : summable f) (hf : ∀b, summable (λc, f ⟨b, c⟩)) : - summable (λb, ∑'c, f ⟨b, c⟩) := -(ha.has_sum.sigma (assume b, (hf b).has_sum)).summable - -lemma has_sum.sigma_of_has_sum [t3_space α] {γ : β → Type*} {f : (Σ b:β, γ b) → α} {g : β → α} - {a : α} (ha : has_sum g a) (hf : ∀b, has_sum (λc, f ⟨b, c⟩) (g b)) (hf' : summable f) : - has_sum f a := -by simpa [(hf'.has_sum.sigma hf).unique ha] using hf'.has_sum - -/-- Version of `has_sum.update` for `add_comm_monoid` rather than `add_comm_group`. -Rather than showing that `f.update` has a specific sum in terms of `has_sum`, +/-- If a series `f` on `β × γ` has product `a` and for each `b` the restriction of `f` to `{b} × γ` +has product `g b`, then the series `g` has product `a`. -/ +@[to_additive has_sum.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`."] +lemma has_prod.prod_fiberwise [regular_space α] {f : β × γ → α} (ha : has_prod f a) + (hf : ∀ b, has_prod (λ c, f (b, c)) (g b)) : has_prod g a := +has_prod.sigma ((equiv.sigma_equiv_prod β γ).has_prod_iff.2 ha) hf + +@[to_additive] lemma prodable.sigma' [regular_space α] {γ : β → Type*} + {f : (Σ b, γ b) → α} (ha : prodable f) (hf : ∀ b, prodable (λ c, f ⟨b, c⟩)) : + prodable (λ b, ∏' c, f ⟨b, c⟩) := +(ha.has_prod.sigma $ λ b, (hf b).has_prod).prodable + +@[to_additive] lemma has_prod.sigma_of_has_prod [t3_space α] {γ : β → Type*} {f : (Σ b, γ b) → α} + (ha : has_prod g a) (hf : ∀ b, has_prod (λ c, f ⟨b, c⟩) (g b)) (hf' : prodable f) : + has_prod f a := +by simpa [(hf'.has_prod.sigma hf).unique ha] using hf'.has_prod + +/-- Version of `has_prod.update` for `comm_monoid` rather than `comm_group`. +Rather than showing that `f.update` has a specific sum in terms of `has_prod`, it gives a relationship between the sums of `f` and `f.update` given that both exist. -/ -lemma has_sum.update' {α β : Type*} [topological_space α] [add_comm_monoid α] [t2_space α] - [has_continuous_add α] {f : β → α} {a a' : α} (hf : has_sum f a) - (b : β) (x : α) (hf' : has_sum (f.update b x) a') : a + x = a' + f b := +@[to_additive "Version of `has_sum.update` for `add_comm_monoid` rather than `add_comm_group`. +Rather than showing that `f.update` has a specific sum in terms of `has_sum`, +it gives a relationship between the sums of `f` and `f.update` given that both exist."] +lemma has_prod.update' [t2_space α] {f : β → α} (hf : has_prod f a) (b : β) (x : α) + (hf' : has_prod (f.update b x) a') : a * x = a' * f b := begin - have : ∀ b', f b' + ite (b' = b) x 0 = f.update b x b' + ite (b' = b) (f b) 0, + have : ∀ b', f b' * ite (b' = b) x 1 = f.update b x b' * ite (b' = b) (f b) 1, { 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 ((has_sum_ite_eq b x)), + have h := hf.mul ((has_prod_ite_eq b x)), simp_rw this at h, - exact has_sum.unique h (hf'.add (has_sum_ite_eq b (f b))) + exact has_prod.unique h (hf'.mul $ has_prod_ite_eq b (f b)), end -/-- Version of `has_sum_ite_sub_has_sum` for `add_comm_monoid` rather than `add_comm_group`. +/-- Version of `has_prod_ite_div_has_prod` for `comm_monoid` rather than `comm_group`. +Rather than showing that the `ite` expression has a specific sum in terms of `has_prod`, +it gives a relationship between the sums of `f` and `ite (n = b) 1 (f n)` given that both exist. -/ +@[to_additive +"Version of `has_sum_ite_sub_has_sum` for `add_comm_monoid` rather than `add_comm_group`. Rather than showing that the `ite` expression has a specific sum in terms of `has_sum`, -it gives a relationship between the sums of `f` and `ite (n = b) 0 (f n)` given that both exist. -/ -lemma eq_add_of_has_sum_ite {α β : Type*} [topological_space α] [add_comm_monoid α] - [t2_space α] [has_continuous_add α] {f : β → α} {a : α} (hf : has_sum f a) (b : β) (a' : α) - (hf' : has_sum (λ n, ite (n = b) 0 (f n)) a') : a = a' + f b := +it gives a relationship between the sums of `f` and `ite (n = b) 0 (f n)` given that both exist."] +lemma eq_mul_of_has_prod_ite [t2_space α] (hf : has_prod f a) (b : β) (a' : α) + (hf' : has_prod (λ n, ite (n = b) 1 (f n)) a') : a = a' * f b := begin - refine (add_zero a).symm.trans (hf.update' b 0 _), + refine (mul_one a).symm.trans (hf.update' b 1 _), convert hf', - exact funext (f.update_apply b 0), + exact funext (f.update_apply b 1), end -end has_sum +end has_prod -section tsum -variables [add_comm_monoid α] [topological_space α] +section tprod +variables [comm_monoid α] [topological_space α] {f g : β → α} {a a₁ a₂ : α} -lemma tsum_congr_subtype (f : β → α) {s t : set β} (h : s = t) : - ∑' (x : s), f x = ∑' (x : t), f x := -by rw h +@[to_additive] lemma tprod_congr_subtype (f : β → α) {s t : set β} (h : s = t) : + ∏' x : s, f x = ∏' x : t, f x := by rw h -lemma tsum_zero' (hz : is_closed ({0} : set α)) : ∑' b : β, (0 : α) = 0 := +@[to_additive] lemma tprod_one' (hz : is_closed ({1} : set α)) : ∏' b : β, (1 : α) = 1 := begin classical, - rw [tsum, dif_pos summable_zero], - suffices : ∀ (x : α), has_sum (λ (b : β), (0 : α)) x → x = 0, + rw [tprod, dif_pos prodable_one], + suffices : ∀ (x : α), has_prod (λ (b : β), (1 : α)) x → x = 1, { exact this _ (classical.some_spec _) }, intros x hx, contrapose! hx, - simp only [has_sum, tendsto_nhds, finset.sum_const_zero, filter.mem_at_top_sets, ge_iff_le, + simp only [has_prod, tendsto_nhds, finset.prod_const_one, filter.mem_at_top_sets, ge_iff_le, finset.le_eq_subset, set.mem_preimage, not_forall, not_exists, exists_prop, exists_and_distrib_right], - refine ⟨{0}ᶜ, ⟨is_open_compl_iff.mpr hz, _⟩, λ y, ⟨⟨y, subset_refl _⟩, _⟩⟩, + refine ⟨{1}ᶜ, ⟨is_open_compl_iff.mpr hz, _⟩, λ y, ⟨⟨y, subset_refl _⟩, _⟩⟩, { simpa using hx }, { simp } end -@[simp] lemma tsum_zero [t1_space α] : ∑' b : β, (0 : α) = 0 := tsum_zero' is_closed_singleton +@[simp, to_additive] lemma tprod_one [t1_space α] : ∏' b : β, (1 : α) = 1 := +tprod_one' is_closed_singleton -variables [t2_space α] {f g : β → α} {a a₁ a₂ : α} +@[to_additive] lemma tprod_congr (hfg : ∀ b, f b = g b) : ∏' b, f b = ∏' b, g b := +congr_arg tprod $ funext hfg -lemma has_sum.tsum_eq (ha : has_sum f a) : ∑'b, f b = a := -(summable.has_sum ⟨a, ha⟩).unique ha +variables [t2_space α] {s : finset β} -lemma summable.has_sum_iff (h : summable f) : has_sum f a ↔ ∑'b, f b = a := -iff.intro has_sum.tsum_eq (assume eq, eq ▸ h.has_sum) +@[to_additive] lemma has_prod.tprod_eq (ha : has_prod f a) : ∏' b, f b = a := +(prodable.has_prod ⟨a, ha⟩).unique ha -@[simp] lemma tsum_empty [is_empty β] : ∑'b, f b = 0 := has_sum_empty.tsum_eq +@[to_additive] lemma prodable.has_prod_iff (h : prodable f) : has_prod f a ↔ ∏' b, f b = a := +iff.intro has_prod.tprod_eq (assume eq, eq ▸ h.has_prod) -lemma tsum_eq_sum {f : β → α} {s : finset β} (hf : ∀b∉s, f b = 0) : - ∑' b, f b = ∑ b in s, f b := -(has_sum_sum_of_ne_finset_zero hf).tsum_eq +@[simp, to_additive] lemma tprod_empty [is_empty β] : ∏' b, f b = 1 := has_prod_empty.tprod_eq -lemma sum_eq_tsum_indicator (f : β → α) (s : finset β) : - ∑ x in s, f x = ∑' x, set.indicator ↑s f x := -have ∀ x ∉ s, set.indicator ↑s f x = 0, -from λ x hx, set.indicator_apply_eq_zero.2 (λ hx', (hx $ finset.mem_coe.1 hx').elim), -(finset.sum_congr rfl (λ x hx, (set.indicator_apply_eq_self.2 $ - λ hx', (hx' $ finset.mem_coe.2 hx).elim).symm)).trans (tsum_eq_sum this).symm +@[to_additive] lemma tprod_eq_prod (hf : ∀ b ∉ s, f b = 1) : ∏' b, f b = ∏ b in s, f b := +(has_prod_prod_of_ne_finset_one hf).tprod_eq -lemma tsum_congr {α β : Type*} [add_comm_monoid α] [topological_space α] - {f g : β → α} (hfg : ∀ b, f b = g b) : ∑' b, f b = ∑' b, g b := -congr_arg tsum (funext hfg) +@[to_additive] lemma prod_eq_tprod_mul_indicator (f : β → α) (s : finset β) : + ∏ x in s, f x = ∏' x, set.mul_indicator ↑s f x := +have ∀ x ∉ s, set.mul_indicator ↑s f x = 1, +from λ x hx, set.mul_indicator_apply_eq_one.2 (λ hx', (hx $ finset.mem_coe.1 hx').elim), +(finset.prod_congr rfl (λ x hx, (set.mul_indicator_apply_eq_self.2 $ + λ hx', (hx' $ finset.mem_coe.2 hx).elim).symm)).trans (tprod_eq_prod this).symm -lemma tsum_fintype [fintype β] (f : β → α) : ∑'b, f b = ∑ b, f b := -(has_sum_fintype f).tsum_eq +@[to_additive] lemma tprod_fintype [fintype β] (f : β → α) : ∏' b, f b = ∏ b, f b := +(has_prod_fintype f).tprod_eq -lemma tsum_bool (f : bool → α) : ∑' i : bool, f i = f false + f true := -by { rw [tsum_fintype, finset.sum_eq_add]; simp } +@[to_additive] lemma tprod_bool (f : bool → α) : ∏' i : bool, f i = f false * f true := +by rw [tprod_fintype, finset.prod_eq_mul]; simp -lemma tsum_eq_single {f : β → α} (b : β) (hf : ∀b' ≠ b, f b' = 0) : - ∑'b, f b = f b := -(has_sum_single b hf).tsum_eq +@[to_additive] lemma tprod_eq_single (b : β) (hf : ∀ b' ≠ b, f b' = 1) : ∏' b, f b = f b := +(has_prod_single b hf).tprod_eq -lemma tsum_tsum_eq_single (f : β → γ → α) (b : β) (c : γ) (hfb : ∀ b' ≠ b, f b' c = 0) - (hfc : ∀ (b' : β) (c' : γ), c' ≠ c → f b' c' = 0) : - ∑' b' c', f b' c' = f b c := -calc ∑' b' c', f b' c' = ∑' b', f b' c : tsum_congr $ λ b', tsum_eq_single _ (hfc b') -... = f b c : tsum_eq_single _ hfb +@[to_additive] lemma tprod_tprod_eq_single (f : β → γ → α) (b : β) (c : γ) + (hfb : ∀ b' ≠ b, f b' c = 1) (hfc : ∀ b' c', c' ≠ c → f b' c' = 1) : + ∏' b' c', f b' c' = f b c := +calc ∏' b' c', f b' c' = ∏' b', f b' c : tprod_congr $ λ b', tprod_eq_single _ (hfc b') +... = f b c : tprod_eq_single _ hfb -@[simp] lemma tsum_ite_eq (b : β) [decidable_pred (= b)] (a : α) : - ∑' b', (if b' = b then a else 0) = a := -(has_sum_ite_eq b a).tsum_eq +@[simp, to_additive] lemma tprod_ite_eq (b : β) [decidable_pred (= b)] (a : α) : + ∏' b', (if b' = b then a else 1) = a := +(has_prod_ite_eq b a).tprod_eq -@[simp] lemma tsum_pi_single [decidable_eq β] (b : β) (a : α) : - ∑' b', pi.single b a b' = a := -(has_sum_pi_single b a).tsum_eq +@[simp, to_additive] lemma tprod_pi_mul_single [decidable_eq β] (b : β) (a : α) : + ∏' b', pi.mul_single b a b' = a := +(has_prod_pi_mul_single b a).tprod_eq -lemma 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 := +@[to_additive] lemma 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] -lemma 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 := +@[to_additive] lemma 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] -lemma function.surjective.tsum_eq_tsum_of_has_sum_iff_has_sum {α' : Type*} [add_comm_monoid α'] - [topological_space α'] {e : α' → α} (hes : function.surjective e) (h0 : e 0 = 0) - {f : β → α} {g : γ → α'} - (h : ∀ {a}, has_sum f (e a) ↔ has_sum g a) : - ∑' b, f b = e (∑' c, g c) := +@[to_additive] lemma function.surjective.tprod_eq_tprod_of_has_prod_iff_has_prod [comm_monoid α'] + [topological_space α'] {e : α' → α} (hes : function.surjective e) (h1 : e 1 = 1) {g : γ → α'} + (h : ∀ {a}, has_prod f (e a) ↔ has_prod g a) : + ∏' b, f b = e (∏' c, g c) := by_cases - (assume : summable g, (h.mpr this.has_sum).tsum_eq) - (assume hg : ¬ summable g, - have hf : ¬ summable f, from mt (hes.summable_iff_of_has_sum_iff @h).1 hg, - by simp [tsum, hf, hg, h0]) - -lemma tsum_eq_tsum_of_has_sum_iff_has_sum {f : β → α} {g : γ → α} - (h : ∀{a}, has_sum f a ↔ has_sum g a) : - ∑'b, f b = ∑'c, g c := -surjective_id.tsum_eq_tsum_of_has_sum_iff_has_sum rfl @h - -lemma equiv.tsum_eq (j : γ ≃ β) (f : β → α) : ∑'c, f (j c) = ∑'b, f b := -tsum_eq_tsum_of_has_sum_iff_has_sum $ λ a, j.has_sum_iff - -lemma 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 := -tsum_eq_tsum_of_has_sum_iff_has_sum $ λ _, e.has_sum_iff_of_support he - -lemma tsum_eq_tsum_of_ne_zero_bij {g : γ → α} (i : support g → β) - (hi : ∀ ⦃x y⦄, i x = i y → (x : γ) = y) - (hf : support f ⊆ set.range i) (hfg : ∀ x, f (i x) = g x) : - ∑' x, f x = ∑' y, g y := -tsum_eq_tsum_of_has_sum_iff_has_sum $ λ _, has_sum_iff_has_sum_of_ne_zero_bij i hi hf hfg - -/-! ### `tsum` on subsets -/ - -@[simp] lemma finset.tsum_subtype (s : finset β) (f : β → α) : - ∑' x : {x // x ∈ s}, f x = ∑ x in s, f x := -(s.has_sum f).tsum_eq - -@[simp] lemma finset.tsum_subtype' (s : finset β) (f : β → α) : - ∑' x : (s : set β), f x = ∑ x in s, f x := -s.tsum_subtype f - -lemma tsum_subtype (s : set β) (f : β → α) : - ∑' x : s, f x = ∑' x, s.indicator f x := -tsum_eq_tsum_of_has_sum_iff_has_sum $ λ _, has_sum_subtype_iff_indicator - -lemma tsum_subtype_eq_of_support_subset {f : β → α} {s : set β} (hs : support f ⊆ s) : - ∑' x : s, f x = ∑' x, f x := -tsum_eq_tsum_of_has_sum_iff_has_sum $ λ x, has_sum_subtype_iff_of_support_subset hs - -@[simp] lemma tsum_univ (f : β → α) : ∑' x : (set.univ : set β), f x = ∑' x, f x := -tsum_subtype_eq_of_support_subset $ set.subset_univ _ - -@[simp] lemma tsum_singleton (b : β) (f : β → α) : - ∑' x : ({b} : set β), f x = f b := + (assume : prodable g, (h.mpr this.has_prod).tprod_eq) + (assume hg : ¬ prodable g, + have hf : ¬ prodable f, from mt (hes.prodable_iff_of_has_prod_iff @h).1 hg, + by simp [tprod, hf, hg, h1]) + +@[to_additive] +lemma tprod_eq_tprod_of_has_prod_iff_has_prod {g : γ → α} (h : ∀ {a}, has_prod f a ↔ has_prod g a) : + ∏' b, f b = ∏'c, g c := +surjective_id.tprod_eq_tprod_of_has_prod_iff_has_prod rfl @h + +@[to_additive] lemma equiv.tprod_eq (j : γ ≃ β) (f : β → α) : ∏'c, f (j c) = ∏' b, f b := +tprod_eq_tprod_of_has_prod_iff_has_prod $ λ a, j.has_prod_iff + +@[to_additive] lemma equiv.tprod_eq_tprod_of_mul_support {g : γ → α} + (e : mul_support f ≃ mul_support g) (he : ∀ x, g (e x) = f x) : + (∏' x, f x) = ∏' y, g y := +tprod_eq_tprod_of_has_prod_iff_has_prod $ λ _, e.has_prod_iff_of_mul_support he + +@[to_additive] +lemma tprod_eq_tprod_of_ne_one_bij {g : γ → α} (i : mul_support g → β) + (hi : ∀ ⦃x y⦄, i x = i y → (x : γ) = y) (hf : mul_support f ⊆ set.range i) + (hfg : ∀ x, f (i x) = g x) : + ∏' x, f x = ∏' y, g y := +tprod_eq_tprod_of_has_prod_iff_has_prod $ λ _, has_prod_iff_has_prod_of_ne_one_bij i hi hf hfg + +/-! ### `tprod` on subsets -/ + +@[simp, to_additive] lemma finset.tprod_subtype (s : finset β) (f : β → α) : + ∏' x : {x // x ∈ s}, f x = ∏ x in s, f x := +(s.has_prod f).tprod_eq + +@[simp, to_additive] lemma finset.tprod_subtype' (s : finset β) (f : β → α) : + ∏' x : (s : set β), f x = ∏ x in s, f x := +s.tprod_subtype f + +@[to_additive] lemma tprod_subtype (s : set β) (f : β → α) : + ∏' x : s, f x = ∏' x, s.mul_indicator f x := +tprod_eq_tprod_of_has_prod_iff_has_prod $ λ _, has_prod_subtype_iff_mul_indicator + +@[to_additive] +lemma tprod_subtype_eq_of_mul_support_subset {s : set β} (hs : mul_support f ⊆ s) : + ∏' x : s, f x = ∏' x, f x := +tprod_eq_tprod_of_has_prod_iff_has_prod $ λ x, has_prod_subtype_iff_of_mul_support_subset hs + +@[simp, to_additive] lemma tprod_univ (f : β → α) : + ∏' x : (set.univ : set β), f x = ∏' x, f x := +tprod_subtype_eq_of_mul_support_subset $ set.subset_univ _ + +@[simp, to_additive] lemma tprod_singleton (b : β) (f : β → α) : ∏' x : ({b} : set β), f x = f b := begin - rw [tsum_subtype, tsum_eq_single b], + rw [tprod_subtype, tprod_eq_single b], { simp }, { intros b' hb', - rw set.indicator_of_not_mem, + rw set.mul_indicator_of_not_mem, rwa set.mem_singleton_iff }, { apply_instance } end -lemma tsum_image {g : γ → β} (f : β → α) {s : set γ} (hg : set.inj_on g s) : - ∑' x : g '' s, f x = ∑' x : s, f (g x) := -((equiv.set.image_of_inj_on _ _ hg).tsum_eq (λ x, f x)).symm +@[to_additive] lemma tprod_image {g : γ → β} (f : β → α) {s : set γ} (hg : set.inj_on g s) : + ∏' x : g '' s, f x = ∏' x : s, f (g x) := +((equiv.set.image_of_inj_on _ _ hg).tprod_eq (λ x, f x)).symm -lemma 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.inj_on _), tsum_univ (f ∘ g)] +@[to_additive] lemma 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.inj_on _), tprod_univ (f ∘ g)] -section has_continuous_add -variable [has_continuous_add α] +section has_continuous_mul +variable [has_continuous_mul α] -lemma tsum_add (hf : summable f) (hg : summable g) : ∑'b, (f b + g b) = (∑'b, f b) + (∑'b, g b) := -(hf.has_sum.add hg.has_sum).tsum_eq +@[to_additive] lemma tprod_mul (hf : prodable f) (hg : prodable g) : + ∏' b, f b * g b = (∏' b, f b) * (∏' b, g b) := +(hf.has_prod.mul hg.has_prod).tprod_eq -lemma 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 := -(has_sum_sum $ assume i hi, (hf i hi).has_sum).tsum_eq +@[to_additive tsum_sum] +lemma tprod_prod'' {f : γ → β → α} {s : finset γ} (hf : ∀ i ∈ s, prodable (f i)) : + ∏' b, ∏ i in s, f i b = ∏ i in s, ∏' b, f i b := +(has_prod_prod $ λ i hi, (hf i hi).has_prod).tprod_eq -/-- Version of `tsum_eq_add_tsum_ite` for `add_comm_monoid` rather than `add_comm_group`. +/-- Version of `tprod_eq_mul_tprod_ite` for `comm_monoid` rather than `comm_group`. Requires a different convergence assumption involving `function.update`. -/ -lemma tsum_eq_add_tsum_ite' {f : β → α} (b : β) (hf : summable (f.update b 0)) : - ∑' x, f x = f b + ∑' x, ite (x = b) 0 (f x) := -calc ∑' x, f x = ∑' x, ((ite (x = b) (f x) 0) + (f.update b 0 x)) : - tsum_congr (λ n, by split_ifs; simp [function.update_apply, h]) - ... = ∑' x, ite (x = b) (f x) 0 + ∑' x, f.update b 0 x : - tsum_add ⟨ite (b = b) (f b) 0, has_sum_single b (λ b hb, if_neg hb)⟩ (hf) - ... = (ite (b = b) (f b) 0) + ∑' x, f.update b 0 x : - by { congr, exact (tsum_eq_single b (λ b' hb', if_neg hb')) } - ... = f b + ∑' x, ite (x = b) 0 (f x) : +@[to_additive "Version of `tsum_eq_mul_tsum_ite` for `add_comm_monoid` rather +than `add_comm_group`. Requires a different convergence assumption involving `function.update`."] +lemma tprod_eq_mul_tprod_ite' (b : β) (hf : prodable (f.update b 1)) : + ∏' x, f x = f b * ∏' x, ite (x = b) 1 (f x) := +calc ∏' x, f x = ∏' x, ((ite (x = b) (f x) 1) * (f.update b 1 x)) : + tprod_congr (λ n, by split_ifs; simp [function.update_apply, h]) + ... = (∏' x, ite (x = b) (f x) 1) * ∏' x, f.update b 1 x : + tprod_mul ⟨ite (b = b) (f b) 1, has_prod_single b (λ b hb, if_neg hb)⟩ hf + ... = ite (b = b) (f b) 1 * ∏' x, f.update b 1 x : + by { congr, exact (tprod_eq_single b (λ b' hb', if_neg hb')) } + ... = f b * ∏' x, ite (x = b) 1 (f x) : by simp only [function.update, eq_self_iff_true, if_true, eq_rec_constant, dite_eq_ite] -variables [add_comm_monoid δ] [topological_space δ] [t3_space δ] [has_continuous_add δ] +variables [comm_monoid δ] [topological_space δ] [t3_space δ] [has_continuous_mul δ] -lemma tsum_sigma' {γ : β → Type*} {f : (Σb:β, γ b) → δ} (h₁ : ∀b, summable (λc, f ⟨b, c⟩)) - (h₂ : summable f) : ∑'p, f p = ∑'b c, f ⟨b, c⟩ := -(h₂.has_sum.sigma (assume b, (h₁ b).has_sum)).tsum_eq.symm +@[to_additive] +lemma tprod_sigma' {γ : β → Type*} {f : (Σ b, γ b) → δ} (h₁ : ∀ b, prodable (λ c, f ⟨b, c⟩)) + (h₂ : prodable f) : ∏' p, f p = ∏' b c, f ⟨b, c⟩ := +(h₂.has_prod.sigma $ λ b, (h₁ b).has_prod).tprod_eq.symm -lemma tsum_prod' {f : β × γ → δ} (h : summable f) (h₁ : ∀b, summable (λc, f (b, c))) : - ∑'p, f p = ∑'b c, f (b, c) := -(h.has_sum.prod_fiberwise (assume b, (h₁ b).has_sum)).tsum_eq.symm +@[to_additive tsum_prod'] +lemma tprod_prod' {f : β × γ → δ} (h : prodable f) (h₁ : ∀ b, prodable (λ c, f (b, c))) : + ∏' p, f p = ∏' b c, f (b, c) := +(h.has_prod.prod_fiberwise $ λ b, (h₁ b).has_prod).tprod_eq.symm -lemma tsum_comm' {f : β → γ → δ} (h : summable (function.uncurry f)) (h₁ : ∀b, summable (f b)) - (h₂ : ∀ c, summable (λ b, f b c)) : - ∑' c b, f b c = ∑' b c, f b c := +@[to_additive] +lemma tprod_comm' {f : β → γ → δ} (h : prodable (uncurry f)) (h₁ : ∀ b, prodable (f b)) + (h₂ : ∀ c, prodable (λ b, f b c)) : + ∏' c b, f b c = ∏' b c, f b c := begin - erw [← tsum_prod' h h₁, ← tsum_prod' h.prod_symm h₂, ← (equiv.prod_comm γ β).tsum_eq (uncurry f)], + erw [←tprod_prod' h h₁, ←tprod_prod' h.prod_symm h₂, ←(equiv.prod_comm γ β).tprod_eq (uncurry f)], refl end -end has_continuous_add +end has_continuous_mul open encodable section encodable variable [encodable γ] -/-- You can compute a sum over an encodably type by summing over the natural numbers and - taking a supremum. This is useful for outer measures. -/ -theorem tsum_supr_decode₂ [complete_lattice β] (m : β → α) (m0 : m ⊥ = 0) - (s : γ → β) : ∑' i : ℕ, m (⨆ b ∈ decode₂ γ i, s b) = ∑' b : γ, m (s b) := +/-- You can compute a product over an encodable type by multiplying over the natural numbers and +taking a supremum. This is useful for outer measures. -/ +@[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."] +lemma tprod_supr_decode₂ [complete_lattice β] (m : β → α) (m1 : m ⊥ = 1) (s : γ → β) : + ∏' i : ℕ, m (⨆ b ∈ decode₂ γ i, s b) = ∏' b : γ, m (s b) := begin - have H : ∀ n, m (⨆ b ∈ decode₂ γ n, s b) ≠ 0 → (decode₂ γ n).is_some, + have H : ∀ n, m (⨆ b ∈ decode₂ γ n, s b) ≠ 1 → (decode₂ γ n).is_some, { intros n h, cases decode₂ γ n with b, - { refine (h $ by simp [m0]).elim }, + { refine (h $ by simp [m1]).elim }, { exact rfl } }, - symmetry, refine tsum_eq_tsum_of_ne_zero_bij (λ a, option.get (H a.1 a.2)) _ _ _, + symmetry, refine tprod_eq_tprod_of_ne_one_bij (λ a, option.get (H a.1 a.2)) _ _ _, { rintros ⟨m, hm⟩ ⟨n, hn⟩ e, have := mem_decode₂.1 (option.get_mem (H n hn)), rwa [← e, mem_decode₂.1 (option.get_mem (H m hm))] at this }, { intros b h, refine ⟨⟨encode b, _⟩, _⟩, - { simp only [mem_support, encodek₂] at h ⊢, convert h, simp [set.ext_iff, encodek₂] }, + { simp only [mem_mul_support, encodek₂] at h ⊢, convert h, simp [set.ext_iff, encodek₂] }, { exact option.get_of_mem _ (encodek₂ _) } }, { rintros ⟨n, h⟩, dsimp only [subtype.coe_mk], transitivity, swap, @@ -625,10 +660,11 @@ begin congr, simp [ext_iff, -option.some_get] } end -/-- `tsum_supr_decode₂` specialized to the complete lattice of sets. -/ -theorem tsum_Union_decode₂ (m : set β → α) (m0 : m ∅ = 0) - (s : γ → set β) : ∑' i, m (⋃ b ∈ decode₂ γ i, s b) = ∑' b, m (s b) := -tsum_supr_decode₂ m m0 s +/-- `tprod_supr_decode₂` specialized to the complete lattice of sets. -/ +@[to_additive "`tsum_supr_decode₂` specialized to the complete lattice of sets."] +lemma tprod_Union_decode₂ (m : set β → α) (m1 : m ∅ = 1) (s : γ → set β) : + ∏' i, m (⋃ b ∈ decode₂ γ i, s b) = ∏' b, m (s b) := +tprod_supr_decode₂ m m1 s end encodable @@ -641,169 +677,175 @@ end encodable section countable variables [countable γ] -/-- If a function is countably sub-additive then it is sub-additive on countable types -/ -theorem rel_supr_tsum [complete_lattice β] (m : β → α) (m0 : m ⊥ = 0) - (R : α → α → Prop) (m_supr : ∀(s : ℕ → β), R (m (⨆ i, s i)) ∑' i, m (s i)) - (s : γ → β) : R (m (⨆ b : γ, s b)) ∑' b : γ, m (s b) := -by { casesI nonempty_encodable γ, rw [←supr_decode₂, ←tsum_supr_decode₂ _ m0 s], exact m_supr _ } - -/-- If a function is countably sub-additive then it is sub-additive on finite sets -/ -theorem rel_supr_sum [complete_lattice β] (m : β → α) (m0 : m ⊥ = 0) - (R : α → α → Prop) (m_supr : ∀(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 [supr_subtype', ←finset.tsum_subtype], exact rel_supr_tsum m m0 R m_supr _ } - -/-- If a function is countably sub-additive then it is binary sub-additive -/ -theorem rel_sup_add [complete_lattice β] (m : β → α) (m0 : m ⊥ = 0) - (R : α → α → Prop) (m_supr : ∀(s : ℕ → β), R (m (⨆ i, s i)) (∑' i, m (s i))) - (s₁ s₂ : β) : R (m (s₁ ⊔ s₂)) (m s₁ + m s₂) := +/-- If a function is countably submultiplicative then it is submultiplicative on countable types. -/ +@[to_additive +"If a function is countably subadditive then it is subadditive on countable types."] +lemma rel_supr_tprod [complete_lattice β] (m : β → α) (m1 : m ⊥ = 1) (R : α → α → Prop) + (m_supr : ∀ s : ℕ → β, R (m (⨆ i, s i)) ∏' i, m (s i)) (s : γ → β) : + R (m (⨆ b : γ, s b)) ∏' b : γ, m (s b) := +by { casesI nonempty_encodable γ, rw [←supr_decode₂, ←tprod_supr_decode₂ _ m1 s], exact m_supr _ } + +/-- If a function is countably submultiplicative then it is submultiplicative on finite sets. -/ +@[to_additive "If a function is countably subadditive then it is subadditive on finite sets."] +lemma rel_supr_prod [complete_lattice β] (m : β → α) (m1 : m ⊥ = 1) (R : α → α → Prop) + (m_supr : ∀ 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 [supr_subtype', ←finset.tprod_subtype], exact rel_supr_tprod m m1 R m_supr _ } + +/-- If a function is countably submultiplicative then it is binary submultiplicative. -/ +@[to_additive "If a function is countably subadditive then it is binary subadditive."] +lemma rel_sup_mul [complete_lattice β] (m : β → α) (m1 : m ⊥ = 1) (R : α → α → Prop) + (m_supr : ∀ s : ℕ → β, R (m (⨆ i, s i)) (∏' i, m (s i))) (s₁ s₂ : β) : + R (m (s₁ ⊔ s₂)) (m s₁ * m s₂) := begin - convert rel_supr_tsum m m0 R m_supr (λ b, cond b s₁ s₂), + convert rel_supr_tprod m m1 R m_supr (λ b, cond b s₁ s₂), { simp only [supr_bool_eq, cond] }, - { rw [tsum_fintype, fintype.sum_bool, cond, cond] } + { rw [tprod_fintype, fintype.prod_bool, cond, cond] } end end countable -variables [has_continuous_add α] +variables [has_continuous_mul α] -lemma tsum_add_tsum_compl {s : set β} (hs : summable (f ∘ coe : s → α)) - (hsc : summable (f ∘ coe : sᶜ → α)) : - (∑' x : s, f x) + (∑' x : sᶜ, f x) = ∑' x, f x := -(hs.has_sum.add_compl hsc.has_sum).tsum_eq.symm +@[to_additive] lemma tprod_mul_tprod_compl {s : set β} (hs : prodable (f ∘ coe : s → α)) + (hsc : prodable (f ∘ coe : sᶜ → α)) : + (∏' x : s, f x) * (∏' x : sᶜ, f x) = ∏' x, f x := +(hs.has_prod.mul_compl hsc.has_prod).tprod_eq.symm -lemma tsum_union_disjoint {s t : set β} (hd : disjoint s t) - (hs : summable (f ∘ coe : s → α)) (ht : summable (f ∘ coe : t → α)) : - (∑' x : s ∪ t, f x) = (∑' x : s, f x) + (∑' x : t, f x) := -(hs.has_sum.add_disjoint hd ht.has_sum).tsum_eq +@[to_additive] lemma tprod_union_disjoint {s t : set β} (hd : disjoint s t) + (hs : prodable (f ∘ coe : s → α)) (ht : prodable (f ∘ coe : t → α)) : + (∏' x : s ∪ t, f x) = (∏' x : s, f x) * (∏' x : t, f x) := +(hs.has_prod.mul_disjoint hd ht.has_prod).tprod_eq -lemma tsum_finset_bUnion_disjoint {ι} {s : finset ι} {t : ι → set β} +@[to_additive] lemma tprod_finset_bUnion_disjoint {ι} {s : finset ι} {t : ι → set β} (hd : (s : set ι).pairwise (disjoint on t)) - (hf : ∀ i ∈ s, summable (f ∘ coe : t i → α)) : - (∑' x : (⋃ i ∈ s, t i), f x) = ∑ i in s, ∑' x : t i, f x := -(has_sum_sum_disjoint _ hd (λ i hi, (hf i hi).has_sum)).tsum_eq + (hf : ∀ i ∈ s, prodable (f ∘ coe : t i → α)) : + ∏' x : (⋃ i ∈ s, t i), f x = ∏ i in s, ∏' x : t i, f x := +(has_prod_prod_disjoint _ hd (λ i hi, (hf i hi).has_prod)).tprod_eq -lemma tsum_even_add_odd {f : ℕ → α} (he : summable (λ k, f (2 * k))) - (ho : summable (λ k, f (2 * k + 1))) : - (∑' k, f (2 * k)) + (∑' k, f (2 * k + 1)) = ∑' k, f k := -(he.has_sum.even_add_odd ho.has_sum).tsum_eq.symm +@[to_additive] lemma tprod_even_mul_odd {f : ℕ → α} (he : prodable (λ k, f (2 * k))) + (ho : prodable (λ k, f (2 * k + 1))) : + (∏' k, f (2 * k)) * (∏' k, f (2 * k + 1)) = ∏' k, f k := +(he.has_prod.even_mul_odd ho.has_prod).tprod_eq.symm -end tsum +end tprod section topological_group -variables [add_comm_group α] [topological_space α] [topological_add_group α] -variables {f g : β → α} {a a₁ a₂ : α} +variables [comm_group α] [topological_space α] [topological_group α] {f g : β → α} {a a₁ a₂ : α} -- `by simpa using` speeds up elaboration. Why? -lemma has_sum.neg (h : has_sum f a) : has_sum (λb, - f b) (- a) := -by simpa only using h.map (-add_monoid_hom.id α) continuous_neg +@[to_additive] lemma has_prod.inv (h : has_prod f a) : has_prod (λ b, (f b)⁻¹) a⁻¹ := +by simpa only using h.map (monoid_hom.id α)⁻¹ continuous_inv -lemma summable.neg (hf : summable f) : summable (λb, - f b) := -hf.has_sum.neg.summable +@[to_additive] lemma prodable.inv (hf : prodable f) : prodable (λ b, (f b)⁻¹) := +hf.has_prod.inv.prodable -lemma summable.of_neg (hf : summable (λb, - f b)) : summable f := -by simpa only [neg_neg] using hf.neg +@[to_additive] lemma prodable.of_inv (hf : prodable (λ b, (f b)⁻¹)) : prodable f := +by simpa only [inv_inv] using hf.inv -lemma summable_neg_iff : summable (λ b, - f b) ↔ summable f := -⟨summable.of_neg, summable.neg⟩ +@[to_additive] lemma prodable_inv_iff : prodable (λ b, (f b)⁻¹) ↔ prodable f := +⟨prodable.of_inv, prodable.inv⟩ -lemma has_sum.sub (hf : has_sum f a₁) (hg : has_sum g a₂) : has_sum (λb, f b - g b) (a₁ - a₂) := -by { simp only [sub_eq_add_neg], exact hf.add hg.neg } +@[to_additive] lemma has_prod.div (hf : has_prod f a₁) (hg : has_prod g a₂) : + has_prod (λ b, f b / g b) (a₁ / a₂) := +by { simp only [div_eq_mul_inv], exact hf.mul hg.inv } -lemma summable.sub (hf : summable f) (hg : summable g) : summable (λb, f b - g b) := -(hf.has_sum.sub hg.has_sum).summable +@[to_additive] lemma prodable.div (hf : prodable f) (hg : prodable g) : prodable (λ b, f b / g b) := +(hf.has_prod.div hg.has_prod).prodable -lemma summable.trans_sub (hg : summable g) (hfg : summable (λb, f b - g b)) : - summable f := -by simpa only [sub_add_cancel] using hfg.add hg +@[to_additive] lemma prodable.trans_div (hg : prodable g) (hfg : prodable (λ b, f b / g b)) : + prodable f := +by simpa only [div_mul_cancel'] using hfg.mul hg -lemma summable_iff_of_summable_sub (hfg : summable (λb, f b - g b)) : - summable f ↔ summable g := -⟨λ hf, hf.trans_sub $ by simpa only [neg_sub] using hfg.neg, λ hg, hg.trans_sub hfg⟩ +@[to_additive] lemma prodable_iff_of_prodable_div (hfg : prodable (λ b, f b / g b)) : + prodable f ↔ prodable g := +⟨λ hf, hf.trans_div $ by simpa only [inv_div] using hfg.inv, λ hg, hg.trans_div hfg⟩ -lemma has_sum.update (hf : has_sum f a₁) (b : β) [decidable_eq β] (a : α) : - has_sum (update f b a) (a - f b + a₁) := +@[to_additive] lemma has_prod.update (hf : has_prod f a₁) (b : β) [decidable_eq β] (a : α) : + has_prod (update f b a) (a / f b * a₁) := begin - convert ((has_sum_ite_eq b _).add hf), + convert (has_prod_ite_eq b _).mul hf, ext b', - by_cases h : b' = b, - { rw [h, update_same], - simp only [eq_self_iff_true, if_true, sub_add_cancel] }, - simp only [h, update_noteq, if_false, ne.def, zero_add, not_false_iff], + split_ifs, + { rw [h, update_same, div_mul_cancel'] }, + { rw [update_noteq h, one_mul] } end -lemma summable.update (hf : summable f) (b : β) [decidable_eq β] (a : α) : - summable (update f b a) := -(hf.has_sum.update b a).summable +@[to_additive] lemma prodable.update (hf : prodable f) (b : β) [decidable_eq β] (a : α) : + prodable (update f b a) := +(hf.has_prod.update b a).prodable -lemma has_sum.has_sum_compl_iff {s : set β} (hf : has_sum (f ∘ coe : s → α) a₁) : - has_sum (f ∘ coe : sᶜ → α) a₂ ↔ has_sum f (a₁ + a₂) := +@[to_additive] lemma has_prod.has_prod_compl_iff {s : set β} (hf : has_prod (f ∘ coe : s → α) a₁) : + has_prod (f ∘ coe : sᶜ → α) a₂ ↔ has_prod f (a₁ * a₂) := begin - refine ⟨λ h, hf.add_compl h, λ h, _⟩, - rw [has_sum_subtype_iff_indicator] at hf ⊢, - rw [set.indicator_compl], - simpa only [add_sub_cancel'] using h.sub hf + refine ⟨λ h, hf.mul_compl h, λ h, _⟩, + rw [has_prod_subtype_iff_mul_indicator] at hf ⊢, + rw [set.mul_indicator_compl, ←div_eq_mul_inv], + simpa only [mul_div_cancel'''] using h.div hf, end -lemma has_sum.has_sum_iff_compl {s : set β} (hf : has_sum (f ∘ coe : s → α) a₁) : - has_sum f a₂ ↔ has_sum (f ∘ coe : sᶜ → α) (a₂ - a₁) := -iff.symm $ hf.has_sum_compl_iff.trans $ by rw [add_sub_cancel'_right] +@[to_additive] lemma has_prod.has_prod_iff_compl {s : set β} (hf : has_prod (f ∘ coe : s → α) a₁) : + has_prod f a₂ ↔ has_prod (f ∘ coe : sᶜ → α) (a₂ / a₁) := +iff.symm $ hf.has_prod_compl_iff.trans $ by rw [mul_div_cancel'_right] -lemma summable.summable_compl_iff {s : set β} (hf : summable (f ∘ coe : s → α)) : - summable (f ∘ coe : sᶜ → α) ↔ summable f := -⟨λ ⟨a, ha⟩, (hf.has_sum.has_sum_compl_iff.1 ha).summable, - λ ⟨a, ha⟩, (hf.has_sum.has_sum_iff_compl.1 ha).summable⟩ +@[to_additive] lemma prodable.prodable_compl_iff {s : set β} (hf : prodable (f ∘ coe : s → α)) : + prodable (f ∘ coe : sᶜ → α) ↔ prodable f := +⟨λ ⟨a, ha⟩, (hf.has_prod.has_prod_compl_iff.1 ha).prodable, + λ ⟨a, ha⟩, (hf.has_prod.has_prod_iff_compl.1 ha).prodable⟩ -protected lemma finset.has_sum_compl_iff (s : finset β) : - has_sum (λ x : {x // x ∉ s}, f x) a ↔ has_sum f (a + ∑ i in s, f i) := -(s.has_sum f).has_sum_compl_iff.trans $ by rw [add_comm] +@[to_additive] protected lemma finset.has_prod_compl_iff (s : finset β) : + has_prod (λ x : {x // x ∉ s}, f x) a ↔ has_prod f (a * ∏ i in s, f i) := +(s.has_prod f).has_prod_compl_iff.trans $ by rw [mul_comm] -protected lemma finset.has_sum_iff_compl (s : finset β) : - has_sum f a ↔ has_sum (λ x : {x // x ∉ s}, f x) (a - ∑ i in s, f i) := -(s.has_sum f).has_sum_iff_compl +@[to_additive] protected lemma finset.has_prod_iff_compl (s : finset β) : + has_prod f a ↔ has_prod (λ x : {x // x ∉ s}, f x) (a / ∏ i in s, f i) := +(s.has_prod f).has_prod_iff_compl -protected lemma finset.summable_compl_iff (s : finset β) : - summable (λ x : {x // x ∉ s}, f x) ↔ summable f := -(s.summable f).summable_compl_iff +@[to_additive] protected lemma finset.prodable_compl_iff (s : finset β) : + prodable (λ x : {x // x ∉ s}, f x) ↔ prodable f := +(s.prodable f).prodable_compl_iff -lemma set.finite.summable_compl_iff {s : set β} (hs : s.finite) : - summable (f ∘ coe : sᶜ → α) ↔ summable f := -(hs.summable f).summable_compl_iff +@[to_additive] lemma set.finite.prodable_compl_iff {s : set β} (hs : s.finite) : + prodable (f ∘ coe : sᶜ → α) ↔ prodable f := +(hs.prodable f).prodable_compl_iff -lemma has_sum_ite_sub_has_sum [decidable_eq β] (hf : has_sum f a) (b : β) : - has_sum (λ n, ite (n = b) 0 (f n)) (a - f b) := +@[to_additive] lemma has_prod_ite_div_has_prod [decidable_eq β] (hf : has_prod f a) (b : β) : + has_prod (λ n, ite (n = b) 1 (f n)) (a / f b) := begin - convert hf.update b 0 using 1, - { ext n, rw function.update_apply, }, - { rw [sub_add_eq_add_sub, zero_add], }, + convert hf.update b 1 using 1, + { ext n, + rw function.update_apply }, + { rw [div_mul_eq_mul_div, one_mul] } end section tsum variables [t2_space α] -lemma tsum_neg : ∑'b, - f b = - ∑'b, f b := +@[to_additive] lemma tprod_inv : ∏' b, (f b)⁻¹ = (∏' b, f b)⁻¹ := begin - by_cases hf : summable f, - { exact hf.has_sum.neg.tsum_eq, }, - { simp [tsum_eq_zero_of_not_summable hf, tsum_eq_zero_of_not_summable (mt summable.of_neg hf)] }, + by_cases hf : prodable f, + { exact hf.has_prod.inv.tprod_eq }, + { simp [tprod_eq_one_of_not_prodable hf, tprod_eq_one_of_not_prodable (mt prodable.of_inv hf)] }, end -lemma tsum_sub (hf : summable f) (hg : summable g) : ∑'b, (f b - g b) = ∑'b, f b - ∑'b, g b := -(hf.has_sum.sub hg.has_sum).tsum_eq - -lemma sum_add_tsum_compl {s : finset β} (hf : summable f) : - (∑ x in s, f x) + (∑' x : (↑s : set β)ᶜ, f x) = ∑' x, f x := -((s.has_sum f).add_compl (s.summable_compl_iff.2 hf).has_sum).tsum_eq.symm - -/-- 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 -remaining terms. -/ -lemma tsum_eq_add_tsum_ite [decidable_eq β] (hf : summable f) (b : β) : - ∑' n, f n = f b + ∑' n, ite (n = b) 0 (f n) := +@[to_additive] lemma tprod_div (hf : prodable f) (hg : prodable g) : + ∏' b, (f b / g b) = (∏' b, f b) / ∏' b, g b := +(hf.has_prod.div hg.has_prod).tprod_eq + +@[to_additive] lemma prod_mul_tprod_compl {s : finset β} (hf : prodable f) : + (∏ x in s, f x) * (∏' x : (↑s : set β)ᶜ, f x) = ∏' x, f x := +((s.has_prod f).mul_compl (s.prodable_compl_iff.2 hf).has_prod).tprod_eq.symm + +/-- Let `f : β → α` be a sequence with prodable series and let `b ∈ β` be an index. This lemma +writes `∏ f n` as the sum of `f b` plus the series of the remaining terms. -/ +@[to_additive +"Let `f : β → α` be a sequence with summable series and let `b ∈ β` be an index. This lemma writes +`Σ f n` as the sum of `f b` plus the series of the remaining terms."] +lemma tprod_eq_mul_tprod_ite [decidable_eq β] (hf : prodable f) (b : β) : + ∏' n, f n = f b * ∏' n, ite (n = b) 1 (f n) := begin - rw (has_sum_ite_sub_has_sum hf.has_sum b).tsum_eq, - exact (add_sub_cancel'_right _ _).symm, + rw (has_prod_ite_div_has_prod hf.has_prod b).tprod_eq, + exact (mul_div_cancel'_right _ _).symm, end end tsum @@ -816,93 +858,96 @@ We show the formula `(∑ i in range k, f i) + (∑' i, f (i + k)) = (∑' i, f -/ section nat -lemma has_sum_nat_add_iff {f : ℕ → α} (k : ℕ) {a : α} : - has_sum (λ n, f (n + k)) a ↔ has_sum f (a + ∑ i in range k, f i) := +@[to_additive] lemma has_prod_nat_add_iff {f : ℕ → α} (k : ℕ) {a : α} : + has_prod (λ n, f (n + k)) a ↔ has_prod f (a * ∏ i in range k, f i) := begin - refine iff.trans _ ((range k).has_sum_compl_iff), - rw [← (not_mem_range_equiv k).symm.has_sum_iff], + refine iff.trans _ (range k).has_prod_compl_iff, + rw ←(not_mem_range_equiv k).symm.has_prod_iff, refl end -lemma summable_nat_add_iff {f : ℕ → α} (k : ℕ) : summable (λ n, f (n + k)) ↔ summable f := -iff.symm $ (equiv.add_right (∑ i in range k, f i)).surjective.summable_iff_of_has_sum_iff $ - λ a, (has_sum_nat_add_iff k).symm - -lemma has_sum_nat_add_iff' {f : ℕ → α} (k : ℕ) {a : α} : - has_sum (λ n, f (n + k)) (a - ∑ i in range k, f i) ↔ has_sum f a := -by simp [has_sum_nat_add_iff] - -lemma sum_add_tsum_nat_add [t2_space α] {f : ℕ → α} (k : ℕ) (h : summable f) : - (∑ i in range k, f i) + (∑' i, f (i + k)) = ∑' i, f i := -by simpa only [add_comm] using - ((has_sum_nat_add_iff k).1 ((summable_nat_add_iff k).2 h).has_sum).unique h.has_sum - -lemma tsum_eq_zero_add [t2_space α] {f : ℕ → α} (hf : summable f) : - ∑'b, f b = f 0 + ∑'b, f (b + 1) := -by simpa only [sum_range_one] using (sum_add_tsum_nat_add 1 hf).symm - -/-- For `f : ℕ → α`, then `∑' k, f (k + i)` tends to zero. This does not require a summability -assumption on `f`, as otherwise all sums are zero. -/ -lemma tendsto_sum_nat_add [t2_space α] (f : ℕ → α) : tendsto (λ i, ∑' k, f (k + i)) at_top (𝓝 0) := +@[to_additive] lemma prodable_nat_add_iff {f : ℕ → α} (k : ℕ) : + prodable (λ n, f (n + k)) ↔ prodable f := +iff.symm $ (equiv.mul_right (∏ i in range k, f i)).surjective.prodable_iff_of_has_prod_iff $ + λ a, (has_prod_nat_add_iff k).symm + +@[to_additive] lemma has_prod_nat_add_iff' {f : ℕ → α} (k : ℕ) {a : α} : + has_prod (λ n, f (n + k)) (a / ∏ i in range k, f i) ↔ has_prod f a := +by simp [has_prod_nat_add_iff] + +@[to_additive] lemma prod_mul_tprod_nat_add [t2_space α] {f : ℕ → α} (k : ℕ) (h : prodable f) : + (∏ i in range k, f i) * (∏' i, f (i + k)) = ∏' i, f i := +by simpa only [mul_comm] using + ((has_prod_nat_add_iff k).1 ((prodable_nat_add_iff k).2 h).has_prod).unique h.has_prod + +@[to_additive] lemma tprod_eq_zero_mul [t2_space α] {f : ℕ → α} (hf : prodable f) : + ∏' b, f b = f 0 * ∏' b, f (b + 1) := +by simpa only [prod_range_one] using (prod_mul_tprod_nat_add 1 hf).symm + +/-- For `f : ℕ → α`, then `∏' k, f (k + i)` tends to zero. This does not require a productability +assumption on `f`, as otherwise all products are zero. -/ +@[to_additive "For `f : ℕ → α`, then `∑' k, f (k + i)` tends to zero. This does not require a +summability assumption on `f`, as otherwise all sums are zero."] +lemma tendsto_prod_nat_add [t2_space α] (f : ℕ → α) : tendsto (λ i, ∏' k, f (k + i)) at_top (𝓝 1) := begin - by_cases hf : summable f, - { have h₀ : (λ i, (∑' i, f i) - ∑ j in range i, f j) = λ i, ∑' (k : ℕ), f (k + i), + by_cases hf : prodable f, + { have h₀ : (λ i, (∏' i, f i) / ∏ j in range i, f j) = λ i, ∏' k, f (k + i), { ext1 i, - rw [sub_eq_iff_eq_add, add_comm, sum_add_tsum_nat_add i hf] }, - have h₁ : tendsto (λ i : ℕ, ∑' i, f i) at_top (𝓝 (∑' i, f i)) := tendsto_const_nhds, - simpa only [h₀, sub_self] using tendsto.sub h₁ hf.has_sum.tendsto_sum_nat }, + rw [div_eq_iff_eq_mul, mul_comm, prod_mul_tprod_nat_add i hf] }, + have h₁ : tendsto (λ i : ℕ, ∏' i, f i) at_top (𝓝 (∏' i, f i)) := tendsto_const_nhds, + simpa only [h₀, div_self'] using h₁.div' hf.has_prod.tendsto_prod_nat }, { convert tendsto_const_nhds, ext1 i, - rw ← summable_nat_add_iff i at hf, - { exact tsum_eq_zero_of_not_summable hf }, + rw ← prodable_nat_add_iff i at hf, + { exact tprod_eq_one_of_not_prodable hf }, { apply_instance } } end -/-- If `f₀, f₁, f₂, ...` and `g₀, g₁, g₂, ...` are both convergent then so is the `ℤ`-indexed +/-- If `f₀, f₁, f₂, ...` and `g₀, g₁, g₂, ...` are both convergent series then so is the `ℤ`-indexed sequence: `..., g₂, g₁, g₀, f₀, f₁, f₂, ...`. -/ -lemma has_sum.int_rec {b : α} {f g : ℕ → α} (hf : has_sum f a) (hg : has_sum g b) : - @has_sum α _ _ _ (@int.rec (λ _, α) f g : ℤ → α) (a + b) := +@[to_additive "If `f₀, f₁, f₂, ...` and `g₀, g₁, g₂, ...` are both convergent series then so is the +`ℤ`-indexed sequence: `..., g₂, g₁, g₀, f₀, f₁, f₂, ...`."] +lemma has_prod.int_rec {b : α} {f g : ℕ → α} (hf : has_prod f a) (hg : has_prod g b) : + @has_prod α _ _ _ (@int.rec (λ _, α) f g : ℤ → α) (a * b) := begin -- note this proof works for any two-case inductive have h₁ : injective (coe : ℕ → ℤ) := @int.of_nat.inj, have h₂ : injective int.neg_succ_of_nat := @int.neg_succ_of_nat.inj, - have : is_compl (set.range (coe : ℕ → ℤ)) (set.range int.neg_succ_of_nat), - { split, - { rw disjoint_iff_inf_le, - rintros _ ⟨⟨i, rfl⟩, ⟨j, ⟨⟩⟩⟩ }, - { rw codisjoint_iff_le_sup, - rintros (i | j) h, - exacts [or.inl ⟨_, rfl⟩, or.inr ⟨_, rfl⟩] } }, - exact has_sum.add_is_compl this (h₁.has_sum_range_iff.mpr hf) (h₂.has_sum_range_iff.mpr hg), + refine has_prod.mul_is_compl ⟨_, _⟩ (h₁.has_prod_range_iff.mpr hf) (h₂.has_prod_range_iff.mpr hg), + { rw disjoint_iff_inf_le, + rintro _ ⟨⟨i, rfl⟩, ⟨j, ⟨⟩⟩⟩ }, + { rw codisjoint_iff_le_sup, + rintro (i | j) h, + exacts [or.inl ⟨_, rfl⟩, or.inr ⟨_, rfl⟩] } end -lemma has_sum.nonneg_add_neg {b : α} {f : ℤ → α} - (hnonneg : has_sum (λ n : ℕ, f n) a) (hneg : has_sum (λ (n : ℕ), f (-n.succ)) b) : - has_sum f (a + b) := +@[to_additive] lemma has_prod.nonneg_mul_neg {b : α} {f : ℤ → α} + (hnonneg : has_prod (λ n : ℕ, f n) a) (hneg : has_prod (λ n : ℕ, f (-n.succ)) b) : + has_prod f (a * b) := begin simp_rw ← int.neg_succ_of_nat_coe at hneg, convert hnonneg.int_rec hneg using 1, ext (i | j); refl, end -lemma has_sum.pos_add_zero_add_neg {b : α} {f : ℤ → α} - (hpos : has_sum (λ n:ℕ, f(n + 1)) a) (hneg : has_sum (λ (n : ℕ), f (-n.succ)) b) : - has_sum f (a + f 0 + b) := +@[to_additive] lemma has_prod.pos_mul_zero_mul_neg {b : α} {f : ℤ → α} + (hpos : has_prod (λ n : ℕ, f (n + 1)) a) (hneg : has_prod (λ n : ℕ, f (-n.succ)) b) : + has_prod f (a * f 0 * b) := begin - have : ∀ g : ℕ → α, has_sum (λ k, g (k + 1)) a → has_sum g (a + g 0), - { intros g hg, simpa using (has_sum_nat_add_iff _).mp hg }, - exact (this (λ n, f n) hpos).nonneg_add_neg hneg, + have : ∀ g : ℕ → α, has_prod (λ k, g (k + 1)) a → has_prod g (a * g 0), + { intros g hg, simpa using (has_prod_nat_add_iff _).mp hg }, + exact (this (λ n, f n) hpos).nonneg_mul_neg hneg, end -lemma summable_int_of_summable_nat {f : ℤ → α} - (hp : summable (λ n:ℕ, f n)) (hn : summable (λ n:ℕ, f (-n))) : summable f := -(has_sum.nonneg_add_neg hp.has_sum $ summable.has_sum $ (summable_nat_add_iff 1).mpr hn).summable +@[to_additive] lemma prodable_int_of_prodable_nat {f : ℤ → α} + (hp : prodable (λ n : ℕ, f n)) (hn : prodable (λ n : ℕ, f (-n))) : prodable f := +(has_prod.nonneg_mul_neg hp.has_prod $ prodable.has_prod $ (prodable_nat_add_iff 1).mpr hn).prodable -lemma has_sum.sum_nat_of_sum_int {α : Type*} [add_comm_monoid α] [topological_space α] - [has_continuous_add α] {a : α} {f : ℤ → α} (hf : has_sum f a) : - has_sum (λ n:ℕ, f n + f (-n)) (a + f 0) := +@[to_additive] lemma has_prod.prod_nat_of_prod_int {α : Type*} [comm_monoid α] [topological_space α] + [has_continuous_mul α] {a : α} {f : ℤ → α} (hf : has_prod f a) : + has_prod (λ n : ℕ, f n * f (-n)) (a * f 0) := begin - apply (hf.add (has_sum_ite_eq (0 : ℤ) (f 0))).has_sum_of_sum_eq (λ u, _), + apply (hf.mul (has_prod_ite_eq (0 : ℤ) (f 0))).has_prod_of_prod_eq (λ u, _), refine ⟨u.image int.nat_abs, λ v' hv', _⟩, let u1 := v'.image (λ (x : ℕ), (x : ℤ)), let u2 := v'.image (λ (x : ℕ), - (x : ℤ)), @@ -921,12 +966,12 @@ begin exact ⟨x, hx, rfl⟩ }, { simp only [abs_of_nonpos h'x, int.coe_nat_abs, neg_neg] } } }, refine ⟨u1 ∪ u2, A, _⟩, - calc ∑ x in u1 ∪ u2, (f x + ite (x = 0) (f 0) 0) - = ∑ x in u1 ∪ u2, f x + ∑ x in u1 ∩ u2, f x : + calc ∏ x in u1 ∪ u2, (f x * ite (x = 0) (f 0) 1) + = (∏ x in u1 ∪ u2, f x) * ∏ x in u1 ∩ u2, f x : begin - rw sum_add_distrib, + 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, { assume x hx, suffices : x ≠ 0, by simp only [this, if_false], rintros rfl, @@ -942,10 +987,10 @@ begin simp only [nat.cast_nonneg] } }, simp only [this, eq_self_iff_true, if_true] } end - ... = ∑ 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 [sum_image, nat.cast_inj, imp_self, implies_true_iff, 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 [prod_image, nat.cast_inj, imp_self, implies_true_iff, neg_inj] + ... = ∏ b in v', f b * f (-b) : prod_mul_distrib.symm end end nat @@ -953,177 +998,177 @@ end nat end topological_group section uniform_group +variables [comm_group α] [uniform_space α] -variables [add_comm_group α] [uniform_space α] - -/-- The **Cauchy criterion** for infinite sums, also known as the **Cauchy convergence test** -/ -lemma summable_iff_cauchy_seq_finset [complete_space α] {f : β → α} : - summable f ↔ cauchy_seq (λ (s : finset β), ∑ b in s, f b) := +/-- 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**"] +lemma prodable_iff_cauchy_seq_finset [complete_space α] {f : β → α} : + prodable f ↔ cauchy_seq (λ s, ∏ b in s, f b) := cauchy_map_iff_exists_tendsto.symm -variables [uniform_add_group α] {f g : β → α} {a a₁ a₂ : α} +variables [uniform_group α] {f g : β → α} {a a₁ a₂ : α} -lemma cauchy_seq_finset_iff_vanishing : - cauchy_seq (λ (s : finset β), ∑ b in s, f b) - ↔ ∀ e ∈ 𝓝 (0:α), (∃s:finset β, ∀t, disjoint t s → ∑ b in t, f b ∈ e) := +@[to_additive] lemma cauchy_seq_finset_prod_iff_vanishing : + cauchy_seq (λ s, ∏ b in s, f b) ↔ + ∀ e ∈ 𝓝 (1 : α), ∃ s, ∀ t, disjoint t s → ∏ b in t, f b ∈ e := begin simp only [cauchy_seq, cauchy_map_iff, and_iff_right at_top_ne_bot, - prod_at_top_at_top_eq, uniformity_eq_comap_nhds_zero α, tendsto_comap_iff, (∘)], + prod_at_top_at_top_eq, uniformity_eq_comap_nhds_one α, tendsto_comap_iff, (∘)], rw [tendsto_at_top'], - split, - { assume h e he, - rcases h e he with ⟨⟨s₁, s₂⟩, h⟩, - use [s₁ ∪ s₂], - assume t ht, + refine ⟨λ h e he, _, λ h e he, _⟩, + { obtain ⟨⟨s₁, s₂⟩, h⟩ := h _ he, + refine ⟨s₁ ∪ s₂, λ 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'] using h }, - { assume h e he, - rcases exists_nhds_half_neg he with ⟨d, hd, hde⟩, - rcases h d hd with ⟨s, h⟩, + simpa only [finset.prod_union ht.symm, mul_div_cancel'''] using h }, + { obtain ⟨d, hd, hde⟩ := exists_nhds_split_inv he, + obtain ⟨s, h⟩ := h _ hd, use [(s, s)], rintros ⟨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, - { simp only [(finset.sum_sdiff ht₁).symm, (finset.sum_sdiff ht₂).symm, - 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, + { simp only [←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) } end -/-- 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. -/ -lemma tendsto_tsum_compl_at_top_zero (f : β → α) : - tendsto (λ (s : finset β), ∑' b : {x // x ∉ s}, f b) at_top (𝓝 0) := +/-- The prod over the complement of a finset tends to `1` when the finset grows to cover the whole +space. This does not need a summability assumption, as otherwise all prods 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 sums are zero."] +lemma tendsto_tprod_compl_at_top_one (f : β → α) : + tendsto (λ s : finset β, ∏' b : {x // x ∉ s}, f b) at_top (𝓝 1) := begin - by_cases H : summable f, - { assume e he, + by_cases H : prodable f, + { rintro e he, rcases exists_mem_nhds_is_closed_subset he with ⟨o, ho, o_closed, oe⟩, simp only [le_eq_subset, set.mem_preimage, mem_at_top_sets, filter.mem_map, ge_iff_le], - obtain ⟨s, hs⟩ : ∃ (s : finset β), ∀ (t : finset β), disjoint t s → ∑ (b : β) in t, f b ∈ o := - cauchy_seq_finset_iff_vanishing.1 (tendsto.cauchy_seq H.has_sum) o ho, + obtain ⟨s, hs⟩ := cauchy_seq_finset_prod_iff_vanishing.1 H.has_prod.cauchy_seq o ho, refine ⟨s, λ a sa, oe _⟩, - have A : summable (λ b : {x // x ∉ a}, f b) := a.summable_compl_iff.2 H, - apply is_closed.mem_of_tendsto o_closed A.has_sum (eventually_of_forall (λ b, _)), - have : disjoint (finset.image (λ (i : {x // x ∉ a}), (i : β)) b) s, - { apply disjoint_left.2 (λ i hi his, _), - rcases mem_image.1 hi with ⟨i', hi', rfl⟩, - exact i'.2 (sa his), }, - convert hs _ this using 1, - rw sum_image, - assume i hi j hj hij, - exact subtype.ext hij }, + have A : prodable (λ b : {x // x ∉ a}, f b) := a.prodable_compl_iff.2 H, + refine o_closed.mem_of_tendsto A.has_prod (eventually_of_forall $ λ b, _), + rw ←prod_image (subtype.coe_injective.inj_on _), + refine hs _ (disjoint_left.2 (λ i hi his, _)), + apply_instance, + obtain ⟨i', hi', rfl⟩ := mem_image.1 hi, + exact i'.2 (sa his) }, { convert tendsto_const_nhds, ext s, - apply tsum_eq_zero_of_not_summable, - rwa finset.summable_compl_iff } + apply tprod_eq_one_of_not_prodable, + rwa finset.prodable_compl_iff } end variable [complete_space α] -lemma summable_iff_vanishing : - summable f ↔ ∀ e ∈ 𝓝 (0:α), (∃s:finset β, ∀t, disjoint t s → ∑ b in t, f b ∈ e) := -by rw [summable_iff_cauchy_seq_finset, cauchy_seq_finset_iff_vanishing] - -/- TODO: generalize to monoid with a uniform continuous subtraction operator: `(a + b) - b = a` -/ -lemma summable.summable_of_eq_zero_or_self (hf : summable f) (h : ∀b, g b = 0 ∨ g b = f b) : - summable g := -summable_iff_vanishing.2 $ - assume e he, - let ⟨s, hs⟩ := summable_iff_vanishing.1 hf e he in - ⟨s, assume t ht, - have eq : ∑ b in t.filter (λb, g b = f b), f b = ∑ b in t, g b := - calc ∑ b in t.filter (λb, g b = f b), f b = ∑ b in t.filter (λb, g b = f b), g b : - finset.sum_congr rfl (assume b hb, (finset.mem_filter.1 hb).2.symm) - ... = ∑ b in t, g b : +@[to_additive] lemma prodable_iff_vanishing : + prodable f ↔ ∀ e ∈ 𝓝 (1 : α), ∃ s, ∀ t, disjoint t s → ∏ b in t, f b ∈ e := +by rw [prodable_iff_cauchy_seq_finset, cauchy_seq_finset_prod_iff_vanishing] + +/- TODO: generalize to monoid with a uniform continuous subtraction operator: `(a * b) / b = a` -/ +@[to_additive] +lemma prodable.prodable_of_eq_one_or_self (hf : prodable f) (h : ∀ b, g b = 1 ∨ g b = f b) : + prodable g := +prodable_iff_vanishing.2 $ + λ e he, + let ⟨s, hs⟩ := prodable_iff_vanishing.1 hf e he in + ⟨s, λ t ht, + have eq : ∏ b in t.filter (λb, g b = f b), f b = ∏ b in t, g b := + calc ∏ b in t.filter (λb, g b = f b), f b = ∏ b in t.filter (λb, g b = f b), g b : + finset.prod_congr rfl (λ b hb, (finset.mem_filter.1 hb).2.symm) + ... = ∏ b in t, g b : begin - refine finset.sum_subset (finset.filter_subset _ _) _, + refine finset.prod_subset (finset.filter_subset _ _) _, assume b hbt hb, simp only [(∉), finset.mem_filter, and_iff_right hbt] at hb, exact (h b).resolve_right hb end, eq ▸ hs _ $ finset.disjoint_of_subset_left (finset.filter_subset _ _) ht⟩ -protected lemma 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 lemma prodable.mul_indicator (hf : prodable f) (s : set β) : + prodable (s.mul_indicator f) := +hf.prodable_of_eq_one_or_self $ set.mul_indicator_eq_one_or_self _ _ -lemma summable.comp_injective {i : γ → β} (hf : summable f) (hi : injective i) : - summable (f ∘ i) := +@[to_additive] lemma prodable.comp_injective {i : γ → β} (hf : prodable f) (hi : injective i) : + prodable (f ∘ i) := begin - simpa only [set.indicator_range_comp] - using (hi.summable_iff _).2 (hf.indicator (set.range i)), - exact λ x hx, set.indicator_of_not_mem hx _ + simpa only [set.mul_indicator_range_comp] + using (hi.prodable_iff _).2 (hf.mul_indicator (set.range i)), + exact λ x hx, set.mul_indicator_of_not_mem hx _ end -lemma summable.subtype (hf : summable f) (s : set β) : summable (f ∘ coe : s → α) := +@[to_additive] protected lemma prodable.subtype (hf : prodable f) (s : set β) : + prodable (f ∘ coe : s → α) := hf.comp_injective subtype.coe_injective -lemma summable_subtype_and_compl {s : set β} : - summable (λ x : s, f x) ∧ summable (λ x : sᶜ, f x) ↔ summable f := -⟨and_imp.2 summable.add_compl, λ h, ⟨h.subtype s, h.subtype sᶜ⟩⟩ +@[to_additive] lemma prodable_subtype_and_compl {s : set β} : + prodable (λ x : s, f x) ∧ prodable (λ x : sᶜ, f x) ↔ prodable f := +⟨and_imp.2 prodable.mul_compl, λ h, ⟨h.subtype s, h.subtype sᶜ⟩⟩ -lemma summable.sigma_factor {γ : β → Type*} {f : (Σb:β, γ b) → α} - (ha : summable f) (b : β) : summable (λc, f ⟨b, c⟩) := +@[to_additive] +lemma prodable.sigma_factor {γ : β → Type*} {f : (Σ b, γ b) → α} (ha : prodable f) (b : β) : + prodable (λ c, f ⟨b, c⟩) := ha.comp_injective sigma_mk_injective -lemma summable.sigma {γ : β → Type*} {f : (Σb:β, γ b) → α} - (ha : summable f) : summable (λb, ∑'c, f ⟨b, c⟩) := +@[to_additive] +protected lemma prodable.sigma {γ : β → Type*} {f : (Σ b, γ b) → α} (ha : prodable f) : + prodable (λ b, ∏'c, f ⟨b, c⟩) := ha.sigma' (λ b, ha.sigma_factor b) -lemma summable.prod_factor {f : β × γ → α} (h : summable f) (b : β) : - summable (λ c, f (b, c)) := +@[to_additive] lemma prodable.prod_factor {f : β × γ → α} (h : prodable f) (b : β) : + prodable (λ c, f (b, c)) := h.comp_injective $ λ c₁ c₂ h, (prod.ext_iff.1 h).2 section loc_instances -- enable inferring a T3-topological space from a topological group -local attribute [instance] topological_add_group.t3_space +local attribute [instance] topological_group.t3_space -- disable getting a T0-space from a T3-space as this causes loops local attribute [-instance] t3_space.to_t0_space -lemma tsum_sigma [t0_space α] {γ : β → Type*} {f : (Σb:β, γ b) → α} - (ha : summable f) : ∑'p, f p = ∑'b c, f ⟨b, c⟩ := -tsum_sigma' (λ b, ha.sigma_factor b) ha +@[to_additive] +lemma tprod_sigma [t0_space α] {γ : β → Type*} {f : (Σ b, γ b) → α} (ha : prodable f) : + ∏' p, f p = ∏' b c, f ⟨b, c⟩ := +tprod_sigma' (λ b, ha.sigma_factor b) ha -lemma tsum_prod [t0_space α] {f : β × γ → α} (h : summable f) : - ∑'p, f p = ∑'b c, f ⟨b, c⟩ := -tsum_prod' h h.prod_factor +@[to_additive tsum_prod] lemma tprod_prod [t0_space α] {f : β × γ → α} (h : prodable f) : + ∏' p, f p = ∏' b c, f ⟨b, c⟩ := +tprod_prod' h h.prod_factor -lemma tsum_comm [t0_space α] {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] lemma tprod_comm [t0_space α] {f : β → γ → α} (h : prodable (uncurry f)) : + ∏' c b, f b c = ∏' b c, f b c := +tprod_comm' h h.prod_factor h.prod_symm.prod_factor end loc_instances -lemma tsum_subtype_add_tsum_subtype_compl [t2_space α] {f : β → α} (hf : summable f) (s : set β) : - ∑' x : s, f x + ∑' x : sᶜ, f x = ∑' x, f x := -((hf.subtype s).has_sum.add_compl (hf.subtype {x | x ∉ s}).has_sum).unique hf.has_sum +@[to_additive] +lemma tprod_subtype_mul_tprod_subtype_compl [t2_space α] (hf : prodable f) (s : set β) : + (∏' x : s, f x) * ∏' x : sᶜ, f x = ∏' x, f x := +((hf.subtype s).has_prod.mul_compl (hf.subtype {x | x ∉ s}).has_prod).unique hf.has_prod -lemma sum_add_tsum_subtype_compl [t2_space α] {f : β → α} (hf : summable f) (s : finset β) : - ∑ x in s, f x + ∑' x : {x // x ∉ s}, f x = ∑' x, f x := -begin - rw ← tsum_subtype_add_tsum_subtype_compl hf s, - simp only [finset.tsum_subtype', add_right_inj], - refl, -end +@[to_additive] +lemma prod_mul_tprod_subtype_compl [t2_space α] (hf : prodable 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, finset.tprod_subtype'], refl } end uniform_group section topological_group +variables [topological_space G] [comm_group G] [topological_group G] {f : α → G} -variables {G : Type*} [topological_space G] [add_comm_group G] [topological_add_group G] - {f : α → G} - -lemma summable.vanishing (hf : summable f) ⦃e : set G⦄ (he : e ∈ 𝓝 (0 : G)) : - ∃ s : finset α, ∀ t, disjoint t s → ∑ k in t, f k ∈ e := +@[to_additive] +lemma prodable.vanishing (hf : prodable f) ⦃e : set G⦄ (he : e ∈ 𝓝 (1 : G)) : + ∃ s : finset α, ∀ t, disjoint t s → ∏ k in t, f k ∈ e := begin - letI : uniform_space G := topological_add_group.to_uniform_space G, - letI : uniform_add_group G := topological_add_comm_group_is_uniform, + letI : uniform_space G := topological_group.to_uniform_space G, + letI : uniform_group G := topological_comm_group_is_uniform, rcases hf with ⟨y, hy⟩, - exact cauchy_seq_finset_iff_vanishing.1 hy.cauchy_seq e he + exact cauchy_seq_finset_prod_iff_vanishing.1 hy.cauchy_seq e he, end -/-- Series divergence test: if `f` is a convergent series, then `f x` tends to zero along +/-- Series divergence test: if `f` is a convergent series, then `f x` tends to one along `cofinite`. -/ -lemma summable.tendsto_cofinite_zero (hf : summable f) : tendsto f cofinite (𝓝 0) := +@[to_additive "Series divergence test: if `f` is a convergent series, then `f x` tends to zero along +`cofinite`."] +lemma prodable.tendsto_cofinite_one (hf : prodable f) : tendsto f cofinite (𝓝 1) := begin intros e he, rw [filter.mem_map], @@ -1132,8 +1177,9 @@ begin by simpa using hs {x} (disjoint_singleton_left.2 hx) end -lemma summable.tendsto_at_top_zero {f : ℕ → G} (hf : summable f) : tendsto f at_top (𝓝 0) := -by { rw ←nat.cofinite_eq_at_top, exact hf.tendsto_cofinite_zero } +@[to_additive] lemma prodable.tendsto_at_top_one {f : ℕ → G} (hf : prodable f) : + tendsto f at_top (𝓝 1) := +by { rw ←nat.cofinite_eq_at_top, exact hf.tendsto_cofinite_one } end topological_group @@ -1155,32 +1201,33 @@ end const_smul /-! ### Product and pi types -/ section prod -variables [add_comm_monoid α] [topological_space α] [add_comm_monoid γ] [topological_space γ] +variables [comm_monoid α] [topological_space α] [comm_monoid γ] [topological_space γ] -lemma has_sum.prod_mk {f : β → α} {g : β → γ} {a : α} {b : γ} - (hf : has_sum f a) (hg : has_sum g b) : - has_sum (λ x, (⟨f x, g x⟩ : α × γ)) ⟨a, b⟩ := -by simp [has_sum, ← prod_mk_sum, filter.tendsto.prod_mk_nhds hf hg] +@[to_additive has_sum.prod_mk] +lemma has_prod.prod_mk {f : β → α} {g : β → γ} {a : α} {b : γ} + (hf : has_prod f a) (hg : has_prod g b) : + has_prod (λ x, (⟨f x, g x⟩ : α × γ)) ⟨a, b⟩ := +by simp [has_prod, ← prod_mk_prod, hf.prod_mk_nhds hg] end prod section pi -variables {ι : Type*} {π : α → Type*} [∀ x, add_comm_monoid (π x)] [∀ x, topological_space (π x)] +variables {ι : Type*} {π : α → Type*} [∀ x, comm_monoid (π x)] [∀ x, topological_space (π x)] + {f : ι → ∀ x, π x} -lemma pi.has_sum {f : ι → ∀ x, π x} {g : ∀ x, π x} : - has_sum f g ↔ ∀ x, has_sum (λ i, f i x) (g x) := -by simp only [has_sum, tendsto_pi_nhds, sum_apply] +@[to_additive] lemma pi.has_prod {g : ∀ x, π x} : has_prod f g ↔ ∀ x, has_prod (λ i, f i x) (g x) := +by simp only [has_prod, tendsto_pi_nhds, prod_apply] -lemma pi.summable {f : ι → ∀ x, π x} : summable f ↔ ∀ x, summable (λ i, f i x) := -by simp only [summable, pi.has_sum, skolem] +@[to_additive] lemma pi.prodable : prodable f ↔ ∀ x, prodable (λ i, f i x) := +by simp only [prodable, pi.has_prod, skolem] -lemma tsum_apply [∀ x, t2_space (π x)] {f : ι → ∀ x, π x}{x : α} (hf : summable f) : - (∑' i, f i) x = ∑' i, f i x := -(pi.has_sum.mp hf.has_sum x).tsum_eq.symm +@[to_additive] lemma tprod_apply [∀ x, t2_space (π x)] {x : α} (hf : prodable f) : + (∏' i, f i) x = ∏' i, f i x := +(pi.has_prod.1 hf.has_prod x).tprod_eq.symm end pi -/-! ### Multiplicative opposite -/ +/-! ### Multiplicative/additive opposite -/ section mul_opposite open mul_opposite @@ -1225,6 +1272,50 @@ mul_opposite.op_injective tsum_op.symm end mul_opposite +section add_opposite +open add_opposite +variables [comm_monoid α] [topological_space α] {f : β → α} {a : α} + +lemma has_prod.op (hf : has_prod f a) : has_prod (λ a, op (f a)) (op a) := +(hf.map (@op_mul_equiv α _) continuous_op : _) + +lemma prodable.op (hf : prodable f) : prodable (op ∘ f) := hf.has_prod.op.prodable + +lemma has_prod.unop {f : β → αᵃᵒᵖ} {a : αᵃᵒᵖ} (hf : has_prod f a) : + has_prod (λ a, unop (f a)) (unop a) := +(hf.map (@op_mul_equiv α _).symm continuous_unop : _) + +lemma prodable.unop {f : β → αᵃᵒᵖ} (hf : prodable f) : prodable (unop ∘ f) := +hf.has_prod.unop.prodable + +@[simp] lemma has_prod_op : has_prod (λ a, op (f a)) (op a) ↔ has_prod f a := +⟨has_prod.unop, has_prod.op⟩ + +@[simp] lemma has_prod_unop {f : β → αᵃᵒᵖ} {a : αᵃᵒᵖ} : + has_prod (λ a, unop (f a)) (unop a) ↔ has_prod f a := +⟨has_prod.op, has_prod.unop⟩ + +@[simp] lemma prodable_op : prodable (λ a, op (f a)) ↔ prodable f := +⟨prodable.unop, prodable.op⟩ + +@[simp] lemma prodable_unop {f : β → αᵃᵒᵖ} : prodable (λ a, unop (f a)) ↔ prodable f := +⟨prodable.op, prodable.unop⟩ + +variables [t2_space α] + +lemma tprod_op : ∏' x, add_opposite.op (f x) = add_opposite.op (∏' x, f x) := +begin + by_cases h : prodable f, + { exact h.has_prod.op.tprod_eq }, + { have ho := prodable_op.not.mpr h, + rw [tprod_eq_one_of_not_prodable h, tprod_eq_one_of_not_prodable ho, add_opposite.op_one] } +end + +lemma tprod_unop {f : β → αᵃᵒᵖ} : ∏' x, add_opposite.unop (f x) = add_opposite.unop (∏' x, f x) := +add_opposite.op_injective tprod_op.symm + +end add_opposite + /-! ### Interaction with the star -/ section has_continuous_star diff --git a/src/topology/algebra/infinite_sum/order.lean b/src/topology/algebra/infinite_sum/order.lean index 24371cd77237c..a371ef149fc90 100644 --- a/src/topology/algebra/infinite_sum/order.lean +++ b/src/topology/algebra/infinite_sum/order.lean @@ -23,37 +23,44 @@ open_locale big_operators classical variables {ι κ α : Type*} section preorder -variables [preorder α] [add_comm_monoid α] [topological_space α] [order_closed_topology α] +variables [preorder α] [comm_monoid α] [topological_space α] [order_closed_topology α] [t2_space α] {f : ℕ → α} {c : α} -lemma tsum_le_of_sum_range_le (hf : summable f) (h : ∀ n, ∑ i in range n, f i ≤ c) : - ∑' n, f n ≤ c := -let ⟨l, hl⟩ := hf in hl.tsum_eq.symm ▸ le_of_tendsto' hl.tendsto_sum_nat h +@[to_additive] lemma tprod_le_of_prod_range_le (hprod : prodable f) + (h : ∀ n, ∏ i in finset.range n, f i ≤ c) : ∏' n, f n ≤ c := +let ⟨l, hl⟩ := hprod in hl.tprod_eq.symm ▸ le_of_tendsto' hl.tendsto_prod_nat h end preorder -section ordered_add_comm_monoid -variables [ordered_add_comm_monoid α] [topological_space α] [order_closed_topology α] {f g : ι → α} +section ordered_comm_monoid +variables [ordered_comm_monoid α] [topological_space α] [order_closed_topology α] {f g : ι → α} {a a₁ a₂ : α} -lemma has_sum_le (h : ∀ i, f i ≤ g i) (hf : has_sum f a₁) (hg : has_sum g a₂) : a₁ ≤ a₂ := -le_of_tendsto_of_tendsto' hf hg $ λ s, sum_le_sum $ λ i _, h i +@[to_additive] +lemma has_prod_le (h : ∀ i, f i ≤ g i) (hf : has_prod f a₁) (hg : has_prod g a₂) : a₁ ≤ a₂ := +le_of_tendsto_of_tendsto' hf hg $ λ s, finset.prod_le_prod' $ λ b _, h b -@[mono] lemma has_sum_mono (hf : has_sum f a₁) (hg : has_sum g a₂) (h : f ≤ g) : a₁ ≤ a₂ := -has_sum_le h hf hg +@[to_additive] +lemma has_prod_mono (hf : has_prod f a₁) (hg : has_prod g a₂) (h : f ≤ g) : a₁ ≤ a₂ := +has_prod_le h hf hg -lemma has_sum_le_of_sum_le (hf : has_sum f a) (h : ∀ s, ∑ i in s, f i ≤ a₂) : a ≤ a₂ := +attribute [mono] has_prod_mono has_sum_mono + +@[to_additive] lemma has_prod_le_of_prod_le (hf : has_prod f a) (h : ∀ s, ∏ i in s, f i ≤ a₂) : + a ≤ a₂ := le_of_tendsto' hf h -lemma le_has_sum_of_le_sum (hf : has_sum f a) (h : ∀ s, a₂ ≤ ∑ i in s, f i) : a₂ ≤ a := +@[to_additive] lemma le_has_prod_of_le_prod (hf : has_prod f a) (h : ∀ s, a₂ ≤ ∏ i in s, f i) : + a₂ ≤ a := ge_of_tendsto' hf h -lemma has_sum_le_inj {g : κ → α} (e : ι → κ) (he : injective e) (hs : ∀ c ∉ set.range e, 0 ≤ g c) - (h : ∀ i, f i ≤ g (e i)) (hf : has_sum f a₁) (hg : has_sum g a₂) : a₁ ≤ a₂ := -have has_sum (λ c, (partial_inv e c).cases_on' 0 f) a₁, +@[to_additive] +lemma has_prod_le_inj {g : κ → α} (e : ι → κ) (he : injective e) (hs : ∀ c ∉ set.range e, 1 ≤ g c) + (h : ∀ i, f i ≤ g (e i)) (hf : has_prod f a₁) (hg : has_prod g a₂) : a₁ ≤ a₂ := +have has_prod (λ c, (partial_inv e c).cases_on' 1 f) a₁, begin - refine (has_sum_iff_has_sum_of_ne_zero_bij (e ∘ coe) (λ c₁ c₂ hc, he hc) (λ c hc, _) _).2 hf, - { rw mem_support at hc, + refine (has_prod_iff_has_prod_of_ne_one_bij (e ∘ coe) (λ c₁ c₂ hc, he hc) (λ c hc, _) _).2 hf, + { rw mem_mul_support at hc, cases eq : partial_inv e c with i; rw eq at hc, { contradiction }, { rw [partial_inv_of_injective he] at eq, @@ -62,7 +69,7 @@ begin simp [partial_inv_left he, option.cases_on'] } end, begin - refine has_sum_le (λ c, _) this hg, + refine has_prod_le (λ c, _) this hg, obtain ⟨i, rfl⟩ | h := em (c ∈ set.range e), { rw [partial_inv_left he, option.cases_on'], exact h _ }, @@ -71,131 +78,150 @@ begin exact hs _ h } end -lemma tsum_le_tsum_of_inj {g : κ → α} (e : ι → κ) (he : injective e) - (hs : ∀ c ∉ set.range e, 0 ≤ g c) (h : ∀ i, f i ≤ g (e i)) (hf : summable f) (hg : summable g) : - tsum f ≤ tsum g := -has_sum_le_inj _ he hs h hf.has_sum hg.has_sum +@[to_additive] lemma tprod_le_tprod_of_inj {g : κ → α} (e : ι → κ) (he : injective e) + (hs : ∀ c ∉ set.range e, 1 ≤ g c) (h : ∀ i, f i ≤ g (e i)) (hf : prodable f) (hg : prodable g) : + tprod f ≤ tprod g := +has_prod_le_inj _ he hs h hf.has_prod hg.has_prod + +@[to_additive] lemma prod_le_has_prod (s : finset ι) (hs : ∀ i ∉ s, 1 ≤ f i) (hf : has_prod f a) : + ∏ i in s, f i ≤ a := +ge_of_tendsto hf $ eventually_at_top.2 ⟨s, λ t hst, + prod_le_prod_of_subset_of_one_le' hst $ λ i hit, hs _⟩ -lemma sum_le_has_sum (s : finset ι) (hs : ∀ i ∉ s, 0 ≤ f i) (hf : has_sum f a) : - ∑ i in s, f i ≤ a := -ge_of_tendsto hf (eventually_at_top.2 ⟨s, λ t hst, - sum_le_sum_of_subset_of_nonneg hst $ λ i hbt hbs, hs i hbs⟩) +@[to_additive] lemma is_lub_has_prod (h : ∀ i, 1 ≤ f i) (hf : has_prod f a) : + is_lub (set.range (λ s, ∏ i in s, f i)) a := +is_lub_of_tendsto_at_top (prod_mono_set_of_one_le' h) hf -lemma is_lub_has_sum (h : ∀ i, 0 ≤ f i) (hf : has_sum f a) : - is_lub (set.range $ λ s, ∑ i in s, f i) a := -is_lub_of_tendsto_at_top (finset.sum_mono_set_of_nonneg h) hf +@[to_additive] lemma le_has_prod (hf : has_prod f a) (i : ι) (hi : ∀ i' ≠ i, 1 ≤ f i') : f i ≤ a := +calc f i = ∏ i in {i}, f i : finset.prod_singleton.symm +... ≤ a : prod_le_has_prod _ (by { convert hi, simp }) hf -lemma le_has_sum (hf : has_sum f a) (i : ι) (hb : ∀ b' ≠ i, 0 ≤ f b') : f i ≤ a := -calc f i = ∑ i in {i}, f i : finset.sum_singleton.symm -... ≤ a : sum_le_has_sum _ (by { convert hb, simp }) hf +@[to_additive] +lemma prod_le_tprod {f : ι → α} (s : finset ι) (hs : ∀ i ∉ s, 1 ≤ f i) (hf : prodable f) : + ∏ i in s, f i ≤ ∏' i, f i := +prod_le_has_prod s hs hf.has_prod -lemma sum_le_tsum {f : ι → α} (s : finset ι) (hs : ∀ i ∉ s, 0 ≤ f i) (hf : summable f) : - ∑ i in s, f i ≤ ∑' i, f i := -sum_le_has_sum s hs hf.has_sum +@[to_additive] lemma le_tprod (hf : prodable f) (i : ι) (hi : ∀ i' ≠ i, 1 ≤ f i') : + f i ≤ ∏' i, f i := +le_has_prod (prodable.has_prod hf) i hi -lemma le_tsum (hf : summable f) (i : ι) (hb : ∀ b' ≠ i, 0 ≤ f b') : f i ≤ ∑' i, f i := -le_has_sum (summable.has_sum hf) i hb +@[to_additive] lemma tprod_le_tprod (h : ∀ i, f i ≤ g i) (hf : prodable f) (hg : prodable g) : + ∏' i, f i ≤ ∏' i, g i := +has_prod_le h hf.has_prod hg.has_prod -lemma tsum_le_tsum (h : ∀ i, f i ≤ g i) (hf : summable f) (hg : summable g) : - ∑' i, f i ≤ ∑' i, g i := -has_sum_le h hf.has_sum hg.has_sum +@[to_additive] lemma tprod_mono (hf : prodable f) (hg : prodable g) (h : f ≤ g) : + ∏' n, f n ≤ ∏' n, g n := +tprod_le_tprod h hf hg -@[mono] lemma tsum_mono (hf : summable f) (hg : summable g) (h : f ≤ g) : - ∑' n, f n ≤ ∑' n, g n := -tsum_le_tsum h hf hg +attribute [mono] tprod_mono tsum_mono -lemma tsum_le_of_sum_le (hf : summable f) (h : ∀ s, ∑ i in s, f i ≤ a₂) : ∑' i, f i ≤ a₂ := -has_sum_le_of_sum_le hf.has_sum h +@[to_additive] lemma tprod_le_of_prod_le (hf : prodable f) (h : ∀ s, ∏ i in s, f i ≤ a₂) : + ∏' i, f i ≤ a₂ := +has_prod_le_of_prod_le hf.has_prod h -lemma tsum_le_of_sum_le' (ha₂ : 0 ≤ a₂) (h : ∀ s, ∑ i in s, f i ≤ a₂) : ∑' i, f i ≤ a₂ := +@[to_additive] lemma tprod_le_of_prod_le' (ha₂ : 1 ≤ a₂) (h : ∀ s, ∏ i in s, f i ≤ a₂) : + ∏' i, f i ≤ a₂ := begin - by_cases hf : summable f, - { exact tsum_le_of_sum_le hf h }, - { rw tsum_eq_zero_of_not_summable hf, + by_cases hf : prodable f, + { exact tprod_le_of_prod_le hf h }, + { rw tprod_eq_one_of_not_prodable hf, exact ha₂ } end -lemma has_sum.nonneg (h : ∀ i, 0 ≤ g i) (ha : has_sum g a) : 0 ≤ a := has_sum_le h has_sum_zero ha -lemma has_sum.nonpos (h : ∀ i, g i ≤ 0) (ha : has_sum g a) : a ≤ 0 := has_sum_le h ha has_sum_zero +@[to_additive] lemma has_prod.one_le (h : ∀ i, 1 ≤ g i) (ha : has_prod g a) : 1 ≤ a := +has_prod_le h has_prod_one ha -lemma tsum_nonneg (h : ∀ i, 0 ≤ g i) : 0 ≤ ∑' i, g i := +@[to_additive] lemma has_prod.le_one (h : ∀ i, g i ≤ 1) (ha : has_prod g a) : a ≤ 1 := +has_prod_le h ha has_prod_one + +@[to_additive tsum_nonneg] lemma one_le_tprod (h : ∀ i, 1 ≤ g i) : 1 ≤ ∏' i, g i := begin - by_cases hg : summable g, - { exact hg.has_sum.nonneg h }, - { simp [tsum_eq_zero_of_not_summable hg] } + by_cases hg : prodable g, + { exact hg.has_prod.one_le h }, + { simp [tprod_eq_one_of_not_prodable hg] } end -lemma tsum_nonpos (h : ∀ i, f i ≤ 0) : ∑' i, f i ≤ 0 := +@[to_additive] lemma tprod_le_one (h : ∀ i, f i ≤ 1) : ∏' i, f i ≤ 1 := begin - by_cases hf : summable f, - { exact hf.has_sum.nonpos h }, - { simp [tsum_eq_zero_of_not_summable hf] } + by_cases hf : prodable f, + { exact hf.has_prod.le_one h }, + { simp [tprod_eq_one_of_not_prodable hf] } end -end ordered_add_comm_monoid +end ordered_comm_monoid + +section ordered_comm_group +variables [ordered_comm_group α] [topological_space α] [topological_group α] + [order_closed_topology α] {f g : ι → α} {a₁ a₂ : α} -section ordered_add_comm_group -variables [ordered_add_comm_group α] [topological_space α] [topological_add_group α] - [order_closed_topology α] {f g : ι → α} {a₁ a₂ : α} {i : ι} +@[to_additive] lemma has_prod_lt {i : ι} (h : ∀ (i : ι), f i ≤ g i) (hi : f i < g i) + (hf : has_prod f a₁) (hg : has_prod g a₂) : + a₁ < a₂ := +have update f i 1 ≤ update g i 1 := update_le_update_iff.mpr ⟨rfl.le, λ i _, h i⟩, +have 1 / f i * a₁ ≤ 1 / g i * a₂ := has_prod_le this (hf.update i 1) (hg.update i 1), +by simpa only [one_div, mul_inv_cancel_left] using mul_lt_mul_of_lt_of_le hi this -lemma has_sum_lt (h : f ≤ g) (hi : f i < g i) (hf : has_sum f a₁) (hg : has_sum g a₂) : a₁ < a₂ := -have update f i 0 ≤ update g i 0 := update_le_update_iff.mpr ⟨rfl.le, λ i _, h i⟩, -have 0 - f i + a₁ ≤ 0 - g i + a₂ := has_sum_le this (hf.update i 0) (hg.update i 0), -by simpa only [zero_sub, add_neg_cancel_left] using add_lt_add_of_lt_of_le hi this +@[to_additive] +lemma has_prod_strict_mono (hf : has_prod f a₁) (hg : has_prod g a₂) (h : f < g) : a₁ < a₂ := +let ⟨hle, i, hi⟩ := pi.lt_def.mp h in has_prod_lt hle hi hf hg -@[mono] lemma has_sum_strict_mono (hf : has_sum f a₁) (hg : has_sum g a₂) (h : f < g) : a₁ < a₂ := -let ⟨hle, i, hi⟩ := pi.lt_def.mp h in has_sum_lt hle hi hf hg +@[to_additive] lemma tprod_lt_tprod {i : ι} (h : ∀ (i : ι), f i ≤ g i) (hi : f i < g i) + (hf : prodable f) (hg : prodable g) : + ∏' n, f n < ∏' n, g n := +has_prod_lt h hi hf.has_prod hg.has_prod -lemma tsum_lt_tsum (h : f ≤ g) (hi : f i < g i) (hf : summable f) (hg : summable g) : - ∑' n, f n < ∑' n, g n := -has_sum_lt h hi hf.has_sum hg.has_sum +@[to_additive] lemma tprod_strict_mono (hf : prodable f) (hg : prodable g) (h : f < g) : + ∏' n, f n < ∏' n, g n := +let ⟨hle, i, hi⟩ := pi.lt_def.mp h in tprod_lt_tprod hle hi hf hg -@[mono] lemma tsum_strict_mono (hf : summable f) (hg : summable g) (h : f < g) : - ∑' n, f n < ∑' n, g n := -let ⟨hle, i, hi⟩ := pi.lt_def.mp h in tsum_lt_tsum hle hi hf hg +attribute [mono] has_prod_strict_mono has_sum_strict_mono tprod_strict_mono tsum_strict_mono -lemma 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] +lemma one_lt_tprod (hg' : prodable 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 prodable_one hg' } -lemma has_sum_zero_iff_of_nonneg (hf : ∀ i, 0 ≤ f i) : has_sum f 0 ↔ f = 0 := +@[to_additive] lemma has_prod_one_iff_of_one_le (hf : ∀ i, 1 ≤ f i) : has_prod f 1 ↔ f = 1 := begin refine ⟨λ hf', _, _⟩, { ext i, refine (hf i).eq_of_not_gt (λ hi, _), - simpa using has_sum_lt hf hi has_sum_zero hf' }, + simpa using has_prod_lt hf hi has_prod_one hf' }, { rintro rfl, - exact has_sum_zero } + exact has_prod_one }, end -end ordered_add_comm_group +end ordered_comm_group -section canonically_ordered_add_monoid -variables [canonically_ordered_add_monoid α] [topological_space α] [order_closed_topology α] +section canonically_ordered_monoid +variables [canonically_ordered_monoid α] [topological_space α] [order_closed_topology α] {f : ι → α} {a : α} -lemma le_has_sum' (hf : has_sum f a) (i : ι) : f i ≤ a := le_has_sum hf i $ λ _ _, zero_le _ +@[to_additive] lemma le_has_prod' (hf : has_prod f a) (i : ι) : f i ≤ a := +le_has_prod hf i $ λ _ _, one_le _ -lemma le_tsum' (hf : summable f) (i : ι) : f i ≤ ∑' i, f i := le_tsum hf i $ λ _ _, zero_le _ +@[to_additive] lemma le_tprod' (hf : prodable f) (i : ι) : f i ≤ ∏' i, f i := +le_tprod hf i $ λ _ _, one_le _ -lemma has_sum_zero_iff : has_sum f 0 ↔ ∀ x, f x = 0 := +@[to_additive] lemma has_prod_one_iff : has_prod f 1 ↔ ∀ x, f x = 1 := begin refine ⟨_, λ h, _⟩, { contrapose!, - exact λ ⟨x, hx⟩ h, hx (nonpos_iff_eq_zero.1$ le_has_sum' h x) }, - { convert has_sum_zero, + exact λ ⟨x, hx⟩ h, hx (le_one_iff_eq_one.1 $ le_has_prod' h x) }, + { convert has_prod_one, exact funext h } end -lemma tsum_eq_zero_iff (hf : summable f) : ∑' i, f i = 0 ↔ ∀ x, f x = 0 := -by rw [←has_sum_zero_iff, hf.has_sum_iff] +@[to_additive] lemma tprod_eq_one_iff (hf : prodable f) : ∏' i, f i = 1 ↔ ∀ x, f x = 1 := +by rw [←has_prod_one_iff, hf.has_prod_iff] -lemma 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] lemma tprod_ne_one_iff (hf : prodable f) : ∏' i, f i ≠ 1 ↔ ∃ x, f x ≠ 1 := +by rw [ne.def, tprod_eq_one_iff hf, not_forall] -lemma is_lub_has_sum' (hf : has_sum f a) : is_lub (set.range $ λ s, ∑ i in s, f i) a := -is_lub_of_tendsto_at_top (finset.sum_mono_set f) hf +@[to_additive] lemma is_lub_has_prod' (hf : has_prod f a) : + is_lub (set.range (λ s, ∏ i in s, f i)) a := +is_lub_of_tendsto_at_top (finset.prod_mono_set' f) hf -end canonically_ordered_add_monoid +end canonically_ordered_monoid section linear_order @@ -208,19 +234,19 @@ conditionally complete linear order, such as `ℝ`, `ℝ≥0`, `ℝ≥0∞`, bec the existence of a least upper bound. -/ -lemma has_sum_of_is_lub_of_nonneg [linear_ordered_add_comm_monoid α] [topological_space α] - [order_topology α] {f : ι → α} (i : α) (h : ∀ i, 0 ≤ f i) - (hf : is_lub (set.range $ λ s, ∑ i in s, f i) i) : - has_sum f i := -tendsto_at_top_is_lub (finset.sum_mono_set_of_nonneg h) hf +@[to_additive] lemma has_prod_of_is_lub_of_one_le [linear_ordered_comm_monoid α] + [topological_space α] [order_topology α] {f : ι → α} (a : α) (h : ∀ i, 1 ≤ f i) + (hf : is_lub (set.range $ λ s, ∏ i in s, f i) a) : + has_prod f a := +tendsto_at_top_is_lub (finset.prod_mono_set_of_one_le' h) hf -lemma has_sum_of_is_lub [canonically_linear_ordered_add_monoid α] [topological_space α] - [order_topology α] {f : ι → α} (b : α) (hf : is_lub (set.range $ λ s, ∑ i in s, f i) b) : - has_sum f b := -tendsto_at_top_is_lub (finset.sum_mono_set f) hf +@[to_additive] lemma has_prod_of_is_lub [canonically_linear_ordered_monoid α] [topological_space α] + [order_topology α] {f : ι → α} (a : α) (hf : is_lub (set.range (λ s, ∏ i in s, f i)) a) : + has_prod f a := +tendsto_at_top_is_lub (finset.prod_mono_set' f) hf -lemma summable_abs_iff [linear_ordered_add_comm_group α] [uniform_space α] [uniform_add_group α] - [complete_space α] {f : ι → α} : +lemma summable_abs_iff [linear_ordered_add_comm_group α] [uniform_space α] + [uniform_add_group α] [complete_space α] {f : ι → α} : summable (λ x, |f x|) ↔ summable f := have h1 : ∀ x : {x | 0 ≤ f x}, |f x| = f x := λ x, abs_of_nonneg x.2, have h2 : ∀ x : {x | 0 ≤ f x}ᶜ, |f x| = -f x := λ x, abs_of_neg (not_le.1 x.2), diff --git a/src/topology/instances/nnreal.lean b/src/topology/instances/nnreal.lean index ceb03496d65d4..64ff727b33686 100644 --- a/src/topology/instances/nnreal.lean +++ b/src/topology/instances/nnreal.lean @@ -227,7 +227,7 @@ lemma tendsto_tsum_compl_at_top_zero {α : Type*} (f : α → ℝ≥0) : tendsto (λ (s : finset α), ∑' b : {x // x ∉ s}, f b) at_top (𝓝 0) := begin simp_rw [← tendsto_coe, coe_tsum, nnreal.coe_zero], - exact tendsto_tsum_compl_at_top_zero (λ (a : α), (f a : ℝ)) + convert tendsto_tsum_compl_at_top_zero (λ a, (f a : ℝ)), end /-- `x ↦ x ^ n` as an order isomorphism of `ℝ≥0`. -/