From 8dc85dabdd5d3a28785474de9e163ed582fdb08a Mon Sep 17 00:00:00 2001 From: AItoBit <321732397+AItoBit@users.noreply.github.com> Date: Mon, 12 Oct 2026 11:29:14 +0200 Subject: [PATCH 1/2] Extend Chapter 29 with checkerboard, counting, packing, and box proofs --- FormalBook/Chapter_29.lean | 984 +++++++++++++++++++++++++++++++++++-- 1 file changed, 935 insertions(+), 49 deletions(-) diff --git a/FormalBook/Chapter_29.lean b/FormalBook/Chapter_29.lean index 43d4b25..f31ed5f 100644 --- a/FormalBook/Chapter_29.lean +++ b/FormalBook/Chapter_29.lean @@ -1,21 +1,55 @@ /- -Authors: Matteo Del Vecchio, Aristotle (Harmonic) +Authors: Matteo Del Vecchio, Aristotle (Harmonic), AItoBit -/ module public import Mathlib.MeasureTheory.Integral.Bochner.Basic public import Mathlib.MeasureTheory.Measure.Haar.OfBasis public import Mathlib.NumberTheory.Real.Irrational -import Mathlib.Analysis.SpecialFunctions.Integrals.Basic -import Mathlib.MeasureTheory.Integral.Prod +public import Mathlib.Analysis.SpecialFunctions.Integrals.Basic +public import Mathlib.MeasureTheory.Integral.Prod +public import Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus +public import Mathlib.MeasureTheory.Function.Floor +public import Mathlib.Combinatorics.Enumerative.DoubleCounting +public import Mathlib.Topology.Order.LeftRightNhds +public import Mathlib.Algebra.BigOperators.Fin +public import Mathlib.MeasureTheory.Integral.Pi +public import Mathlib.MeasureTheory.Measure.Lebesgue.Basic @[expose] public section +/-! Small general-purpose helper lemmas, stated here so that the file does not depend on +lemma names that differ between Mathlib versions. -/ + +theorem ch29_if_pos {c : Prop} [Decidable c] (h : c) {α : Sort*} {a b : α} : + (if c then a else b) = a := by simp [h] + +theorem ch29_if_neg {c : Prop} [Decidable c] (h : ¬c) {α : Sort*} {a b : α} : + (if c then a else b) = b := by simp [h] + +/-- A finite union of almost-everywhere equal families of sets is almost-everywhere equal. -/ +theorem ch29_eventuallyEq_biUnion {α ι : Type*} {l : Filter α} {s : Set ι} (hs : s.Finite) + {f g : ι → Set α} (h : ∀ i ∈ s, f i =ᶠ[l] g i) : (⋃ i ∈ s, f i) =ᶠ[l] ⋃ i ∈ s, g i := by + have hall : ∀ᶠ x in l, ∀ i ∈ s, (x ∈ f i ↔ x ∈ g i) := + (Filter.eventually_all_finite hs).2 fun i hi => Filter.eventuallyEq_set.1 (h i hi) + rw [Filter.eventuallyEq_set] + filter_upwards [hall] with x hx + simp only [Set.mem_iUnion] + exact ⟨fun ⟨i, hi, hx'⟩ => ⟨i, hi, (hx i hi).1 hx'⟩, fun ⟨i, hi, hx'⟩ => ⟨i, hi, (hx i hi).2 hx'⟩⟩ + + +/-! --------------------------------------------------------------------------- +## Part from `Chapter_29.lean` +--------------------------------------------------------------------------- -/ + +section + /-! # Tiling rectangles -## TODO - - Second and third proofs of the first statement. +This file collects the supplied formalization of the chapter: the first proof of +de Bruijn's theorem and Dehn's theorem, shared affine facts, the second (checkerboard) and +third (counting) proofs, de Bruijn's packing corollary and the `n`-dimensional version. -/ @@ -103,30 +137,22 @@ lemma integral_f_eq_zero_iff_int_side (r : Rectangle) : ring +/-- A rectangle and its interior agree up to a set of measure zero. -/ +lemma Rectangle.toSet_ae_eq_interior (r : Rectangle) : + r.toSet =ᵐ[MeasureTheory.volume] r.interior := by + refine (MeasureTheory.ae_eq_of_subset_of_measure_ge + (Set.prod_mono Set.Ioo_subset_Icc_self Set.Ioo_subset_Icc_self) (le_of_eq ?_) + (measurableSet_Ioo.prod measurableSet_Ioo).nullMeasurableSet ?_).symm + · simp only [MeasureTheory.Measure.volume_eq_prod, MeasureTheory.Measure.prod_prod, + Real.volume_Icc, Real.volume_Ioo] + · simp only [MeasureTheory.Measure.volume_eq_prod, MeasureTheory.Measure.prod_prod, + Real.volume_Icc] + exact ENNReal.mul_ne_top ENNReal.ofReal_ne_top ENNReal.ofReal_ne_top + /-- The integral of `f` over a rectangle is equal to the integral of `f` over its interior. -/ lemma integral_rectangle_eq_integral_interior (r : Rectangle) : ∫ p in r.toSet, f p = ∫ p in r.interior, f p := by - rw [ MeasureTheory.Measure.restrict_congr_set ]; - have h_boundary_zero : - MeasureTheory.volume (Set.Icc r.x (r.x + r.w) ×ˢ Set.Icc r.y (r.y + r.h) \ - Set.Ioo r.x (r.x + r.w) ×ˢ Set.Ioo r.y (r.y + r.h)) = 0 := by - erw [ MeasureTheory.measure_sdiff ] <;> norm_num; - · erw [ show ( Set.Icc ( r.x, r.y ) ( r.x + r.w, r.y + r.h ) : Set ( ℝ × ℝ ) ) = - Set.Icc r.x ( r.x + r.w ) ×ˢ Set.Icc r.y ( r.y + r.h ) by ext ; aesop, - show ( Set.Ioo r.x ( r.x + r.w ) ×ˢ Set.Ioo r.y ( r.y + r.h ) : Set ( ℝ × ℝ ) ) = - Set.Ioo r.x ( r.x + r.w ) ×ˢ Set.Ioo r.y ( r.y + r.h ) by rfl, - MeasureTheory.Measure.prod_prod, MeasureTheory.Measure.prod_prod ] - norm_num - · exact fun x hx => ⟨ ⟨ hx.1.1.le, hx.2.1.le ⟩, ⟨ hx.1.2.le, hx.2.2.le ⟩ ⟩; - · exact measurableSet_Ioo.prod measurableSet_Ioo |> MeasurableSet.nullMeasurableSet; - · erw [ MeasureTheory.Measure.prod_prod ] ; norm_num; - exact ENNReal.mul_ne_top ( ENNReal.ofReal_ne_top ) ( ENNReal.ofReal_ne_top ); - rw [ MeasureTheory.ae_eq_set ]; - constructor - · exact h_boundary_zero - · rw [Set.sdiff_eq_empty.mpr - (by exact Set.prod_mono (Set.Ioo_subset_Icc_self) (Set.Ioo_subset_Icc_self))] - norm_num + rw [MeasureTheory.Measure.restrict_congr_set (Rectangle.toSet_ae_eq_interior r)] /-- The integral of `f` over the union of a list of rectangles with disjoint interiors is the sum of the integrals over each rectangle. -/ @@ -158,21 +184,8 @@ lemma integral_union_rectangles (Ts : List Rectangle) exact h_cont.integrableOn_compact ( isCompact_Icc.prod CompactIccSpace.isCompact_Icc ) |> fun h => h.mono_set ( Set.prod_mono Set.Ioo_subset_Icc_self Set.Ioo_subset_Icc_self ); rw [ ← h_split, MeasureTheory.setIntegral_congr_set ]; - have h_boundary_zero : ∀ t : Rectangle, MeasureTheory.volume (t.toSet \ t.interior) = 0 := by - intro t; - rw [ show t.toSet \ t.interior = ( Set.Icc t.x ( t.x + t.w ) ×ˢ Set.Icc t.y ( t.y + t.h ) ) - \ ( Set.Ioo t.x ( t.x + t.w ) ×ˢ Set.Ioo t.y ( t.y + t.h ) ) by rfl ]; - erw [ MeasureTheory.measure_sdiff ] ; - norm_num; - · erw [ show ( Set.Icc ( t.x, t.y ) ( t.x + t.w, t.y + t.h ) : Set ( ℝ × ℝ ) ) = - Set.Icc t.x ( t.x + t.w ) ×ˢ Set.Icc t.y ( t.y + t.h ) - by ext ; aesop, MeasureTheory.Measure.prod_prod ] ; - norm_num; - erw [ MeasureTheory.Measure.prod_prod ] ; norm_num [ t.w_pos, t.h_pos ]; - · exact Set.prod_mono ( Set.Ioo_subset_Icc_self ) ( Set.Ioo_subset_Icc_self ); - · exact measurableSet_Ioo.prod measurableSet_Ioo |> MeasurableSet.nullMeasurableSet; - · erw [ MeasureTheory.Measure.prod_prod ] ; norm_num; - exact ENNReal.mul_ne_top ( ENNReal.ofReal_ne_top ) ( ENNReal.ofReal_ne_top ); + have h_boundary_zero : ∀ t : Rectangle, MeasureTheory.volume (t.toSet \ t.interior) = 0 := + fun t => (MeasureTheory.ae_eq_set.1 (Rectangle.toSet_ae_eq_interior t)).1 have h_boundary_zero : MeasureTheory.volume (⋃ t ∈ Ts.toFinset, (t.toSet \ t.interior)) = 0 := MeasureTheory.measure_biUnion_null_iff (I := Ts.toFinset) ( Finset.countable_toSet _ ) |>.2 fun t ht => h_boundary_zero t @@ -556,14 +569,14 @@ lemma subgrid_bounds (g : Grid) (r : Rectangle) have := (subgrid g r hx1 hy1).ys_ne_nil exact this) = r.y + r.h := by refine' ⟨ _, _, _, _ ⟩; - · (convert head_filter_interval_eq_left g.xs g.xs_sorted r.x ( r.x + r.w ) hx1 - ( by linarith [ r.w_pos ] ); simp [subgrid]); - · (convert last_filter_interval_eq_right g.xs g.xs_sorted r.x ( r.x + r.w ) hx2 - ( by linarith [ r.w_pos ] ); simp [subgrid]); - · (convert head_filter_interval_eq_left g.ys g.ys_sorted r.y ( r.y + r.h ) hy1 - ( by linarith [ r.h_pos ] ); simp [subgrid]); - · (convert last_filter_interval_eq_right g.ys g.ys_sorted r.y ( r.y + r.h ) hy2 - ( by linarith [ r.h_pos ] ); simp [subgrid]); + · exact head_filter_interval_eq_left g.xs g.xs_sorted r.x ( r.x + r.w ) hx1 + ( by linarith [ r.w_pos ] ) + · exact last_filter_interval_eq_right g.xs g.xs_sorted r.x ( r.x + r.w ) hx2 + ( by linarith [ r.w_pos ] ) + · exact head_filter_interval_eq_left g.ys g.ys_sorted r.y ( r.y + r.h ) hy1 + ( by linarith [ r.h_pos ] ) + · exact last_filter_interval_eq_right g.ys g.ys_sorted r.y ( r.y + r.h ) hy2 + ( by linarith [ r.h_pos ] ) /-- If a rectangle's boundaries are in the grid, then the sum of the `f`-areas of the grid cells contained in the rectangle equals the `f`-area of the rectangle. -/ @@ -1125,3 +1138,876 @@ theorem tiling_iff_rational_ratio (R : Rectangle) : · intro t x x_1 a a_1 a_2 subst a_2 rfl; + +end -- noncomputable section + +end + + +/-! --------------------------------------------------------------------------- +## Part from `Chapter_29/Affine.lean` +--------------------------------------------------------------------------- -/ + +section + +/-! +# Scaling and translating tilings + +The chapter repeatedly uses that tilings can be scaled and moved around: the second and third +proofs of de Bruijn's theorem assume that the big rectangle has its lower left corner at `(0, 0)`, +and de Bruijn's packing corollary scales a tiling down by a factor `1 / a`. +We record that the image of a tiling under a map `(x, y) ↦ (k x + u, k y + v)` with `k > 0` is +again a tiling. +-/ + +noncomputable section + +/-- The image of a rectangle under the map `(x, y) ↦ (k x + u, k y + v)`, where `k > 0`. -/ +def Rectangle.affine (k u v : ℝ) (hk : 0 < k) (r : Rectangle) : Rectangle where + x := k * r.x + u + y := k * r.y + v + w := k * r.w + h := k * r.h + w_pos := mul_pos hk r.w_pos + h_pos := mul_pos hk r.h_pos + +/-- The inverse of the map `(x, y) ↦ (k x + u, k y + v)`. -/ +def affineInv (k u v : ℝ) (p : ℝ × ℝ) : ℝ × ℝ := ((p.1 - u) / k, (p.2 - v) / k) + +lemma affine_Icc_iff {k u a b z : ℝ} (hk : 0 < k) : + (k * a + u ≤ z ∧ z ≤ k * a + u + k * b) ↔ (a ≤ (z - u) / k ∧ (z - u) / k ≤ a + b) := by + rw [le_div_iff₀ hk, div_le_iff₀ hk] + constructor <;> rintro ⟨h1, h2⟩ <;> constructor <;> nlinarith + +lemma affine_Ioo_iff {k u a b z : ℝ} (hk : 0 < k) : + (k * a + u < z ∧ z < k * a + u + k * b) ↔ (a < (z - u) / k ∧ (z - u) / k < a + b) := by + rw [lt_div_iff₀ hk, div_lt_iff₀ hk] + constructor <;> rintro ⟨h1, h2⟩ <;> constructor <;> nlinarith + +lemma Rectangle.affine_toSet (k u v : ℝ) (hk : 0 < k) (r : Rectangle) : + (r.affine k u v hk).toSet = affineInv k u v ⁻¹' r.toSet := by + ext p + simp only [Rectangle.toSet, Rectangle.affine, affineInv, Set.mem_prod, Set.mem_Icc, + Set.mem_preimage] + rw [affine_Icc_iff hk, affine_Icc_iff hk] + +lemma Rectangle.affine_interior (k u v : ℝ) (hk : 0 < k) (r : Rectangle) : + (r.affine k u v hk).interior = affineInv k u v ⁻¹' r.interior := by + ext p + simp only [Rectangle.interior, Rectangle.affine, affineInv, Set.mem_prod, Set.mem_Ioo, + Set.mem_preimage] + rw [affine_Ioo_iff hk, affine_Ioo_iff hk] + +/-- The image of a tiling under the map `(x, y) ↦ (k x + u, k y + v)`, `k > 0`, is a tiling. -/ +theorem is_tiling.affine {R : Rectangle} {Ts : List Rectangle} (h : is_tiling R Ts) + (k u v : ℝ) (hk : 0 < k) : + is_tiling (R.affine k u v hk) (Ts.map (Rectangle.affine k u v hk)) := by + obtain ⟨h1, h2⟩ := h + constructor + · intro i j hij + have := h1 ⟨i, by simpa using i.2⟩ ⟨j, by simpa using j.2⟩ + (fun e => hij (Fin.ext (by simpa using congrArg Fin.val e))) + simp only [List.get_eq_getElem, List.getElem_map, Rectangle.affine_interior] at this ⊢ + rw [← Set.preimage_inter, this, Set.preimage_empty] + · rw [Rectangle.affine_toSet, ← h2, Set.preimage_iUnion₂] + ext p + simp [Rectangle.affine_toSet] + +/-- Distinct tiles of a tiling have disjoint interiors. -/ +lemma tiling_interior_disjoint {R : Rectangle} {Ts : List Rectangle} (h : is_tiling R Ts) + {t t' : Rectangle} (ht : t ∈ Ts) (ht' : t' ∈ Ts) (hne : t ≠ t') : + t.interior ∩ t'.interior = ∅ := by + obtain ⟨i, rfl⟩ := List.mem_iff_get.1 ht + obtain ⟨j, rfl⟩ := List.mem_iff_get.1 ht' + exact h.1 i j (fun e => hne (e ▸ rfl)) + +/-- Translating a tiling so that the big rectangle has its lower left corner at the origin. -/ +def Rectangle.toOrigin (R r : Rectangle) : Rectangle := r.affine 1 (-R.x) (-R.y) one_pos + +lemma Rectangle.toOrigin_self (R : Rectangle) : + (R.toOrigin R).x = 0 ∧ (R.toOrigin R).y = 0 := by + simp [Rectangle.toOrigin, Rectangle.affine] + +/-- **Reduction to the origin.** To prove a property of tilings that only depends on the side +lengths of the rectangles involved, it suffices to consider tilings of rectangles whose lower left +corner is `(0, 0)`. -/ +theorem tiling_reduce_to_origin (P : ℝ → ℝ → Prop) + (H : ∀ (R : Rectangle) (Ts : List Rectangle), R.x = 0 → R.y = 0 → is_tiling R Ts → + (∀ t ∈ Ts, P t.w t.h) → P R.w R.h) + (R : Rectangle) (Ts : List Rectangle) (h : is_tiling R Ts) (hP : ∀ t ∈ Ts, P t.w t.h) : + P R.w R.h := by + have := H (R.toOrigin R) (Ts.map (R.toOrigin)) (R.toOrigin_self).1 (R.toOrigin_self).2 + (h.affine 1 (-R.x) (-R.y) one_pos) + (by + intro t ht + obtain ⟨t', ht', rfl⟩ := List.mem_map.1 ht + simpa [Rectangle.toOrigin, Rectangle.affine] using hP t' ht') + simpa [Rectangle.toOrigin, Rectangle.affine] using this + +end + +end + + +/-! --------------------------------------------------------------------------- +## Part from `Chapter_29/SecondProof.lean` +--------------------------------------------------------------------------- -/ + +section + +/-! +# Tiling rectangles: the second proof (Rochberg–Stein) + +Color the plane in a checkerboard fashion with black/white squares of size `1/2 × 1/2`, starting +with a black square at `(0, 0)`. We encode the coloring by the function `checker`, which is `+1` on +black squares and `-1` on white squares, so that the integral of `checker` over a region is +"amount of black minus amount of white" in that region (see `integral_checker_eq_black_sub_white`). + +Every rectangle with an integer side contains equally much black and white; by additivity, so does +the big rectangle `R`. But a rectangle with lower left corner `(0, 0)` and no integer side contains +strictly more black than white. In our formalization the amount of black minus white in the +rectangle `[a, b] × [c, d]` is `(D b - D a) * (D d - D c)`, where `D x` is the distance of `x` +to the nearest integer. +-/ + +noncomputable section + +open MeasureTheory Set Filter Topology + +namespace SecondProof + +/-- The one-dimensional coloring: `+1` on `[k, k + 1/2)` and `-1` on `[k + 1/2, k + 1)`. -/ +def stripe (x : ℝ) : ℝ := if Even ⌊2 * x⌋ then 1 else -1 + +/-- The checkerboard coloring with black/white squares of size `1/2 × 1/2`, black square at the +origin: `checker p = 1` if `p` is black, `checker p = -1` if `p` is white. -/ +def checker (p : ℝ × ℝ) : ℝ := stripe p.1 * stripe p.2 + +/-- The black part of the plane. -/ +def black : Set (ℝ × ℝ) := {p | checker p = 1} + +/-- The white part of the plane. -/ +def white : Set (ℝ × ℝ) := {p | checker p = -1} + +/-- The distance from `x` to the nearest integer. It is a primitive of `stripe`. -/ +def distInt (x : ℝ) : ℝ := |x - round x| + +lemma measurable_stripe : Measurable stripe := by + unfold stripe + refine Measurable.ite ?_ measurable_const measurable_const + exact (Measurable.comp Int.measurable_floor (measurable_id.const_mul (2 : ℝ))) + (MeasurableSet.of_discrete (s := {n : ℤ | Even n})) + +lemma abs_stripe_le (x : ℝ) : |stripe x| ≤ 1 := by + unfold stripe; split_ifs <;> simp + +lemma distInt_lipschitz : LipschitzWith 1 distInt := by + refine LipschitzWith.of_dist_le_mul fun x y => ?_ + simp only [Real.dist_eq, NNReal.coe_one, one_mul, distInt] + rw [abs_sub_le_iff] + constructor + · linarith [round_le x (round y), abs_sub_le x y (round y : ℝ), abs_nonneg (y - round y)] + · linarith [round_le y (round x), abs_sub_le y x (round x : ℝ), abs_sub_comm x y] + +lemma distInt_of_floor_even {s : ℝ} {n : ℤ} (h : ⌊2 * s⌋ = 2 * n) : distInt s = s - n := by + rw [Int.floor_eq_iff] at h + push_cast at h + have hr : round s = n := by + rw [round_eq, Int.floor_eq_iff]; constructor <;> linarith + rw [distInt, hr, abs_of_nonneg (by linarith)] + +lemma distInt_of_floor_odd {s : ℝ} {n : ℤ} (h : ⌊2 * s⌋ = 2 * n + 1) : + distInt s = n + 1 - s := by + rw [Int.floor_eq_iff] at h + push_cast at h + have hr : round s = n + 1 := by + rw [round_eq, Int.floor_eq_iff]; push_cast; constructor <;> linarith + rw [distInt, hr, abs_of_nonpos (by push_cast; linarith)]; push_cast; ring + +lemma floor_two_mul_eventually (x : ℝ) : ∀ᶠ s in 𝓝[>] x, ⌊2 * s⌋ = ⌊2 * x⌋ := by + have h1 := Int.floor_le (2 * x) + have h2 := Int.lt_floor_add_one (2 * x) + have : x < (⌊2 * x⌋ + 1) / 2 := by linarith + filter_upwards [Ioo_mem_nhdsGT this] with s ⟨hs1, hs2⟩ + rw [Int.floor_eq_iff]; constructor <;> linarith + +lemma hasDerivWithinAt_distInt (x : ℝ) : HasDerivWithinAt distInt (stripe x) (Ioi x) x := by + have hev := floor_two_mul_eventually x + rcases Int.even_or_odd' ⌊2 * x⌋ with ⟨n, hn | hn⟩ + · have hs : stripe x = 1 := by simp [stripe, hn] + rw [hs] + refine ((hasDerivAt_id x).sub_const (n : ℝ)).hasDerivWithinAt.congr_of_eventuallyEq ?_ + (distInt_of_floor_even hn) + filter_upwards [hev] with s hs + exact distInt_of_floor_even (hs.trans hn) + · have hs : stripe x = -1 := by + simp only [stripe, hn]; rw [ch29_if_neg]; rw [Int.not_even_iff_odd]; exact ⟨n, rfl⟩ + rw [hs] + refine ((hasDerivAt_id x).const_sub ((n : ℝ) + 1)).hasDerivWithinAt.congr_of_eventuallyEq ?_ + (distInt_of_floor_odd hn) + filter_upwards [hev] with s hs + exact distInt_of_floor_odd (hs.trans hn) + +lemma intervalIntegrable_stripe (a b : ℝ) : IntervalIntegrable stripe volume a b := by + rw [intervalIntegrable_iff] + exact Measure.integrableOn_of_bounded (by simp) measurable_stripe.aestronglyMeasurable + (Eventually.of_forall fun x => by simpa using abs_stripe_le x) + +lemma integral_stripe_of_le {a b : ℝ} (hab : a ≤ b) : + ∫ x in a..b, stripe x = distInt b - distInt a := + intervalIntegral.integral_eq_sub_of_hasDeriv_right_of_le hab + distInt_lipschitz.continuous.continuousOn (fun x _ => hasDerivWithinAt_distInt x) + (intervalIntegrable_stripe a b) + +/-- `∫_a^b stripe = D b - D a`. -/ +lemma integral_stripe (a b : ℝ) : ∫ x in a..b, stripe x = distInt b - distInt a := by + rcases le_total a b with h | h + · exact integral_stripe_of_le h + · rw [intervalIntegral.integral_symm, integral_stripe_of_le h]; ring + +lemma distInt_add_int (x : ℝ) (n : ℤ) : distInt (x + n) = distInt x := by + simp [distInt, round_add_intCast] + +lemma distInt_pos {x : ℝ} (hx : x ≠ ⌊x⌋) : 0 < distInt x := by + refine abs_pos.2 (sub_ne_zero.2 fun e => hx ?_) + rw [e, Int.floor_intCast] + +lemma distInt_zero : distInt 0 = 0 := by + simp [distInt] + +lemma measurable_checker : Measurable checker := + (measurable_stripe.comp measurable_fst).mul (measurable_stripe.comp measurable_snd) + +lemma volume_toSet_ne_top (r : Rectangle) : volume r.toSet ≠ ⊤ := by + simp only [Rectangle.toSet, Measure.volume_eq_prod, Measure.prod_prod, Real.volume_Icc] + exact ENNReal.mul_ne_top ENNReal.ofReal_ne_top ENNReal.ofReal_ne_top + +/-- The amount of black minus white in a rectangle. -/ +lemma integral_checker_rect (r : Rectangle) : + ∫ p in r.toSet, checker p = + (distInt (r.x + r.w) - distInt r.x) * (distInt (r.y + r.h) - distInt r.y) := by + show ∫ p in Icc r.x (r.x + r.w) ×ˢ Icc r.y (r.y + r.h), stripe p.1 * stripe p.2 = _ + rw [Measure.volume_eq_prod, setIntegral_prod_mul stripe stripe, integral_Icc_eq_integral_Ioc, + integral_Icc_eq_integral_Ioc, ← intervalIntegral.integral_of_le (by linarith [r.w_pos]), + ← intervalIntegral.integral_of_le (by linarith [r.h_pos]), integral_stripe, integral_stripe] + +/-- The integral of `checker` over a region is the amount of black minus the amount of white. -/ +lemma integral_checker_eq_black_sub_white (r : Rectangle) : + ∫ p in r.toSet, checker p = volume.real (r.toSet ∩ black) - volume.real (r.toSet ∩ white) := by + have hB : MeasurableSet black := measurable_checker (measurableSet_singleton 1) + have hW : MeasurableSet white := measurable_checker (measurableSet_singleton (-1)) + have hpt : ∀ p, checker p = + black.indicator (fun _ => (1 : ℝ)) p - white.indicator (fun _ => (1 : ℝ)) p := by + intro p + have : checker p = 1 ∨ checker p = -1 := by + unfold checker stripe; split_ifs <;> simp + rcases this with h | h + · simp [indicator, black, white, h]; norm_num + · simp [indicator, black, white, h]; norm_num + have : IsFiniteMeasure (volume.restrict r.toSet) := + isFiniteMeasure_restrict.2 (volume_toSet_ne_top r) + simp_rw [hpt] + rw [integral_sub ((integrable_const (1 : ℝ)).indicator hB) + ((integrable_const (1 : ℝ)).indicator hW), integral_indicator_const _ hB, + integral_indicator_const _ hW, measureReal_restrict_apply hB, measureReal_restrict_apply hW, + inter_comm black, inter_comm white, smul_eq_mul, smul_eq_mul, mul_one, mul_one] + +/-- A rectangle with an integer side contains equal amounts of black and white. -/ +lemma integral_checker_eq_zero_of_int_side (r : Rectangle) (hr : r.w = ⌊r.w⌋ ∨ r.h = ⌊r.h⌋) : + ∫ p in r.toSet, checker p = 0 := by + rw [integral_checker_rect] + rcases hr with hw | hh + · rw [hw, distInt_add_int, sub_self, zero_mul] + · rw [hh, distInt_add_int, sub_self, mul_zero] + +lemma interior_ae_eq_toSet (r : Rectangle) : r.interior =ᵐ[volume] r.toSet := by + refine ae_eq_of_subset_of_measure_ge + (prod_mono Ioo_subset_Icc_self Ioo_subset_Icc_self) (le_of_eq ?_) + (measurableSet_Ioo.prod measurableSet_Ioo).nullMeasurableSet (volume_toSet_ne_top r) + simp only [Rectangle.toSet, Rectangle.interior, Measure.volume_eq_prod, Measure.prod_prod, + Real.volume_Icc, Real.volume_Ioo] + +lemma integrableOn_checker (r : Rectangle) : IntegrableOn checker r.toSet := by + exact Measure.integrableOn_of_bounded (volume_toSet_ne_top r) + measurable_checker.aestronglyMeasurable (M := 1) + (Eventually.of_forall fun p => by + have h1 := abs_stripe_le p.1 + have h2 := abs_stripe_le p.2 + simp only [checker, Real.norm_eq_abs, abs_mul] + nlinarith [abs_nonneg (stripe p.1), abs_nonneg (stripe p.2)]) + +/-- Additivity of the amount of black minus white over a tiling. -/ +lemma integral_checker_tiling {R : Rectangle} {Ts : List Rectangle} (h : is_tiling R Ts) : + ∫ p in R.toSet, checker p = ∑ t ∈ Ts.toFinset, ∫ p in t.toSet, checker p := by + rw [← h.2] + have h1 : (⋃ t ∈ Ts, t.toSet) =ᵐ[volume] ⋃ t ∈ Ts.toFinset, t.interior := by + have e1 : (⋃ t ∈ Ts, t.toSet) = ⋃ t ∈ (Ts.toFinset : Set Rectangle), t.toSet := by simp + have e2 : (⋃ t ∈ Ts.toFinset, t.interior) = + ⋃ t ∈ (Ts.toFinset : Set Rectangle), t.interior := by simp + rw [e1, e2] + exact ch29_eventuallyEq_biUnion Ts.toFinset.finite_toSet + fun t _ => (interior_ae_eq_toSet t).symm + rw [setIntegral_congr_set h1, integral_biUnion_finset] + · exact Finset.sum_congr rfl fun t _ => setIntegral_congr_set (interior_ae_eq_toSet t) + · exact fun t _ => measurableSet_Ioo.prod measurableSet_Ioo + · intro t ht t' ht' hne + exact Set.disjoint_iff_inter_eq_empty.2 + (tiling_interior_disjoint h (by simpa using ht) (by simpa using ht') hne) + · exact fun t _ => (integrableOn_checker t).mono_set + (prod_mono Ioo_subset_Icc_self Ioo_subset_Icc_self) + +/-- A rectangle with lower left corner `(0,0)` and no integer side contains strictly more black +than white. -/ +lemma integral_checker_pos_of_origin (R : Rectangle) (hx : R.x = 0) (hy : R.y = 0) + (hw : R.w ≠ ⌊R.w⌋) (hh : R.h ≠ ⌊R.h⌋) : 0 < ∫ p in R.toSet, checker p := by + rw [integral_checker_rect, hx, hy, zero_add, zero_add, distInt_zero, sub_zero, sub_zero] + exact mul_pos (distInt_pos hw) (distInt_pos hh) + +theorem integer_side_of_origin (R : Rectangle) (Ts : List Rectangle) (hx : R.x = 0) (hy : R.y = 0) + (h_tiling : is_tiling R Ts) (h_integer : ∀ t ∈ Ts, t.w = ⌊t.w⌋ ∨ t.h = ⌊t.h⌋) : + R.w = ⌊R.w⌋ ∨ R.h = ⌊R.h⌋ := by + by_contra hcon + push Not at hcon + have hpos := integral_checker_pos_of_origin R hx hy hcon.1 hcon.2 + rw [integral_checker_tiling h_tiling, + Finset.sum_eq_zero (fun t ht => integral_checker_eq_zero_of_int_side t + (h_integer t (by simpa using ht)))] at hpos + exact lt_irrefl _ hpos + +end SecondProof + +open SecondProof in +/-- **De Bruijn's theorem, second proof.** Whenever a rectangle is tiled by rectangles all of +which have at least one side of integer length, then the tiled rectangle has at least one side of +integer length. -/ +theorem rectangle_tiling_integer_side_second_proof (R : Rectangle) (Ts : List Rectangle) + (h_tiling : is_tiling R Ts) (h_integer : ∀ t ∈ Ts, t.w = ⌊t.w⌋ ∨ t.h = ⌊t.h⌋) : + R.w = ⌊R.w⌋ ∨ R.h = ⌊R.h⌋ := + tiling_reduce_to_origin (fun w h => w = ⌊w⌋ ∨ h = ⌊h⌋) + (fun R Ts hx hy h hP => integer_side_of_origin R Ts hx hy h hP) R Ts h_tiling h_integer + +end + +end + + +/-! --------------------------------------------------------------------------- +## Part from `Chapter_29/ThirdProof.lean` +--------------------------------------------------------------------------- -/ + +section + +/-! +# Tiling rectangles: the third proof (Mike Paterson) + +Let `C` be the set of corners of tiles with both coordinates integral, and `T` the set of tiles. +Form the bipartite graph joining a corner `c ∈ C` to every tile of which it is a corner. +Every tile is joined to `0`, `2` or `4` vertices of `C`; every `c ∈ C` that is not a corner of `R` +is joined to an even number of tiles, while `(0, 0)` is joined to exactly one tile. Counting the +edges of this graph in two ways gives a contradiction unless `R` has another corner in `C`, i.e. +unless `R` has an integer side. + +The only geometric input is the statement that a point `c` which is not a corner of the big +rectangle is a corner of an even number of tiles. We prove it by looking at the four "quadrants" +around `c`: each quadrant (near `c`) lying inside `R` is occupied by exactly one tile, and a tile +occupies an odd number of quadrants at `c` (namely exactly one) iff `c` is one of its corners. +-/ + +noncomputable section + +open Filter Topology Finset + +open scoped Classical + +namespace ThirdProof + +/-- One-dimensional version of a quadrant: the interval `[a, b]` occupies the right side of `z` +(`s = true`) if `a ≤ z < b`, and the left side of `z` (`s = false`) if `a < z ≤ b`. -/ +def occ1 (a b z : ℝ) (s : Bool) : Prop := if s then a ≤ z ∧ z < b else a < z ∧ z ≤ b + +/-- The rectangle `r` occupies the quadrant `q` around the point `c`, i.e. points of the form +`c + (±ε, ±ε)` lie in `r` for small `ε > 0` (signs given by `q`). -/ +def occupies (r : Rectangle) (c : ℝ × ℝ) (q : Bool × Bool) : Prop := + occ1 r.x (r.x + r.w) c.1 q.1 ∧ occ1 r.y (r.y + r.h) c.2 q.2 + +/-- The point `c` is a corner of the rectangle `r`. -/ +def IsCorner (r : Rectangle) (c : ℝ × ℝ) : Prop := + (c.1 = r.x ∨ c.1 = r.x + r.w) ∧ (c.2 = r.y ∨ c.2 = r.y + r.h) + +/-- The corner of `r` selected by a pair of booleans. -/ +def cornerPt (r : Rectangle) (b : Bool × Bool) : ℝ × ℝ := + (if b.1 then r.x + r.w else r.x, if b.2 then r.y + r.h else r.y) + +/-- The four corners of a rectangle. -/ +def corners (r : Rectangle) : Finset (ℝ × ℝ) := univ.image (cornerPt r) + +/-- A point of the plane with both coordinates integral. -/ +def IsLatticePoint (c : ℝ × ℝ) : Prop := (∃ m : ℤ, c.1 = m) ∧ (∃ n : ℤ, c.2 = n) + +/-- The point `c + ε (±1, ±1)`, with signs given by `q`. -/ +def qpoint (c : ℝ × ℝ) (q : Bool × Bool) (ε : ℝ) : ℝ × ℝ := + (c.1 + (if q.1 then ε else -ε), c.2 + (if q.2 then ε else -ε)) + +lemma occ1_eventually (a b z : ℝ) (s : Bool) : + ∀ᶠ ε in 𝓝[>] (0 : ℝ), + ((a ≤ z + (if s then ε else -ε) ∧ z + (if s then ε else -ε) ≤ b) ↔ occ1 a b z s) ∧ + ((a < z + (if s then ε else -ε) ∧ z + (if s then ε else -ε) < b) ↔ occ1 a b z s) := by + cases s + · simp only [occ1, Bool.false_eq_true, ↓reduceIte] + by_cases h1 : a < z ∧ z ≤ b + · filter_upwards [Ioo_mem_nhdsGT (sub_pos.2 h1.1)] with ε ⟨hε0, hε⟩ + exact ⟨iff_of_true ⟨by linarith, by linarith⟩ h1, iff_of_true ⟨by linarith, by linarith⟩ h1⟩ + · rcases not_and_or.1 h1 with h2 | h2 <;> push Not at h2 + · filter_upwards [self_mem_nhdsWithin] with ε (hε0 : 0 < ε) + exact ⟨iff_of_false (fun h => by linarith [h.1]) h1, + iff_of_false (fun h => by linarith [h.1]) h1⟩ + · filter_upwards [Ioo_mem_nhdsGT (sub_pos.2 h2)] with ε ⟨hε0, hε⟩ + exact ⟨iff_of_false (fun h => by linarith [h.2]) h1, + iff_of_false (fun h => by linarith [h.2]) h1⟩ + · simp only [occ1, ↓reduceIte] + by_cases h1 : a ≤ z ∧ z < b + · filter_upwards [Ioo_mem_nhdsGT (sub_pos.2 h1.2)] with ε ⟨hε0, hε⟩ + exact ⟨iff_of_true ⟨by linarith, by linarith⟩ h1, iff_of_true ⟨by linarith, by linarith⟩ h1⟩ + · rcases not_and_or.1 h1 with h2 | h2 <;> push Not at h2 + · filter_upwards [Ioo_mem_nhdsGT (sub_pos.2 h2)] with ε ⟨hε0, hε⟩ + exact ⟨iff_of_false (fun h => by linarith [h.1]) h1, + iff_of_false (fun h => by linarith [h.1]) h1⟩ + · filter_upwards [self_mem_nhdsWithin] with ε (hε0 : 0 < ε) + exact ⟨iff_of_false (fun h => by linarith [h.2]) h1, + iff_of_false (fun h => by linarith [h.2]) h1⟩ + +lemma occupies_eventually (r : Rectangle) (c : ℝ × ℝ) (q : Bool × Bool) : + ∀ᶠ ε in 𝓝[>] (0 : ℝ), + (qpoint c q ε ∈ r.toSet ↔ occupies r c q) ∧ (qpoint c q ε ∈ r.interior ↔ occupies r c q) := by + filter_upwards [occ1_eventually r.x (r.x + r.w) c.1 q.1, + occ1_eventually r.y (r.y + r.h) c.2 q.2] with ε h1 h2 + simp only [qpoint, occupies, Rectangle.toSet, Rectangle.interior, Set.mem_prod, Set.mem_Icc, + Set.mem_Ioo] + exact ⟨and_congr h1.1 h2.1, and_congr h1.2 h2.2⟩ + +/-- Each quadrant around `c` inside `R` is occupied by exactly one tile, and quadrants outside +`R` are occupied by no tile. -/ +lemma card_occupies_eq {R : Rectangle} {Ts : List Rectangle} (h : is_tiling R Ts) + (c : ℝ × ℝ) (q : Bool × Bool) : + (Ts.toFinset.filter (fun t => occupies t c q)).card = if occupies R c q then 1 else 0 := by + have hev : ∀ᶠ ε in 𝓝[>] (0:ℝ), + ((qpoint c q ε ∈ R.toSet ↔ occupies R c q) ∧ + (qpoint c q ε ∈ R.interior ↔ occupies R c q)) ∧ + ∀ t ∈ Ts.toFinset, (qpoint c q ε ∈ t.toSet ↔ occupies t c q) ∧ + (qpoint c q ε ∈ t.interior ↔ occupies t c q) := + (occupies_eventually R c q).and + ((Finset.eventually_all _).2 fun t _ => occupies_eventually t c q) + obtain ⟨ε, hR, ht⟩ := hev.exists + split_ifs with hocc + · rw [Finset.card_eq_one] + have hp : qpoint c q ε ∈ ⋃ t ∈ Ts, t.toSet := h.2 ▸ hR.1.2 hocc + simp only [Set.mem_iUnion] at hp + obtain ⟨t, htT, hpt⟩ := hp + refine ⟨t, ?_⟩ + ext t' + simp only [Finset.mem_filter, List.mem_toFinset, Finset.mem_singleton] + constructor + · rintro ⟨ht'T, ht'occ⟩ + by_contra hne + have hdis := tiling_interior_disjoint h ht'T htT hne + have a1 := (ht t' (by simpa using ht'T)).2.2 ht'occ + have a2 := (ht t (by simpa using htT)).2.2 ((ht t (by simpa using htT)).1.1 hpt) + exact (Set.eq_empty_iff_forall_notMem.1 hdis) _ ⟨a1, a2⟩ + · intro e + rw [e] + exact ⟨htT, (ht t (by simpa using htT)).1.1 hpt⟩ + · rw [Finset.card_eq_zero, Finset.filter_eq_empty_iff] + intro t htT hocc' + have hp := (ht t htT).1.2 hocc' + have hmem : qpoint c q ε ∈ ⋃ t ∈ Ts, t.toSet := + Set.mem_iUnion₂.2 ⟨t, List.mem_toFinset.1 htT, hp⟩ + rw [h.2] at hmem + exact hocc (hR.1.1 hmem) + +lemma odd_one_dim {a b : ℝ} (hab : a < b) (z : ℝ) : + Odd ((if a ≤ z ∧ z < b then 1 else 0) + (if a < z ∧ z ≤ b then 1 else 0) : ℕ) ↔ + z = a ∨ z = b := by + by_cases h1 : z < a + · rw [ch29_if_neg (by intro h; linarith [h.1]), ch29_if_neg (by intro h; linarith [h.1])] + simp; constructor <;> intro h <;> linarith + rcases (not_lt.1 h1).lt_or_eq with h1 | rfl + · rcases lt_trichotomy z b with h2 | rfl | h2 + · rw [ch29_if_pos ⟨h1.le, h2⟩, ch29_if_pos ⟨h1, h2.le⟩] + refine ⟨fun h => absurd h (by decide), ?_⟩; rintro (h | h) <;> linarith + · rw [ch29_if_neg (by intro h; linarith [h.2]), ch29_if_pos ⟨h1, le_rfl⟩]; simp + · rw [ch29_if_neg (by intro h; linarith [h.2]), ch29_if_neg (by intro h; linarith [h.2])] + simp; constructor <;> intro h <;> linarith + · rw [ch29_if_pos ⟨le_rfl, hab⟩, ch29_if_neg (by intro h; linarith [h.1])]; simp + +lemma nat_mod_two_eq (n : ℕ) : n % 2 = if Odd n then 1 else 0 := by + split_ifs with hn + · exact Nat.odd_iff.1 hn + · exact Nat.even_iff.1 (Nat.not_odd_iff_even.1 hn) + +/-- The number of quadrants around `c` occupied by `r`. -/ +def nquad (r : Rectangle) (c : ℝ × ℝ) : ℕ := ∑ q : Bool × Bool, if occupies r c q then 1 else 0 + +lemma odd_nquad_iff (r : Rectangle) (c : ℝ × ℝ) : Odd (nquad r c) ↔ IsCorner r c := by + have hsplit : nquad r c = + (∑ s : Bool, if occ1 r.x (r.x + r.w) c.1 s then 1 else 0) * + (∑ s : Bool, if occ1 r.y (r.y + r.h) c.2 s then 1 else 0) := by + rw [nquad, Fintype.sum_mul_sum, ← Finset.univ_product_univ, Finset.sum_product] + refine Finset.sum_congr rfl fun x _ => Finset.sum_congr rfl fun y _ => ?_ + rw [ite_zero_mul_ite_zero, mul_one] + exact if_congr Iff.rfl rfl rfl + rw [hsplit, Nat.odd_mul, IsCorner] + simp only [Fintype.sum_bool, occ1, ↓reduceIte, Bool.false_eq_true] + exact and_congr (odd_one_dim (lt_add_of_pos_right r.x r.w_pos) c.1) + (odd_one_dim (lt_add_of_pos_right r.y r.h_pos) c.2) + +/-- **Local parity.** For every point `c`, the number of tiles having `c` as a corner has the same +parity as the number of corners of `R` equal to `c`. -/ +lemma card_corner_mod_two {R : Rectangle} {Ts : List Rectangle} (h : is_tiling R Ts) + (c : ℝ × ℝ) : + (Ts.toFinset.filter (fun t => IsCorner t c)).card % 2 = if IsCorner R c then 1 else 0 := by + have key : ∑ t ∈ Ts.toFinset, nquad t c = nquad R c := by + simp only [nquad] + rw [Finset.sum_comm] + refine Finset.sum_congr rfl fun q _ => ?_ + rw [← card_occupies_eq h c q, Finset.card_filter] + calc (Ts.toFinset.filter (fun t => IsCorner t c)).card % 2 + = (∑ t ∈ Ts.toFinset, if Odd (nquad t c) then 1 else 0) % 2 := by + rw [Finset.card_filter]; simp_rw [odd_nquad_iff] + _ = (∑ t ∈ Ts.toFinset, nquad t c % 2) % 2 := by + congr 1; exact Finset.sum_congr rfl fun t _ => (nat_mod_two_eq _).symm + _ = nquad R c % 2 := by rw [← Finset.sum_nat_mod, key] + _ = _ := by rw [nat_mod_two_eq]; exact if_congr (odd_nquad_iff R c) rfl rfl + +lemma mem_corners_iff (r : Rectangle) (c : ℝ × ℝ) : c ∈ corners r ↔ IsCorner r c := by + simp only [corners, Finset.mem_image, Finset.mem_univ, true_and, IsCorner] + constructor + · rintro ⟨⟨b1, b2⟩, rfl⟩ + cases b1 <;> cases b2 <;> simp [cornerPt] + · rintro ⟨h1 | h1, h2 | h2⟩ + · exact ⟨(false, false), Prod.ext (by simp [cornerPt, h1]) (by simp [cornerPt, h2])⟩ + · exact ⟨(false, true), Prod.ext (by simp [cornerPt, h1]) (by simp [cornerPt, h2])⟩ + · exact ⟨(true, false), Prod.ext (by simp [cornerPt, h1]) (by simp [cornerPt, h2])⟩ + · exact ⟨(true, true), Prod.ext (by simp [cornerPt, h1]) (by simp [cornerPt, h2])⟩ + +/-- A tile with an integer side has an even number of integral corners. -/ +lemma even_card_lattice_corners (t : Rectangle) (ht : t.w = ⌊t.w⌋ ∨ t.h = ⌊t.h⌋) : + Even ((corners t).filter IsLatticePoint).card := by + have hinj : Function.Injective (cornerPt t) := by + have hw := t.w_pos + have hh := t.h_pos + rintro ⟨a1, a2⟩ ⟨b1, b2⟩ e + simp only [cornerPt, Prod.mk.injEq] at e + obtain ⟨e1, e2⟩ := e + cases a1 <;> cases b1 <;> cases a2 <;> cases b2 <;> simp_all + rw [corners, Finset.filter_image, Finset.card_image_of_injective _ hinj, Finset.card_filter] + have hsplit : (∑ q : Bool × Bool, if IsLatticePoint (cornerPt t q) then 1 else 0) = + (∑ s : Bool, if ∃ m : ℤ, (if s then t.x + t.w else t.x) = m then 1 else 0) * + (∑ s : Bool, if ∃ m : ℤ, (if s then t.y + t.h else t.y) = m then 1 else 0) := by + rw [Fintype.sum_mul_sum, ← Finset.univ_product_univ, Finset.sum_product] + refine Finset.sum_congr rfl fun x _ => Finset.sum_congr rfl fun y _ => ?_ + rw [ite_zero_mul_ite_zero, mul_one] + exact if_congr Iff.rfl rfl rfl + rw [hsplit] + have hint : ∀ a w : ℝ, w = ⌊w⌋ → ((∃ m : ℤ, a + w = m) ↔ ∃ m : ℤ, a = m) := by + intro a w hw + constructor + · rintro ⟨m, hm⟩; exact ⟨m - ⌊w⌋, by push_cast; linarith⟩ + · rintro ⟨m, hm⟩; exact ⟨m + ⌊w⌋, by push_cast; linarith⟩ + rcases ht with hw | hh + · apply Even.mul_right + simp only [Fintype.sum_bool, ↓reduceIte, Bool.false_eq_true] + rw [if_congr (hint t.x t.w hw) rfl rfl] + exact ⟨_, rfl⟩ + · apply Even.mul_left + simp only [Fintype.sum_bool, ↓reduceIte, Bool.false_eq_true] + rw [if_congr (hint t.y t.h hh) rfl rfl] + exact ⟨_, rfl⟩ + +/-- De Bruijn's theorem for a big rectangle with lower left corner `(0, 0)`, by double counting +the edges of the bipartite corner–tile graph. -/ +theorem integer_side_of_origin (R : Rectangle) (Ts : List Rectangle) (hx : R.x = 0) (hy : R.y = 0) + (h_tiling : is_tiling R Ts) (h_integer : ∀ t ∈ Ts, t.w = ⌊t.w⌋ ∨ t.h = ⌊t.h⌋) : + R.w = ⌊R.w⌋ ∨ R.h = ⌊R.h⌋ := by + by_contra hcon + push Not at hcon + obtain ⟨hw, hh⟩ := hcon + set T := Ts.toFinset with hT + set C := (T.biUnion corners).filter IsLatticePoint with hC + -- for lattice points, being a corner of `R` means being the origin + have hcornerR : ∀ c, IsLatticePoint c → (IsCorner R c ↔ c = (0, 0)) := by + rintro c ⟨⟨m, hm⟩, ⟨n, hn⟩⟩ + simp only [IsCorner, hx, hy, zero_add] + constructor + · rintro ⟨h1 | h1, h2 | h2⟩ + · exact Prod.ext h1 h2 + · exact absurd (by rw [← h2, hn, Int.floor_intCast]) hh + · exact absurd (by rw [← h1, hm, Int.floor_intCast]) hw + · exact absurd (by rw [← h1, hm, Int.floor_intCast]) hw + · intro e; subst e; exact ⟨Or.inl rfl, Or.inl rfl⟩ + have h00 : ((0 : ℝ), (0 : ℝ)) ∈ C := by + have hlat : IsLatticePoint ((0 : ℝ), (0 : ℝ)) := ⟨⟨0, by simp⟩, ⟨0, by simp⟩⟩ + have hodd := card_corner_mod_two h_tiling ((0 : ℝ), (0 : ℝ)) + rw [ch29_if_pos ((hcornerR _ hlat).2 rfl)] at hodd + obtain ⟨t, ht⟩ : (T.filter (fun t => IsCorner t ((0 : ℝ), (0 : ℝ)))).Nonempty := by + rw [← Finset.card_pos, hT]; omega + rw [Finset.mem_filter] at ht + rw [hC, Finset.mem_filter, Finset.mem_biUnion] + exact ⟨⟨t, ht.1, (mem_corners_iff _ _).2 ht.2⟩, hlat⟩ + have hdc := Finset.sum_card_bipartiteAbove_eq_sum_card_bipartiteBelow + (fun (c : ℝ × ℝ) (t : Rectangle) => IsCorner t c) (s := C) (t := T) + -- each tile is joined to an even number of corners in `C` + have hRHS : Even (∑ t ∈ T, (bipartiteBelow (fun c t => IsCorner t c) C t).card) := by + apply Finset.even_sum + intro t ht + have : bipartiteBelow (fun c t => IsCorner t c) C t = (corners t).filter IsLatticePoint := by + ext c + simp only [bipartiteBelow, hC, Finset.mem_filter, Finset.mem_biUnion] + constructor + · rintro ⟨⟨-, hc⟩, hct⟩ + exact ⟨(mem_corners_iff _ _).2 hct, hc⟩ + · rintro ⟨hct, hc⟩ + exact ⟨⟨⟨t, ht, hct⟩, hc⟩, (mem_corners_iff _ _).1 hct⟩ + rw [this] + exact even_card_lattice_corners t (h_integer t (by simpa [hT] using ht)) + -- only the origin is joined to an odd number of tiles + have hLHS : (∑ c ∈ C, (bipartiteAbove (fun c t => IsCorner t c) T c).card) % 2 = 1 := by + rw [Finset.sum_nat_mod] + have : ∀ c ∈ C, (bipartiteAbove (fun c t => IsCorner t c) T c).card % 2 = + if ((0 : ℝ), (0 : ℝ)) = c then 1 else 0 := by + intro c hc + rw [bipartiteAbove, card_corner_mod_two h_tiling c] + exact if_congr ((hcornerR c (Finset.mem_filter.1 hc).2).trans eq_comm) rfl rfl + rw [Finset.sum_congr rfl this, Finset.sum_ite_eq C, ch29_if_pos h00] + rw [hdc] at hLHS + exact Nat.not_even_iff_odd.2 (Nat.odd_iff.2 hLHS) hRHS + +end ThirdProof + +open ThirdProof in +/-- **De Bruijn's theorem, third proof.** Whenever a rectangle is tiled by rectangles all of which +have at least one side of integer length, then the tiled rectangle has at least one side of integer +length. -/ +theorem rectangle_tiling_integer_side_third_proof (R : Rectangle) (Ts : List Rectangle) + (h_tiling : is_tiling R Ts) (h_integer : ∀ t ∈ Ts, t.w = ⌊t.w⌋ ∨ t.h = ⌊t.h⌋) : + R.w = ⌊R.w⌋ ∨ R.h = ⌊R.h⌋ := + tiling_reduce_to_origin (fun w h => w = ⌊w⌋ ∨ h = ⌊h⌋) + (fun R Ts hx hy h hP => integer_side_of_origin R Ts hx hy h hP) R Ts h_tiling h_integer + +end + +end + + +/-! --------------------------------------------------------------------------- +## Part from `Chapter_29/DeBruijnPacking.lean` +--------------------------------------------------------------------------- -/ + +section + +/-! +# De Bruijn's packing theorem + +De Bruijn proved the following result about packing copies of an `a × b` rectangle into a +`c × d` rectangle: if `a, b, c, d` are integers, then each of `a` and `b` must divide one of `c` +or `d`. As explained in the chapter, this follows from two applications of the integer side +theorem `rectangle_tiling_integer_side`, after scaling the figure down by a factor `1 / a`, +respectively `1 / b`. +-/ + +noncomputable section + +/-- If every tile of a tiling of `R` has a side of length `a > 0`, then `R.w / a` or `R.h / a` +is an integer. This is the integer side theorem applied to the tiling scaled by `1 / a`. -/ +lemma side_div_integer_of_tiling {R : Rectangle} {Ts : List Rectangle} (h : is_tiling R Ts) + {a : ℝ} (ha : 0 < a) (hTs : ∀ t ∈ Ts, t.w = a ∨ t.h = a) : + (∃ n : ℤ, R.w / a = n) ∨ (∃ n : ℤ, R.h / a = n) := by + have hk : 0 < 1 / a := by positivity + have key := rectangle_tiling_integer_side _ _ (h.affine (1 / a) 0 0 hk) (by + intro t ht + obtain ⟨t', ht', rfl⟩ := List.mem_map.1 ht + rcases hTs t' ht' with e | e + · left; simp [Rectangle.affine, e, ha.ne'] + · right; simp [Rectangle.affine, e, ha.ne']) + simp only [Rectangle.affine, one_div] at key + rcases key with e | e + · exact Or.inl ⟨_, by rw [div_eq_inv_mul]; exact e⟩ + · exact Or.inr ⟨_, by rw [div_eq_inv_mul]; exact e⟩ + +lemma nat_dvd_of_div_eq_int {a c : ℕ} (ha : 0 < a) {n : ℤ} (h : (c : ℝ) / a = n) : a ∣ c := by + have ha' : (a : ℝ) ≠ 0 := by positivity + have : (c : ℝ) = a * n := by rw [← h]; field_simp + have : (c : ℤ) = a * n := by exact_mod_cast this + exact Int.natCast_dvd_natCast.1 ⟨n, this⟩ + +/-- **De Bruijn's packing theorem.** If a `c × d` rectangle is tiled by copies of an `a × b` +rectangle (each copy placed either horizontally or vertically), where `a, b, c, d` are positive +integers, then each of `a` and `b` divides `c` or `d`. -/ +theorem deBruijn_packing (a b c d : ℕ) (ha : 0 < a) (hb : 0 < b) (R : Rectangle) + (hRw : R.w = c) (hRh : R.h = d) (Ts : List Rectangle) (h : is_tiling R Ts) + (hTs : ∀ t ∈ Ts, (t.w = a ∧ t.h = b) ∨ (t.w = b ∧ t.h = a)) : + (a ∣ c ∨ a ∣ d) ∧ (b ∣ c ∨ b ∣ d) := by + constructor + · have := side_div_integer_of_tiling h (a := a) (by exact_mod_cast ha) (by + intro t ht; rcases hTs t ht with e | e + · exact Or.inl e.1 + · exact Or.inr e.2) + rw [hRw, hRh] at this + rcases this with ⟨n, hn⟩ | ⟨n, hn⟩ + · exact Or.inl (nat_dvd_of_div_eq_int ha hn) + · exact Or.inr (nat_dvd_of_div_eq_int ha hn) + · have := side_div_integer_of_tiling h (a := b) (by exact_mod_cast hb) (by + intro t ht; rcases hTs t ht with e | e + · exact Or.inr e.2 + · exact Or.inl e.1) + rw [hRw, hRh] at this + rcases this with ⟨n, hn⟩ | ⟨n, hn⟩ + · exact Or.inl (nat_dvd_of_div_eq_int hb hn) + · exact Or.inr (nat_dvd_of_div_eq_int hb hn) + +end + +end + + +/-! --------------------------------------------------------------------------- +## Part from `Chapter_29/HigherDim.lean` +--------------------------------------------------------------------------- -/ + +section + +/-! +# De Bruijn's theorem in `n` dimensions + +The chapter remarks that the proofs adapt to an `n`-dimensional version of de Bruijn's result: +whenever an `n`-dimensional box `R` is tiled by boxes all of which have at least one integer +side, then `R` has an integer side. We formalize this by adapting the first proof: the integral of +`∏ᵢ e^{2πi xᵢ}` over a box is the product of the one-dimensional integrals, which vanishes if and +only if the box has an integer side. +-/ + +noncomputable section + +open MeasureTheory Set Complex Real + +/-- An axis-parallel box in `ℝⁿ`, given by its lower corner `x` and its positive side lengths +`w`. -/ +structure Box (n : ℕ) where + /-- The lower corner of the box. -/ + x : Fin n → ℝ + /-- The side lengths of the box. -/ + w : Fin n → ℝ + w_pos : ∀ i, 0 < w i + +variable {n : ℕ} + +open scoped Classical + +/-- The closed box as a subset of `ℝⁿ`. -/ +def Box.toSet (b : Box n) : Set (Fin n → ℝ) := pi univ fun i => Icc (b.x i) (b.x i + b.w i) + +/-- The interior of the box. -/ +def Box.interior (b : Box n) : Set (Fin n → ℝ) := pi univ fun i => Ioo (b.x i) (b.x i + b.w i) + +/-- A list of boxes tiles the box `B` if the boxes have pairwise disjoint interiors and their +union is `B`. -/ +@[nolint defsWithUnderscore] +def is_box_tiling (B : Box n) (Ts : List (Box n)) : Prop := + (∀ i j : Fin Ts.length, i ≠ j → (Ts.get i).interior ∩ (Ts.get j).interior = ∅) ∧ + (⋃ t ∈ Ts, t.toSet) = B.toSet + +/-- The function `x ↦ ∏ᵢ e^{2πi xᵢ}`. -/ +def expChar (x : Fin n → ℝ) : ℂ := ∏ i, Complex.exp (2 * π * x i * I) + +/-- The one-dimensional computation `(2)` of the first proof: +`∫_a^{a+w} e^{2πit} dt = 0` if and only if `w` is an integer. -/ +lemma integral_exp_Icc_eq_zero_iff (a w : ℝ) (hw : 0 < w) : + ∫ t in Icc a (a + w), Complex.exp (2 * π * t * I) = 0 ↔ ∃ k : ℤ, w = k := by + rw [integral_Icc_eq_integral_Ioc, ← intervalIntegral.integral_of_le (by linarith)] + have hc : (2 * π * I : ℂ) ≠ 0 := by simp [Real.pi_ne_zero, I_ne_zero] + have key := integral_exp_mul_complex (a := a) (b := a + w) hc + simp_rw [show ∀ t : ℝ, (2 * π * t * I : ℂ) = 2 * π * I * t by intro; ring] + rw [key, div_eq_zero_iff, or_iff_left hc, sub_eq_zero, + show (2 * π * I * ↑(a + w) : ℂ) = 2 * π * I * w + 2 * π * I * a by push_cast; ring, + Complex.exp_add] + constructor + · intro h + have h1 : Complex.exp (2 * π * I * w) = 1 := by + have hne := Complex.exp_ne_zero (2 * π * I * a) + exact (mul_eq_right₀ hne).1 h + obtain ⟨n, hn⟩ := Complex.exp_eq_one_iff.1 h1 + refine ⟨n, ?_⟩ + have : (w : ℂ) = n := by + have := congrArg (fun z => z / (2 * π * I)) hn + field_simp at this + linear_combination this + exact_mod_cast this + · rintro ⟨k, rfl⟩ + rw [Complex.exp_eq_one_iff.2 ⟨k, by push_cast; ring⟩, one_mul] + +/-- The integral of `expChar` over a box is the product of the one-dimensional integrals. -/ +lemma integral_expChar_box (b : Box n) : + ∫ x in b.toSet, expChar x = + ∏ i, ∫ t in Icc (b.x i) (b.x i + b.w i), Complex.exp (2 * π * t * I) := by + rw [Box.toSet, volume_pi, Measure.restrict_pi_pi] + exact integral_fintype_prod_eq_prod (E := fun _ : Fin n => ℝ) + (fun (_ : Fin n) (t : ℝ) => Complex.exp (2 * π * t * I)) + (μ := fun i => volume.restrict (Icc (b.x i) (b.x i + b.w i))) + +/-- The integral of `expChar` over a box vanishes iff the box has an integer side. -/ +lemma integral_expChar_box_eq_zero_iff (b : Box n) : + ∫ x in b.toSet, expChar x = 0 ↔ ∃ i, b.w i = ⌊b.w i⌋ := by + rw [integral_expChar_box, Finset.prod_eq_zero_iff] + simp only [Finset.mem_univ, true_and] + refine exists_congr fun i => ?_ + rw [integral_exp_Icc_eq_zero_iff _ _ (b.w_pos i)] + constructor + · rintro ⟨k, hk⟩; rw [hk, Int.floor_intCast] + · intro h; exact ⟨_, h⟩ + +lemma Box.interior_ae_eq_toSet (b : Box n) : b.interior =ᵐ[volume] b.toSet := by + rw [Box.toSet, pi_univ_Icc] + exact Measure.univ_pi_Ioo_ae_eq_Icc + +lemma Box.isCompact_toSet (b : Box n) : IsCompact b.toSet := + isCompact_univ_pi fun _ => isCompact_Icc + +lemma continuous_expChar : Continuous (expChar (n := n)) := by + unfold expChar + fun_prop + +/-- Additivity of the integral of `expChar` over a tiling. -/ +lemma integral_expChar_tiling {B : Box n} {Ts : List (Box n)} (h : is_box_tiling B Ts) : + ∫ x in B.toSet, expChar x = ∑ t ∈ Ts.toFinset, ∫ x in t.toSet, expChar x := by + rw [← h.2] + have h1 : (⋃ t ∈ Ts, t.toSet) =ᵐ[volume] ⋃ t ∈ Ts.toFinset, t.interior := by + have e1 : (⋃ t ∈ Ts, t.toSet) = ⋃ t ∈ (Ts.toFinset : Set (Box n)), t.toSet := by simp + have e2 : (⋃ t ∈ Ts.toFinset, t.interior) = + ⋃ t ∈ (Ts.toFinset : Set (Box n)), t.interior := by simp + rw [e1, e2] + exact ch29_eventuallyEq_biUnion Ts.toFinset.finite_toSet + fun t _ => (Box.interior_ae_eq_toSet t).symm + rw [setIntegral_congr_set h1, integral_biUnion_finset] + · exact Finset.sum_congr rfl fun t _ => setIntegral_congr_set (Box.interior_ae_eq_toSet t) + · exact fun t _ => MeasurableSet.univ_pi fun _ => measurableSet_Ioo + · intro t ht t' ht' hne + simp only [Finset.mem_coe, List.mem_toFinset] at ht ht' + obtain ⟨i, rfl⟩ := List.mem_iff_get.1 ht + obtain ⟨j, rfl⟩ := List.mem_iff_get.1 ht' + exact Set.disjoint_iff_inter_eq_empty.2 (h.1 i j (fun e => hne (e ▸ rfl))) + · exact fun t _ => (continuous_expChar.continuousOn.integrableOn_compact + t.isCompact_toSet).mono_set (pi_mono fun _ _ => Ioo_subset_Icc_self) + +/-- **De Bruijn's theorem in `n` dimensions.** Whenever an `n`-dimensional box `B` is tiled by +boxes all of which have at least one side of integer length, then `B` has a side of integer +length. -/ +theorem box_tiling_integer_side (B : Box n) (Ts : List (Box n)) (h_tiling : is_box_tiling B Ts) + (h_integer : ∀ t ∈ Ts, ∃ i, t.w i = ⌊t.w i⌋) : + ∃ i, B.w i = ⌊B.w i⌋ := by + rw [← integral_expChar_box_eq_zero_iff, integral_expChar_tiling h_tiling] + exact Finset.sum_eq_zero fun t ht => + (integral_expChar_box_eq_zero_iff t).2 (h_integer t (by simpa using ht)) + +end + +end + From 5d21dc5e226cb278572fe891233a7166b782cd22 Mon Sep 17 00:00:00 2001 From: AItoBit <321732397+AItoBit@users.noreply.github.com> Date: Mon, 12 Oct 2026 11:29:39 +0200 Subject: [PATCH 2/2] Remove the trailing blank line in Chapter 29 --- FormalBook/Chapter_29.lean | 1 - 1 file changed, 1 deletion(-) diff --git a/FormalBook/Chapter_29.lean b/FormalBook/Chapter_29.lean index f31ed5f..a4ee889 100644 --- a/FormalBook/Chapter_29.lean +++ b/FormalBook/Chapter_29.lean @@ -2010,4 +2010,3 @@ theorem box_tiling_integer_side (B : Box n) (Ts : List (Box n)) (h_tiling : is_b end end -