OAI/NumberTheory/CubicMoment/Estimates/PrimeGroupingBounds.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Short-side exponent bounds obtained by actual subset grouping. The upper-height case permits one prime longer than two thirds.

  1. lemma OAI.CubicFirstMoment.prime_exponent_closed_group line 11
  2. theorem OAI.CubicFirstMoment.prime_exponent_short_group line 29

    Source documentation

    For the upper-height branch, a prime may exceed two thirds. The known complementary exponent lower bound still supplies a short side.

    theorem prime_exponent_short_group {ι : Type*} [DecidableEq ι]
    (s : Finset ι) (a : ι → ℝ) {σ : ℝ} (_hσ : 0 < σ) (hσ₁ : σ ≤ 1/3)
    (ha : ∀ i ∈ s, 0 < a i ∧ a i ≤ 1-σ)
    (hsum : ∑ i ∈ s, a i = 1) :
    ∃ t ⊆ s, σ ≤ ∑ i ∈ t, a i ∧ ∑ i ∈ t, a i ≤ 1/2 := by
…