FormalConjectures/GreensOpenProblems/85.lean
Explanation legend Lean4 Domain Explanation Language (L4DEL)
L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.
- L4DEL
- Lean4 Domain Explanation Language
Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.
Project sources: Pinned project documentation, Formal Conjectures paper, arXiv v1
2 declarations, 2 contain sorry, 0 declared as axioms
Green's Open Problem 85
Carbery’s rectangle problem
References:
- [Gr24] Green, Ben. "100 open problems." (2024).
- [CCW99] Carbery, Anthony, Michael Christ, and James Wright. "Multidimensional van der Corput and sublevel set estimates." Journal of the American Mathematical Society 12.4 (1999): 981-1015 Section 6.
- [Ke00] Keleti, Tamás. "Density and covering properties of intervals of ℝn." Mathematika 47.1-2 (2000): 229-242.
- [KKM02] Katz, Nets Hawk, Elliot Krop, and Mauro Maggioni. "Remarks on the box problem." Mathematical Research Letters 9.4 (2002): 515-520.
- [Mu02] Mubayi, Dhruv. "Some exact results and new asymptotics for hypergraph Turán numbers." Combinatorics, Probability and Computing 11.3 (2002): 299-309 Conjecture 1.4.
- [CPZ20] Conlon, David, Cosmin Pohoata, and Dmitriy Zakharov. "Random multilinear maps and the Erd\H {o} s box problem." arXiv preprint arXiv:2011.09024 (2020).
Imports (1)
- theorem
Green85.green_85Suppose that $A$ is an open subset of $[0, 1]^2$ with measure $\alpha$ sorry line 45 sourceSource documentation
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$?
depends on sorry what this means
Statement uses:
Iff,True,Exists,Real,And,GT.gt,OfNat.ofNat,Set,Prod,IsOpen,LE.le,SProd.sprod,Set.Icc,Set.Nonempty,ENNReal.toReal,MeasureTheory.Measure,ENNReal,MeasureTheory.MeasureSpace.volume,Insert.insert,Prod.mkand 6 moreProof uses:
sorryAx,Lean.Name,Bool.false,Lean.Name.num,Lean.Name.str,Lean.Name.anonymous62 instances, coercions and auxiliary constants left out.
Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
theorem green_85 : answer(sorry) ↔ ∃ c > 0, ∀ A : Set (ℝ × ℝ), IsOpen A → A ⊆ Icc 0 1 ×ˢ Icc 0 1 → A.Nonempty → let α := (volume A).toReal …Mentions: c
- theorem
Green85.green_85_looseFrom [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}$." sorry line 61 sourceSource documentation
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}$."
depends on sorry what this means
Statement uses:
Exists,Real,And,GT.gt,OfNat.ofNat,Filter.Eventually,Set,Prod,IsOpen,LE.le,SProd.sprod,Set.Icc,Set.Nonempty,Eq,ENNReal.toReal,MeasureTheory.Measure,ENNReal,MeasureTheory.MeasureSpace.volume,Insert.insert,Prod.mkand 11 moreProof uses:
sorryAx,Lean.Name,Bool.false,Lean.Name.num,Lean.Name.str,Lean.Name.anonymous70 instances, coercions and auxiliary constants left out.
Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
theorem green_85_loose : ∃ c > 0, ∀ᶠ α in 𝓝[>] 0, ∀ A : Set (ℝ × ℝ), IsOpen A → A ⊆ Icc 0 1 ×ˢ Icc 0 1 → A.Nonempty → α = (volume A).toReal → ∃ x₁ x₂ y₁ y₂, {(x₁, y₁), (x₂, y₁), (x₂, y₂), (x₁, y₂)} ⊆ A ∧ c * α ^ 2 * (Real.log (1/α))⁻¹ ≤ |x₁ - x₂| * |y₁ - y₂| := by …Mentions: c