The asymptotic lower bound for the explicit construction.

noncomputable def SumDifferenceExponent.ColumnConstruction.exponentLower (l : ℕ) : ℝ

The logarithmic lower estimate obtained from the sum and difference cardinality bounds.

Equations

• SumDifferenceExponent.ColumnConstruction.exponentLower l = Real.log (↑l ^ 2 / 2) / Real.log (12 * ↑l)

theorem SumDifferenceExponent.ColumnConstruction.A_card_two_le {l : ℕ} (hl : 0 < l) : 2 ≤ (A l).card

theorem SumDifferenceExponent.ColumnConstruction.sigma_A_lower {l : ℕ} (hl : 0 < l) : ↑l ^ 2 / 2 ≤ sigma (A l)

theorem SumDifferenceExponent.ColumnConstruction.delta_A_upper {l : ℕ} (hl : 0 < l) : delta (A l) ≤ 12 * ↑l

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

theorem SumDifferenceExponent.ColumnConstruction.exponentLower_formula {l : ℕ} (hl : 0 < l) : exponentLower l = 2 - (Real.log 2 + 2 * Real.log 12) / (Real.log ↑l + Real.log 12)

theorem SumDifferenceExponent.ColumnConstruction.exponentLower_eventually_formula : ∀ᶠ (l : ℕ) in Filter.atTop, exponentLower l = 2 - (Real.log 2 + 2 * Real.log 12) / (Real.log ↑l + Real.log 12)

theorem SumDifferenceExponent.ColumnConstruction.tendsto_exponentLower : Filter.Tendsto exponentLower Filter.atTop (nhds 2)