mathlib3 documentation

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

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:

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
@[simp]
@[simp]
theorem box_integral.prepartition.mem_mk {ι : Type u_1} {I J : box_integral.box ι} {s : finset (box_integral.box ι)} {h₁ : (J : box_integral.box ι), J s J I} {h₂ : s.pairwise (disjoint on coe)} :
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 ι} (π : box_integral.prepartition I) (h₁ : J₁ π) (h₂ : J₂ π) (h : J₁ J₂) :
disjoint J₁ J₂
theorem box_integral.prepartition.eq_of_mem_of_mem {ι : Type u_1} {I J₁ J₂ : box_integral.box ι} (π : box_integral.prepartition I) {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 ι} (π : box_integral.prepartition I) (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 ι} (π : box_integral.prepartition I) (h₁ : J₁ π) (h₂ : J₂ π) (hle : J₁ J₂) :
J₁ = J₂
theorem box_integral.prepartition.le_of_mem {ι : Type u_1} {I J : box_integral.box ι} (π : box_integral.prepartition I) (hJ : J π) :
J I
@[ext]
theorem box_integral.prepartition.ext {ι : Type u_1} {I : box_integral.box ι} {π₁ π₂ : box_integral.prepartition I} (h : (J : box_integral.box ι), J π₁ J π₂) :
π₁ = π₂

The singleton prepartition {J}, J ≤ I.

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

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

Equations
@[protected, instance]
Equations
theorem box_integral.prepartition.le_def {ι : Type u_1} {I : box_integral.box ι} {π₁ π₂ : box_integral.prepartition I} :
π₁ π₂ (J : box_integral.box ι), J π₁ ( (J' : box_integral.box ι) (H : J' π₂), J J')
@[simp]
theorem box_integral.prepartition.mem_top {ι : Type u_1} {I J : box_integral.box ι} :
J J = I
@[simp]
@[simp]

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

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

@[protected]

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

Equations
@[simp]
theorem box_integral.prepartition.mem_Union {ι : Type u_1} {I : box_integral.box ι} (π : box_integral.prepartition I) {x : ι } :
x π.Union (J : box_integral.box ι) (H : J π), x J
@[simp]
@[simp]
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 : box_integral.box ι), J π₁ (J' : box_integral.box ι), 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) :
π₁ = π₂

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]
@[simp]
theorem box_integral.prepartition.mem_bUnion {ι : Type u_1} {I J : box_integral.box ι} (π : box_integral.prepartition I) {πi : Π (J : box_integral.box ι), box_integral.prepartition J} :
J π.bUnion πi (J' : box_integral.box ι) (H : J' π), J πi J'
@[simp]
theorem box_integral.prepartition.bUnion_congr {ι : Type u_1} {I : box_integral.box ι} {π₁ π₂ : box_integral.prepartition I} {πi₁ πi₂ : Π (J : box_integral.box ι), box_integral.prepartition J} (h : π₁ = π₂) (hi : (J : box_integral.box ι), 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 : box_integral.box ι), box_integral.prepartition J} (h : π₁ = π₂) (hi : (J : box_integral.box ι), J I πi₁ J = πi₂ J) :
π₁.bUnion πi₁ = π₂.bUnion πi₂
@[simp]
theorem box_integral.prepartition.Union_bUnion {ι : Type u_1} {I : box_integral.box ι} (π : box_integral.prepartition I) (πi : Π (J : box_integral.box ι), box_integral.prepartition J) :
(π.bUnion πi).Union = (J : box_integral.box ι) (H : J π), (πi J).Union
@[simp]
theorem box_integral.prepartition.sum_bUnion_boxes {ι : Type u_1} {I : box_integral.box ι} {M : Type u_2} [add_comm_monoid M] (π : box_integral.prepartition I) (πi : Π (J : box_integral.box ι), box_integral.prepartition J) (f : box_integral.box ι M) :
(π.boxes.bUnion (λ (J : box_integral.box ι), (πi J).boxes)).sum (λ (J : box_integral.box ι), f J) = π.boxes.sum (λ (J : box_integral.box ι), (πi J).boxes.sum (λ (J' : box_integral.box ι), f J'))

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.mem_bUnion_index {ι : Type u_1} {I J : box_integral.box ι} (π : box_integral.prepartition I) {πi : Π (J : box_integral.box ι), box_integral.prepartition J} (hJ : J π.bUnion πi) :
J πi (π.bUnion_index πi J)
theorem box_integral.prepartition.bUnion_index_of_mem {ι : Type u_1} {I J : box_integral.box ι} (π : box_integral.prepartition I) {πi : Π (J : box_integral.box ι), box_integral.prepartition 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 ι} (π : box_integral.prepartition I) (πi : Π (J : box_integral.box ι), box_integral.prepartition J) (πi' : box_integral.box ι Π (J : box_integral.box ι), box_integral.prepartition J) :
π.bUnion (λ (J : box_integral.box ι), (πi J).bUnion (πi' J)) = (π.bUnion πi).bUnion (λ (J : box_integral.box ι), π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 : with_bot (box_integral.box ι)), 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 : with_bot (box_integral.box ι)), J boxes J I} {h₂ : boxes.pairwise disjoint} :
@[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 : with_bot (box_integral.box ι)), J boxes J I) (pairwise_disjoint : boxes.pairwise disjoint) :
(box_integral.prepartition.of_with_bot boxes le_of_mem pairwise_disjoint).Union = (J : with_bot (box_integral.box ι)) (H : J boxes), J
theorem box_integral.prepartition.of_with_bot_le {ι : Type u_1} {I : box_integral.box ι} (π : box_integral.prepartition I) {boxes : finset (with_bot (box_integral.box ι))} {le_of_mem : (J : with_bot (box_integral.box ι)), J boxes J I} {pairwise_disjoint : boxes.pairwise disjoint} (H : (J : with_bot (box_integral.box ι)), J boxes J ( (J' : box_integral.box ι) (H : J' π), J J')) :
box_integral.prepartition.of_with_bot boxes le_of_mem pairwise_disjoint π
theorem box_integral.prepartition.le_of_with_bot {ι : Type u_1} {I : box_integral.box ι} (π : box_integral.prepartition I) {boxes : finset (with_bot (box_integral.box ι))} {le_of_mem : (J : with_bot (box_integral.box ι)), J boxes J I} {pairwise_disjoint : boxes.pairwise disjoint} (H : (J : box_integral.box ι), J π ( (J' : with_bot (box_integral.box ι)) (H : J' boxes), J J')) :
π box_integral.prepartition.of_with_bot boxes 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 : with_bot (box_integral.box ι)), J boxes₁ J I} {pairwise_disjoint₁ : boxes₁.pairwise disjoint} {boxes₂ : finset (with_bot (box_integral.box ι))} {le_of_mem₂ : (J : with_bot (box_integral.box ι)), J boxes₂ J I} {pairwise_disjoint₂ : boxes₂.pairwise disjoint} (H : (J : with_bot (box_integral.box ι)), J boxes₁ J ( (J' : with_bot (box_integral.box ι)) (H : J' boxes₂), J J')) :
box_integral.prepartition.of_with_bot boxes₁ le_of_mem₁ pairwise_disjoint₁ box_integral.prepartition.of_with_bot boxes₂ le_of_mem₂ pairwise_disjoint₂
theorem box_integral.prepartition.sum_of_with_bot {ι : Type u_1} {I : box_integral.box ι} {M : Type u_2} [add_comm_monoid M] (boxes : finset (with_bot (box_integral.box ι))) (le_of_mem : (J : with_bot (box_integral.box ι)), J boxes J I) (pairwise_disjoint : boxes.pairwise disjoint) (f : box_integral.box ι M) :
(box_integral.prepartition.of_with_bot boxes le_of_mem pairwise_disjoint).boxes.sum (λ (J : box_integral.box ι), f J) = boxes.sum (λ (J : with_bot (box_integral.box ι)), option.elim 0 f J)

Restrict a prepartition to a box.

Equations
@[simp]
theorem box_integral.prepartition.mem_restrict {ι : Type u_1} {I J J₁ : box_integral.box ι} (π : box_integral.prepartition I) :
J₁ π.restrict J (J' : box_integral.box ι) (H : J' π), J₁ = J J'
theorem box_integral.prepartition.mem_restrict' {ι : Type u_1} {I J J₁ : box_integral.box ι} (π : box_integral.prepartition I) :
J₁ π.restrict J (J' : box_integral.box ι) (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

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_bUnion {ι : Type u_1} {I J : box_integral.box ι} (π : box_integral.prepartition I) (πi : Π (J : box_integral.box ι), box_integral.prepartition J) (hJ : J π) :
(π.bUnion πi).restrict J = πi J
@[protected, instance]
Equations
theorem box_integral.prepartition.inf_def {ι : Type u_1} {I : box_integral.box ι} (π₁ π₂ : box_integral.prepartition I) :
π₁ π₂ = π₁.bUnion (λ (J : box_integral.box ι), π₂.restrict J)
@[simp]
theorem box_integral.prepartition.mem_inf {ι : Type u_1} {I J : box_integral.box ι} {π₁ π₂ : box_integral.prepartition I} :
J π₁ π₂ (J₁ : box_integral.box ι) (H : J₁ π₁) (J₂ : box_integral.box ι) (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

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

Equations
@[simp]
theorem box_integral.prepartition.mem_filter {ι : Type u_1} {I J : box_integral.box ι} (π : box_integral.prepartition I) {p : box_integral.box ι Prop} :
J π.filter p J π p J
theorem box_integral.prepartition.filter_of_true {ι : Type u_1} {I : box_integral.box ι} (π : box_integral.prepartition I) {p : box_integral.box ι Prop} (hp : (J : box_integral.box ι), J π p J) :
π.filter p = π
@[simp]
@[simp]
theorem box_integral.prepartition.Union_filter_not {ι : Type u_1} {I : box_integral.box ι} (π : box_integral.prepartition I) (p : box_integral.box ι Prop) :
(π.filter (λ (J : box_integral.box ι), ¬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} [add_comm_monoid M] (π : box_integral.prepartition I) (f : box_integral.box ι α) (g : box_integral.box ι M) :
(finset.image f π.boxes).sum (λ (y : α), (π.filter (λ (J : box_integral.box ι), f J = y)).boxes.sum (λ (J : box_integral.box ι), g J)) = π.boxes.sum (λ (J : box_integral.box ι), g J)
noncomputable def box_integral.prepartition.disj_union {ι : Type u_1} {I : box_integral.box ι} (π₁ π₂ : box_integral.prepartition I) (h : disjoint π₁.Union π₂.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 : disjoint π₁.Union π₂.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 : disjoint π₁.Union π₂.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 : disjoint π₁.Union π₂.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} [add_comm_monoid M] (h : disjoint π₁.Union π₂.Union) (f : box_integral.box ι M) :
(π₁.boxes π₂.boxes).sum (λ (J : box_integral.box ι), f J) = π₁.boxes.sum (λ (J : box_integral.box ι), f J) + π₂.boxes.sum (λ (J : box_integral.box ι), f J)

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

Equations
@[simp]
theorem box_integral.prepartition.distortion_of_const {ι : Type u_1} {I : box_integral.box ι} (π : box_integral.prepartition I) [fintype ι] {c : nnreal} (h₁ : π.boxes.nonempty) (h₂ : (J : box_integral.box ι), J π J.distortion = c) :

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

Equations
@[protected]
theorem box_integral.prepartition.is_partition.exists_unique {ι : Type u_1} {I : box_integral.box ι} {π : box_integral.prepartition I} {x : ι } (h : π.is_partition) (hx : x I) :
∃! (J : box_integral.box ι) (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 : box_integral.box ι), J π₁ (J' : box_integral.box ι), J' π₂ (J J').nonempty J J'
@[protected]
@[protected]
@[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