diff --git a/src/algebra/big_operators/basic.lean b/src/algebra/big_operators/basic.lean index 00e10065534aa..dc5da005d13ce 100644 --- a/src/algebra/big_operators/basic.lean +++ b/src/algebra/big_operators/basic.lean @@ -774,6 +774,12 @@ begin { rw [nat.add_succ, prod_range_succ, hm, prod_range_succ, mul_assoc], }, end +@[to_additive] +lemma prod_range_add_div_prod_range {α : Type*} [comm_group α] (f : ℕ → α) (n m : ℕ) : + (∏ k in range (n + m), f k) / (∏ k in range n, f k) = ∏ k in finset.range m, f (n + k) := +div_eq_of_eq_mul' (prod_range_add f n m) + + @[to_additive] lemma prod_range_zero (f : ℕ → β) : ∏ k in range 0, f k = 1 := diff --git a/src/algebra/group/basic.lean b/src/algebra/group/basic.lean index cd43b0856a785..1c4f948c6c00d 100644 --- a/src/algebra/group/basic.lean +++ b/src/algebra/group/basic.lean @@ -336,6 +336,8 @@ calc a / 1 = a * 1⁻¹ : div_eq_mul_inv a 1 end group section add_group +-- TODO: Generalize the contents of this section with to_additive as per +-- https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/.238667 variables {G : Type u} [add_group G] {a b c d : G} @[simp] lemma sub_self (a : G) : a - a = 0 := @@ -445,9 +447,15 @@ variables {G : Type u} [comm_group G] lemma mul_inv (a b : G) : (a * b)⁻¹ = a⁻¹ * b⁻¹ := by rw [mul_inv_rev, mul_comm] +@[to_additive] +lemma div_eq_of_eq_mul' {a b c : G} (h : a = b * c) : a / b = c := +by rw [h, div_eq_mul_inv, mul_comm, inv_mul_cancel_left] + end comm_group section add_comm_group +-- TODO: Generalize the contents of this section with to_additive as per +-- https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/.238667 variables {G : Type u} [add_comm_group G] {a b c d : G} local attribute [simp] add_assoc add_comm add_left_comm sub_eq_add_neg @@ -473,9 +481,6 @@ by simp lemma eq_sub_of_add_eq' (h : c + a = b) : a = b - c := by simp [h.symm] -lemma sub_eq_of_eq_add' (h : a = b + c) : a - b = c := -begin simp [h], rw [add_left_comm], simp end - lemma eq_add_of_sub_eq' (h : a - b = c) : a = b + c := by simp [h.symm] diff --git a/src/data/complex/exponential.lean b/src/data/complex/exponential.lean index 0f20ee63741b6..3db31ed1fc464 100644 --- a/src/data/complex/exponential.lean +++ b/src/data/complex/exponential.lean @@ -210,6 +210,7 @@ by rw [sum_sigma', sum_sigma']; exact sum_bij mem_range.2 (nat.lt_succ_of_le (nat.le_add_left _ _))⟩, sigma.mk.inj_iff.2 ⟨rfl, heq_of_eq (nat.add_sub_cancel _ _).symm⟩⟩⟩) +-- TODO move to src/algebra/big_operators/basic.lean, rewrite with comm_group, and make to_additive lemma sum_range_sub_sum_range {α : Type*} [add_comm_group α] {f : ℕ → α} {n m : ℕ} (hnm : n ≤ m) : ∑ k in range m, f k - ∑ k in range n, f k = ∑ k in (range m).filter (λ k, n ≤ k), f k := @@ -1279,10 +1280,10 @@ begin refine sum_le_sum (λ m hm, _), rw [abs_mul, abv_pow abs, abs_div, abs_cast_nat], refine mul_le_mul_of_nonneg_left ((div_le_div_right _).2 _) _, - exact nat.cast_pos.2 (nat.factorial_pos _), - rw abv_pow abs, - exact (pow_le_one _ (abs_nonneg _) hx), - exact pow_nonneg (abs_nonneg _) _ + { exact nat.cast_pos.2 (nat.factorial_pos _), }, + { rw abv_pow abs, + exact (pow_le_one _ (abs_nonneg _) hx), }, + { exact pow_nonneg (abs_nonneg _) _ }, end ... = abs x ^ n * (∑ m in (range j).filter (λ k, n ≤ k), (1 / m! : ℝ)) : by simp [abs_mul, abv_pow abs, abs_div, mul_sum.symm] @@ -1290,6 +1291,41 @@ begin mul_le_mul_of_nonneg_left (sum_div_factorial_le _ _ hn) (pow_nonneg (abs_nonneg _) _) end +lemma exp_bound' {x : ℂ} {n : ℕ} (hx : abs x / (n.succ) ≤ 1 / 2) : + abs (exp x - ∑ m in range n, x ^ m / m!) ≤ abs x ^ n / (n!) * 2 := +begin + rw [← lim_const (∑ m in range n, _), exp, sub_eq_add_neg, ← lim_neg, lim_add, ← lim_abs], + refine lim_le (cau_seq.le_of_exists ⟨n, λ j hj, _⟩), + simp_rw [←sub_eq_add_neg], + show abs (∑ m in range j, x ^ m / m! - ∑ m in range n, x ^ m / m!) ≤ abs x ^ n / (n!) * 2, + let k := j - n, + have hj : j = n + k := (nat.add_sub_of_le hj).symm, + rw [hj, sum_range_add_sub_sum_range], + calc abs (∑ (i : ℕ) in range k, x ^ (n + i) / ((n + i)! : ℂ)) + ≤ ∑ (i : ℕ) in range k, abs (x ^ (n + i) / ((n + i)! : ℂ)) : abv_sum_le_sum_abv _ _ + ... ≤ ∑ (i : ℕ) in range k, (abs x) ^ (n + i) / (n + i)! : + by simp only [complex.abs_cast_nat, complex.abs_div, abv_pow abs] + ... ≤ ∑ (i : ℕ) in range k, (abs x) ^ (n + i) / (n! * n.succ ^ i) : _ + ... = ∑ (i : ℕ) in range k, (abs x) ^ (n) / (n!) * ((abs x)^i / n.succ ^ i) : _ + ... ≤ abs x ^ n / (↑n!) * 2 : _, + { refine sum_le_sum (λ m hm, div_le_div (pow_nonneg (abs_nonneg x) (n + m)) (le_refl _) _ _), + { exact_mod_cast mul_pos n.factorial_pos (pow_pos n.succ_pos _), }, + { exact_mod_cast (nat.factorial_mul_pow_le_factorial), }, }, + { refine finset.sum_congr rfl (λ _ _, _), + simp only [pow_add, div_eq_inv_mul, mul_inv', mul_left_comm, mul_assoc], }, + { rw [←mul_sum], + apply mul_le_mul_of_nonneg_left, + { simp_rw [←div_pow], + rw [←geom_sum_def, geom_sum_eq, div_le_iff_of_neg], + { transitivity (-1 : ℝ), + { linarith }, + { simp only [neg_le_sub_iff_le_add, div_pow, nat.cast_succ, le_add_iff_nonneg_left], + exact div_nonneg (pow_nonneg (abs_nonneg x) k) (pow_nonneg (n+1).cast_nonneg k) } }, + { linarith }, + { linarith }, }, + { exact div_nonneg (pow_nonneg (abs_nonneg x) n) (nat.cast_nonneg (n!)), }, }, +end + lemma abs_exp_sub_one_le {x : ℂ} (hx : abs x ≤ 1) : abs (exp x - 1) ≤ 2 * abs x := calc abs (exp x - 1) = abs (exp x - ∑ m in range 1, x ^ m / m!) : diff --git a/src/data/nat/factorial.lean b/src/data/nat/factorial.lean index 6f35f5e9a1b63..d8c97a02ca429 100644 --- a/src/data/nat/factorial.lean +++ b/src/data/nat/factorial.lean @@ -159,6 +159,18 @@ begin exact add_factorial_succ_le_factorial_add_succ i h, end +lemma factorial_mul_pow_sub_le_factorial {n m : ℕ} (hnm : n ≤ m) : n! * n ^ (m - n) ≤ m! := +begin + suffices : n! * (n + 1) ^ (m - n) ≤ m!, + { apply trans _ this, + rw mul_le_mul_left, + apply pow_le_pow_of_le_left (zero_le n) (le_succ n), + exact factorial_pos n,}, + convert nat.factorial_mul_pow_le_factorial, + exact (nat.add_sub_of_le hnm).symm, +end + + end factorial /-! ### Ascending and descending factorials -/