Skip to content

Commit bdecf41

Browse files
mans0954mans0954
committed
Merge branch 'master' into mans0954/quadratic-form-bilinear-map
2 parents a4351bf + 0a0bb6e commit bdecf41

File tree

216 files changed

+2239
-1715
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

216 files changed

+2239
-1715
lines changed

‎Archive.lean‎

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -6,7 +6,9 @@ import Archive.Examples.MersennePrimes
66
import Archive.Examples.PropEncodable
77
import Archive.Hairer
88
import Archive.Imo.Imo1959Q1
9+
import Archive.Imo.Imo1959Q2
910
import Archive.Imo.Imo1960Q1
11+
import Archive.Imo.Imo1960Q2
1012
import Archive.Imo.Imo1962Q1
1113
import Archive.Imo.Imo1962Q4
1214
import Archive.Imo.Imo1964Q1
@@ -15,6 +17,7 @@ import Archive.Imo.Imo1972Q5
1517
import Archive.Imo.Imo1975Q1
1618
import Archive.Imo.Imo1977Q6
1719
import Archive.Imo.Imo1981Q3
20+
import Archive.Imo.Imo1986Q5
1821
import Archive.Imo.Imo1987Q1
1922
import Archive.Imo.Imo1988Q6
2023
import Archive.Imo.Imo1994Q1

‎Archive/Imo/Imo1959Q2.lean‎

Lines changed: 112 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,112 @@
1+
/-
2+
Copyright (c) 2024 Yury Kudryashov. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Yury Kudryashov
5+
-/
6+
import Mathlib.Data.Real.Sqrt
7+
8+
/-!
9+
# IMO 1959 Q2
10+
11+
For what real values of $x$ is
12+
13+
$\sqrt{x+\sqrt{2x-1}} + \sqrt{x-\sqrt{2x-1}} = A,$
14+
15+
given (a) $A=\sqrt{2}$, (b) $A=1$, (c) $A=2$,
16+
where only non-negative real numbers are admitted for square roots?
17+
18+
We encode the equation as a predicate saying both that the equation holds
19+
and that all arguments of square roots are nonnegative.
20+
21+
Then we follow second solution from the
22+
[Art of Problem Solving](https://artofproblemsolving.com/wiki/index.php/1959_IMO_Problems/Problem_2)
23+
website.
24+
Namely, we rewrite the equation as $\sqrt{2x-1}+1+|\sqrt{2x-1}-1|=A\sqrt{2}$,
25+
then consider the cases $\sqrt{2x-1}\le 1$ and $1 < \sqrt{2x-1}$ separately.
26+
-/
27+
28+
open Set Real
29+
30+
namespace Imo1959Q2
31+
32+
def IsGood (x A : ℝ) : Prop :=
33+
sqrt (x + sqrt (2 * x - 1)) + sqrt (x - sqrt (2 * x - 1)) = A ∧ 0 ≤ 2 * x - 1 ∧
34+
0 ≤ x + sqrt (2 * x - 1) ∧ 0 ≤ x - sqrt (2 * x - 1)
35+
36+
variable {x A : ℝ}
37+
38+
theorem isGood_iff : IsGood x A ↔
39+
sqrt (2 * x - 1) + 1 + |sqrt (2 * x - 1) - 1| = A * sqrt 2 ∧ 1 / 2 ≤ x := by
40+
cases le_or_lt (1 / 2) x with
41+
| inl hx =>
42+
have hx' : 0 ≤ 2 * x - 1 := by linarith
43+
have h₁ : x + sqrt (2 * x - 1) = (sqrt (2 * x - 1) + 1) ^ 2 / 2 := by
44+
rw [add_sq, sq_sqrt hx']; field_simp; ring
45+
have h₂ : x - sqrt (2 * x - 1) = (sqrt (2 * x - 1) - 1) ^ 2 / 2 := by
46+
rw [sub_sq, sq_sqrt hx']; field_simp; ring
47+
simp only [IsGood, *, div_nonneg (sq_nonneg _) (zero_le_two (α := ℝ)), sqrt_div (sq_nonneg _),
48+
and_true]
49+
rw [sqrt_sq, sqrt_sq_eq_abs] <;> [skip; positivity]
50+
field_simp
51+
| inr hx =>
52+
have : 2 * x - 1 < 0 := by linarith
53+
simp only [IsGood, this.not_le, hx.not_le]; simp
54+
55+
theorem IsGood.one_half_le (h : IsGood x A) : 1 / 2 ≤ x := (isGood_iff.1 h).2
56+
57+
theorem sqrt_two_mul_sub_one_le_one : sqrt (2 * x - 1) ≤ 1 ↔ x ≤ 1 := by
58+
simp [sqrt_le_iff, ← two_mul]
59+
60+
theorem isGood_iff_eq_sqrt_two (hx : x ∈ Icc (1 / 2) 1) : IsGood x A ↔ A = sqrt 2 := by
61+
have : sqrt (2 * x - 1) ≤ 1 := sqrt_two_mul_sub_one_le_one.2 hx.2
62+
simp only [isGood_iff, hx.1, abs_sub_comm _ (1 : ℝ), abs_of_nonneg (sub_nonneg.2 this), and_true]
63+
suffices 2 = A * sqrt 2 ↔ A = sqrt 2 by convert this using 2; ring
64+
rw [← div_eq_iff, div_sqrt, eq_comm]
65+
positivity
66+
67+
theorem isGood_iff_eq_sqrt (hx : 1 < x) : IsGood x A ↔ A = sqrt (4 * x - 2) := by
68+
have h₁ : 1 < sqrt (2 * x - 1) := by simpa only [← not_le, sqrt_two_mul_sub_one_le_one] using hx
69+
have h₂ : 1 / 2 ≤ x := by linarith
70+
simp only [isGood_iff, h₂, abs_of_pos (sub_pos.2 h₁), add_add_sub_cancel, and_true]
71+
rw [← mul_two, ← div_eq_iff (by positivity), mul_div_assoc, div_sqrt, ← sqrt_mul' _ zero_le_two,
72+
eq_comm]
73+
ring_nf
74+
75+
theorem IsGood.sqrt_two_lt_of_one_lt (h : IsGood x A) (hx : 1 < x) : sqrt 2 < A := by
76+
rw [(isGood_iff_eq_sqrt hx).1 h]
77+
refine sqrt_lt_sqrt zero_le_two ?_
78+
linarith
79+
80+
theorem IsGood.eq_sqrt_two_iff_le_one (h : IsGood x A) : A = sqrt 2 ↔ x ≤ 1 :=
81+
⟨fun hA ↦ not_lt.1 fun hx ↦ (h.sqrt_two_lt_of_one_lt hx).ne' hA, fun hx ↦
82+
(isGood_iff_eq_sqrt_two ⟨h.one_half_le, hx⟩).1 h⟩
83+
84+
theorem IsGood.sqrt_two_lt_iff_one_lt (h : IsGood x A) : sqrt 2 < A ↔ 1 < x :=
85+
⟨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⟩
86+
87+
theorem IsGood.sqrt_two_le (h : IsGood x A) : sqrt 2 ≤ A :=
88+
(le_or_lt x 1).elim (fun hx ↦ (h.eq_sqrt_two_iff_le_one.2 hx).ge) fun hx ↦
89+
(h.sqrt_two_lt_of_one_lt hx).le
90+
91+
theorem isGood_iff_of_sqrt_two_lt (hA : sqrt 2 < A) : IsGood x A ↔ x = (A / 2) ^ 2 + 1 / 2 := by
92+
have : 0 < A := lt_trans (by simp) hA
93+
constructor
94+
· intro h
95+
have hx : 1 < x := by rwa [h.sqrt_two_lt_iff_one_lt] at hA
96+
rw [isGood_iff_eq_sqrt hx, eq_comm, sqrt_eq_iff_sq_eq] at h <;> linarith
97+
· rintro rfl
98+
rw [isGood_iff_eq_sqrt]
99+
· conv_lhs => rw [← sqrt_sq this.le]
100+
ring_nf
101+
· rw [sqrt_lt' this] at hA
102+
linarith
103+
104+
theorem isGood_sqrt2_iff : IsGood x (sqrt 2) ↔ x ∈ Icc (1 / 2) 1 := by
105+
refine ⟨fun h ↦ ?_, fun h ↦ (isGood_iff_eq_sqrt_two h).2 rfl⟩
106+
exact ⟨h.one_half_le, not_lt.1 fun h₁ ↦ (h.sqrt_two_lt_of_one_lt h₁).false⟩
107+
108+
theorem not_isGood_one : ¬IsGood x 1 := fun h ↦
109+
h.sqrt_two_le.not_lt <| (lt_sqrt zero_le_one).2 (by norm_num)
110+
111+
theorem isGood_two_iff : IsGood x 2 ↔ x = 3 / 2 :=
112+
(isGood_iff_of_sqrt_two_lt <| (sqrt_lt' two_pos).2 (by norm_num)).trans <| by norm_num

‎Archive/Imo/Imo1960Q2.lean‎

Lines changed: 68 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,68 @@
1+
/-
2+
Copyright (c) 2024 Yury Kudryashov. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Yury Kudryashov
5+
-/
6+
import Mathlib.Data.Real.Sqrt
7+
8+
/-!
9+
# IMO 1960 Q2
10+
11+
For what values of the variable $x$ does the following inequality hold:
12+
13+
\[\dfrac{4x^2}{(1 - \sqrt {2x + 1})^2} < 2x + 9 \ ?\]
14+
15+
We follow solution at
16+
[Art of Problem Solving](https://artofproblemsolving.com/wiki/index.php/1960_IMO_Problems/Problem_2)
17+
with minor modifications.
18+
-/
19+
20+
open Real Set
21+
22+
namespace Imo1960Q2
23+
24+
/-- The predicate says that `x` satisfies the inequality
25+
26+
\[\dfrac{4x^2}{(1 - \sqrt {2x + 1})^2} < 2x + 9\]
27+
28+
and belongs to the domain of the function on the left-hand side.
29+
-/
30+
@[mk_iff isGood_iff']
31+
structure IsGood (x : ℝ) : Prop where
32+
/-- The number satisfies the inequality. -/
33+
ineq : 4 * x ^ 2 / (1 - sqrt (2 * x + 1)) ^ 2 < 2 * x + 9
34+
/-- The number belongs to the domain of \(\sqrt {2x + 1}\). -/
35+
sqrt_dom : 0 ≤ 2 * x + 1
36+
/-- The number belongs to the domain of the denominator. -/
37+
denom_dom : (1 - sqrt (2 * x + 1)) ^ 2 ≠ 0
38+
39+
/-- Solution of IMO 1960 Q2: solutions of the inequality
40+
are the numbers of the half-closed interval \([-1/2, 45/8)\) except for the number zero. -/
41+
theorem isGood_iff {x} : IsGood x ↔ x ∈ Ico (-1/2) (45/8) \ {0} := by
42+
-- First, note that the denominator is equal to zero at `x = 0`, hence it's not a solution.
43+
rcases eq_or_ne x 0 with rfl | hx
44+
· simp [isGood_iff']
45+
cases lt_or_le x (-1/2) with
46+
| inl hx2 =>
47+
-- Next, if `x < -1/2`, then the square root is undefined.
48+
have : 2 * x + 1 < 0 := by linarith
49+
simp [hx2.not_le, isGood_iff', this.not_le]
50+
| inr hx2 =>
51+
-- Now, if `x ≥ -1/2`, `x ≠ 0`, then the expression is well-defined.
52+
have hx2' : 0 ≤ 2 * x + 1 := by linarith
53+
have H : 1 - sqrt (2 * x + 1) ≠ 0 := by
54+
rw [sub_ne_zero, ne_comm, ne_eq, sqrt_eq_iff_sq_eq hx2' zero_le_one]
55+
simpa
56+
calc
57+
-- Note that the fraction in the LHS is equal to `(1 + sqrt (2 * x + 1)) ^ 2`
58+
IsGood x ↔ (1 + sqrt (2 * x + 1)) ^ 2 < 2 * x + 9 := by
59+
have : 4 * x ^ 2 = (1 + sqrt (2 * x + 1)) ^ 2 * (1 - sqrt (2 * x + 1)) ^ 2 := by
60+
rw [← mul_pow, ← sq_sub_sq, sq_sqrt hx2']
61+
ring
62+
simp [isGood_iff', *]
63+
-- Simplify the inequality
64+
_ ↔ sqrt (2 * x + 1) < 7 / 2 := by
65+
rw [add_sq, sq_sqrt hx2']; constructor <;> intro <;> linarith
66+
_ ↔ 2 * x + 1 < (7 / 2) ^ 2 := sqrt_lt' <| by positivity
67+
_ ↔ x < 45 / 8 := by constructor <;> intro <;> linarith
68+
_ ↔ x ∈ Ico (-1/2) (45/8) \ {0} := by simp [*]

‎Archive/Imo/Imo1986Q5.lean‎

Lines changed: 84 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,84 @@
1+
/-
2+
Copyright (c) 2024 Yury Kudryashov. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Yury Kudryashov
5+
-/
6+
import Mathlib.Data.Real.NNReal
7+
8+
/-!
9+
# IMO 1986 Q5
10+
11+
Find all functions `f`, defined on the non-negative real numbers and taking nonnegative real values,
12+
such that:
13+
14+
- $f(xf(y))f(y) = f(x + y)$ for all $x, y \ge 0$,
15+
- $f(2) = 0$,
16+
- $f(x) \ne 0$ for $0 \le x < 2$.
17+
18+
We formalize the assumptions on `f` in `Imo1986Q5.IsGood` predicate,
19+
then prove `Imo1986Q5.IsGood f ↔ f = fun x ↦ 2 / (2 - x)`.
20+
21+
Note that this formalization relies on the fact that Mathlib uses 0 as the "garbage value",
22+
namely for `2 ≤ x` we have `2 - x = 0` and `2 / (2 - x) = 0`.
23+
24+
Formalization is based on
25+
[Art of Problem Solving](https://artofproblemsolving.com/wiki/index.php/1986_IMO_Problems/Problem_5)
26+
with minor modifications.
27+
-/
28+
29+
open Set NNReal Classical
30+
31+
namespace Imo1986Q5
32+
33+
structure IsGood (f : ℝ≥0 → ℝ≥0) : Prop where
34+
map_add_rev x y : f (x * f y) * f y = f (x + y)
35+
map_two : f 2 = 0
36+
map_ne_zero : ∀ x < 2, f x ≠ 0
37+
38+
namespace IsGood
39+
40+
variable {f : ℝ≥0 → ℝ≥0} (hf : IsGood f) {x y : ℝ≥0}
41+
42+
theorem map_add (x y : ℝ≥0) : f (x + y) = f (x * f y) * f y :=
43+
(hf.map_add_rev x y).symm
44+
45+
theorem map_eq_zero : f x = 0 ↔ 2 ≤ x := by
46+
refine ⟨fun hx₀ ↦ not_lt.1 fun hlt ↦ hf.map_ne_zero x hlt hx₀, fun hle ↦ ?_⟩
47+
rcases exists_add_of_le hle with ⟨x, rfl⟩
48+
rw [add_comm, hf.map_add, hf.map_two, mul_zero]
49+
50+
theorem map_ne_zero_iff : f x ≠ 0 ↔ x < 2 := by simp [hf.map_eq_zero]
51+
52+
theorem map_of_lt_two (hx : x < 2) : f x = 2 / (2 - x) := by
53+
have hx' : 2 - x ≠ 0 := (tsub_pos_of_lt hx).ne'
54+
have hfx : f x ≠ 0 := hf.map_ne_zero_iff.2 hx
55+
apply le_antisymm
56+
· rw [NNReal.le_div_iff hx', ← NNReal.le_div_iff' hfx, tsub_le_iff_right, ← hf.map_eq_zero,
57+
hf.map_add, div_mul_cancel _ hfx, hf.map_two, zero_mul]
58+
· rw [NNReal.div_le_iff' hx', ← hf.map_eq_zero]
59+
refine (mul_eq_zero.1 ?_).resolve_right hfx
60+
rw [hf.map_add_rev, hf.map_eq_zero, tsub_add_cancel_of_le hx.le]
61+
62+
theorem map_eq (x : ℝ≥0) : f x = 2 / (2 - x) :=
63+
match lt_or_le x 2 with
64+
| .inl hx => hf.map_of_lt_two hx
65+
| .inr hx => by rwa [tsub_eq_zero_of_le hx, div_zero, hf.map_eq_zero]
66+
67+
end IsGood
68+
69+
theorem isGood_iff {f : ℝ≥0 → ℝ≥0} : IsGood f ↔ f = fun x ↦ 2 / (2 - x) := by
70+
refine ⟨fun hf ↦ funext hf.map_eq, ?_⟩
71+
rintro rfl
72+
constructor
73+
case map_two => simp
74+
case map_ne_zero => intro x hx; simpa
75+
case map_add_rev =>
76+
intro x y
77+
cases lt_or_le y 2 with
78+
| inl hy =>
79+
have hy' : 2 - y ≠ 0 := (tsub_pos_of_lt hy).ne'
80+
rw [div_mul_div_comm, tsub_mul, mul_assoc, div_mul_cancel _ hy', mul_comm x,
81+
← mul_tsub, tsub_add_eq_tsub_tsub_swap, mul_div_mul_left _ _ two_ne_zero]
82+
| inr hy =>
83+
have : 2 ≤ x + y := le_add_left hy
84+
simp [tsub_eq_zero_of_le, *]

‎Archive/Imo/Imo2008Q3.lean‎

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,6 @@ Copyright (c) 2021 Manuel Candales. All rights reserved.
33
Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Manuel Candales
55
-/
6-
import Mathlib.Algebra.GroupPower.Lemmas
76
import Mathlib.Data.Real.Basic
87
import Mathlib.Data.Real.Sqrt
98
import Mathlib.Data.Nat.Prime

0 commit comments

Comments
 (0)