feat(algebra/big_operators/finprod): add a few lemmas (#8261)

* add `finprod_eq_single` and `finsum_eq_single`;
* add `finprod_induction` and `finsum_induction`;
* add `single_le_finprod` and `single_le_finsum`;
* add `one_le_finprod'` and `finsum_nonneg`.

src/algebra/big_operators/finprod.lean

@@ -137,15 +137,18 @@ by { rw ← finprod_one, congr }
 @[simp, to_additive] lemma finprod_false (f : false → M) : ∏ᶠ i, f i = 1 :=
 finprod_of_is_empty _
 
-@[to_additive] lemma finprod_unique [unique α] (f : α → M) : ∏ᶠ i, f i = f (default α) :=
+@[to_additive] lemma finprod_eq_single (f : α → M) (a : α) (ha : ∀ x ≠ a, f x = 1) :
+  ∏ᶠ x, f x = f a :=
 begin
-  have : mul_support (f ∘ plift.down) ⊆ (finset.univ : finset (plift α)),
-    from λ x _, finset.mem_univ x,
-  rw [finprod_eq_prod_plift_of_mul_support_subset this, univ_unique,
-    finset.prod_singleton],
-  exact congr_arg f (plift.down_up _)
+  have : mul_support (f ∘ plift.down) ⊆ ({plift.up a} : finset (plift α)),
+  { intro x, contrapose,
+    simpa [plift.eq_up_iff_down_eq] using ha x.down },
+  rw [finprod_eq_prod_plift_of_mul_support_subset this, finset.prod_singleton],
 end
 
+@[to_additive] lemma finprod_unique [unique α] (f : α → M) : ∏ᶠ i, f i = f (default α) :=
+finprod_eq_single f (default α) $ λ x hx, (hx $ unique.eq_default _).elim
+
 @[simp, to_additive] lemma finprod_true (f : true → M) : ∏ᶠ i, f i = f trivial :=
 @finprod_unique M true _ ⟨⟨trivial⟩, λ _, rfl⟩ f
 
@@ -172,15 +175,30 @@ by { subst q, exact finprod_congr hfg }
 
 attribute [congr] finsum_congr_Prop
 
-lemma finprod_nonneg {R : Type*} [ordered_comm_semiring R] {f : α → R} (hf : ∀ x, 0 ≤ f x) :
-  0 ≤ ∏ᶠ x, f x :=
+/-- To prove a property of a finite product, it suffices to prove that the property is
+multiplicative and holds on multipliers. -/
+@[to_additive] lemma finprod_induction {f : α → M} (p : M → Prop) (hp₀ : p 1)
+  (hp₁ : ∀ x y, p x → p y → p (x * y)) (hp₂ : ∀ i, p (f i)) :
+  p (∏ᶠ i, f i) :=
 begin
   rw finprod,
   split_ifs,
-  { exact finset.prod_nonneg (λ x _, hf _) },
-  { exact zero_le_one }
+  exacts [finset.prod_induction _ _ hp₁ hp₀ (λ i hi, hp₂ _), hp₀]
 end
 
+/-- To prove a property of a finite sum, it suffices to prove that the property is
+additive and holds on summands. -/
+add_decl_doc finsum_induction
+
+lemma finprod_nonneg {R : Type*} [ordered_comm_semiring R] {f : α → R} (hf : ∀ x, 0 ≤ f x) :
+  0 ≤ ∏ᶠ x, f x :=
+finprod_induction (λ x, 0 ≤ x) zero_le_one (λ x y, mul_nonneg) hf
+
+@[to_additive finsum_nonneg]
+lemma one_le_finprod' {M : Type*} [ordered_comm_monoid M] {f : α → M} (hf : ∀ i, 1 ≤ f i) :
+  1 ≤ ∏ᶠ i, f i :=
+finprod_induction _ le_rfl (λ _ _, one_le_mul) hf
+
 @[to_additive] lemma monoid_hom.map_finprod_plift (f : M →* N) (g : α → M)
   (h : finite (mul_support $ g ∘ plift.down)) :
   f (∏ᶠ x, g x) = ∏ᶠ x, f (g x) :=
@@ -651,19 +669,23 @@ multiplicative and holds on multipliers. -/
 @[to_additive] lemma finprod_mem_induction (p : M → Prop) (hp₀ : p 1)
   (hp₁ : ∀ x y, p x → p y → p (x * y)) (hp₂ : ∀ x ∈ s, p $ f x) :
   p (∏ᶠ i ∈ s, f i) :=
-begin
-  by_cases hs : (s ∩ mul_support f).finite,
-  { rw [finprod_mem_eq_prod _ hs],
-    refine finset.prod_induction _ p hp₁ hp₀ (λ x hx, hp₂ x _),
-    rw hs.mem_to_finset at hx, exact hx.1 },
-  { exact (finprod_mem_eq_one_of_infinite hs).symm ▸ hp₀ }
-end
+finprod_induction _ hp₀ hp₁ $ λ x, finprod_induction _ hp₀ hp₁ $ hp₂ x
 
 lemma finprod_cond_nonneg {R : Type*} [ordered_comm_semiring R] {p : α → Prop} {f : α → R}
   (hf : ∀ x, p x → 0 ≤ f x) :
   0 ≤ ∏ᶠ x (h : p x), f x :=
 finprod_nonneg $ λ x, finprod_nonneg $ hf x
 
+@[to_additive]
+lemma single_le_finprod {M : Type*} [ordered_comm_monoid M] (i : α) {f : α → M}
+  (hf : finite (mul_support f)) (h : ∀ j, 1 ≤ f j) :
+  f i ≤ ∏ᶠ j, f j :=
+by classical;
+calc f i ≤ ∏ j in insert i hf.to_finset, f j :
+  finset.single_le_prod' (λ j hj, h j) (finset.mem_insert_self _ _)
+     ... = ∏ᶠ j, f j                :
+  (finprod_eq_prod_of_mul_support_to_finset_subset _ hf (finset.subset_insert _ _)).symm
+
 lemma finprod_eq_zero {M₀ : Type*} [comm_monoid_with_zero M₀] (f : α → M₀) (x : α)
   (hx : f x = 0) (hf : finite (mul_support f)) :
   ∏ᶠ x, f x = 0 :=

src/data/equiv/basic.lean

@@ -2001,6 +2001,9 @@ end swap
 
 end equiv
 
+lemma plift.eq_up_iff_down_eq {x : plift α} {y : α} : x = plift.up y ↔ x.down = y :=
+equiv.plift.eq_symm_apply
+
 lemma function.injective.map_swap {α β : Type*} [decidable_eq α] [decidable_eq β]
   {f : α → β} (hf : function.injective f) (x y z : α) :
   f (equiv.swap x y z) = equiv.swap (f x) (f y) (f z) :=