-
Notifications
You must be signed in to change notification settings - Fork 8
/
Imo1959P2.lean
135 lines (107 loc) · 4.89 KB
/
Imo1959P2.lean
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
/-
Copyright (c) 2024 Yury Kudryashov. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Yury Kudryashov
-/
import Mathlib.Data.Real.Sqrt
import ProblemExtraction
problem_file {
tags := [.Algebra]
importedFrom :=
"https://github.com/leanprover-community/mathlib4/blob/master/Archive/Imo/Imo1959Q2.lean"
}
/-!
# International Mathematical Olympiad 1959, Problem 2
For what real values of x is
√(x+√(2x-1)) + √(x-√(2x-1)) = A,
given:
(a) A = √2
(b) A = 1
(c) A = 2,
where only non-negative real numbers are admitted for square roots?
-/
open Set Real
namespace Imo1959P2
def IsGood (x A : ℝ) : Prop :=
sqrt (x + sqrt (2 * x - 1)) + sqrt (x - sqrt (2 * x - 1)) = A ∧ 0 ≤ 2 * x - 1 ∧
0 ≤ x + sqrt (2 * x - 1) ∧ 0 ≤ x - sqrt (2 * x - 1)
variable {x A : ℝ}
snip begin
/-
We follow second solution from the
[Art of Problem Solving](https://artofproblemsolving.com/wiki/index.php/1959_IMO_Problems/Problem_2)
website.
Namely, we rewrite the equation as $\sqrt{2x-1}+1+|\sqrt{2x-1}-1|=A\sqrt{2}$,
then consider the cases $\sqrt{2x-1}\le 1$ and $1 < \sqrt{2x-1}$ separately.
-/
theorem isGood_iff : IsGood x A ↔
sqrt (2 * x - 1) + 1 + |sqrt (2 * x - 1) - 1| = A * sqrt 2 ∧ 1 / 2 ≤ x := by
cases le_or_lt (1 / 2) x with
| inl hx =>
have hx' : 0 ≤ 2 * x - 1 := by linarith
have h₁ : x + sqrt (2 * x - 1) = (sqrt (2 * x - 1) + 1) ^ 2 / 2 := by
rw [add_sq, sq_sqrt hx']; field_simp; ring
have h₂ : x - sqrt (2 * x - 1) = (sqrt (2 * x - 1) - 1) ^ 2 / 2 := by
rw [sub_sq, sq_sqrt hx']; field_simp; ring
simp only [IsGood, *, div_nonneg (sq_nonneg _) (zero_le_two (α := ℝ)), sqrt_div (sq_nonneg _),
and_true]
rw [sqrt_sq, sqrt_sq_eq_abs] <;> [skip; positivity]
field_simp
| inr hx =>
have : 2 * x - 1 < 0 := by linarith
simp only [IsGood, this.not_le, hx.not_le]; simp
theorem IsGood.one_half_le (h : IsGood x A) : 1 / 2 ≤ x := (isGood_iff.1 h).2
theorem sqrt_two_mul_sub_one_le_one : sqrt (2 * x - 1) ≤ 1 ↔ x ≤ 1 := by
simp [sqrt_le_iff, ← two_mul]
theorem isGood_iff_eq_sqrt_two (hx : x ∈ Icc (1 / 2) 1) : IsGood x A ↔ A = sqrt 2 := by
have : sqrt (2 * x - 1) ≤ 1 := sqrt_two_mul_sub_one_le_one.2 hx.2
simp only [isGood_iff, hx.1, abs_sub_comm _ (1 : ℝ), abs_of_nonneg (sub_nonneg.2 this), and_true]
suffices 2 = A * sqrt 2 ↔ A = sqrt 2 by convert this using 2; ring
rw [← div_eq_iff, div_sqrt, eq_comm]
positivity
theorem isGood_iff_eq_sqrt (hx : 1 < x) : IsGood x A ↔ A = sqrt (4 * x - 2) := by
have h₁ : 1 < sqrt (2 * x - 1) := by simpa only [← not_le, sqrt_two_mul_sub_one_le_one] using hx
have h₂ : 1 / 2 ≤ x := by linarith
simp only [isGood_iff, h₂, abs_of_pos (sub_pos.2 h₁), add_add_sub_cancel, and_true]
rw [← mul_two, ← div_eq_iff (by positivity), mul_div_assoc, div_sqrt, ← sqrt_mul' _ zero_le_two,
eq_comm]
ring_nf
theorem IsGood.sqrt_two_lt_of_one_lt (h : IsGood x A) (hx : 1 < x) : sqrt 2 < A := by
rw [(isGood_iff_eq_sqrt hx).1 h]
refine sqrt_lt_sqrt zero_le_two ?_
linarith
theorem IsGood.eq_sqrt_two_iff_le_one (h : IsGood x A) : A = sqrt 2 ↔ x ≤ 1 :=
⟨fun hA ↦ not_lt.1 fun hx ↦ (h.sqrt_two_lt_of_one_lt hx).ne' hA, fun hx ↦
(isGood_iff_eq_sqrt_two ⟨h.one_half_le, hx⟩).1 h⟩
theorem IsGood.sqrt_two_lt_iff_one_lt (h : IsGood x A) : sqrt 2 < A ↔ 1 < x :=
⟨fun hA ↦ not_le.1 fun hx ↦ hA.ne' <| h.eq_sqrt_two_iff_le_one.2 hx, h.sqrt_two_lt_of_one_lt⟩
theorem IsGood.sqrt_two_le (h : IsGood x A) : sqrt 2 ≤ A :=
(le_or_lt x 1).elim (fun hx ↦ (h.eq_sqrt_two_iff_le_one.2 hx).ge) fun hx ↦
(h.sqrt_two_lt_of_one_lt hx).le
theorem isGood_iff_of_sqrt_two_lt (hA : sqrt 2 < A) : IsGood x A ↔ x = (A / 2) ^ 2 + 1 / 2 := by
have : 0 < A := lt_trans (by simp) hA
constructor
· intro h
have hx : 1 < x := by rwa [h.sqrt_two_lt_iff_one_lt] at hA
rw [isGood_iff_eq_sqrt hx, eq_comm, sqrt_eq_iff_sq_eq] at h <;> linarith
· rintro rfl
rw [isGood_iff_eq_sqrt]
· conv_lhs => rw [← sqrt_sq this.le]
ring_nf
· rw [sqrt_lt' this] at hA
linarith
snip end
determine solution_set_sqrt2 : Set ℝ := Icc (1 / 2) 1
problem imo1959_p2a : IsGood x (sqrt 2) ↔ x ∈ solution_set_sqrt2 := by
refine ⟨fun h ↦ ?_, fun h ↦ (isGood_iff_eq_sqrt_two h).2 rfl⟩
exact ⟨h.one_half_le, not_lt.1 fun h₁ ↦ (h.sqrt_two_lt_of_one_lt h₁).false⟩
determine solution_set_one : Set ℝ := ∅
problem imo1959_p2b : IsGood x 1 ↔ x ∈ solution_set_one := by
have not_isGood_one : ¬IsGood x 1 := fun h ↦
h.sqrt_two_le.not_lt <| (lt_sqrt zero_le_one).2 (by norm_num)
exact iff_of_false not_isGood_one fun a ↦ a
determine solution_set_two : Set ℝ := { 3 / 2 }
problem imo1959_p2c : IsGood x 2 ↔ x ∈ solution_set_two := by
rw [mem_singleton_iff]
exact
(isGood_iff_of_sqrt_two_lt <| (sqrt_lt' two_pos).2 (by norm_num)).trans <| by norm_num