Erdős 312

Stream: Formal conjectures

[AYUSH DEBNATH]

What is the conjecture

https://www.erdosproblems.com/312

Does there exist some c>0 such that, for any K>1, whenever A is a sufficiently large finite multiset of integers with ∑n∈A1n>K there exists some S⊆A such that
1−e−cK<∑n∈S1n≤1?

how do I approach this issue? I have been assigned this issue

[Moritz Firsching]

Thanks for taking a stab at the issue! Where are you stuck at? I would start with something like the following:

import FormalConjectures.Util.ProblemImports

/-!
# Erdős Problem 312

*Reference:* [erdosproblems.com/312](https://www.erdosproblems.com/312)
-/

open Filter

open scoped Topology Real

namespace Erdos312

/--
...
-/
@[category research open, AMS 5 11]
theorem erdos_312 : (∃ᵉ  (c : ℝ), 0 < c ∧
  ∀ (K : ℝ), 1 < K →
    ∃ (N₀ : ℕ),
      ∀ (A : Multiset Nat),
        (A.card ≥ N₀ ∧ (A.map (fun (n : Nat) => (n : ℝ)⁻¹)).sum > K) →
          ∃ (S : Multiset Nat), S ⊆ A ∧
          ...) ↔ answer(sorry) := by sorry

end Erdos312

[Yaël Dillies]

@Moritz Firsching, using subset on multiset is incorrect here. What about using a family indexed by a fintype instead?

[AYUSH DEBNATH]

import FormalConjectures.Util.ProblemImports

/-!

Erdős Problem 312 — Fintype Formulation

Reference: https://www.erdosproblems.com/312

We state a version of the problem using Fin n → ℕ families and Finset (Fin n) subsets
instead of multisets. This makes multiplicities explicit by indexing the family with Fin n.
-/

open scoped BigOperators Topology Real
open Filter

namespace Erdos312
noncomputable section

/--
hsumIdx a S is the harmonic sum of the entries of the indexed family a : Fin n → ℕ
restricted to a subset of indices S : Finset (Fin n).
-/
def hsumIdx {n : ℕ} (a : Fin n → ℕ) (S : Finset (Fin n)) : ℝ :=
∑ i in S, (a i : ℝ)⁻¹

/--
hsumAll a is the total harmonic sum of all entries of a : Fin n → ℕ.
This is just the sum over all indices Fin n.
-/
def hsumAll {n : ℕ} (a : Fin n → ℕ) : ℝ :=
∑ i : Fin n, (a i : ℝ)⁻¹

@[simp]
lemma hsumIdx_empty {n} (a : Fin n → ℕ) : hsumIdx a ∅ = 0 := by
simp [hsumIdx]

@[simp]
lemma hsumAll_eq_univ_sum {n} (a : Fin n → ℕ) :
hsumAll a = ∑ i in (Finset.univ : Finset (Fin n)), (a i : ℝ)⁻¹ := by
classical
simp [hsumAll]

/-!

Main theorem (fintype version)

The problem asks: does there exist a constant c > 0 such that for every K > 1,
whenever a : Fin n → ℕ is large enough and has harmonic sum > K,
we can choose a subfamily (given by S : Finset (Fin n)) whose harmonic sum lies
in the interval (1 - exp(-c*K), 1]?
-/

/--
Fintype-indexed version of Erdős Problem 312.

• c is a positive universal constant.
• For each K > 1, there exists an N₀ such that:
  • For all sufficiently large n ≥ N₀ and families a : Fin n → ℕ,
  • If the total harmonic sum hsumAll a > K,
  • Then there exists a subset of indices S : Finset (Fin n) with
    1 - exp(-(c*K)) < hsumIdx a S ≤ 1.

This statement mirrors the original problem, but is easier to handle formally
because it avoids the subtlety of multiset-subset with multiplicities.
-/
@[category research open, AMS 5 11]
theorem erdos_312_fintype :
(∃ᵉ (c : ℝ), 0 < c ∧
∀ (K : ℝ), 1 < K →
∃ (N₀ : ℕ),
∀ (n : ℕ) (a : Fin n → ℕ),
(n ≥ N₀ ∧ hsumAll a > K) →
∃ (S : Finset (Fin n)),
1 - Real.exp (-(c * K)) < hsumIdx a S ∧
hsumIdx a S ≤ 1)
↔ answer (sorry) := by
/-
Proof sketch (to be filled):

1. Fix K > 1, set ε := exp(-c*K).
2. Randomly thin the family with Bernoulli choices (probabilistic method).
3. Tune parameters so that the expected harmonic sum is ≈ 1 - ε/2.
4. Bound the variance (≲ 1/K) and apply Chebyshev/Hoeffding.
5. Conclude that some outcome gives a subset with harmonic sum in (1 - ε, 1].
6. Extract the corresponding Finset of indices.
-/
sorry

end Erdos312

[Moritz Firsching]

Yaël Dillies said:

Moritz Firsching, using subset on multiset is incorrect here. What about using a family indexed by a fintype instead?

Thanks for pointing this out! Family indexed by fintype sounds like a good idea. Now I'm trying to understand if LE.le, so "≤ " would do the correct thing...

[Moritz Firsching]

This characterization seems to imply it is doing the right thing:
https://leanprover-community.github.io/mathlib4_docs/find/?pattern=Multiset.le_iff_count#doc
so, perhaps it would be more elegant to use Multiset here and instead of "subset" use "le"?

[Yaël Dillies]

It does the right thing, yes. But as always, I heavily discourage indexing sums by a multiset. It is harder to work with (eg properly filtering is impossible) for no benefit. Indexing by an arbitrary indexing type is almost always better

[AYUSH DEBNATH]

Added the copyright header and made changes to the code can we run it again

[AYUSH DEBNATH]

/-

Proof sketch (to be filled):

1. Fix K > 1, set ε := exp(-c*K).

2. Randomly thin the family with Bernoulli choices (probabilistic method).

3. Tune parameters so that the expected harmonic sum is ≈ 1 - ε/2.

4. Bound the variance (≲ 1/K) and apply Chebyshev/Hoeffding.

5. Conclude that some outcome gives a subset with harmonic sum in (1 - ε, 1].

6. Extract the corresponding Finset of indices.
   -/

Outdated?

[AYUSH DEBNATH]

Why is it not accepting even though I have added a copyright header plz tell me?

[AYUSH DEBNATH]

I think I have to add my name to the AUTHORS