fix(ErdosProblems/659): make asymptotic

FormalConjectures/ErdosProblems/659.lean

@@ -22,24 +22,18 @@ import FormalConjectures.Util.ProblemImports
 *Reference:* [erdosproblems.com/659](https://www.erdosproblems.com/659)
 -/
 
-open EuclideanGeometry Finset
+open EuclideanGeometry Finset Real
 
 namespace Erdos659
 
-/-- The minimum number of distinct distances determined by any subset of `points` of size `n`. -/
-noncomputable def minimalDistinctDistancesSubsetOfSize (points : Set ℝ²) (n : ℕ) : ℕ :=
-  sInf {(distinctDistances subset : ℝ) |
-    (subset : Finset ℝ²) (_ : subset.toSet ⊆ points) (_ : subset.card = n)}
-
 /--
 Is there a set of $n$ points in $\mathbb{R}^2$ such that every subset of $4$ points determines at
 least $3$ distances, yet the total number of distinct distances is $\ll \frac{n}{\sqrt{\log n}}$?
 -/
 @[category research open, AMS 52]
-theorem erdos_659 : answer(sorry) ↔ ∃ (a : ℕ → Finset ℝ²), ∀ n, #(a n) = n ∧
-    3 ≤ minimalDistinctDistancesSubsetOfSize (a n) 4 ∧
-    (fun n => (distinctDistances (a n) : ℝ)) ≪ fun (n : ℕ) => n / (n : ℝ).log.sqrt := by
+theorem erdos_659 : answer(sorry) ↔ ∃ A : ℕ → Finset ℝ²,
+   (∀ n, #(A n) = n ∧ ∀ S ⊆ A n, #S = 4 → 3 ≤ distinctDistances S) ∧
+    (fun n ↦ distinctDistances (A n)) ≪ fun n ↦ n / sqrt (log n) :=
   sorry
 
-
 end Erdos659

FormalConjecturesForMathlib/Analysis/Asymptotics/Basic.lean

@@ -17,5 +17,5 @@ limitations under the License.
 import Mathlib.Analysis.Asymptotics.Defs
 import Mathlib.Order.Filter.AtTopBot.Defs
 
-notation f " ≫ " g => Asymptotics.IsBigO Filter.atTop g f
-notation g " ≪ " f => Asymptotics.IsBigO Filter.atTop g f
+notation f " ≫ " g => Asymptotics.IsBigO Filter.atTop (g : ℕ → ℝ) (f : ℕ → ℝ)
+notation g " ≪ " f => Asymptotics.IsBigO Filter.atTop (g : ℕ → ℝ) (f : ℕ → ℝ)