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

source

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

WithBot (BoxIntegral.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

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

Instances For

source

@[simp]

theorem BoxIntegral.Box.coe_splitLower {ι : Type u_1} {I : BoxIntegral.Box ι} {i : ι} {x : ℝ} :

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

source

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

BoxIntegral.Box.splitLower I i x ≤ ↑I

source

@[simp]

theorem BoxIntegral.Box.splitLower_eq_bot {ι : Type u_1} {I : BoxIntegral.Box ι} {i : ι} {x : ℝ} :

BoxIntegral.Box.splitLower I i x = ⊥ ↔ x ≤ I.lower i

source

@[simp]

theorem BoxIntegral.Box.splitLower_eq_self {ι : Type u_1} {I : BoxIntegral.Box ι} {i : ι} {x : ℝ} :

BoxIntegral.Box.splitLower I i x = ↑I ↔ I.upper i ≤ x

source

theorem BoxIntegral.Box.splitLower_def {ι : Type u_1} {I : BoxIntegral.Box ι} [DecidableEq ι] {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) (_ : ∀ (x_1 : ι), I.lower x_1 < Function.update I.upper i x x_1)) :

BoxIntegral.Box.splitLower I i x = ↑{ lower := I.lower, upper := Function.update I.upper i x, lower_lt_upper := h' }

source

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

WithBot (BoxIntegral.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

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

Instances For

source

@[simp]

theorem BoxIntegral.Box.coe_splitUpper {ι : Type u_1} {I : BoxIntegral.Box ι} {i : ι} {x : ℝ} :

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

source

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

BoxIntegral.Box.splitUpper I i x ≤ ↑I

source

@[simp]

theorem BoxIntegral.Box.splitUpper_eq_bot {ι : Type u_1} {I : BoxIntegral.Box ι} {i : ι} {x : ℝ} :

BoxIntegral.Box.splitUpper I i x = ⊥ ↔ I.upper i ≤ x

source

@[simp]

theorem BoxIntegral.Box.splitUpper_eq_self {ι : Type u_1} {I : BoxIntegral.Box ι} {i : ι} {x : ℝ} :

BoxIntegral.Box.splitUpper I i x = ↑I ↔ x ≤ I.lower i

source

theorem BoxIntegral.Box.splitUpper_def {ι : Type u_1} {I : BoxIntegral.Box ι} [DecidableEq ι] {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) (_ : ∀ (x_1 : ι), Function.update I.lower i x x_1 < I.upper x_1)) :

BoxIntegral.Box.splitUpper I i x = ↑{ lower := Function.update I.lower i x, upper := I.upper, lower_lt_upper := h' }

source

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

Disjoint (BoxIntegral.Box.splitLower I i x) (BoxIntegral.Box.splitUpper I i x)

source

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

BoxIntegral.Box.splitLower I i x ≠ BoxIntegral.Box.splitUpper I i x

source

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

BoxIntegral.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

One or more equations did not get rendered due to their size.

Instances For

source

@[simp]

theorem BoxIntegral.Prepartition.mem_split_iff {ι : Type u_1} {I : BoxIntegral.Box ι} {J : BoxIntegral.Box ι} {i : ι} {x : ℝ} :

J ∈ BoxIntegral.Prepartition.split I i x ↔ ↑J = BoxIntegral.Box.splitLower I i x ∨ ↑J = BoxIntegral.Box.splitUpper I i x

source

theorem BoxIntegral.Prepartition.mem_split_iff' {ι : Type u_1} {I : BoxIntegral.Box ι} {J : BoxIntegral.Box ι} {i : ι} {x : ℝ} :

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

source

@[simp]

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

BoxIntegral.Prepartition.iUnion (BoxIntegral.Prepartition.split I i x) = ↑I

source

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

BoxIntegral.Prepartition.IsPartition (BoxIntegral.Prepartition.split I i x)

source

theorem BoxIntegral.Prepartition.sum_split_boxes {ι : Type u_1} {M : Type u_3} [AddCommMonoid M] (I : BoxIntegral.Box ι) (i : ι) (x : ℝ) (f : BoxIntegral.Box ι → M) :

(Finset.sum (BoxIntegral.Prepartition.split I i x).boxes fun (J : BoxIntegral.Box ι) => f J) = Option.elim' 0 f (BoxIntegral.Box.splitLower I i x) + Option.elim' 0 f (BoxIntegral.Box.splitUpper I i x)

source

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

BoxIntegral.Prepartition.split I i x = ⊤

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

source

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

↑J = ↑I ∩ {y : ι → ℝ | y i ≤ x}

source

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

↑J = ↑I ∩ {y : ι → ℝ | x < y i}

source

@[simp]

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

BoxIntegral.Prepartition.restrict (BoxIntegral.Prepartition.split J i x) I = BoxIntegral.Prepartition.split I i x

source

theorem BoxIntegral.Prepartition.inf_split {ι : Type u_1} {I : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I) (i : ι) (x : ℝ) :

π ⊓ BoxIntegral.Prepartition.split I i x = BoxIntegral.Prepartition.biUnion π fun (J : BoxIntegral.Box ι) => BoxIntegral.Prepartition.split J i x

source

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

BoxIntegral.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 = Finset.inf s fun (p : ι × ℝ) => BoxIntegral.Prepartition.split I p.1 p.2

Instances For

source

@[simp]

theorem BoxIntegral.Prepartition.splitMany_empty {ι : Type u_1} (I : BoxIntegral.Box ι) :

BoxIntegral.Prepartition.splitMany I ∅ = ⊤

source

@[simp]

theorem BoxIntegral.Prepartition.splitMany_insert {ι : Type u_1} (I : BoxIntegral.Box ι) (s : Finset (ι × ℝ)) (p : ι × ℝ) :

BoxIntegral.Prepartition.splitMany I (insert p s) = BoxIntegral.Prepartition.splitMany I s ⊓ BoxIntegral.Prepartition.split I p.1 p.2

source

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

BoxIntegral.Prepartition.splitMany I s ≤ BoxIntegral.Prepartition.split I p.1 p.2

source

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

BoxIntegral.Prepartition.IsPartition (BoxIntegral.Prepartition.splitMany I s)

source

@[simp]

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

BoxIntegral.Prepartition.iUnion (BoxIntegral.Prepartition.splitMany I s) = ↑I

source

theorem BoxIntegral.Prepartition.inf_splitMany {ι : Type u_1} {I : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I) (s : Finset (ι × ℝ)) :

π ⊓ BoxIntegral.Prepartition.splitMany I s = BoxIntegral.Prepartition.biUnion π fun (J : BoxIntegral.Box ι) => BoxIntegral.Prepartition.splitMany J s

source

theorem BoxIntegral.Prepartition.not_disjoint_imp_le_of_subset_of_mem_splitMany {ι : Type u_1} {I : BoxIntegral.Box ι} {J : BoxIntegral.Box ι} {Js : BoxIntegral.Box ι} {s : Finset (ι × ℝ)} (H : ∀ (i : ι), {(i, J.lower i), (i, J.upper i)} ⊆ s) (HJs : Js ∈ BoxIntegral.Prepartition.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.

source

theorem BoxIntegral.Prepartition.eventually_not_disjoint_imp_le_of_mem_splitMany {ι : Type u_1} [Finite ι] (s : Finset (BoxIntegral.Box ι)) :

∀ᶠ (t : Finset (ι × ℝ)) in Filter.atTop, ∀ (I J : BoxIntegral.Box ι), J ∈ s → ∀ J' ∈ BoxIntegral.Prepartition.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.