Mathoverflow 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

structure Mathoverflow34145.Rectangle : Type

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⟩

• width : ℝ
• height : ℝ
• start : ℝ × ℝ
• rotation : Real.Angle

noncomputable def Mathoverflow34145.rigidMotion (start : ℝ × ℝ) (θ : Real.Angle) (p : ℝ × ℝ) : ℝ × ℝ

A combination of a rotation and a translation to map the standard rectangle to the desired rectangle.

Equations

• Mathoverflow34145.rigidMotion start θ p = (start.1 + p.1 * θ.cos - p.2 * θ.sin, start.2 + p.1 * θ.sin + p.2 * θ.cos)

theorem Mathoverflow34145.rigidMotion_test : rigidMotion (√2, √11) ↑(2 * Real.pi / 3) (√5, √7) = (√2 - √5 / 2 - √21 / 2, -√7 / 2 + √11 + √15 / 2)

noncomputable def Mathoverflow34145.scale (x y : ℝ) (p : ℝ × ℝ) : ℝ × ℝ

A scaling to map the unit square to a standard rectangle.

Equations

• Mathoverflow34145.scale x y p = (x * p.1, y * p.2)

def Mathoverflow34145.unitSquare : Set (ℝ × ℝ)

The unit square.

Equations

• Mathoverflow34145.unitSquare = {p : ℝ × ℝ | 0 ≤ p.1 ∧ p.1 ≤ 1 ∧ 0 ≤ p.2 ∧ p.2 ≤ 1}

def Mathoverflow34145.Rectangle.toSet (r : Rectangle) : Set (ℝ × ℝ)

Converts a rectangle to a set in ℝ × ℝ.

Equations

• r.toSet = Mathoverflow34145.rigidMotion r.start r.rotation '' (Mathoverflow34145.scale r.width r.height '' Mathoverflow34145.unitSquare)

@[reducible, inline]

noncomputable abbrev Mathoverflow34145.lbMeasure : MeasureTheory.Measure (ℝ × ℝ)

The standard Lebesgue measure on ℝ².

Equations

• Mathoverflow34145.lbMeasure = (Module.Basis.finTwoProd ℝ).addHaar

theorem Mathoverflow34145.lbMeasure_rigidMotion (start : ℝ × ℝ) (θ : Real.Angle) (s : Set (ℝ × ℝ)) : lbMeasure (rigidMotion start θ '' s) = lbMeasure s

lbMeasure is invariant under rigidMotion start θ.

theorem Mathoverflow34145.lbMeasure_scale (x y : ℝ) (s : Set (ℝ × ℝ)) : lbMeasure (scale x y '' s) = ENNReal.ofReal |x * y| * lbMeasure s

lbMeasure is scaled by scale.

theorem Mathoverflow34145.lbMeasure_unitSquare : lbMeasure unitSquare = 1

The Lebesgue measure of the unit square is 1.

theorem Mathoverflow34145.lbMeasure_rectangle_toSet (r : Rectangle) : lbMeasure r.toSet = ENNReal.ofReal |r.width * r.height|

The Lebesgue measure of the a rectangle r is r.width * r.height

theorem Mathoverflow34145.tsum_area_eq_one : ∑' (n : ℕ), 1 / (↑n + 1) * (1 / (↑n + 2)) = 1

The areas of the required rectangles sum to 1.

structure Mathoverflow34145.Configuration : Type

A configuration of rectangles of sides 1 / (n + 1) and 1 / (n + 2).

• rect (n : ℕ) : Rectangle
• rect_width (n : ℕ) : (self.rect n).width = 1 / (↑n + 1)
• rect_height (n : ℕ) : (self.rect n).height = 1 / (↑n + 2)

def Mathoverflow34145.Configuration.IsPacking (c : Configuration) : Prop

A "packing" means that the interiors of any two rectangles are disjoint.

Equations

• c.IsPacking = Pairwise fun (m n : ℕ) => interior (c.rect m).toSet ∩ interior (c.rect n).toSet = ∅

theorem Mathoverflow34145.rectangles_cover_unit_square : (∃ (c : Configuration), ∀ p ∈ unitSquare, ∃ (n : ℕ), p ∈ (c.rect n).toSet) ↔ sorry

Can a unit square be covered by rectangles of width 1 / (n + 1) and height 1 / (n + 2)?

theorem Mathoverflow34145.rectangles_pack_unit_square : (∃ (c : Configuration), (∀ (n : ℕ), (c.rect n).toSet ⊆ unitSquare) ∧ c.IsPacking) ↔ sorry

Equivalently, can a unit square be packed with rectangles of width 1 / (n + 1) and height 1 / (n + 2)?

theorem Mathoverflow34145.rectangles_pack_square_133_div_132 : ∃ (c : Configuration), (∀ (n : ℕ), (c.rect n).toSet ⊆ { width := 133 / 132, height := 133 / 132, start := (0, 0), rotation := 0 }.toSet) ∧ c.IsPacking

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

theorem Mathoverflow34145.rectangles_pack_square_501_div_500 : ∃ (c : Configuration), (∀ (n : ℕ), (c.rect n).toSet ⊆ { width := 501 / 500, height := 501 / 500, start := (0, 0), rotation := 0 }.toSet) ∧ c.IsPacking

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