feat(Algebra/Order): maximally varying version of prod_le_prod_of_subset_of_one_le

Mathlib/Algebra/Module/ZLattice/Summable.lean

@@ -147,9 +147,7 @@ lemma sum_piFinset_Icc_rpow_le {ι : Type*} [Fintype ι] [DecidableEq ι]
         rw [← Real.rpow_natCast, ← Real.rpow_add (by positivity), Nat.cast_sub hd]
         norm_cast
     _ ≤ 2 * d * 3 ^ (d - 1) * ε ^ r * ∑ k ∈ range (n + 1), (k : ℝ) ^ (d - 1 + r) := by
-        gcongr
-        rw [Finset.sum_range_succ', le_add_iff_nonneg_right]
-        positivity
+        grw [Finset.sum_range_succ', Nat.cast_zero, ← Real.rpow_nonneg le_rfl, add_zero]
     _ ≤ 2 * d * 3 ^ (d - 1) * ε ^ r * ∑' k : ℕ, (k : ℝ) ^ (d - 1 + r) := by
         gcongr
         refine Summable.sum_le_tsum _ (fun _ _ ↦ by positivity) (Real.summable_nat_rpow.mpr ?_)

Mathlib/Algebra/Order/BigOperators/Group/Finset.lean

@@ -128,14 +128,26 @@ theorem one_le_prod'' [MulLeftMono N] (h : ∀ i : ι, 1 ≤ f i) : 1 ≤ ∏ i
 theorem prod_le_one' [MulLeftMono N] (h : ∀ i ∈ s, f i ≤ 1) : ∏ i ∈ s, f i ≤ 1 :=
   (prod_le_prod' h).trans_eq (by rw [prod_const_one])
 
-@[to_additive (attr := gcongr) sum_le_sum_of_subset_of_nonneg]
-theorem prod_le_prod_of_subset_of_one_le' [MulLeftMono N] (h : s ⊆ t)
-    (hf : ∀ i ∈ t, i ∉ s → 1 ≤ f i) : ∏ i ∈ s, f i ≤ ∏ i ∈ t, f i := by
+@[to_additive (attr := gcongr)]
+lemma prod_mono_of_subset_of_one_le [MulLeftMono N] (h : s ⊆ t) (hfg : ∀ i ∈ s, f i ≤ g i)
+    (hg : ∀ i ∈ t, i ∉ s → 1 ≤ g i) : ∏ i ∈ s, f i ≤ ∏ i ∈ t, g i := by
   classical calc
-      ∏ i ∈ s, f i ≤ (∏ i ∈ t \ s, f i) * ∏ i ∈ s, f i :=
-        le_mul_of_one_le_left' <| one_le_prod' <| by simpa only [mem_sdiff, and_imp]
-      _ = ∏ i ∈ t \ s ∪ s, f i := (prod_union sdiff_disjoint).symm
-      _ = ∏ i ∈ t, f i := by rw [sdiff_union_of_subset h]
+    ∏ i ∈ s, f i
+    _ ≤ ∏ i ∈ s, g i := by gcongr with i hi; exact hfg i hi
+    _ ≤ (∏ i ∈ t \ s, g i) * ∏ i ∈ s, g i :=
+      le_mul_of_one_le_left' <| one_le_prod' <| by simpa only [mem_sdiff, and_imp]
+    _ = ∏ i ∈ t \ s ∪ s, g i := (prod_union sdiff_disjoint).symm
+    _ = ∏ i ∈ t, g i := by rw [sdiff_union_of_subset h]
+
+@[to_additive]
+lemma prod_mono_of_subset_of_le_one [MulLeftMono N] (h : s ⊆ t) (hfg : ∀ i ∈ s, f i ≤ g i)
+    (hf : ∀ i ∈ t, i ∉ s → f i ≤ 1) : ∏ i ∈ t, f i ≤ ∏ i ∈ s, g i :=
+  prod_mono_of_subset_of_one_le (N := Nᵒᵈ) h hfg hf
+
+@[to_additive sum_le_sum_of_subset_of_nonneg]
+theorem prod_le_prod_of_subset_of_one_le' [MulLeftMono N] (h : s ⊆ t)
+    (hf : ∀ i ∈ t, i ∉ s → 1 ≤ f i) : ∏ i ∈ s, f i ≤ ∏ i ∈ t, f i :=
+  prod_mono_of_subset_of_one_le h (by simp) hf
 
 @[to_additive]
 theorem prod_le_prod_of_subset_of_le_one'

Mathlib/Algebra/Order/BigOperators/GroupWithZero/Finset.lean

@@ -67,27 +67,41 @@ lemma le_prod_max_one {M : Type*} [CommMonoidWithZero M] [LinearOrder M] [ZeroLE
   exact this ▸ prod_le_prod (fun _ _ ↦ by grind [zero_le_one]) fun _ _ ↦ by grind
 
 @[gcongr]
-theorem prod_le_prod_of_subset_of_one_le (h : s ⊆ t)
-    (hf0 : ∀ i ∈ s, 0 ≤ f i)
-    (hf : ∀ i ∈ t, i ∉ s → 1 ≤ f i) : ∏ i ∈ s, f i ≤ ∏ i ∈ t, f i := by
+lemma prod_mono_of_subset_of_one_le₀ (h : s ⊆ t) (hf₀ : ∀ i ∈ s, 0 ≤ f i) (hfg : ∀ i ∈ s, f i ≤ g i)
+    (hf : ∀ i ∈ t, i ∉ s → 1 ≤ g i) : ∏ i ∈ s, f i ≤ ∏ i ∈ t, g i := by
   have := posMulMono_iff_mulPosMono.1 ‹PosMulMono R›
   classical
   calc
-      ∏ i ∈ s, f i ≤ (∏ i ∈ t \ s, f i) * ∏ i ∈ s, f i :=
-        le_mul_of_one_le_left (prod_nonneg hf0) <| one_le_prod <| by simpa only [mem_sdiff, and_imp]
-      _ = ∏ i ∈ t \ s ∪ s, f i := (prod_union sdiff_disjoint).symm
-      _ = ∏ i ∈ t, f i := by rw [sdiff_union_of_subset h]
-
-theorem prod_le_prod_of_subset_of_le_one (h : s ⊆ t) (hf0 : ∀ i ∈ t, 0 ≤ f i)
-    (hf : ∀ i ∈ t, i ∉ s → f i ≤ 1) :
-    ∏ i ∈ t, f i ≤ ∏ i ∈ s, f i := by
+      ∏ i ∈ s, f i
+    _ ≤ ∏ i ∈ s, g i := by gcongr with i hi; exacts [hf₀, hfg i hi]
+    _ ≤ (∏ i ∈ t \ s, g i) * ∏ i ∈ s, g i :=
+      le_mul_of_one_le_left (prod_nonneg fun i hi ↦ (hf₀ i hi).trans (hfg i hi)) <|
+        one_le_prod <| by simpa only [mem_sdiff, and_imp]
+    _ = ∏ i ∈ t \ s ∪ s, g i := (prod_union sdiff_disjoint).symm
+    _ = ∏ i ∈ t, g i := by rw [sdiff_union_of_subset h]
+
+lemma prod_mono_of_subset_of_le_one₀ (h : s ⊆ t) (hg₀ : ∀ i ∈ t, 0 ≤ g i) (hgf : ∀ i ∈ s, g i ≤ f i)
+    (hf : ∀ i ∈ t, i ∉ s → g i ≤ 1) :
+    ∏ i ∈ t, g i ≤ ∏ i ∈ s, f i := by
   have := posMulMono_iff_mulPosMono.1 ‹PosMulMono R›
   classical
   calc
-    ∏ i ∈ t, f i = ∏ i ∈ t \ s ∪ s, f i := by rw [sdiff_union_of_subset h]
-    _ = (∏ i ∈ t \ s, f i) * ∏ i ∈ s, f i := prod_union sdiff_disjoint
-    _ ≤ ∏ i ∈ s, f i :=
+    ∏ i ∈ t, g i
+    _ = ∏ i ∈ t \ s ∪ s, g i := by rw [sdiff_union_of_subset h]
+    _ = (∏ i ∈ t \ s, g i) * ∏ i ∈ s, g i := prod_union sdiff_disjoint
+    _ ≤ ∏ i ∈ s, g i :=
       mul_le_of_le_one_left (prod_nonneg (by grind)) (prod_le_one (by grind) (by grind))
+    _ ≤ ∏ i ∈ s, f i := by gcongr with i hi; exacts [fun i hi ↦ hg₀ _ <| h hi, hgf i hi]
+
+@[gcongr]
+lemma prod_le_prod_of_subset_of_one_le (h : s ⊆ t) (hf₀ : ∀ i ∈ s, 0 ≤ f i)
+    (hf : ∀ i ∈ t, i ∉ s → 1 ≤ f i) : ∏ i ∈ s, f i ≤ ∏ i ∈ t, f i :=
+  prod_mono_of_subset_of_one_le₀ h hf₀ (by simp) hf
+
+lemma prod_le_prod_of_subset_of_le_one (h : s ⊆ t) (hf₀ : ∀ i ∈ t, 0 ≤ f i)
+    (hf : ∀ i ∈ t, i ∉ s → f i ≤ 1) :
+    ∏ i ∈ t, f i ≤ ∏ i ∈ s, f i :=
+  prod_mono_of_subset_of_le_one₀ h hf₀ (by simp) hf
 
 theorem prod_mono_set_of_one_le (hf : ∀ x, 1 ≤ f x) :
     Monotone fun s ↦ ∏ x ∈ s, f x :=

Mathlib/Analysis/Complex/Exponential.lean

@@ -247,8 +247,7 @@ theorem sum_le_exp_of_nonneg {x : ℝ} (hx : 0 ≤ x) (n : ℕ) : ∑ i ∈ rang
       refine le_lim (CauSeq.le_of_exists ⟨n, fun j hj => ?_⟩)
       simp only [exp', const_apply, re_sum]
       norm_cast
-      refine sum_le_sum_of_subset_of_nonneg (range_mono hj) fun _ _ _ ↦ ?_
-      positivity
+      gcongr
     _ = exp x := by rw [exp, Complex.exp, ← cauSeqRe, lim_re]
 
 lemma pow_div_factorial_le_exp (hx : 0 ≤ x) (n : ℕ) : x ^ n / n ! ≤ exp x :=