From cee3693deb17ae2ccc482a43cb68a16c26389aea Mon Sep 17 00:00:00 2001 From: David Renshaw Date: Tue, 17 Dec 2024 21:06:56 -0500 Subject: [PATCH] [Imo1982P3] import the shorter solution that just landed --- Compfiles/Imo1982P3.lean | 321 ++++++++------------------------------- lake-manifest.json | 2 +- 2 files changed, 62 insertions(+), 261 deletions(-) diff --git a/Compfiles/Imo1982P3.lean b/Compfiles/Imo1982P3.lean index 81d418e..4d7c833 100644 --- a/Compfiles/Imo1982P3.lean +++ b/Compfiles/Imo1982P3.lean @@ -10,7 +10,7 @@ import ProblemExtraction problem_file { tags := [.Algebra] importedFrom := - "https://github.com/leanprover-community/mathlib4/pull/16190" + "https://github.com/leanprover-community/mathlib4/blob/master/Archive/Imo/Imo1982Q3.lean" } /-! @@ -33,269 +33,70 @@ namespace Imo1982Q3 snip begin /- -The solution is based on the one at the +The solution is based on Solution 1 from the [Art of Problem Solving](https://artofproblemsolving.com/wiki/index.php/1982_IMO_Problems/Problem_3) -website. +website. For part a, we use Sedrakyan's lemma to show the sum is bounded below by +$\frac{4n}{n + 1}$, which can be made arbitrarily close to $4$ by taking large $n$. For part b, we +show the sequence $x_n = 2^{-n}$ satisfies the desired inequality. -/ -lemma sum_Fin_eq_sum_Ico {x : ℕ → ℝ} {N : ℕ} : ∑ n : Fin N, x n = ∑ n ∈ Finset.Ico 0 N, x n := by - rw [Fin.sum_univ_eq_sum_range, Nat.Ico_zero_eq_range] - -lemma ineq₁ {x : ℕ → ℝ} {N : ℕ} (hN : 1 < N) (hx : ∀ i , x (i + 1) ≤ x i) : - x N ≤ (∑ n : Fin (N - 1), x (n + 1)) / (N - 1) := by - have h : ∀ m n : ℕ, n ≤ m → x m ≤ x n := by - intro m n mlen - induction' m, mlen using Nat.le_induction with k _nlek xk_le_xn - · exact le_refl (x n) - · calc - x (k + 1) ≤ x k := hx k - _ ≤ x n := xk_le_xn - rw [le_div_iff₀ (by aesop)] +/-- `x n` is at most the average of all previous terms in the sequence. +This is expressed here with `∑ k ∈ range n, x k` added to both sides. -/ +lemma le_avg {x : ℕ → ℝ} {n : ℕ} (hn : n ≠ 0) (hx : Antitone x) : + ∑ k ∈ Finset.range (n + 1), x k ≤ (∑ k ∈ Finset.range n, x k) * (1 + 1 / n) := by + rw [Finset.sum_range_succ, mul_one_add, add_le_add_iff_left, mul_one_div, + le_div_iff₀ (mod_cast hn.bot_lt), mul_comm, ← nsmul_eq_mul] + conv_lhs => rw [← Finset.card_range n, ← Finset.sum_const] + refine Finset.sum_le_sum fun k hk ↦ hx (le_of_lt ?_) + simpa using hk + +/-- The main inequality used for part a. -/ +lemma ineq {x : ℕ → ℝ} {n : ℕ} (hn : n ≠ 0) (hx : Antitone x) + (h0 : x 0 = 1) (hp : ∀ k, 0 < x k) : + 4 * n / (n + 1) ≤ ∑ k ∈ Finset.range (n + 1), x k ^ 2 / x (k + 1) := by calc - x N * (↑N - 1) = ((N - 1) : ℕ) * x N := by - rw [mul_comm, Nat.cast_sub, Nat.cast_one]; linarith - _ = ↑(Finset.range (N - 1)).card * x N := by rw [Finset.card_range] - _ = ∑ _ ∈ Finset.range (N - 1), x N := by - simp only [Finset.univ_eq_attach, Finset.sum_const, Finset.card_attach, Nat.card_Ioc, nsmul_eq_mul] - _ ≤ ∑ n ∈ Finset.range (N - 1), x (n + 1) := by - apply Finset.sum_le_sum - intro i hi - rw [Finset.mem_range, Nat.lt_sub_iff_add_lt (a := i) (b := 1) (c := N)] at hi - apply h - apply le_of_lt hi - _ = ∑ n : Fin (N - 1), x (↑n + 1) := by rw [Finset.sum_range] - -lemma ineq₂ {x : ℕ → ℝ} {N : ℕ} - (hN : 1 < N) (hx : ∀ i , x (i + 1) ≤ x i) (x_pos : ∀ i, x i > (0 : ℝ)) : - (N - 1) / N * (1 / ∑ n : Fin (N - 1), x (n + 1)) ≤ 1 / (∑ n : Fin N, x (n + 1)) := by - have ne_zero : N - 1 ≠ 0 := Nat.sub_ne_zero_iff_lt.mpr hN - have ne_zero' : (N : ℝ) - 1 ≠ 0 := by - rw [ne_eq]; intro h - rw [sub_eq_iff_eq_add, zero_add] at h - rw [@Nat.cast_eq_one] at h - rw [h] at hN; apply lt_irrefl _ hN - have sum_range_pos : 0 < ∑ i ∈ Finset.range (N - 1), x (i + 1) := by - apply Finset.sum_pos - · intro i _hi - apply x_pos _ - simp [ne_zero] - have mul_sum_pos : 0 < ∑ i ∈ Finset.range (N - 1), x (i + 1) * ↑N / (↑N - 1) := by - apply Finset.sum_pos - · intro i _hi - apply div_pos - · apply mul_pos - · apply x_pos - simp only [Nat.cast_pos] - linarith - rw [lt_sub_iff_add_lt, zero_add, Nat.one_lt_cast] - apply hN - rw [Finset.nonempty_range_iff] - exact ne_zero - have sum_fin_pos : 0 < ∑ n : Fin N, x (↑n + 1) := by - apply Finset.sum_pos; intro i _hi - · apply x_pos (i +1) - rw [Finset.univ_nonempty_iff, ← Fin.pos_iff_nonempty] - linarith - convert_to - (N - 1) / N * (1 / ∑ n ∈ Finset.range (N - 1), x (n + 1)) ≤ 1 / (∑ n : Fin N, x (n + 1)) using 3 - · rw [Finset.sum_range] - convert_to 1 / (N * (∑ n ∈ Finset.range (N - 1), x (n + 1)) / (N - 1)) ≤ 1 / (∑ n : Fin N, x (n + 1)) - · field_simp - convert_to 1 / ∑ i ∈ Finset.range (N - 1), x (i + 1) * ↑N / (↑N - 1) ≤ 1 / (∑ n : Fin N, x (n + 1)) - · rw [mul_comm, Finset.sum_mul, Finset.sum_div] - rw [div_le_div_iff₀ (mul_sum_pos) (sum_fin_pos), one_mul, one_mul, ] - calc ∑ n : Fin N, x (↑n + 1) = ∑ n ∈ Finset.range N, x (n + 1) := by rw [Finset.sum_range] - _ = ∑ n ∈ Finset.range (N - 1 + 1), x (n + 1) := by - rw [Nat.sub_one_add_one_eq_of_pos (by linarith [hN])] - _ = ∑ n ∈ Finset.range (N - 1), x (n + 1) + x N := by - rw [Finset.sum_range_succ, Nat.sub_one_add_one_eq_of_pos (by linarith [hN])] - _ ≤ ∑ n ∈ Finset.range (N - 1), x (n + 1) + (∑ n ∈ Finset.range (N - 1), x (n + 1)) / (↑N - 1) := by - apply add_le_add_left; rw [Finset.sum_range]; apply ineq₁ hN hx; - _ = ∑ n ∈ Finset.range (N - 1), x (n + 1) + (∑ n ∈ Finset.range (N - 1), x (n + 1) / (↑N - 1)) := by - rw [Finset.sum_div] - _ = ∑ n ∈ Finset.range (N - 1), (x (n + 1) + x (n + 1) / (↑N - 1)) := by rw [Finset.sum_add_distrib] - _ = ∑ n ∈ Finset.range (N - 1), N * x (n + 1) / (↑N - 1) := by - apply Finset.sum_congr (by rfl) - intro n _hn - nth_rewrite 1 [ - ← one_mul (x (n + 1)), - ← div_self (a := (N - 1 : ℝ)) (ne_zero'), - mul_comm, - mul_div, - div_add_div_same - ] - nth_rewrite 2 [← mul_one (x (n + 1))] - rw [← mul_add, mul_comm] - simp only [sub_add_cancel] - _ = ∑ i ∈ Finset.range (N - 1), x (i + 1) * ↑N / (↑N - 1) := by - apply Finset.sum_congr (by rfl); intro n _hn; rw [mul_comm] - -lemma ineq₃ {x : ℕ → ℝ} {N : ℕ } (hN : 1 < N) (x_pos : ∀ i, x i > (0 : ℝ)) : - 2 * (∑ n : Fin N, x (n + 1)) ≤ 1 + (∑ n : Fin N, x (n + 1))^2 := by - have sum_fin_pos : 0 < ∑ n : Fin N, x (↑n + 1) := by - apply Finset.sum_pos - · intro i _hi - apply x_pos (i +1) - rw [Finset.univ_nonempty_iff, ←Fin.pos_iff_nonempty] - linarith - calc - 2 * (∑ n : Fin N, x (n + 1)) = 2 * (1^(1/2 : ℝ) * ((∑ n : Fin N, x (n + 1))^2)^(1/2 : ℝ)) := by - rw [Real.one_rpow, one_mul, ← Real.sqrt_eq_rpow, Real.sqrt_sq _] - apply le_of_lt sum_fin_pos - _ ≤ 2 * ((1/2 : ℝ) * 1 + (1/2 : ℝ) * (∑ n : Fin N, x (n + 1))^2) := by - rw [mul_le_mul_left (by norm_num)] - apply Real.geom_mean_le_arith_mean2_weighted - (by norm_num) (by norm_num) (by norm_num) (sq_nonneg _) (by norm_num) - _ ≤ 1 + (∑ n : Fin N, x (n + 1))^2 := by field_simp - -lemma Ico_sdiff_zero_eq_Ico {N : ℕ} : Finset.Ico 0 N \ {0} = Finset.Ico 1 N := by - rw [Finset.sdiff_singleton_eq_erase, Finset.Ico_erase_left, Nat.Ico_succ_left] - -lemma eq₀ {x : ℕ → ℝ} {N : ℕ} (hN : 1 < N) (hx₀ : x 0 = (1 : ℝ)) : - (∑ n : Fin N, (x n))^2 - = 1 + 2 * (∑ n : Fin (N - 1), x (n + 1)) + (∑ n : Fin (N - 1), x (n + 1))^2 := by - have zero_lt_N : 0 < N := by linarith - have two_le_N : 2 ≤ N := by linarith - have : ∀ N, 2 ≤ N → ∑ n : Fin (N - 1), x (↑n + 1) = (∑ n ∈ Finset.Ico 1 N, x n) := by - intro N hN - let f : ℕ → ℝ := (fun n => x (n + 1)) - induction' N, hN using Nat.le_induction with d two_le_d hd - case base => simp - case succ => - have one_le_d : 1 ≤ d := by exact Nat.one_le_of_lt two_le_d - rw [ - ← Finset.sum_range (n := d + 1 - 1) (f := f), - Nat.sub_add_comm (one_le_d), - Finset.sum_range_succ, Finset.sum_range, hd, Finset.sum_Ico_succ_top one_le_d] - simp only [add_right_inj, f] - rw [Nat.sub_add_cancel one_le_d] - rw [ - sum_Fin_eq_sum_Ico, Finset.sum_eq_sum_diff_singleton_add (i := 0) (by simp [zero_lt_N]), - Ico_sdiff_zero_eq_Ico, pow_two, hx₀ - ] - ring_nf - rw [this _ two_le_N]; ring + -- We first use AM-GM. + _ ≤ (∑ k ∈ Finset.range n, x (k + 1) + 1) ^ 2 / + (∑ k ∈ Finset.range n, x (k + 1)) * n / (n + 1) := by + gcongr + rw [le_div_iff₀] + · simpa using four_mul_le_sq_add (∑ k ∈ Finset.range n, x (k + 1)) 1 + · exact Finset.sum_pos (fun k _ ↦ hp _) (Finset.nonempty_range_iff.2 hn) + -- We move the fraction into the denominator. + _ = (∑ k ∈ Finset.range n, x (k + 1) + 1) ^ 2 / + ((∑ k ∈ Finset.range n, x (k + 1)) * (1 + 1 / n)) := by + field_simp + -- We make use of the `le_avg` lemma. + _ ≤ (∑ k ∈ Finset.range (n + 1), x k) ^ 2 / + ∑ k ∈ Finset.range (n + 1), x (k + 1) := by + gcongr + · exact Finset.sum_pos (fun k _ ↦ hp _) Finset.nonempty_range_succ + · exact add_nonneg (Finset.sum_nonneg fun k _ ↦ (hp _).le) zero_le_one + · rw [Finset.sum_range_succ', h0] + · exact le_avg hn (hx.comp_monotone @Nat.succ_le_succ) + -- We conclude by Sedrakyan. + _ ≤ _ := Finset.sq_sum_div_le_sum_sq_div _ x fun k _ ↦ hp (k + 1) snip end -problem iom1982_p3a {x : ℕ → ℝ} (x_pos : ∀ i, x i > (0 : ℝ)) - (hx₀ : x 0 = (1 : ℝ)) - (hx : ∀ i , x (i + 1) ≤ x i) : - ∃ N : ℕ, 3.999 ≤ ∑ n : Fin N, (x n)^2 / x (n + 1) := by - have div_prev_pos : ∀ N > 1, 0 < (↑N - 1) / (N : ℝ) := by - intro N hN - exact div_pos (by linarith) (by linarith) - have sum_xi_pos : ∀ N > 0, 0 < (∑ n : Fin N, x n) := by - intro N hN - apply Finset.sum_pos - · intro i _hi - apply x_pos i - rw [← Finset.card_pos, Finset.card_fin] - apply hN - have sum_xi_pos' : ∀ N > 1, 0 < (∑ n : Fin (N - 1), x (n + 1)) := by - intro N hN - apply Finset.sum_pos - · intro i _hi - apply x_pos _ - rw [← Finset.card_pos, Finset.card_fin, Nat.lt_sub_iff_add_lt, zero_add] - apply hN - have : - ∃ (N : ℕ), 0 < N ∧ 1 < N ∧ 2 < N ∧ (3.999 : ℝ) ≤ 4 * ((N - 1) / N) := by use 4000; norm_num - obtain ⟨N, zero_lt_N, one_lt_N, two_lt_N, ineq₀⟩ := this - use N - calc (3.999 : ℝ) ≤ 4 * ((N - 1) / N) := ineq₀ - _ = (2 + 2) * ((N - 1) / N) := by norm_num - _ = ((2 * (∑ n : Fin (N - 1), x (n + 1)) - + 2 * (∑ n : Fin (N - 1), x (n + 1))) / (∑ n : Fin (N - 1), x (n + 1))) * ((N - 1) / (N)) := by - rw [← div_add_div_same, ← mul_div, div_self, mul_one] - symm - apply (lt_iff_le_and_ne.mp (sum_xi_pos' _ one_lt_N)).right - _ ≤ (1 + (∑ n : Fin (N - 1), x (n + 1))^2 - + 2 * (∑ n : Fin (N - 1), x (n + 1))) / (∑ n : Fin (N - 1), x (n + 1)) * ((N - 1) / (N)) := by - rw [mul_le_mul_right (by apply div_prev_pos N; simp [one_lt_N])] - apply div_le_div₀ - · apply add_nonneg - · apply add_nonneg (by norm_num) (sq_nonneg _) - apply mul_nonneg (by norm_num) - apply (lt_iff_le_and_ne.mp (sum_xi_pos' _ one_lt_N)).left - · apply add_le_add_right - apply ineq₃ _ x_pos - rw [Nat.lt_sub_iff_add_lt, one_add_one_eq_two] - apply two_lt_N - · apply sum_xi_pos' _ one_lt_N - apply le_refl - _ = ((∑ n : Fin N, (x n))^2 / (∑ n : Fin (N - 1), x (n + 1))) * ((N - 1) / (N)) := by - rw [ - eq₀ one_lt_N hx₀, - add_assoc, - add_comm ((∑ n : Fin (N - 1), x (↑n + 1)) ^ 2), - ← add_assoc - ] - _ = ((∑ n : Fin N, (x n))^2) * ((N - 1) / (N)) * (1 / (∑ n : Fin (N - 1), x (n + 1))) := by - rw [← mul_one (((∑ n : Fin N, x ↑n) ^ 2)), mul_div] - ring - _ ≤ ((∑ n : Fin N, (x n))^2 / (∑ n : Fin N, x (n + 1))) := by - nth_rewrite 2 [← mul_one (((∑ n : Fin N, x ↑n) ^ 2))] - rw [← mul_div _ 1, mul_assoc, mul_le_mul_left] - apply ineq₂ one_lt_N hx x_pos - apply sq_pos_of_pos (sum_xi_pos _ zero_lt_N) - _ ≤ ∑ n : Fin N, (x ↑n) ^ 2 / x (↑n + 1) := - Finset.sq_sum_div_le_sum_sq_div _ _ (fun i hi => x_pos (i + 1)) - -noncomputable determine sol : ℕ → ℝ := fun n => (1/2)^n - -problem imo1982_p3b : - (∀ i, sol i > 0) ∧ (∀ i, sol (i + 1) ≤ sol i) ∧ (sol 0 = 1) - ∧ ∀ N, ∑ n ∈ Finset.range (N + 1), (sol n ^2 / (sol (n + 1))) < 4 := by - constructor - · intro i - apply pow_pos (by norm_num) i - constructor - · intro i - apply pow_le_pow_of_le_one (by norm_num) - · rw [one_div_le (by norm_num) (by norm_num), div_one]; norm_num - · apply Nat.le_succ - constructor - · rfl - intro N - dsimp [sol] - rw [ - Finset.sum_eq_sum_diff_singleton_add - (s := Finset.range (N + 1)) (i := 0) (Finset.mem_range.mpr (by linarith)), - pow_zero, zero_add, one_pow, pow_one, one_div_one_div, add_comm - ] - convert_to (2 + ∑ n ∈ Finset.range N, (1/2) ^ n : ℝ) < 4 using 2 - induction' N with k hk - case zero => - simp only [ - zero_add, Finset.range_one, sdiff_self, Finset.bot_eq_empty, one_div, inv_pow, div_inv_eq_mul, - Finset.sum_empty, Finset.range_zero - ] - case succ => - rw [ - Finset.sum_range_succ, ← hk, Finset.range_add_one - ] - simp only [ - one_div, inv_pow, div_inv_eq_mul, Finset.singleton_subset_iff, Finset.mem_insert, - self_eq_add_left, AddLeftCancelMonoid.add_eq_zero, one_ne_zero, and_false, - Finset.mem_range, lt_add_iff_pos_left, add_pos_iff, zero_lt_one, or_true, - Finset.sum_sdiff_eq_sub, lt_self_iff_false, not_false_eq_true, Finset.sum_insert, - Finset.sum_singleton, pow_zero, one_pow, inv_one, zero_add, pow_one, one_mul - ] - rw [ - ← pow_mul, mul_comm, ← inv_pow - ] - nth_rewrite 1 [← inv_inv 2] - rw [ - mul_comm, inv_pow 2⁻¹, ← pow_sub₀ (a := 2⁻¹) (ha := by norm_num) (h := by linarith), add_mul, - one_mul, add_assoc, one_add_one_eq_two, mul_comm k 2, two_mul, add_assoc, - Nat.add_sub_assoc (by linarith), Nat.sub_self, add_zero, inv_pow, add_sub_assoc, add_comm - ] - rw [ - geom_sum_eq (by norm_num), half_sub, div_neg, div_eq_inv_mul, one_div, inv_inv, - mul_comm, ← neg_mul, neg_sub - ] - have h₁: (0 < (2 : ℝ)⁻¹ ^ N) := by positivity - linarith [h₁] - -end Imo1982Q3 +problem imo1982_q3a {x : ℕ → ℝ} (hx : Antitone x) (h0 : x 0 = 1) (hp : ∀ k, 0 < x k) : + ∃ n : ℕ, 3.999 ≤ ∑ k ∈ Finset.range n, (x k) ^ 2 / x (k + 1) := by + use 4000 + convert Imo1982Q3.ineq (Nat.succ_ne_zero 3998) hx h0 hp + norm_num + +noncomputable determine sol : ℕ → ℝ := fun k ↦ 2⁻¹ ^ k + +problem imo1982_q3b : Antitone sol ∧ sol 0 = 1 ∧ (∀ k, 0 < sol k) + ∧ ∀ n, ∑ k ∈ Finset.range n, sol k ^ 2 / sol (k + 1) < 4 := by + refine ⟨?_, pow_zero _, ?_, fun n ↦ ?_⟩ + · apply (pow_right_strictAnti₀ _ _).antitone <;> norm_num + · simp + · have {k : ℕ} : (2 : ℝ)⁻¹ ^ (k * 2) * ((2 : ℝ)⁻¹ ^ k)⁻¹ = (2 : ℝ)⁻¹ ^ k := by + rw [← pow_sub₀] <;> simp [mul_two] + simp_rw [← pow_mul, pow_succ, ← div_eq_mul_inv, div_div_eq_mul_div, mul_comm, mul_div_assoc, + ← Finset.mul_sum, div_eq_mul_inv, this, ← two_add_two_eq_four, ← mul_two, + mul_lt_mul_iff_of_pos_left two_pos] + convert NNReal.coe_lt_coe.2 <| geom_sum_lt (inv_ne_zero two_ne_zero) two_inv_lt_one n + · simp + · norm_num diff --git a/lake-manifest.json b/lake-manifest.json index ce3a9ca..4a95e1c 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -15,7 +15,7 @@ "type": "git", "subDir": null, "scope": "", - "rev": "d5bed454ee2c347b2d60a12fc609ed827c070617", + "rev": "fb40f7550d02605e9a7bf195b85184714c5d06dc", "name": "mathlib", "manifestFile": "lake-manifest.json", "inputRev": "master",