2025 Israel National Olympiad Problem 7
For a positive integer $n$, let $A_n$ be the set of quadruplets $(a,b,c,d)$ of integers, satisfying the following properties simultaneously:
$0\le a\le c\le n,$
$0\le b\le d\le n,$
$c+d>n,$ and
$bc=ad+1.$
Moreover, define
$$\alpha_n=\sum_{(a,b,c,d)\in A_n}\frac{1}{ab+cd}.$$
Find all real numbers $t$ such that $\alpha_n>t$ for every positive integer $n$.
import Mathlib.Data.Real.Basic
import Mathlib.Data.Fintype.BigOperators
open Finset
open BigOperators
def A (n : ℕ) : Finset ((ℕ × ℕ) × (ℕ × ℕ)) :=
((range (n + 1) ×ˢ range (n + 1)) ×ˢ (range (n + 1) ×ˢ range (n + 1))).filter
(fun ((a, b), (c, d)) => a ≤ c ∧ b ≤ d ∧ c + d > n ∧ b * c = a * d + 1)
noncomputable def α (n : ℕ) : ℝ := ∑ x ∈ A n, (1 : ℝ) / (x.1.1 * x.1.2 + x.2.1 * x.2.2)
noncomputable def answer : ℝ := sorry
theorem solution : IsGLB { α n | n > 0 } answer := sorry
Submit Solution
Login to submit a solution.
Recent Submissions
| # | User | Time (UTC) | Status |
|---|---|---|---|
| 174 | cwrv | Long time ago | PASSED |
| 133 | Kitsune | Long time ago | PASSED |