# 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 : 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)))

Instances For

source
@[simp]
theorem BoxIntegral.Box.coe_splitLower {ι : Type u_1} {I : Box ι} {i : ι} {x : ℝ} :
↑(I.splitLower i x) = ↑I ∩ {y : ι → ℝ | y i ≤ x}
source
theorem BoxIntegral.Box.splitLower_le {ι : Type u_1} {I : Box ι} {i : ι} {x : ℝ} :
I.splitLower i x ≤ ↑I
source
@[simp]
theorem BoxIntegral.Box.splitLower_eq_bot {ι : Type u_1} {I : Box ι} {i : ι} {x : ℝ} :
I.splitLower i x = ⊥ ↔ x ≤ I.lower i
source
@[simp]
theorem BoxIntegral.Box.splitLower_eq_self {ι : Type u_1} {I : Box ι} {i : ι} {x : ℝ} :
I.splitLower i x = ↑I ↔ I.upper i ≤ x
source
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' }
source
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

Instances For

source
@[simp]
theorem BoxIntegral.Box.coe_splitUpper {ι : Type u_1} {I : Box ι} {i : ι} {x : ℝ} :
↑(I.splitUpper i x) = ↑I ∩ {y : ι → ℝ | x < y i}
source
theorem BoxIntegral.Box.splitUpper_le {ι : Type u_1} {I : Box ι} {i : ι} {x : ℝ} :
I.splitUpper i x ≤ ↑I
source
@[simp]
theorem BoxIntegral.Box.splitUpper_eq_bot {ι : Type u_1} {I : Box ι} {i : ι} {x : ℝ} :
I.splitUpper i x = ⊥ ↔ I.upper i ≤ x
source
@[simp]
theorem BoxIntegral.Box.splitUpper_eq_self {ι : Type u_1} {I : Box ι} {i : ι} {x : ℝ} :
I.splitUpper i x = ↑I ↔ x ≤ I.lower i
source
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' }
source
theorem BoxIntegral.Box.disjoint_splitLower_splitUpper {ι : Type u_1} (I : Box ι) (i : ι) (x : ℝ) :
Disjoint (I.splitLower i x) (I.splitUpper i x)
source
theorem BoxIntegral.Box.splitLower_ne_splitUpper {ι : Type u_1} (I : Box ι) (i : ι) (x : ℝ) :
I.splitLower i x ≠ I.splitUpper i x
source
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} ⋯ ⋯

Instances For

source
@[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
source
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}
source
@[simp]
theorem BoxIntegral.Prepartition.iUnion_split {ι : Type u_1} (I : Box ι) (i : ι) (x : ℝ) :
(split I i x).iUnion = ↑I
source
theorem BoxIntegral.Prepartition.isPartitionSplit {ι : Type u_1} (I : Box ι) (i : ι) (x : ℝ) :
(split I i x).IsPartition
source
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)
source
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`.

source
@[deprecated BoxIntegral.Prepartition.split_of_notMem_Ioo (since := "2025-05-23")]
theorem BoxIntegral.Prepartition.split_of_not_mem_Ioo {ι : Type u_1} {I : Box ι} {i : ι} {x : ℝ} (h : x ∉ Set.Ioo (I.lower i) (I.upper i)) :
split I i x = ⊤

Alias of `BoxIntegral.Prepartition.split_of_notMem_Ioo`.

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 J : Box ι} {i : ι} {x : ℝ} {y : ι → ℝ} (h₁ : J ∈ 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 J : Box ι} {i : ι} {x : ℝ} {y : ι → ℝ} (h₁ : J ∈ 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 J : Box ι} (h : I ≤ J) (i : ι) (x : ℝ) :
(split J i x).restrict I = split I i x
source
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
source
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

Instances For

source
@[simp]
theorem BoxIntegral.Prepartition.splitMany_empty {ι : Type u_1} (I : Box ι) :
splitMany I ∅ = ⊤
source
@[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
source
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
source
theorem BoxIntegral.Prepartition.isPartition_splitMany {ι : Type u_1} (I : Box ι) (s : Finset (ι × ℝ)) :
(splitMany I s).IsPartition
source
@[simp]
theorem BoxIntegral.Prepartition.iUnion_splitMany {ι : Type u_1} (I : Box ι) (s : Finset (ι × ℝ)) :
(splitMany I s).iUnion = ↑I
source
theorem BoxIntegral.Prepartition.inf_splitMany {ι : Type u_1} {I : Box ι} (π : Prepartition I) (s : Finset (ι × ℝ)) :
π ⊓ splitMany I s = π.biUnion fun (J : Box ι) => splitMany J s
source
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`.

source
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`.

source
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
source
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
source
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 ≤ π`.

source
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`.

source
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

Instances For

source
@[simp]
theorem BoxIntegral.Prepartition.iUnion_compl {ι : Type u_1} {I : Box ι} [Finite ι] (π : Prepartition I) :
π.compl.iUnion = ↑I \ π.iUnion
source
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`.

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