PrimeGrouping.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

The exact partition alternative behind the large-distinguished- factor branch of the manuscript's prime decomposition.

theorem OAI.CubicFirstMoment.prime_exponent_partition line 13

Source documentation

A partition of one with each part below two thirds either has a strictly interior subset sum or consists of exactly three equal thirds.

theorem prime_exponent_partition {ι : Type*} [DecidableEq ι]
    (s : Finset ι) (a : ι → ℝ) (ha : ∀ i ∈ s, 0 < a i ∧ a i < 2/3)
    (hsum : ∑ i ∈ s, a i = 1) :
    (∃ t ⊆ s, 1/3 < ∑ i ∈ t, a i ∧ ∑ i ∈ t, a i < 2/3) ∨
      (s.card = 3 ∧ ∀ i ∈ s, a i = 1/3) := by
…