Split a box along one or more hyperplanes #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

Main definitions #

A hyperplane {x : ι → ℝ | x i = a} splits a rectangular box I : box_integral.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 box_integral.box.

We introduce the following definitions.

box_integral.box.split_lower I i a and box_integral.box.split_upper I i a are these boxes (as with_bot (box_integral.box ι));
box_integral.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);
box_integral.prepartition.split_many 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 box_integral.prepartition.exists_Union_eq_diff says that any prepartition π of I admits a prepartition π' of I that covers exactly I \ π.Union. One of these prepartitions is available as box_integral.prepartition.compl.

Tags #

rectangular box, partition, hyperplane

source

noncomputable def box_integral.box.split_lower {ι : Type u_1} (I : box_integral.box ι) (i : ι) (x : ℝ) :

with_bot (box_integral.box ι)

Given a box I and x ∈ (I.lower i, I.upper i), the hyperplane {y : ι → ℝ | y i = x} splits I into two boxes. box_integral.box.split_lower 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 with_bot (box_integral.box ι).

Equations

I.split_lower i x = box_integral.box.mk' I.lower (function.update I.upper i (linear_order.min x (I.upper i)))

source

@[simp]

theorem box_integral.box.coe_split_lower {ι : Type u_1} {I : box_integral.box ι} {i : ι} {x : ℝ} :

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

source

theorem box_integral.box.split_lower_le {ι : Type u_1} {I : box_integral.box ι} {i : ι} {x : ℝ} :

I.split_lower i x ≤ ↑I

source

@[simp]

theorem box_integral.box.split_lower_eq_bot {ι : Type u_1} {I : box_integral.box ι} {i : ι} {x : ℝ} :

I.split_lower i x = ⊥ ↔ x ≤ I.lower i

source

@[simp]

theorem box_integral.box.split_lower_eq_self {ι : Type u_1} {I : box_integral.box ι} {i : ι} {x : ℝ} :

I.split_lower i x = ↑I ↔ I.upper i ≤ x

source

theorem box_integral.box.split_lower_def {ι : Type u_1} {I : box_integral.box ι} [decidable_eq ι] {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.split_lower i x = ↑{lower := I.lower, upper := function.update I.upper i x, lower_lt_upper := h'}

source

noncomputable def box_integral.box.split_upper {ι : Type u_1} (I : box_integral.box ι) (i : ι) (x : ℝ) :

with_bot (box_integral.box ι)

Given a box I and x ∈ (I.lower i, I.upper i), the hyperplane {y : ι → ℝ | y i = x} splits I into two boxes. box_integral.box.split_upper 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 with_bot (box_integral.box ι).

Equations

I.split_upper i x = box_integral.box.mk' (function.update I.lower i (linear_order.max x (I.lower i))) I.upper

source

@[simp]

theorem box_integral.box.coe_split_upper {ι : Type u_1} {I : box_integral.box ι} {i : ι} {x : ℝ} :

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

source

theorem box_integral.box.split_upper_le {ι : Type u_1} {I : box_integral.box ι} {i : ι} {x : ℝ} :

I.split_upper i x ≤ ↑I

source

@[simp]

theorem box_integral.box.split_upper_eq_bot {ι : Type u_1} {I : box_integral.box ι} {i : ι} {x : ℝ} :

I.split_upper i x = ⊥ ↔ I.upper i ≤ x

source

@[simp]

theorem box_integral.box.split_upper_eq_self {ι : Type u_1} {I : box_integral.box ι} {i : ι} {x : ℝ} :

I.split_upper i x = ↑I ↔ x ≤ I.lower i

source

theorem box_integral.box.split_upper_def {ι : Type u_1} {I : box_integral.box ι} [decidable_eq ι] {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.split_upper i x = ↑{lower := function.update I.lower i x, upper := I.upper, lower_lt_upper := h'}

source

theorem box_integral.box.disjoint_split_lower_split_upper {ι : Type u_1} (I : box_integral.box ι) (i : ι) (x : ℝ) :

disjoint (I.split_lower i x) (I.split_upper i x)

source

theorem box_integral.box.split_lower_ne_split_upper {ι : Type u_1} (I : box_integral.box ι) (i : ι) (x : ℝ) :

I.split_lower i x ≠ I.split_upper i x

source

noncomputable def box_integral.prepartition.split {ι : Type u_1} (I : box_integral.box ι) (i : ι) (x : ℝ) :

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

box_integral.prepartition.split I i x = box_integral.prepartition.of_with_bot {I.split_lower i x, I.split_upper i x} _ _

source

@[simp]

theorem box_integral.prepartition.mem_split_iff {ι : Type u_1} {I J : box_integral.box ι} {i : ι} {x : ℝ} :

J ∈ box_integral.prepartition.split I i x ↔ ↑J = I.split_lower i x ∨ ↑J = I.split_upper i x

source

theorem box_integral.prepartition.mem_split_iff' {ι : Type u_1} {I J : box_integral.box ι} {i : ι} {x : ℝ} :

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

source

@[simp]

theorem box_integral.prepartition.Union_split {ι : Type u_1} (I : box_integral.box ι) (i : ι) (x : ℝ) :

(box_integral.prepartition.split I i x).Union = ↑I

source

theorem box_integral.prepartition.is_partition_split {ι : Type u_1} (I : box_integral.box ι) (i : ι) (x : ℝ) :

(box_integral.prepartition.split I i x).is_partition

source

theorem box_integral.prepartition.sum_split_boxes {ι : Type u_1} {M : Type u_2} [add_comm_monoid M] (I : box_integral.box ι) (i : ι) (x : ℝ) (f : box_integral.box ι → M) :

(box_integral.prepartition.split I i x).boxes.sum (λ (J : box_integral.box ι), f J) = option.elim 0 f (I.split_lower i x) + option.elim 0 f (I.split_upper i x)

source

theorem box_integral.prepartition.split_of_not_mem_Ioo {ι : Type u_1} {I : box_integral.box ι} {i : ι} {x : ℝ} (h : x ∉ set.Ioo (I.lower i) (I.upper i)) :

box_integral.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 box_integral.prepartition.coe_eq_of_mem_split_of_mem_le {ι : Type u_1} {I J : box_integral.box ι} {i : ι} {x : ℝ} {y : ι → ℝ} (h₁ : J ∈ box_integral.prepartition.split I i x) (h₂ : y ∈ J) (h₃ : y i ≤ x) :

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

source

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

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

source

@[simp]

theorem box_integral.prepartition.restrict_split {ι : Type u_1} {I J : box_integral.box ι} (h : I ≤ J) (i : ι) (x : ℝ) :

(box_integral.prepartition.split J i x).restrict I = box_integral.prepartition.split I i x

source

theorem box_integral.prepartition.inf_split {ι : Type u_1} {I : box_integral.box ι} (π : box_integral.prepartition I) (i : ι) (x : ℝ) :

π ⊓ box_integral.prepartition.split I i x = π.bUnion (λ (J : box_integral.box ι), box_integral.prepartition.split J i x)

source

noncomputable def box_integral.prepartition.split_many {ι : Type u_1} (I : box_integral.box ι) (s : finset (ι × ℝ)) :

box_integral.prepartition I

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

Equations

box_integral.prepartition.split_many I s = s.inf (λ (p : ι × ℝ), box_integral.prepartition.split I p.fst p.snd)

source

@[simp]

theorem box_integral.prepartition.split_many_empty {ι : Type u_1} (I : box_integral.box ι) :

box_integral.prepartition.split_many I ∅ = ⊤

source

@[simp]

theorem box_integral.prepartition.split_many_insert {ι : Type u_1} (I : box_integral.box ι) (s : finset (ι × ℝ)) (p : ι × ℝ) :

box_integral.prepartition.split_many I (has_insert.insert p s) = box_integral.prepartition.split_many I s ⊓ box_integral.prepartition.split I p.fst p.snd

source

theorem box_integral.prepartition.split_many_le_split {ι : Type u_1} (I : box_integral.box ι) {s : finset (ι × ℝ)} {p : ι × ℝ} (hp : p ∈ s) :

box_integral.prepartition.split_many I s ≤ box_integral.prepartition.split I p.fst p.snd

source

theorem box_integral.prepartition.is_partition_split_many {ι : Type u_1} (I : box_integral.box ι) (s : finset (ι × ℝ)) :

(box_integral.prepartition.split_many I s).is_partition

source

@[simp]

theorem box_integral.prepartition.Union_split_many {ι : Type u_1} (I : box_integral.box ι) (s : finset (ι × ℝ)) :

(box_integral.prepartition.split_many I s).Union = ↑I

source

theorem box_integral.prepartition.inf_split_many {ι : Type u_1} {I : box_integral.box ι} (π : box_integral.prepartition I) (s : finset (ι × ℝ)) :

π ⊓ box_integral.prepartition.split_many I s = π.bUnion (λ (J : box_integral.box ι), box_integral.prepartition.split_many J s)

source

theorem box_integral.prepartition.not_disjoint_imp_le_of_subset_of_mem_split_many {ι : Type u_1} {I J Js : box_integral.box ι} {s : finset (ι × ℝ)} (H : ∀ (i : ι), {(i, J.lower i), (i, J.upper i)} ⊆ s) (HJs : Js ∈ box_integral.prepartition.split_many 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 box_integral.prepartition.eventually_not_disjoint_imp_le_of_mem_split_many {ι : Type u_1} [finite ι] (s : finset (box_integral.box ι)) :

∀ᶠ (t : finset (ι × ℝ)) in filter.at_top , ∀ (I J : box_integral.box ι), J ∈ s → ∀ (J' : box_integral.box ι), J' ∈ box_integral.prepartition.split_many 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 box_integral.prepartition.eventually_split_many_inf_eq_filter {ι : Type u_1} {I : box_integral.box ι} [finite ι] (π : box_integral.prepartition I) :

∀ᶠ (t : finset (ι × ℝ)) in filter.at_top , π ⊓ box_integral.prepartition.split_many I t = (box_integral.prepartition.split_many I t).filter (λ (J : box_integral.box ι), ↑J ⊆ π.Union)

source

theorem box_integral.prepartition.exists_split_many_inf_eq_filter_of_finite {ι : Type u_1} {I : box_integral.box ι} [finite ι] (s : set (box_integral.prepartition I)) (hs : s.finite) :

∃ (t : finset (ι × ℝ)), ∀ (π : box_integral.prepartition I), π ∈ s → π ⊓ box_integral.prepartition.split_many I t = (box_integral.prepartition.split_many I t).filter (λ (J : box_integral.box ι), ↑J ⊆ π.Union)

source

theorem box_integral.prepartition.is_partition.exists_split_many_le {ι : Type u_1} [finite ι] {I : box_integral.box ι} {π : box_integral.prepartition I} (h : π.is_partition) :

∃ (s : finset (ι × ℝ)), box_integral.prepartition.split_many I s ≤ π

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

source

theorem box_integral.prepartition.exists_Union_eq_diff {ι : Type u_1} {I : box_integral.box ι} [finite ι] (π : box_integral.prepartition I) :

∃ (π' : box_integral.prepartition I), π'.Union = ↑I \ π.Union

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

source

noncomputable def box_integral.prepartition.compl {ι : Type u_1} {I : box_integral.box ι} [finite ι] (π : box_integral.prepartition I) :

box_integral.prepartition I

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

Equations

π.compl = _.some

source

@[simp]

theorem box_integral.prepartition.Union_compl {ι : Type u_1} {I : box_integral.box ι} [finite ι] (π : box_integral.prepartition I) :

π.compl.Union = ↑I \ π.Union

source

theorem box_integral.prepartition.compl_congr {ι : Type u_1} {I : box_integral.box ι} [finite ι] {π₁ π₂ : box_integral.prepartition I} (h : π₁.Union = π₂.Union) :

π₁.compl = π₂.compl

Since the definition of box_integral.prepartition.compl uses Exists.some, the result depends only on π.Union.

source

theorem box_integral.prepartition.is_partition.compl_eq_bot {ι : Type u_1} {I : box_integral.box ι} [finite ι] {π : box_integral.prepartition I} (h : π.is_partition) :

π.compl = ⊥

source

@[simp]

theorem box_integral.prepartition.compl_top {ι : Type u_1} {I : box_integral.box ι} [finite ι] :

⊤.compl = ⊥