Documentation

FormalConjectures.GreensOpenProblems.«85»

Green's Open Problem 85 #

Carbery’s rectangle problem

References:

theorem Green85.green_85 :
sorry c > 0, ∀ (A : Set ( × )), IsOpen AA Set.Icc 0 1 ×ˢ Set.Icc 0 1A.Nonemptyhave α := (MeasureTheory.volume A).toReal; ∃ (x₁ : ) (x₂ : ) (y₁ : ) (y₂ : ), {(x₁, y₁), (x₂, y₁), (x₂, y₂), (x₁, y₂)} A c * α ^ 2 |x₁ - x₂| * |y₁ - y₂|

Suppose that $A$ is an open subset of $[0, 1]^2$ with measure $\alpha$. Are there four points in $A$ determining an axis-parallel rectangle with area $\gt c \alpha^2$?

theorem Green85.green_85_loose :
c > 0, ∀ (A : Set ( × )), IsOpen AA Set.Icc 0 1 ×ˢ Set.Icc 0 1A.Nonemptyhave α := (MeasureTheory.volume A).toReal; ∃ (x₁ : ) (x₂ : ) (y₁ : ) (y₂ : ), {(x₁, y₁), (x₂, y₁), (x₂, y₂), (x₁, y₂)} A α ^ 2 * (Real.log (1 / α))⁻¹ |x₁ - x₂| * |y₁ - y₂|

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}$."