Split a box along one or more hyperplanes

Main definitions

A hyperplane {x : ι → ℝ | x i = a} splits a rectangular box I : BoxIntegral.Box ι into two smaller boxes. If a ∉ Ioo (I.lower i, I.upper i), then one of these boxes is empty, so it is not a box in the sense of BoxIntegral.Box.

We introduce the following definitions.

• BoxIntegral.Box.splitLower I i a and BoxIntegral.Box.splitUpper I i a are these boxes (as WithBot (BoxIntegral.Box ι));
• BoxIntegral.Prepartition.split I i a is the partition of I made of these two boxes (or of one box I if one of these boxes is empty);
• BoxIntegral.Prepartition.splitMany I s, where s : Finset (ι × ℝ) is a finite set of hyperplanes {x : ι → ℝ | x i = a} encoded as pairs (i, a), is the partition of I made by cutting it along all the hyperplanes in s.

Main results

The main result BoxIntegral.Prepartition.exists_iUnion_eq_diff says that any prepartition π of I admits a prepartition π' of I that covers exactly I \ π.iUnion. One of these prepartitions is available as BoxIntegral.Prepartition.compl.

Tags

rectangular box, partition, hyperplane

def BoxIntegral.Box.splitLower {ι : Type u_1} (I : Box ι) (i : ι) (x : ℝ) : WithBot (Box ι)

Given a box I and x ∈ (I.lower i, I.upper i), the hyperplane {y : ι → ℝ | y i = x} splits I into two boxes. BoxIntegral.Box.splitLower I i x is the box I ∩ {y | y i ≤ x} (if it is nonempty). As usual, we represent a box that may be empty as WithBot (BoxIntegral.Box ι).

Equations

• I.splitLower i x = BoxIntegral.Box.mk' I.lower (Function.update I.upper i (min x (I.upper i)))

@[simp]

theorem BoxIntegral.Box.coe_splitLower {ι : Type u_1} {I : Box ι} {i : ι} {x : ℝ} : ↑(I.splitLower i x) = ↑I ∩ {y : ι → ℝ | y i ≤ x}

theorem BoxIntegral.Box.splitLower_le {ι : Type u_1} {I : Box ι} {i : ι} {x : ℝ} : I.splitLower i x ≤ ↑I

@[simp]

theorem BoxIntegral.Box.splitLower_eq_bot {ι : Type u_1} {I : Box ι} {i : ι} {x : ℝ} : I.splitLower i x = ⊥ ↔ x ≤ I.lower i

@[simp]

theorem BoxIntegral.Box.splitLower_eq_self {ι : Type u_1} {I : Box ι} {i : ι} {x : ℝ} : I.splitLower i x = ↑I ↔ I.upper i ≤ x

theorem BoxIntegral.Box.splitLower_def {ι : Type u_1} {I : Box ι} [DecidableEq ι] {i : ι} {x : ℝ} (h : x ∈ Set.Ioo (I.lower i) (I.upper i)) (h' : ∀ (j : ι), I.lower j < Function.update I.upper i x j := ⋯) : I.splitLower i x = ↑{ lower := I.lower, upper := Function.update I.upper i x, lower_lt_upper := h' }

def BoxIntegral.Box.splitUpper {ι : Type u_1} (I : Box ι) (i : ι) (x : ℝ) : WithBot (Box ι)

Given a box I and x ∈ (I.lower i, I.upper i), the hyperplane {y : ι → ℝ | y i = x} splits I into two boxes. BoxIntegral.Box.splitUpper I i x is the box I ∩ {y | x < y i} (if it is nonempty). As usual, we represent a box that may be empty as WithBot (BoxIntegral.Box ι).

Equations

• I.splitUpper i x = BoxIntegral.Box.mk' (Function.update I.lower i (max x (I.lower i))) I.upper

@[simp]

theorem BoxIntegral.Box.coe_splitUpper {ι : Type u_1} {I : Box ι} {i : ι} {x : ℝ} : ↑(I.splitUpper i x) = ↑I ∩ {y : ι → ℝ | x < y i}

theorem BoxIntegral.Box.splitUpper_le {ι : Type u_1} {I : Box ι} {i : ι} {x : ℝ} : I.splitUpper i x ≤ ↑I

@[simp]

theorem BoxIntegral.Box.splitUpper_eq_bot {ι : Type u_1} {I : Box ι} {i : ι} {x : ℝ} : I.splitUpper i x = ⊥ ↔ I.upper i ≤ x

@[simp]

theorem BoxIntegral.Box.splitUpper_eq_self {ι : Type u_1} {I : Box ι} {i : ι} {x : ℝ} : I.splitUpper i x = ↑I ↔ x ≤ I.lower i

theorem BoxIntegral.Box.splitUpper_def {ι : Type u_1} {I : Box ι} [DecidableEq ι] {i : ι} {x : ℝ} (h : x ∈ Set.Ioo (I.lower i) (I.upper i)) (h' : ∀ (j : ι), Function.update I.lower i x j < I.upper j := ⋯) : I.splitUpper i x = ↑{ lower := Function.update I.lower i x, upper := I.upper, lower_lt_upper := h' }

theorem BoxIntegral.Box.disjoint_splitLower_splitUpper {ι : Type u_1} (I : Box ι) (i : ι) (x : ℝ) : Disjoint (I.splitLower i x) (I.splitUpper i x)

theorem BoxIntegral.Box.splitLower_ne_splitUpper {ι : Type u_1} (I : Box ι) (i : ι) (x : ℝ) : I.splitLower i x ≠ I.splitUpper i x

def BoxIntegral.Prepartition.split {ι : Type u_1} (I : Box ι) (i : ι) (x : ℝ) : Prepartition I

The partition of I : Box ι into the boxes I ∩ {y | y ≤ x i} and I ∩ {y | x i < y}. One of these boxes can be empty, then this partition is just the single-box partition ⊤.

Equations

• BoxIntegral.Prepartition.split I i x = BoxIntegral.Prepartition.ofWithBot {I.splitLower i x, I.splitUpper i x} ⋯ ⋯

@[simp]

theorem BoxIntegral.Prepartition.mem_split_iff {ι : Type u_1} {I J : Box ι} {i : ι} {x : ℝ} : J ∈ split I i x ↔ ↑J = I.splitLower i x ∨ ↑J = I.splitUpper i x

theorem BoxIntegral.Prepartition.mem_split_iff' {ι : Type u_1} {I J : Box ι} {i : ι} {x : ℝ} : J ∈ split I i x ↔ ↑J = ↑I ∩ {y : ι → ℝ | y i ≤ x} ∨ ↑J = ↑I ∩ {y : ι → ℝ | x < y i}

@[simp]

theorem BoxIntegral.Prepartition.iUnion_split {ι : Type u_1} (I : Box ι) (i : ι) (x : ℝ) : (split I i x).iUnion = ↑I

theorem BoxIntegral.Prepartition.isPartitionSplit {ι : Type u_1} (I : Box ι) (i : ι) (x : ℝ) : (split I i x).IsPartition

theorem BoxIntegral.Prepartition.sum_split_boxes {ι : Type u_1} {M : Type u_3} [AddCommMonoid M] (I : Box ι) (i : ι) (x : ℝ) (f : Box ι → M) : ∑ J ∈ (split I i x).boxes, f J = Option.elim' 0 f (I.splitLower i x) + Option.elim' 0 f (I.splitUpper i x)

theorem BoxIntegral.Prepartition.split_of_notMem_Ioo {ι : Type u_1} {I : Box ι} {i : ι} {x : ℝ} (h : x ∉ Set.Ioo (I.lower i) (I.upper i)) : split I i x = ⊤

If x ∉ (I.lower i, I.upper i), then the hyperplane {y | y i = x} does not split I.

theorem BoxIntegral.Prepartition.coe_eq_of_mem_split_of_mem_le {ι : Type u_1} {I J : Box ι} {i : ι} {x : ℝ} {y : ι → ℝ} (h₁ : J ∈ split I i x) (h₂ : y ∈ J) (h₃ : y i ≤ x) : ↑J = ↑I ∩ {y : ι → ℝ | y i ≤ x}

theorem BoxIntegral.Prepartition.coe_eq_of_mem_split_of_lt_mem {ι : Type u_1} {I J : Box ι} {i : ι} {x : ℝ} {y : ι → ℝ} (h₁ : J ∈ split I i x) (h₂ : y ∈ J) (h₃ : x < y i) : ↑J = ↑I ∩ {y : ι → ℝ | x < y i}

@[simp]

theorem BoxIntegral.Prepartition.restrict_split {ι : Type u_1} {I J : Box ι} (h : I ≤ J) (i : ι) (x : ℝ) : (split J i x).restrict I = split I i x

theorem BoxIntegral.Prepartition.inf_split {ι : Type u_1} {I : Box ι} (π : Prepartition I) (i : ι) (x : ℝ) : π ⊓ split I i x = π.biUnion fun (J : Box ι) => split J i x

def BoxIntegral.Prepartition.splitMany {ι : Type u_1} (I : Box ι) (s : Finset (ι × ℝ)) : Prepartition I

Split a box along many hyperplanes {y | y i = x}; each hyperplane is given by the pair (i x).

Equations

• BoxIntegral.Prepartition.splitMany I s = s.inf fun (p : ι × ℝ) => BoxIntegral.Prepartition.split I p.1 p.2

@[simp]

theorem BoxIntegral.Prepartition.splitMany_empty {ι : Type u_1} (I : Box ι) : splitMany I ∅ = ⊤

@[simp]

theorem BoxIntegral.Prepartition.splitMany_insert {ι : Type u_1} (I : Box ι) (s : Finset (ι × ℝ)) (p : ι × ℝ) : splitMany I (insert p s) = splitMany I s ⊓ split I p.1 p.2

theorem BoxIntegral.Prepartition.splitMany_le_split {ι : Type u_1} (I : Box ι) {s : Finset (ι × ℝ)} {p : ι × ℝ} (hp : p ∈ s) : splitMany I s ≤ split I p.1 p.2

theorem BoxIntegral.Prepartition.isPartition_splitMany {ι : Type u_1} (I : Box ι) (s : Finset (ι × ℝ)) : (splitMany I s).IsPartition

@[simp]

theorem BoxIntegral.Prepartition.iUnion_splitMany {ι : Type u_1} (I : Box ι) (s : Finset (ι × ℝ)) : (splitMany I s).iUnion = ↑I

theorem BoxIntegral.Prepartition.inf_splitMany {ι : Type u_1} {I : Box ι} (π : Prepartition I) (s : Finset (ι × ℝ)) : π ⊓ splitMany I s = π.biUnion fun (J : Box ι) => splitMany J s

theorem BoxIntegral.Prepartition.not_disjoint_imp_le_of_subset_of_mem_splitMany {ι : Type u_1} {I J Js : Box ι} {s : Finset (ι × ℝ)} (H : ∀ (i : ι), {(i, J.lower i), (i, J.upper i)} ⊆ s) (HJs : Js ∈ splitMany I s) (Hn : ¬Disjoint ↑J ↑Js) : Js ≤ J

Let s : Finset (ι × ℝ) be a set of hyperplanes {x : ι → ℝ | x i = r} in ι → ℝ encoded as pairs (i, r). Suppose that this set contains all faces of a box J. The hyperplanes of s split a box I into subboxes. Let Js be one of them. If J and Js have nonempty intersection, then Js is a subbox of J.

theorem BoxIntegral.Prepartition.eventually_not_disjoint_imp_le_of_mem_splitMany {ι : Type u_1} [Finite ι] (s : Finset (Box ι)) : ∀ᶠ (t : Finset (ι × ℝ)) in Filter.atTop, ∀ (I J : Box ι), J ∈ s → ∀ J' ∈ splitMany I t, ¬Disjoint ↑J ↑J' → J' ≤ J

Let s be a finite set of boxes in ℝⁿ = ι → ℝ. Then there exists a finite set t₀ of hyperplanes (namely, the set of all hyperfaces of boxes in s) such that for any t ⊇ t₀ and any box I in ℝⁿ the following holds. The hyperplanes from t split I into subboxes. Let J' be one of them, and let J be one of the boxes in s. If these boxes have a nonempty intersection, then J' ≤ J.

theorem BoxIntegral.Prepartition.eventually_splitMany_inf_eq_filter {ι : Type u_1} {I : Box ι} [Finite ι] (π : Prepartition I) : ∀ᶠ (t : Finset (ι × ℝ)) in Filter.atTop, π ⊓ splitMany I t = (splitMany I t).filter fun (J : Box ι) => ↑J ⊆ π.iUnion

theorem BoxIntegral.Prepartition.exists_splitMany_inf_eq_filter_of_finite {ι : Type u_1} {I : Box ι} [Finite ι] (s : Set (Prepartition I)) (hs : s.Finite) : ∃ (t : Finset (ι × ℝ)), ∀ π ∈ s, π ⊓ splitMany I t = (splitMany I t).filter fun (J : Box ι) => ↑J ⊆ π.iUnion

theorem BoxIntegral.Prepartition.IsPartition.exists_splitMany_le {ι : Type u_1} [Finite ι] {I : Box ι} {π : Prepartition I} (h : π.IsPartition) : ∃ (s : Finset (ι × ℝ)), splitMany I s ≤ π

If π is a partition of I, then there exists a finite set s of hyperplanes such that splitMany I s ≤ π.

theorem BoxIntegral.Prepartition.exists_iUnion_eq_diff {ι : Type u_1} {I : Box ι} [Finite ι] (π : Prepartition I) : ∃ (π' : Prepartition I), π'.iUnion = ↑I \ π.iUnion

For every prepartition π of I there exists a prepartition that covers exactly I \ π.iUnion.

def BoxIntegral.Prepartition.compl {ι : Type u_1} {I : Box ι} [Finite ι] (π : Prepartition I) : Prepartition I

If π is a prepartition of I, then π.compl is a prepartition of I such that π.compl.iUnion = I \ π.iUnion.

Equations

• π.compl = ⋯.choose

@[simp]

theorem BoxIntegral.Prepartition.iUnion_compl {ι : Type u_1} {I : Box ι} [Finite ι] (π : Prepartition I) : π.compl.iUnion = ↑I \ π.iUnion

theorem BoxIntegral.Prepartition.compl_congr {ι : Type u_1} {I : Box ι} [Finite ι] {π₁ π₂ : Prepartition I} (h : π₁.iUnion = π₂.iUnion) : π₁.compl = π₂.compl

Since the definition of BoxIntegral.Prepartition.compl uses Exists.choose, the result depends only on π.iUnion.

theorem BoxIntegral.Prepartition.IsPartition.compl_eq_bot {ι : Type u_1} {I : Box ι} [Finite ι] {π : Prepartition I} (h : π.IsPartition) : π.compl = ⊥

@[simp]

theorem BoxIntegral.Prepartition.compl_top {ι : Type u_1} {I : Box ι} [Finite ι] : ⊤.compl = ⊥