The sharp finite-dimensional constant

This file records the elementary real-analysis facts about

bₙ,₁ = (n / (n + 1))ⁿ

which is the δ = 1 value of the second branch in (1.1). The probability-theoretic proof is kept in later modules.

noncomputable def Feige.sharpConstant (n : ℕ) : ℝ

The unit-slack sharp constant bₙ,₁ in dimension n.

Equations

• Feige.sharpConstant n = (↑n / (↑n + 1)) ^ n

@[simp]

theorem Feige.sharpConstant_zero : sharpConstant 0 = 1

theorem Feige.sharpConstant_pos (n : ℕ) : 0 < sharpConstant n

The sharp constant is positive in every dimension, including dimension zero.

theorem Feige.sharpConstant_nonneg (n : ℕ) : 0 ≤ sharpConstant n

The sharp constant is nonnegative.

theorem Feige.sharpConstant_le_one (n : ℕ) : sharpConstant n ≤ 1

The sharp constant is at most one.

theorem Feige.exp_neg_one_lt_sharpConstant {n : ℕ} (hn : 1 ≤ n) : Real.exp (-1) < sharpConstant n

The finite-dimensional sharp constant is strictly larger than exp (-1).

theorem Feige.tendsto_sharpConstant : Filter.Tendsto sharpConstant Filter.atTop (nhds (Real.exp (-1)))

The finite-dimensional sharp constants converge to exp (-1).