# mathlib3documentation

analysis.box_integral.partition.basic

# Partitions of rectangular boxes in ℝⁿ#

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

In this file we define (pre)partitions of rectangular boxes in ℝⁿ. A partition of a box I in ℝⁿ (see box_integral.prepartition and box_integral.prepartition.is_partition) is a finite set of pairwise disjoint boxes such that their union is exactly I. We use boxes : finset (box ι) to store the set of boxes.

Many lemmas about box integrals deal with pairwise disjoint collections of subboxes, so we define a structure box_integral.prepartition (I : box_integral.box ι) that stores a collection of boxes such that

• each box J ∈ boxes is a subbox of I;
• the boxes are pairwise disjoint as sets in ℝⁿ.

Then we define a predicate box_integral.prepartition.is_partition; π.is_partition means that the boxes of π actually cover the whole I. We also define some operations on prepartitions:

• box_integral.partition.bUnion: split each box of a partition into smaller boxes;
• box_integral.partition.restrict: restrict a partition to a smaller box.

We also define a semilattice_inf structure on box_integral.partition I for all I : box_integral.box ι.

## Tags #

rectangular box, partition

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

A prepartition of I : box_integral.box ι is a finite set of pairwise disjoint subboxes of I.

Instances for box_integral.prepartition
@[protected, instance]
Equations
@[simp]
theorem box_integral.prepartition.mem_boxes {ι : Type u_1} {I J : box_integral.box ι}  :
J π.boxes J π
@[simp]
theorem box_integral.prepartition.mem_mk {ι : Type u_1} {I J : box_integral.box ι} {s : finset } {h₁ : (J : , J s J I} {h₂ : s.pairwise } :
J {boxes := s, le_of_mem' := h₁, pairwise_disjoint := h₂} J s
theorem box_integral.prepartition.disjoint_coe_of_mem {ι : Type u_1} {I J₁ J₂ : box_integral.box ι} (h₁ : J₁ π) (h₂ : J₂ π) (h : J₁ J₂) :
J₂
theorem box_integral.prepartition.eq_of_mem_of_mem {ι : Type u_1} {I J₁ J₂ : box_integral.box ι} {x : ι } (h₁ : J₁ π) (h₂ : J₂ π) (hx₁ : x J₁) (hx₂ : x J₂) :
J₁ = J₂
theorem box_integral.prepartition.eq_of_le_of_le {ι : Type u_1} {I J J₁ J₂ : box_integral.box ι} (h₁ : J₁ π) (h₂ : J₂ π) (hle₁ : J J₁) (hle₂ : J J₂) :
J₁ = J₂
theorem box_integral.prepartition.eq_of_le {ι : Type u_1} {I J₁ J₂ : box_integral.box ι} (h₁ : J₁ π) (h₂ : J₂ π) (hle : J₁ J₂) :
J₁ = J₂
theorem box_integral.prepartition.le_of_mem {ι : Type u_1} {I J : box_integral.box ι} (hJ : J π) :
J I
theorem box_integral.prepartition.lower_le_lower {ι : Type u_1} {I J : box_integral.box ι} (hJ : J π) :
theorem box_integral.prepartition.upper_le_upper {ι : Type u_1} {I J : box_integral.box ι} (hJ : J π) :
@[ext]
theorem box_integral.prepartition.ext {ι : Type u_1} {I : box_integral.box ι} {π₁ π₂ : box_integral.prepartition I} (h : (J : , J π₁ J π₂) :
π₁ = π₂
def box_integral.prepartition.single {ι : Type u_1} (I J : box_integral.box ι) (h : J I) :

The singleton prepartition {J}, J ≤ I.

Equations
@[simp]
theorem box_integral.prepartition.single_boxes {ι : Type u_1} (I J : box_integral.box ι) (h : J I) :
= {J}
@[simp]
theorem box_integral.prepartition.mem_single {ι : Type u_1} {I J J' : box_integral.box ι} (h : J I) :
J' = J
@[protected, instance]

We say that π ≤ π' if each box of π is a subbox of some box of π'.

Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
theorem box_integral.prepartition.le_def {ι : Type u_1} {I : box_integral.box ι} {π₁ π₂ : box_integral.prepartition I} :
π₁ π₂ (J : , J π₁ ( (J' : (H : J' π₂), J J')
@[simp]
theorem box_integral.prepartition.mem_top {ι : Type u_1} {I J : box_integral.box ι} :
J J = I
@[simp]
@[simp]
@[simp]
theorem box_integral.prepartition.inj_on_set_of_mem_Icc_set_of_lower_eq {ι : Type u_1} {I : box_integral.box ι} (x : ι ) :
set.inj_on (λ (J : , {i : ι | J.lower i = x i}) {J : | J π

An auxiliary lemma used to prove that the same point can't belong to more than 2 ^ fintype.card ι closed boxes of a prepartition.

theorem box_integral.prepartition.card_filter_mem_Icc_le {ι : Type u_1} {I : box_integral.box ι} [fintype ι] (x : ι ) :
(finset.filter (λ (J : , π.boxes).card

The set of boxes of a prepartition that contain x in their closures has cardinality at most 2 ^ fintype.card ι.

@[protected]
def box_integral.prepartition.Union {ι : Type u_1} {I : box_integral.box ι}  :
set )

Given a prepartition π : box_integral.prepartition I, π.Union is the part of I covered by the boxes of π.

Equations
theorem box_integral.prepartition.Union_def {ι : Type u_1} {I : box_integral.box ι}  :
π.Union = (J : (H : J π), J
theorem box_integral.prepartition.Union_def' {ι : Type u_1} {I : box_integral.box ι}  :
π.Union = (J : (H : J π.boxes), J
@[simp]
theorem box_integral.prepartition.mem_Union {ι : Type u_1} {I : box_integral.box ι} {x : ι } :
x π.Union (J : (H : J π), x J
@[simp]
theorem box_integral.prepartition.Union_single {ι : Type u_1} {I J : box_integral.box ι} (h : J I) :
= J
@[simp]
@[simp]
@[simp]
theorem box_integral.prepartition.subset_Union {ι : Type u_1} {I J : box_integral.box ι} (h : J π) :
theorem box_integral.prepartition.Union_mono {ι : Type u_1} {I : box_integral.box ι} {π₁ π₂ : box_integral.prepartition I} (h : π₁ π₂) :
π₁.Union π₂.Union
theorem box_integral.prepartition.le_iff_nonempty_imp_le_and_Union_subset {ι : Type u_1} {I : box_integral.box ι} {π₁ π₂ : box_integral.prepartition I} :
π₁ π₂ ( (J : , J π₁ (J' : , J' π₂ (J J').nonempty J J') π₁.Union π₂.Union
theorem box_integral.prepartition.eq_of_boxes_subset_Union_superset {ι : Type u_1} {I : box_integral.box ι} {π₁ π₂ : box_integral.prepartition I} (h₁ : π₁.boxes π₂.boxes) (h₂ : π₂.Union π₁.Union) :
π₁ = π₂
noncomputable def box_integral.prepartition.bUnion {ι : Type u_1} {I : box_integral.box ι} (πi : Π (J : , ) :

Given a prepartition π of a box I and a collection of prepartitions πi J of all boxes J ∈ π, returns the prepartition of I into the union of the boxes of all πi J.

Though we only use the values of πi on the boxes of π, we require πi to be a globally defined function.

Equations
@[simp]
theorem box_integral.prepartition.bUnion_boxes {ι : Type u_1} {I : box_integral.box ι} (πi : Π (J : , ) :
(π.bUnion πi).boxes = π.boxes.bUnion (λ (J : , (πi J).boxes)
@[simp]
theorem box_integral.prepartition.mem_bUnion {ι : Type u_1} {I J : box_integral.box ι} {πi : Π (J : , } :
J π.bUnion πi (J' : (H : J' π), J πi J'
theorem box_integral.prepartition.bUnion_le {ι : Type u_1} {I : box_integral.box ι} (πi : Π (J : , ) :
π.bUnion πi π
@[simp]
theorem box_integral.prepartition.bUnion_top {ι : Type u_1} {I : box_integral.box ι}  :
π.bUnion (λ (_x : , ) = π
theorem box_integral.prepartition.bUnion_congr {ι : Type u_1} {I : box_integral.box ι} {π₁ π₂ : box_integral.prepartition I} {πi₁ πi₂ : Π (J : , } (h : π₁ = π₂) (hi : (J : , J π₁ πi₁ J = πi₂ J) :
π₁.bUnion πi₁ = π₂.bUnion πi₂
theorem box_integral.prepartition.bUnion_congr_of_le {ι : Type u_1} {I : box_integral.box ι} {π₁ π₂ : box_integral.prepartition I} {πi₁ πi₂ : Π (J : , } (h : π₁ = π₂) (hi : (J : , J I πi₁ J = πi₂ J) :
π₁.bUnion πi₁ = π₂.bUnion πi₂
@[simp]
theorem box_integral.prepartition.Union_bUnion {ι : Type u_1} {I : box_integral.box ι} (πi : Π (J : , ) :
(π.bUnion πi).Union = (J : (H : J π), (πi J).Union
@[simp]
theorem box_integral.prepartition.sum_bUnion_boxes {ι : Type u_1} {I : box_integral.box ι} {M : Type u_2} (πi : Π (J : , ) (f : M) :
(π.boxes.bUnion (λ (J : , (πi J).boxes)).sum (λ (J : , f J) = π.boxes.sum (λ (J : , (πi J).boxes.sum (λ (J' : , f J'))
noncomputable def box_integral.prepartition.bUnion_index {ι : Type u_1} {I : box_integral.box ι} (πi : Π (J : , ) (J : box_integral.box ι) :

Given a box J ∈ π.bUnion πi, returns the box J' ∈ π such that J ∈ πi J'. For J ∉ π.bUnion πi, returns I.

Equations
theorem box_integral.prepartition.bUnion_index_mem {ι : Type u_1} {I J : box_integral.box ι} {πi : Π (J : , } (hJ : J π.bUnion πi) :
π.bUnion_index πi J π
theorem box_integral.prepartition.bUnion_index_le {ι : Type u_1} {I : box_integral.box ι} (πi : Π (J : , ) (J : box_integral.box ι) :
π.bUnion_index πi J I
theorem box_integral.prepartition.mem_bUnion_index {ι : Type u_1} {I J : box_integral.box ι} {πi : Π (J : , } (hJ : J π.bUnion πi) :
J πi (π.bUnion_index πi J)
theorem box_integral.prepartition.le_bUnion_index {ι : Type u_1} {I J : box_integral.box ι} {πi : Π (J : , } (hJ : J π.bUnion πi) :
J π.bUnion_index πi J
theorem box_integral.prepartition.bUnion_index_of_mem {ι : Type u_1} {I J : box_integral.box ι} {πi : Π (J : , } (hJ : J π) {J' : box_integral.box ι} (hJ' : J' πi J) :
π.bUnion_index πi J' = J

Uniqueness property of box_integral.partition.bUnion_index.

theorem box_integral.prepartition.bUnion_assoc {ι : Type u_1} {I : box_integral.box ι} (πi : Π (J : , ) (πi' : ) :
π.bUnion (λ (J : , (πi J).bUnion (πi' J)) = (π.bUnion πi).bUnion (λ (J : , πi' (π.bUnion_index πi J) J)
def box_integral.prepartition.of_with_bot {ι : Type u_1} {I : box_integral.box ι} (boxes : finset (with_bot (box_integral.box ι))) (le_of_mem : (J : , J boxes J I) (pairwise_disjoint : boxes.pairwise disjoint) :

Create a box_integral.prepartition from a collection of possibly empty boxes by filtering out the empty one if it exists.

Equations
@[simp]
theorem box_integral.prepartition.mem_of_with_bot {ι : Type u_1} {I J : box_integral.box ι} {boxes : finset (with_bot (box_integral.box ι))} {h₁ : (J : , J boxes J I} {h₂ : boxes.pairwise disjoint} :
J h₂ J boxes
@[simp]
theorem box_integral.prepartition.Union_of_with_bot {ι : Type u_1} {I : box_integral.box ι} (boxes : finset (with_bot (box_integral.box ι))) (le_of_mem : (J : , J boxes J I) (pairwise_disjoint : boxes.pairwise disjoint) :
le_of_mem pairwise_disjoint).Union = (J : (H : J boxes), J
theorem box_integral.prepartition.of_with_bot_le {ι : Type u_1} {I : box_integral.box ι} {boxes : finset (with_bot (box_integral.box ι))} {le_of_mem : (J : , J boxes J I} {pairwise_disjoint : boxes.pairwise disjoint} (H : (J : , J boxes J ( (J' : (H : J' π), J J')) :
le_of_mem pairwise_disjoint π
theorem box_integral.prepartition.le_of_with_bot {ι : Type u_1} {I : box_integral.box ι} {boxes : finset (with_bot (box_integral.box ι))} {le_of_mem : (J : , J boxes J I} {pairwise_disjoint : boxes.pairwise disjoint} (H : (J : , J π ( (J' : (H : J' boxes), J J')) :
π le_of_mem pairwise_disjoint
theorem box_integral.prepartition.of_with_bot_mono {ι : Type u_1} {I : box_integral.box ι} {boxes₁ : finset (with_bot (box_integral.box ι))} {le_of_mem₁ : (J : , J boxes₁ J I} {pairwise_disjoint₁ : boxes₁.pairwise disjoint} {boxes₂ : finset (with_bot (box_integral.box ι))} {le_of_mem₂ : (J : , J boxes₂ J I} {pairwise_disjoint₂ : boxes₂.pairwise disjoint} (H : (J : , J boxes₁ J ( (J' : (H : J' boxes₂), J J')) :
le_of_mem₁ pairwise_disjoint₁ le_of_mem₂ pairwise_disjoint₂
theorem box_integral.prepartition.sum_of_with_bot {ι : Type u_1} {I : box_integral.box ι} {M : Type u_2} (boxes : finset (with_bot (box_integral.box ι))) (le_of_mem : (J : , J boxes J I) (pairwise_disjoint : boxes.pairwise disjoint) (f : M) :
le_of_mem pairwise_disjoint).boxes.sum (λ (J : , f J) = boxes.sum (λ (J : , f J)
noncomputable def box_integral.prepartition.restrict {ι : Type u_1} {I : box_integral.box ι} (J : box_integral.box ι) :

Restrict a prepartition to a box.

Equations
@[simp]
theorem box_integral.prepartition.mem_restrict {ι : Type u_1} {I J J₁ : box_integral.box ι}  :
J₁ π.restrict J (J' : (H : J' π), J₁ = J J'
theorem box_integral.prepartition.mem_restrict' {ι : Type u_1} {I J J₁ : box_integral.box ι}  :
J₁ π.restrict J (J' : (H : J' π), J₁ = J J'
theorem box_integral.prepartition.restrict_mono {ι : Type u_1} {I J : box_integral.box ι} {π₁ π₂ : box_integral.prepartition I} (Hle : π₁ π₂) :
π₁.restrict J π₂.restrict J
theorem box_integral.prepartition.monotone_restrict {ι : Type u_1} {I J : box_integral.box ι} :
monotone (λ (π : , π.restrict J)
theorem box_integral.prepartition.restrict_boxes_of_le {ι : Type u_1} {I J : box_integral.box ι} (h : I J) :
(π.restrict J).boxes = π.boxes

Restricting to a larger box does not change the set of boxes. We cannot claim equality of prepartitions because they have different types.

@[simp]
theorem box_integral.prepartition.restrict_self {ι : Type u_1} {I : box_integral.box ι}  :
π.restrict I = π
@[simp]
@[simp]
theorem box_integral.prepartition.restrict_bUnion {ι : Type u_1} {I J : box_integral.box ι} (πi : Π (J : , ) (hJ : J π) :
(π.bUnion πi).restrict J = πi J
theorem box_integral.prepartition.bUnion_le_iff {ι : Type u_1} {I : box_integral.box ι} {πi : Π (J : , } {π' : box_integral.prepartition I} :
π.bUnion πi π' (J : , J π πi J π'.restrict J
theorem box_integral.prepartition.le_bUnion_iff {ι : Type u_1} {I : box_integral.box ι} {πi : Π (J : , } {π' : box_integral.prepartition I} :
π' π.bUnion πi π' π (J : , J π π'.restrict J πi J
@[protected, instance]
noncomputable def box_integral.prepartition.has_inf {ι : Type u_1} {I : box_integral.box ι} :
Equations
theorem box_integral.prepartition.inf_def {ι : Type u_1} {I : box_integral.box ι} (π₁ π₂ : box_integral.prepartition I) :
π₁ π₂ = π₁.bUnion (λ (J : , π₂.restrict J)
@[simp]
theorem box_integral.prepartition.mem_inf {ι : Type u_1} {I J : box_integral.box ι} {π₁ π₂ : box_integral.prepartition I} :
J π₁ π₂ (J₁ : (H : J₁ π₁) (J₂ : (H : J₂ π₂), J = J₁ J₂
@[simp]
theorem box_integral.prepartition.Union_inf {ι : Type u_1} {I : box_integral.box ι} (π₁ π₂ : box_integral.prepartition I) :
(π₁ π₂).Union = π₁.Union π₂.Union
@[protected, instance]
noncomputable def box_integral.prepartition.semilattice_inf {ι : Type u_1} {I : box_integral.box ι} :
Equations
noncomputable def box_integral.prepartition.filter {ι : Type u_1} {I : box_integral.box ι} (p : Prop) :

The prepartition with boxes {J ∈ π | p J}.

Equations
@[simp]
theorem box_integral.prepartition.filter_boxes {ι : Type u_1} {I : box_integral.box ι} (p : Prop) :
(π.filter p).boxes =
@[simp]
theorem box_integral.prepartition.mem_filter {ι : Type u_1} {I J : box_integral.box ι} {p : Prop} :
J π.filter p J π p J
theorem box_integral.prepartition.filter_le {ι : Type u_1} {I : box_integral.box ι} (p : Prop) :
π.filter p π
theorem box_integral.prepartition.filter_of_true {ι : Type u_1} {I : box_integral.box ι} {p : Prop} (hp : (J : , J π p J) :
π.filter p = π
@[simp]
theorem box_integral.prepartition.filter_true {ι : Type u_1} {I : box_integral.box ι}  :
π.filter (λ (_x : , true) = π
@[simp]
theorem box_integral.prepartition.Union_filter_not {ι : Type u_1} {I : box_integral.box ι} (p : Prop) :
(π.filter (λ (J : , ¬p J)).Union = π.Union \ (π.filter p).Union
theorem box_integral.prepartition.sum_fiberwise {ι : Type u_1} {I : box_integral.box ι} {α : Type u_2} {M : Type u_3} (f : α) (g : M) :
π.boxes).sum (λ (y : α), (π.filter (λ (J : , f J = y)).boxes.sum (λ (J : , g J)) = π.boxes.sum (λ (J : , g J)
noncomputable def box_integral.prepartition.disj_union {ι : Type u_1} {I : box_integral.box ι} (π₁ π₂ : box_integral.prepartition I) (h : π₂.Union) :

Union of two disjoint prepartitions.

Equations
@[simp]
theorem box_integral.prepartition.disj_union_boxes {ι : Type u_1} {I : box_integral.box ι} (π₁ π₂ : box_integral.prepartition I) (h : π₂.Union) :
(π₁.disj_union π₂ h).boxes = π₁.boxes π₂.boxes
@[simp]
theorem box_integral.prepartition.mem_disj_union {ι : Type u_1} {I J : box_integral.box ι} {π₁ π₂ : box_integral.prepartition I} (H : π₂.Union) :
J π₁.disj_union π₂ H J π₁ J π₂
@[simp]
theorem box_integral.prepartition.Union_disj_union {ι : Type u_1} {I : box_integral.box ι} {π₁ π₂ : box_integral.prepartition I} (h : π₂.Union) :
(π₁.disj_union π₂ h).Union = π₁.Union π₂.Union
@[simp]
theorem box_integral.prepartition.sum_disj_union_boxes {ι : Type u_1} {I : box_integral.box ι} {π₁ π₂ : box_integral.prepartition I} {M : Type u_2} (h : π₂.Union) (f : M) :
(π₁.boxes π₂.boxes).sum (λ (J : , f J) = π₁.boxes.sum (λ (J : , f J) + π₂.boxes.sum (λ (J : , f J)
noncomputable def box_integral.prepartition.distortion {ι : Type u_1} {I : box_integral.box ι} [fintype ι] :

The distortion of a prepartition is the maximum of the distortions of the boxes of this prepartition.

Equations
theorem box_integral.prepartition.distortion_le_of_mem {ι : Type u_1} {I J : box_integral.box ι} [fintype ι] (h : J π) :
theorem box_integral.prepartition.distortion_bUnion {ι : Type u_1} {I : box_integral.box ι} [fintype ι] (πi : Π (J : , ) :
(π.bUnion πi).distortion = π.boxes.sup (λ (J : , (πi J).distortion)
@[simp]
theorem box_integral.prepartition.distortion_disj_union {ι : Type u_1} {I : box_integral.box ι} {π₁ π₂ : box_integral.prepartition I} [fintype ι] (h : π₂.Union) :
(π₁.disj_union π₂ h).distortion =
theorem box_integral.prepartition.distortion_of_const {ι : Type u_1} {I : box_integral.box ι} [fintype ι] {c : nnreal} (h₁ : π.boxes.nonempty) (h₂ : (J : , J π J.distortion = c) :
@[simp]
@[simp]

A prepartition π of I is a partition if the boxes of π cover the whole I.

Equations
@[simp]
theorem box_integral.prepartition.is_partition_single_iff {ι : Type u_1} {I J : box_integral.box ι} (h : J I) :
J = I
@[protected]
theorem box_integral.prepartition.is_partition.exists_unique {ι : Type u_1} {I : box_integral.box ι} {x : ι } (h : π.is_partition) (hx : x I) :
∃! (J : (H : J π), x J
theorem box_integral.prepartition.is_partition.eq_of_boxes_subset {ι : Type u_1} {I : box_integral.box ι} {π₁ π₂ : box_integral.prepartition I} (h₁ : π₁.is_partition) (h₂ : π₁.boxes π₂.boxes) :
π₁ = π₂
theorem box_integral.prepartition.is_partition.le_iff {ι : Type u_1} {I : box_integral.box ι} {π₁ π₂ : box_integral.prepartition I} (h : π₂.is_partition) :
π₁ π₂ (J : , J π₁ (J' : , J' π₂ (J J').nonempty J J'
@[protected]
theorem box_integral.prepartition.is_partition.bUnion {ι : Type u_1} {I : box_integral.box ι} {πi : Π (J : , } (h : π.is_partition) (hi : (J : , J π (πi J).is_partition) :
@[protected]
theorem box_integral.prepartition.is_partition.restrict {ι : Type u_1} {I J : box_integral.box ι} (h : π.is_partition) (hJ : J I) :
@[protected]
theorem box_integral.prepartition.is_partition.inf {ι : Type u_1} {I : box_integral.box ι} {π₁ π₂ : box_integral.prepartition I} (h₁ : π₁.is_partition) (h₂ : π₂.is_partition) :
(π₁ π₂).is_partition
theorem box_integral.prepartition.Union_bUnion_partition {ι : Type u_1} {I : box_integral.box ι} {πi : Π (J : , } (h : (J : , J π (πi J).is_partition) :
(π.bUnion πi).Union = π.Union