/-
Copyright 2025 The Formal Conjectures Authors.
Licensed under the Apache License, Version 2.0 (the "License");
you may not use this file except in compliance with the License.
You may obtain a copy of the License at
https://www.apache.org/licenses/LICENSE-2.0
Unless required by applicable law or agreed to in writing, software
distributed under the License is distributed on an "AS IS" BASIS,
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
See the License for the specific language governing permissions and
limitations under the License.
-/
import FormalConjecturesUtilMathoverflow 34145
Can the unit square be covered by $1/k$-by-$1/(k+1)$ rectangles (across $1 \le k$ natural)?
I am deliberately not requiring that the rotations can only be $0^\circ, 90^\circ, 180^\circ, \text{ or } 270^\circ$.
Because of indexing, since n : ℕ starts at 0, we change the side lengths to $1 / (n + 1)$ and
$1 / (n + 2)$, so that the first rectangle is $1/1$ by $1/2$, the second is $1/2$ by $1/3$, etc.
Reference: mathoverflow/34145 asked by user Kaveh
open Real MeasureTheory Measure Modulenamespace Mathoverflow34145
A rectangle is specified by its width, height, starting point, and rotation.
The rectangle is assumed to start in the lower left corner. For example, the unit square
${ (x, y) \mid 0 \le x \le 1, 0 \le y \le 1 }$ is specified as ⟨1, 1, (0, 0), 0⟩
structure Rectangle : Type where
width : ℝ
height : ℝ
start : ℝ × ℝ
rotation : AngleA combination of a rotation and a translation to map the standard rectangle to the desired rectangle.
noncomputable def rigidMotion (start : ℝ × ℝ) (θ : Angle) (p : ℝ × ℝ) : (ℝ × ℝ) :=
(start.1 + p.1 * θ.cos - p.2 * θ.sin, start.2 + p.1 * θ.sin + p.2 * θ.cos)@[category test, AMS 51]
lemma rigidMotion_test : rigidMotion (sqrt 2, sqrt 11) (2 * π / 3 : ℝ) (sqrt 5, sqrt 7) =
(sqrt 2 - sqrt 5 / 2 - sqrt 21 / 2, -sqrt 7 / 2 + sqrt 11 + sqrt 15 / 2) := ⊢ rigidMotion (√2, √11) ↑(2 * π / 3) (√5, √7) = (√2 - √5 / 2 - √21 / 2, -√7 / 2 + √11 + √15 / 2)
⊢ √2 + √5 * (2 * (2 ^ 2)⁻¹ - 1) - √7 * (2 * (√3 / 2) * 2⁻¹) = √2 - √5 / 2 - √3 * (√7 / 2) ∧
√11 + √5 * (2 * (√3 / 2) * 2⁻¹) + √7 * (2 * (2 ^ 2)⁻¹ - 1) = -√7 / 2 + √11 + √3 * (√5 / 2)
⊢ True ∧ True; All goals completed! 🐙A scaling to map the unit square to a standard rectangle.
noncomputable def scale (x y : ℝ) (p : ℝ × ℝ) : (ℝ × ℝ) :=
(x * p.1, y * p.2)The unit square.
def unitSquare : Set (ℝ × ℝ) :=
{ p | 0 ≤ p.1 ∧ p.1 ≤ 1 ∧ 0 ≤ p.2 ∧ p.2 ≤ 1 }
Converts a rectangle to a set in ℝ × ℝ.
def Rectangle.toSet (r : Rectangle) : Set (ℝ × ℝ) :=
rigidMotion r.start r.rotation '' (scale r.width r.height '' unitSquare)
The standard Lebesgue measure on ℝ².
noncomputable abbrev lbMeasure : Measure (ℝ × ℝ) :=
(Basis.finTwoProd ℝ).addHaar
lbMeasure is invariant under rigidMotion start θ.
start:ℝ × ℝθ:Angles:Set (ℝ × ℝ)α:ℝ × ℝ → ℝ × ℝ := fun x ↦ (x.1 * θ.cos - x.2 * θ.sin, x.1 * θ.sin + x.2 * θ.cos)β:Basis (Fin 2) ℝ (ℝ × ℝ) := Basis.finTwoProd ℝ⊢ lbMeasure s =
ENNReal.ofReal
|(LinearMap.toMatrix β β) ((β.constr ℝ) ![α (β 0), α (β 1)]) 0 0 *
(LinearMap.toMatrix β β) ((β.constr ℝ) ![α (β 0), α (β 1)]) 1 1 -
(LinearMap.toMatrix β β) ((β.constr ℝ) ![α (β 0), α (β 1)]) 0 1 *
(LinearMap.toMatrix β β) ((β.constr ℝ) ![α (β 0), α (β 1)]) 1 0| *
β.addHaar s
All goals completed! 🐙
lbMeasure is scaled by scale.
x:ℝy:ℝs:Set (ℝ × ℝ)scaleLinear:ℝ × ℝ →ₗ[ℝ] ℝ × ℝ := { toFun := fun p ↦ (x * p.1, y * p.2), map_add' := ⋯, map_smul' := ⋯ }h₁:scale x y = ⇑scaleLinearh₂:(LinearMap.toMatrix (Basis.finTwoProd ℝ) (Basis.finTwoProd ℝ)) scaleLinear = !![x, 0; 0, y]⊢ lbMeasure (scale x y '' s) = ENNReal.ofReal |x * y| * lbMeasure s
All goals completed! 🐙
The Lebesgue measure of the unit square is 1.
@[category test, AMS 51]
lemma lbMeasure_unitSquare : lbMeasure unitSquare = 1 := ⊢ lbMeasure unitSquare = 1
⊢ unitSquare = ↑(Basis.finTwoProd ℝ).parallelepiped
p:ℝ × ℝ⊢ p ∈ unitSquare ↔ p ∈ ↑(Basis.finTwoProd ℝ).parallelepiped
p:ℝ × ℝ⊢ 0 ≤ p.1 ∧ p.1 ≤ 1 ∧ 0 ≤ p.2 ∧ p.2 ≤ 1 ↔ ∃ t, ((∀ (i : Fin 2), 0 i ≤ t i) ∧ ∀ (i : Fin 2), t i ≤ 1 i) ∧ p = (t 0, t 1)
exact ⟨fun h ↦ ⟨![p.1, p.2], p:ℝ × ℝh:0 ≤ p.1 ∧ p.1 ≤ 1 ∧ 0 ≤ p.2 ∧ p.2 ≤ 1⊢ ((∀ (i : Fin 2), 0 i ≤ ![p.1, p.2] i) ∧ ∀ (i : Fin 2), ![p.1, p.2] i ≤ 1 i) ∧ p = (![p.1, p.2] 0, ![p.1, p.2] 1) All goals completed! 🐙⟩,
fun ⟨t, ht⟩ ↦ ht.2 ▸ ⟨ht.1.1 0, ht.1.2 0, ht.1.1 1, ht.1.2 1⟩⟩
The Lebesgue measure of the a rectangle r is r.width * r.height
All goals completed! 🐙The areas of the required rectangles sum to 1.
this:∀ (n : ℕ), ∑ i ∈ Finset.range n, 1 / (↑i + 1) * (1 / (↑i + 2)) = 1 - 1 / (↑n + 1)⊢ ∑' (n : ℕ), 1 / (↑n + 1) * (1 / (↑n + 2)) = 1
this:∀ (n : ℕ), ∑ i ∈ Finset.range n, 1 / (↑i + 1) * (1 / (↑i + 2)) = 1 - 1 / (↑n + 1)i:ℕ⊢ 0 ≤ 1 / (↑i + 1) * (1 / (↑i + 2))this:∀ (n : ℕ), ∑ i ∈ Finset.range n, 1 / (↑i + 1) * (1 / (↑i + 2)) = 1 - 1 / (↑n + 1)⊢ Filter.Tendsto (fun n ↦ ∑ i ∈ Finset.range n, 1 / (↑i + 1) * (1 / (↑i + 2))) Filter.atTop (nhds 1)
this:∀ (n : ℕ), ∑ i ∈ Finset.range n, 1 / (↑i + 1) * (1 / (↑i + 2)) = 1 - 1 / (↑n + 1)i:ℕ⊢ 0 ≤ 1 / (↑i + 1) * (1 / (↑i + 2)) All goals completed! 🐙
this:∀ (n : ℕ), ∑ i ∈ Finset.range n, 1 / (↑i + 1) * (1 / (↑i + 2)) = 1 - 1 / (↑n + 1)⊢ Filter.Tendsto (fun n ↦ ∑ i ∈ Finset.range n, 1 / (↑i + 1) * (1 / (↑i + 2))) Filter.atTop (nhds 1) simp_rw this:∀ (n : ℕ), ∑ i ∈ Finset.range n, 1 / (↑i + 1) * (1 / (↑i + 2)) = 1 - 1 / (↑n + 1)⊢ Filter.Tendsto (fun n ↦ ∑ i ∈ Finset.range n, 1 / (↑i + 1) * (1 / (↑i + 2))) Filter.atTop (nhds 1)this:∀ (n : ℕ), ∑ i ∈ Finset.range n, 1 / (↑i + 1) * (1 / (↑i + 2)) = 1 - 1 / (↑n + 1)⊢ Filter.Tendsto (fun n ↦ 1 - 1 / (↑n + 1)) Filter.atTop (nhds 1)]
this:∀ (n : ℕ), ∑ i ∈ Finset.range n, 1 / (↑i + 1) * (1 / (↑i + 2)) = 1 - 1 / (↑n + 1)⊢ nhds 1 = nhds (1 - 0)
All goals completed! 🐙
A configuration of rectangles of sides 1 / (n + 1) and 1 / (n + 2).
structure Configuration : Type where
rect (n : ℕ) : Rectangle
rect_width (n : ℕ) : (rect n).width = 1 / (n + 1)
rect_height (n : ℕ) : (rect n).height = 1 / (n + 2)A "packing" means that the interiors of any two rectangles are disjoint.
def Configuration.IsPacking (c : Configuration) : Prop :=
Pairwise fun m n ↦ interior (c.rect m).toSet ∩ interior (c.rect n).toSet = ∅
Can a unit square be covered by rectangles of width 1 / (n + 1) and height 1 / (n + 2)?
@[category research open, AMS 51]
theorem rectangles_cover_unit_square :
answer(sorry) ↔ ∃ c : Configuration, ∀ p ∈ unitSquare, ∃ n, p ∈ (c.rect n).toSet := ⊢ True ↔ ∃ c, ∀ p ∈ unitSquare, ∃ n, p ∈ (c.rect n).toSet
All goals completed! 🐙
Equivalently, can a unit square be packed with rectangles of width 1 / (n + 1) and height
1 / (n + 2)?
@[category research open, AMS 51]
theorem rectangles_pack_unit_square :
answer(sorry) ↔ ∃ c : Configuration, (∀ n, (c.rect n).toSet ⊆ unitSquare) ∧ c.IsPacking := ⊢ True ↔ ∃ c, (∀ (n : ℕ), (c.rect n).toSet ⊆ unitSquare) ∧ c.IsPacking
All goals completed! 🐙
It is known that packing the rectangles into a square of side length 133/132 is possible.
Reference: https://www.sciencedirect.com/science/article/pii/0097316594901163
@[category research solved, AMS 51]
theorem rectangles_pack_square_133_div_132 :
(∃ c : Configuration,
(∀ n, (c.rect n).toSet ⊆ Rectangle.toSet ⟨133/132, 133/132, (0, 0), 0⟩) ∧
c.IsPacking) := ⊢ ∃ c,
(∀ (n : ℕ), (c.rect n).toSet ⊆ { width := 133 / 132, height := 133 / 132, start := (0, 0), rotation := 0 }.toSet) ∧
c.IsPacking
All goals completed! 🐙
It is known that packing the rectangles into a square of side length 501/500 is possible.
Reference: https://www.sciencedirect.com/science/article/pii/S0167506008706009
@[category research solved, AMS 51]
theorem rectangles_pack_square_501_div_500 :
(∃ c : Configuration,
(∀ n, (c.rect n).toSet ⊆ Rectangle.toSet ⟨501/500, 501/500, (0, 0), 0⟩) ∧
c.IsPacking) := ⊢ ∃ c,
(∀ (n : ℕ), (c.rect n).toSet ⊆ { width := 501 / 500, height := 501 / 500, start := (0, 0), rotation := 0 }.toSet) ∧
c.IsPacking
All goals completed! 🐙end Mathoverflow34145