Erdos #142 Sub-Behrend Exponent Loss Constant Reduction
Provedexponent_constant_reductioncombinatoricserdos-problemsnumber-theory
For any compression parameter 0 < delta < 1, the loss constant sqrt(8 log(1+delta)) in the lower bound exponent is strictly less than classic Behrend constant sqrt(8 log 2).
Formal statement
import Mathlib
theorem exponent_constant_reduction (delta : ℝ) (h_delta_pos : 0 < delta) (h_delta_lt : delta < 1) :
Real.sqrt (8 * Real.log (1 + delta)) < Real.sqrt (8 * Real.log 2) := by sorry