# 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 : ) (i : ι) (x : ) :

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
Instances For
@[simp]
theorem BoxIntegral.Box.coe_splitLower {ι : Type u_1} {I : } {i : ι} {x : } :
(I.splitLower i x) = I {y : ι | y i x}
theorem BoxIntegral.Box.splitLower_le {ι : Type u_1} {I : } {i : ι} {x : } :
I.splitLower i x I
@[simp]
theorem BoxIntegral.Box.splitLower_eq_bot {ι : Type u_1} {I : } {i : ι} {x : } :
I.splitLower i x = x I.lower i
@[simp]
theorem BoxIntegral.Box.splitLower_eq_self {ι : Type u_1} {I : } {i : ι} {x : } :
I.splitLower i x = I I.upper i x
theorem BoxIntegral.Box.splitLower_def {ι : Type u_1} {I : } [] {i : ι} {x : } (h : x Set.Ioo (I.lower i) (I.upper i)) (h' : optParam (∀ (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 : ) (i : ι) (x : ) :

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
Instances For
@[simp]
theorem BoxIntegral.Box.coe_splitUpper {ι : Type u_1} {I : } {i : ι} {x : } :
(I.splitUpper i x) = I {y : ι | x < y i}
theorem BoxIntegral.Box.splitUpper_le {ι : Type u_1} {I : } {i : ι} {x : } :
I.splitUpper i x I
@[simp]
theorem BoxIntegral.Box.splitUpper_eq_bot {ι : Type u_1} {I : } {i : ι} {x : } :
I.splitUpper i x = I.upper i x
@[simp]
theorem BoxIntegral.Box.splitUpper_eq_self {ι : Type u_1} {I : } {i : ι} {x : } :
I.splitUpper i x = I x I.lower i
theorem BoxIntegral.Box.splitUpper_def {ι : Type u_1} {I : } [] {i : ι} {x : } (h : x Set.Ioo (I.lower i) (I.upper i)) (h' : optParam (∀ (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 : ) (i : ι) (x : ) :
Disjoint (I.splitLower i x) (I.splitUpper i x)
theorem BoxIntegral.Box.splitLower_ne_splitUpper {ι : Type u_1} (I : ) (i : ι) (x : ) :
I.splitLower i x I.splitUpper i x
def BoxIntegral.Prepartition.split {ι : Type u_1} (I : ) (i : ι) (x : ) :

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
Instances For
@[simp]
theorem BoxIntegral.Prepartition.mem_split_iff {ι : Type u_1} {I : } {J : } {i : ι} {x : } :
J = I.splitLower i x J = I.splitUpper i x
theorem BoxIntegral.Prepartition.mem_split_iff' {ι : Type u_1} {I : } {J : } {i : ι} {x : } :
J = I {y : ι | y i x} J = I {y : ι | x < y i}
@[simp]
theorem BoxIntegral.Prepartition.iUnion_split {ι : Type u_1} (I : ) (i : ι) (x : ) :
().iUnion = I
theorem BoxIntegral.Prepartition.isPartitionSplit {ι : Type u_1} (I : ) (i : ι) (x : ) :
().IsPartition
theorem BoxIntegral.Prepartition.sum_split_boxes {ι : Type u_1} {M : Type u_3} [] (I : ) (i : ι) (x : ) (f : M) :
J().boxes, f J = Option.elim' 0 f (I.splitLower i x) + Option.elim' 0 f (I.splitUpper i x)
theorem BoxIntegral.Prepartition.split_of_not_mem_Ioo {ι : Type u_1} {I : } {i : ι} {x : } (h : xSet.Ioo (I.lower i) (I.upper i)) :

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 : } {i : ι} {x : } {y : ι} (h₁ : ) (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 : } {i : ι} {x : } {y : ι} (h₁ : ) (h₂ : y J) (h₃ : x < y i) :
J = I {y : ι | x < y i}
@[simp]
theorem BoxIntegral.Prepartition.restrict_split {ι : Type u_1} {I : } {J : } (h : I J) (i : ι) (x : ) :
().restrict I =
theorem BoxIntegral.Prepartition.inf_split {ι : Type u_1} {I : } (π : ) (i : ι) (x : ) :
= π.biUnion fun (J : ) =>
def BoxIntegral.Prepartition.splitMany {ι : Type u_1} (I : ) (s : Finset (ι × )) :

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

Equations
• = s.inf fun (p : ι × ) =>
Instances For
@[simp]
@[simp]
theorem BoxIntegral.Prepartition.splitMany_insert {ι : Type u_1} (I : ) (s : Finset (ι × )) (p : ι × ) :
theorem BoxIntegral.Prepartition.splitMany_le_split {ι : Type u_1} (I : ) {s : Finset (ι × )} {p : ι × } (hp : p s) :
theorem BoxIntegral.Prepartition.isPartition_splitMany {ι : Type u_1} (I : ) (s : Finset (ι × )) :
.IsPartition
@[simp]
theorem BoxIntegral.Prepartition.iUnion_splitMany {ι : Type u_1} (I : ) (s : Finset (ι × )) :
.iUnion = I
theorem BoxIntegral.Prepartition.inf_splitMany {ι : Type u_1} {I : } (π : ) (s : Finset (ι × )) :
= π.biUnion fun (J : ) =>
theorem BoxIntegral.Prepartition.not_disjoint_imp_le_of_subset_of_mem_splitMany {ι : Type u_1} {I : } {J : } {Js : } {s : Finset (ι × )} (H : ∀ (i : ι), {(i, J.lower i), (i, J.upper i)} s) (HJs : ) (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} [] (s : ) :
∀ᶠ (t : Finset (ι × )) in Filter.atTop, ∀ (I J : ), J sJ', ¬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 : } [] (π : ) :
∀ᶠ (t : Finset (ι × )) in Filter.atTop, = .filter fun (J : ) => J π.iUnion
theorem BoxIntegral.Prepartition.exists_splitMany_inf_eq_filter_of_finite {ι : Type u_1} {I : } [] (s : ) (hs : s.Finite) :
∃ (t : Finset (ι × )), πs, = .filter fun (J : ) => J π.iUnion
theorem BoxIntegral.Prepartition.IsPartition.exists_splitMany_le {ι : Type u_1} [] {I : } {π : } (h : π.IsPartition) :
∃ (s : Finset (ι × )),

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 : } [] (π : ) :
∃ (π' : ), π'.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 : } [] (π : ) :

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

Equations
• π.compl = .choose
Instances For
@[simp]
theorem BoxIntegral.Prepartition.iUnion_compl {ι : Type u_1} {I : } [] (π : ) :
π.compl.iUnion = I \ π.iUnion
theorem BoxIntegral.Prepartition.compl_congr {ι : Type u_1} {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 : } [] {π : } (h : π.IsPartition) :
π.compl =
@[simp]
theorem BoxIntegral.Prepartition.compl_top {ι : Type u_1} {I : } [] :
.compl =