feat(algebra/big_operators/ring): add finset.prod_[one_]sub_ordered (#…

…6811)

Add 2 lemmas useful for partition of unity, `finset.prod_sub_ordered` and `finset.prod_one_sub_ordered`.

Also add an explicit `[decidable_eq]` assumption to `finset.induction_on_max` (without it some `rw`s failed).

src/algebra/big_operators/ring.lean

@@ -118,6 +118,43 @@ calc ∏ a in s, (f a + g a)
       by simp, by funext; intros; simp *⟩ }
 end
 
+/-- `∏ i, (f i + g i) = (∏ i, f i) + ∑ i, g i * (∏ j < i, f j + g j) * (∏ j > i, f j)`. -/
+lemma prod_add_ordered {ι R : Type*} [comm_semiring R] [linear_order ι] (s : finset ι)
+  (f g : ι → R) :
+  (∏ i in s, (f i + g i)) = (∏ i in s, f i) +
+    ∑ i in s, g i * (∏ j in s.filter (< i), (f j + g j)) * ∏ j in s.filter (λ j, i < j), f j :=
+begin
+  refine finset.induction_on_max s (by simp) _,
+  clear s, intros a s ha ihs,
+  have ha' : a ∉ s, from λ ha', (ha a ha').false,
+  rw [prod_insert ha', prod_insert ha', sum_insert ha', filter_insert, if_neg (lt_irrefl a),
+    filter_true_of_mem ha, ihs, add_mul, mul_add, mul_add, add_assoc],
+  congr' 1, rw add_comm, congr' 1,
+  { rw [filter_false_of_mem, prod_empty, mul_one],
+    exact (forall_mem_insert _ _ _).2 ⟨lt_irrefl a, λ i hi, (ha i hi).not_lt⟩ },
+  { rw mul_sum,
+    refine sum_congr rfl (λ i hi, _),
+    rw [filter_insert, if_neg (ha i hi).not_lt, filter_insert, if_pos (ha i hi), prod_insert,
+      mul_left_comm],
+    exact mt (λ ha, (mem_filter.1 ha).1) ha' }
+end
+
+/-- `∏ i, (f i - g i) = (∏ i, f i) - ∑ i, g i * (∏ j < i, f j - g j) * (∏ j > i, f j)`. -/
+lemma prod_sub_ordered {ι R : Type*} [comm_ring R] [linear_order ι] (s : finset ι) (f g : ι → R) :
+  (∏ i in s, (f i - g i)) = (∏ i in s, f i) -
+    ∑ i in s, g i * (∏ j in s.filter (< i), (f j - g j)) * ∏ j in s.filter (λ j, i < j), f j :=
+begin
+  simp only [sub_eq_add_neg],
+  convert prod_add_ordered s f (λ i, -g i),
+  simp,
+end
+
+/-- `∏ i, (1 - f i) = 1 - ∑ i, f i * (∏ j < i, 1 - f j)`. This formula is useful in construction of
+a partition of unity from a collection of “bump” functions.  -/
+lemma prod_one_sub_ordered {ι R : Type*} [comm_ring R] [linear_order ι] (s : finset ι) (f : ι → R) :
+  (∏ i in s, (1 - f i)) = 1 - ∑ i in s, f i * ∏ j in s.filter (< i), (1 - f j) :=
+by { rw prod_sub_ordered, simp }
+
 /--  Summing `a^s.card * b^(n-s.card)` over all finite subsets `s` of a `finset`
 gives `(a + b)^s.card`.-/
 lemma sum_pow_mul_eq_add_pow

src/data/finset/lattice.lean

@@ -445,7 +445,7 @@ lemma min'_insert (a : α) (s : finset α) (H : s.nonempty) :
 * for every `s : finset α` and an element `a` strictly greater than all elements of `s`, `p s`
   implies `p (insert a s)`. -/
 @[elab_as_eliminator]
-lemma induction_on_max {p : finset α → Prop} (s : finset α) (h0 : p ∅)
+lemma induction_on_max [decidable_eq α] {p : finset α → Prop} (s : finset α) (h0 : p ∅)
   (step : ∀ a s, (∀ x ∈ s, x < a) → p s → p (insert a s)) : p s :=
 begin
   induction hn : s.card with n ihn generalizing s,
@@ -465,12 +465,9 @@ end
 * for every `s : finset α` and an element `a` strictly less than all elements of `s`, `p s`
   implies `p (insert a s)`. -/
 @[elab_as_eliminator]
-lemma induction_on_min {p : finset α → Prop} (s : finset α) (h0 : p ∅)
+lemma induction_on_min [decidable_eq α] {p : finset α → Prop} (s : finset α) (h0 : p ∅)
   (step : ∀ a s, (∀ x ∈ s, a < x) → p s → p (insert a s)) : p s :=
-begin
-  refine @induction_on_max (order_dual α) _ _ s h0 (λ a s has hs, _),
-  convert step a s has hs
-end
+@induction_on_max (order_dual α) _ _ _ s h0 step
 
 end max_min