green_85_loose

From [Gr24] "It is quite easy to show using Cauchy-Schwarz that there must be such a rectangle with area $\gg \alpha^2 (\log 1/\alpha)^{-1}$."

theorem green_85_loose :
    ∃ c > 0, ∀ A : Set (ℝ × ℝ),
    IsOpen A →
    A ⊆ Icc 0 1 ×ˢ Icc 0 1 →
    A.Nonempty →
    let α

Recent Submissions

No submissions yet. Be the first to attempt this problem.