feat(topology/algebra/infinite_sum): Multiplicativise

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
 
 /-!

src/analysis/normed/group/infinite_sum.lean

@@ -36,24 +36,24 @@ 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'⟩ }
 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,

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
 

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 :=

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 α) :

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

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 []                        := []