The complete sharp-supremum theorem.

@[reducible, inline]

abbrev SumDifferenceExponent.approximatingSet : ℕ → Finset ℤ

The explicit row-and-column family whose exponents approach two.

Equations

• SumDifferenceExponent.approximatingSet = SumDifferenceExponent.ColumnConstruction.A

theorem SumDifferenceExponent.approximatingSet_card_two_le {l : ℕ} (hl : 0 < l) : 2 ≤ (approximatingSet l).card

theorem SumDifferenceExponent.exponentLower_le_growthExponent_approximatingSet {l : ℕ} (hl : 2 ≤ l) : ColumnConstruction.exponentLower l ≤ growthExponent (approximatingSet l)

theorem SumDifferenceExponent.tendsto_growthExponent_approximatingSet : Filter.Tendsto (fun (l : ℕ) => growthExponent (approximatingSet l)) Filter.atTop (nhds 2)

The explicit finite integer sets approximatingSet l have growth exponent tending to the sharp upper bound 2.

def SumDifferenceExponent.admissibleExponents : Set ℝ

The set of all admissible growth exponents in the optimization problem.

Equations

• SumDifferenceExponent.admissibleExponents = {x : ℝ | ∃ (B : Finset ℤ), 2 ≤ B.card ∧ x = SumDifferenceExponent.growthExponent B}

theorem SumDifferenceExponent.isLUB_admissibleExponents : IsLUB admissibleExponents 2

The number 2 is the least upper bound of all admissible exponents.

theorem SumDifferenceExponent.sSup_admissibleExponents : sSup admissibleExponents = 2

The supremum in the main problem is exactly 2.

theorem SumDifferenceExponent.supremum_not_attained (B : Finset ℤ) (hB : 2 ≤ B.card) : growthExponent B ≠ 2

The supremum is not attained by any admissible finite integer set.