Fix Erdős 330 statement. (google-deepmind#1518)

The definitions of `Rep`, `UnrepWithout`, and `MinAsymptoticAddBasis`
are updated to include a parameter `h` representing the maximum number
of terms in the sum. The main theorem statement now quantifies over such
an order `h`.

Author: mo271

FormalConjectures/ErdosProblems/330.lean

@@ -27,19 +27,19 @@ namespace Erdos330
 open Set
 open scoped BigOperators
 
-/-- `Rep A m` means `m` is a sum of **finitely many** elements of `A`
-    (i.e., representable by *some* finite number of terms, not a fixed order). -/
-def Rep (A : Set ℕ) (m : ℕ) : Prop :=
-  ∃ k : ℕ, ∃ f : Fin k → ℕ, (∀ i, f i ∈ A) ∧ (∑ i : Fin k, f i) = m
+/-- `Rep A m h` means `m` is a sum of at most `h` elements of `A`x. -/
+def Rep (A : Set ℕ) (m h : ℕ) : Prop :=
+  ∃ k : ℕ, k ≤ h ∧ ∃ f : Fin k → ℕ, (∀ i, f i ∈ A) ∧ (∑ i : Fin k, f i) = m
 
-/-- Integers **not** representable as a finite sum of elements of `A` **while avoiding** `n`. -/
-def UnrepWithout (A : Set ℕ) (n : ℕ) : Set ℕ :=
-  {m | ¬ Rep (A \ {n}) m}
+/-- Integers **not** representable as a finite sum of elements with at most `h` terms of `A`
+**while avoiding** `n`. -/
+def UnrepWithout (A : Set ℕ) (n h: ℕ) : Set ℕ :=
+  {m | ¬ Rep (A \ {n}) m h}
 
-/-- An asymptotic additive basis is minimal when one cannot obtain an asymptotic
+/-- An asymptotic additive basis of order `h` is minimal when one cannot obtain an asymptotic
 additive basis by removing any element from it. -/
-def MinAsymptoticAddBasis (A : Set ℕ) : Prop :=
-  IsAsymptoticAddBasis A ∧ ∀ n ∈ A, ¬ IsAsymptoticAddBasis (A \ {n})
+def MinAsymptoticAddBasisOfOrder (A : Set ℕ) (h : ℕ) : Prop :=
+  IsAsymptoticAddBasisOfOrder A h ∧ ∀ n ∈ A, ¬ IsAsymptoticAddBasisOfOrder (A \ {n}) h
 
 /--
 Does there exist a minimal basis $A \subset \mathbb{N}$ with positive density
@@ -48,8 +48,8 @@ cannot be represented without using $n$ is positive?
 -/
 @[category research open, AMS 5 11]
 theorem erdos_330_statement :
-    answer(sorry) ↔ ∃ (A : Set ℕ),  MinAsymptoticAddBasis A ∧ A.HasPosDensity ∧
-    ∀ n ∈ A, Set.HasPosDensity (UnrepWithout A n) := by
+    answer(sorry) ↔ ∃ (A : Set ℕ), ∃ h, MinAsymptoticAddBasisOfOrder A h ∧ A.HasPosDensity ∧
+    ∀ n ∈ A, Set.HasPosDensity (UnrepWithout A n h) := by
   sorry
 
 end Erdos330