# Partitions of rectangular boxes in ℝⁿ#

In this file we define (pre)partitions of rectangular boxes in ℝⁿ. A partition of a box I in ℝⁿ (see BoxIntegral.Prepartition and BoxIntegral.Prepartition.IsPartition) 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 BoxIntegral.Prepartition (I : BoxIntegral.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 BoxIntegral.Prepartition.IsPartition; π.IsPartition means that the boxes of π actually cover the whole I. We also define some operations on prepartitions:

• BoxIntegral.Prepartition.biUnion: split each box of a partition into smaller boxes;
• BoxIntegral.Prepartition.restrict: restrict a partition to a smaller box.

We also define a SemilatticeInf structure on BoxIntegral.Prepartition I for all I : BoxIntegral.Box ι.

## Tags #

rectangular box, partition

structure BoxIntegral.Prepartition {ι : Type u_1} (I : ) :
Type u_1

A prepartition of I : BoxIntegral.Box ι is a finite set of pairwise disjoint subboxes of I.

• boxes :

The underlying set of boxes

• le_of_mem' : Jself.boxes, J I

Each box is a sub-box of I

• pairwiseDisjoint : (self.boxes).Pairwise (Disjoint on BoxIntegral.Box.toSet)

The boxes in a prepartition are pairwise disjoint.

Instances For
theorem BoxIntegral.Prepartition.le_of_mem' {ι : Type u_1} {I : } (self : ) (J : ) :
J self.boxesJ I

Each box is a sub-box of I

theorem BoxIntegral.Prepartition.pairwiseDisjoint {ι : Type u_1} {I : } (self : ) :
(self.boxes).Pairwise (Disjoint on BoxIntegral.Box.toSet)

The boxes in a prepartition are pairwise disjoint.

Equations
• BoxIntegral.Prepartition.instMembershipBox = { mem := fun (J : ) (π : ) => J π.boxes }
@[simp]
theorem BoxIntegral.Prepartition.mem_boxes {ι : Type u_1} {I : } {J : } (π : ) :
J π.boxes J π
@[simp]
theorem BoxIntegral.Prepartition.mem_mk {ι : Type u_1} {I : } {J : } {s : } {h₁ : Js, J I} {h₂ : (s).Pairwise (Disjoint on BoxIntegral.Box.toSet)} :
J { boxes := s, le_of_mem' := h₁, pairwiseDisjoint := h₂ } J s
theorem BoxIntegral.Prepartition.disjoint_coe_of_mem {ι : Type u_1} {I : } {J₁ : } {J₂ : } (π : ) (h₁ : J₁ π) (h₂ : J₂ π) (h : J₁ J₂) :
Disjoint J₁ J₂
theorem BoxIntegral.Prepartition.eq_of_mem_of_mem {ι : Type u_1} {I : } {J₁ : } {J₂ : } (π : ) {x : ι} (h₁ : J₁ π) (h₂ : J₂ π) (hx₁ : x J₁) (hx₂ : x J₂) :
J₁ = J₂
theorem BoxIntegral.Prepartition.eq_of_le_of_le {ι : Type u_1} {I : } {J : } {J₁ : } {J₂ : } (π : ) (h₁ : J₁ π) (h₂ : J₂ π) (hle₁ : J J₁) (hle₂ : J J₂) :
J₁ = J₂
theorem BoxIntegral.Prepartition.eq_of_le {ι : Type u_1} {I : } {J₁ : } {J₂ : } (π : ) (h₁ : J₁ π) (h₂ : J₂ π) (hle : J₁ J₂) :
J₁ = J₂
theorem BoxIntegral.Prepartition.le_of_mem {ι : Type u_1} {I : } {J : } (π : ) (hJ : J π) :
J I
theorem BoxIntegral.Prepartition.lower_le_lower {ι : Type u_1} {I : } {J : } (π : ) (hJ : J π) :
I.lower J.lower
theorem BoxIntegral.Prepartition.upper_le_upper {ι : Type u_1} {I : } {J : } (π : ) (hJ : J π) :
J.upper I.upper
theorem BoxIntegral.Prepartition.injective_boxes {ι : Type u_1} {I : } :
Function.Injective BoxIntegral.Prepartition.boxes
theorem BoxIntegral.Prepartition.ext {ι : Type u_1} {I : } {π₁ : } {π₂ : } (h : ∀ (J : ), J π₁ J π₂) :
π₁ = π₂
@[simp]
theorem BoxIntegral.Prepartition.single_boxes {ι : Type u_1} (I : ) (J : ) (h : J I) :
().boxes = {J}
def BoxIntegral.Prepartition.single {ι : Type u_1} (I : ) (J : ) (h : J I) :

The singleton prepartition {J}, J ≤ I.

Equations
• = { boxes := {J}, le_of_mem' := , pairwiseDisjoint := }
Instances For
@[simp]
theorem BoxIntegral.Prepartition.mem_single {ι : Type u_1} {I : } {J : } {J' : } (h : J I) :
J' J' = J
instance BoxIntegral.Prepartition.instLE {ι : Type u_1} {I : } :

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

Equations
• BoxIntegral.Prepartition.instLE = { le := fun (π π' : ) => ∀ ⦃I_1 : ⦄, I_1 πI'π', I_1 I' }
instance BoxIntegral.Prepartition.partialOrder {ι : Type u_1} {I : } :
Equations
• BoxIntegral.Prepartition.partialOrder =
instance BoxIntegral.Prepartition.instOrderTop {ι : Type u_1} {I : } :
Equations
• BoxIntegral.Prepartition.instOrderTop =
instance BoxIntegral.Prepartition.instOrderBot {ι : Type u_1} {I : } :
Equations
• BoxIntegral.Prepartition.instOrderBot =
instance BoxIntegral.Prepartition.instInhabited {ι : Type u_1} {I : } :
Equations
• BoxIntegral.Prepartition.instInhabited = { default := }
theorem BoxIntegral.Prepartition.le_def {ι : Type u_1} {I : } {π₁ : } {π₂ : } :
π₁ π₂ Jπ₁, J'π₂, J J'
@[simp]
theorem BoxIntegral.Prepartition.mem_top {ι : Type u_1} {I : } {J : } :
J J = I
@[simp]
theorem BoxIntegral.Prepartition.top_boxes {ι : Type u_1} {I : } :
.boxes = {I}
@[simp]
theorem BoxIntegral.Prepartition.not_mem_bot {ι : Type u_1} {I : } {J : } :
J
@[simp]
theorem BoxIntegral.Prepartition.bot_boxes {ι : Type u_1} {I : } :
.boxes =
theorem BoxIntegral.Prepartition.injOn_setOf_mem_Icc_setOf_lower_eq {ι : Type u_1} {I : } (π : ) (x : ι) :
Set.InjOn (fun (J : ) => {i : ι | J.lower i = x i}) {J : | J π x BoxIntegral.Box.Icc 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 BoxIntegral.Prepartition.card_filter_mem_Icc_le {ι : Type u_1} {I : } (π : ) [] (x : ι) :
(Finset.filter (fun (J : ) => x BoxIntegral.Box.Icc J) π.boxes).card

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

def BoxIntegral.Prepartition.iUnion {ι : Type u_1} {I : } (π : ) :
Set (ι)

Given a prepartition π : BoxIntegral.Prepartition I, π.iUnion is the part of I covered by the boxes of π.

Equations
• π.iUnion = Jπ, J
Instances For
theorem BoxIntegral.Prepartition.iUnion_def {ι : Type u_1} {I : } (π : ) :
π.iUnion = Jπ, J
theorem BoxIntegral.Prepartition.iUnion_def' {ι : Type u_1} {I : } (π : ) :
π.iUnion = Jπ.boxes, J
@[simp]
theorem BoxIntegral.Prepartition.mem_iUnion {ι : Type u_1} {I : } (π : ) {x : ι} :
x π.iUnion Jπ, x J
@[simp]
theorem BoxIntegral.Prepartition.iUnion_single {ι : Type u_1} {I : } {J : } (h : J I) :
().iUnion = J
@[simp]
theorem BoxIntegral.Prepartition.iUnion_top {ι : Type u_1} {I : } :
.iUnion = I
@[simp]
theorem BoxIntegral.Prepartition.iUnion_eq_empty {ι : Type u_1} {I : } {π₁ : } :
π₁.iUnion = π₁ =
@[simp]
theorem BoxIntegral.Prepartition.iUnion_bot {ι : Type u_1} {I : } :
.iUnion =
theorem BoxIntegral.Prepartition.subset_iUnion {ι : Type u_1} {I : } {J : } (π : ) (h : J π) :
J π.iUnion
theorem BoxIntegral.Prepartition.iUnion_subset {ι : Type u_1} {I : } (π : ) :
π.iUnion I
theorem BoxIntegral.Prepartition.iUnion_mono {ι : Type u_1} {I : } {π₁ : } {π₂ : } (h : π₁ π₂) :
π₁.iUnion π₂.iUnion
theorem BoxIntegral.Prepartition.disjoint_boxes_of_disjoint_iUnion {ι : Type u_1} {I : } {π₁ : } {π₂ : } (h : Disjoint π₁.iUnion π₂.iUnion) :
Disjoint π₁.boxes π₂.boxes
theorem BoxIntegral.Prepartition.le_iff_nonempty_imp_le_and_iUnion_subset {ι : Type u_1} {I : } {π₁ : } {π₂ : } :
π₁ π₂ (Jπ₁, J'π₂, (J J').NonemptyJ J') π₁.iUnion π₂.iUnion
theorem BoxIntegral.Prepartition.eq_of_boxes_subset_iUnion_superset {ι : Type u_1} {I : } {π₁ : } {π₂ : } (h₁ : π₁.boxes π₂.boxes) (h₂ : π₂.iUnion π₁.iUnion) :
π₁ = π₂
@[simp]
theorem BoxIntegral.Prepartition.biUnion_boxes {ι : Type u_1} {I : } (π : ) (πi : (J : ) → ) :
(π.biUnion πi).boxes = π.boxes.biUnion fun (J : ) => (πi J).boxes
def BoxIntegral.Prepartition.biUnion {ι : Type u_1} {I : } (π : ) (π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
• π.biUnion πi = { boxes := π.boxes.biUnion fun (J : ) => (πi J).boxes, le_of_mem' := , pairwiseDisjoint := }
Instances For
@[simp]
theorem BoxIntegral.Prepartition.mem_biUnion {ι : Type u_1} {I : } {J : } (π : ) {πi : (J : ) → } :
J π.biUnion πi J'π, J πi J'
theorem BoxIntegral.Prepartition.biUnion_le {ι : Type u_1} {I : } (π : ) (πi : (J : ) → ) :
π.biUnion πi π
@[simp]
theorem BoxIntegral.Prepartition.biUnion_top {ι : Type u_1} {I : } (π : ) :
(π.biUnion fun (x : ) => ) = π
theorem BoxIntegral.Prepartition.biUnion_congr {ι : Type u_1} {I : } {π₁ : } {π₂ : } {πi₁ : (J : ) → } {πi₂ : (J : ) → } (h : π₁ = π₂) (hi : Jπ₁, πi₁ J = πi₂ J) :
π₁.biUnion πi₁ = π₂.biUnion πi₂
theorem BoxIntegral.Prepartition.biUnion_congr_of_le {ι : Type u_1} {I : } {π₁ : } {π₂ : } {πi₁ : (J : ) → } {πi₂ : (J : ) → } (h : π₁ = π₂) (hi : JI, πi₁ J = πi₂ J) :
π₁.biUnion πi₁ = π₂.biUnion πi₂
@[simp]
theorem BoxIntegral.Prepartition.iUnion_biUnion {ι : Type u_1} {I : } (π : ) (πi : (J : ) → ) :
(π.biUnion πi).iUnion = Jπ, (πi J).iUnion
@[simp]
theorem BoxIntegral.Prepartition.sum_biUnion_boxes {ι : Type u_1} {I : } {M : Type u_2} [] (π : ) (πi : (J : ) → ) (f : M) :
Jπ.boxes.biUnion fun (J : ) => (πi J).boxes, f J = Jπ.boxes, J'(πi J).boxes, f J'
def BoxIntegral.Prepartition.biUnionIndex {ι : Type u_1} {I : } (π : ) (πi : (J : ) → ) (J : ) :

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

Equations
• π.biUnionIndex πi J = if hJ : J π.biUnion πi then .choose else I
Instances For
theorem BoxIntegral.Prepartition.biUnionIndex_mem {ι : Type u_1} {I : } {J : } (π : ) {πi : (J : ) → } (hJ : J π.biUnion πi) :
π.biUnionIndex πi J π
theorem BoxIntegral.Prepartition.biUnionIndex_le {ι : Type u_1} {I : } (π : ) (πi : (J : ) → ) (J : ) :
π.biUnionIndex πi J I
theorem BoxIntegral.Prepartition.mem_biUnionIndex {ι : Type u_1} {I : } {J : } (π : ) {πi : (J : ) → } (hJ : J π.biUnion πi) :
J πi (π.biUnionIndex πi J)
theorem BoxIntegral.Prepartition.le_biUnionIndex {ι : Type u_1} {I : } {J : } (π : ) {πi : (J : ) → } (hJ : J π.biUnion πi) :
J π.biUnionIndex πi J
theorem BoxIntegral.Prepartition.biUnionIndex_of_mem {ι : Type u_1} {I : } {J : } (π : ) {πi : (J : ) → } (hJ : J π) {J' : } (hJ' : J' πi J) :
π.biUnionIndex πi J' = J

Uniqueness property of BoxIntegral.Prepartition.biUnionIndex.

theorem BoxIntegral.Prepartition.biUnion_assoc {ι : Type u_1} {I : } (π : ) (πi : (J : ) → ) (πi' : (J : ) → ) :
(π.biUnion fun (J : ) => (πi J).biUnion (πi' J)) = (π.biUnion πi).biUnion fun (J : ) => πi' (π.biUnionIndex πi J) J
def BoxIntegral.Prepartition.ofWithBot {ι : Type u_1} {I : } (boxes : Finset ()) (le_of_mem : Jboxes, J I) (pairwise_disjoint : (boxes).Pairwise Disjoint) :

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

Equations
Instances For
@[simp]
theorem BoxIntegral.Prepartition.mem_ofWithBot {ι : Type u_1} {I : } {J : } {boxes : Finset ()} {h₁ : Jboxes, J I} {h₂ : (boxes).Pairwise Disjoint} :
J BoxIntegral.Prepartition.ofWithBot boxes h₁ h₂ J boxes
@[simp]
theorem BoxIntegral.Prepartition.iUnion_ofWithBot {ι : Type u_1} {I : } (boxes : Finset ()) (le_of_mem : Jboxes, J I) (pairwise_disjoint : (boxes).Pairwise Disjoint) :
(BoxIntegral.Prepartition.ofWithBot boxes le_of_mem pairwise_disjoint).iUnion = Jboxes, J
theorem BoxIntegral.Prepartition.ofWithBot_le {ι : Type u_1} {I : } (π : ) {boxes : Finset ()} {le_of_mem : Jboxes, J I} {pairwise_disjoint : (boxes).Pairwise Disjoint} (H : Jboxes, J J'π, J J') :
BoxIntegral.Prepartition.ofWithBot boxes le_of_mem pairwise_disjoint π
theorem BoxIntegral.Prepartition.le_ofWithBot {ι : Type u_1} {I : } (π : ) {boxes : Finset ()} {le_of_mem : Jboxes, J I} {pairwise_disjoint : (boxes).Pairwise Disjoint} (H : Jπ, J'boxes, J J') :
π BoxIntegral.Prepartition.ofWithBot boxes le_of_mem pairwise_disjoint
theorem BoxIntegral.Prepartition.ofWithBot_mono {ι : Type u_1} {I : } {boxes₁ : Finset ()} {le_of_mem₁ : Jboxes₁, J I} {pairwise_disjoint₁ : (boxes₁).Pairwise Disjoint} {boxes₂ : Finset ()} {le_of_mem₂ : Jboxes₂, J I} {pairwise_disjoint₂ : (boxes₂).Pairwise Disjoint} (H : Jboxes₁, J J'boxes₂, J J') :
BoxIntegral.Prepartition.ofWithBot boxes₁ le_of_mem₁ pairwise_disjoint₁ BoxIntegral.Prepartition.ofWithBot boxes₂ le_of_mem₂ pairwise_disjoint₂
theorem BoxIntegral.Prepartition.sum_ofWithBot {ι : Type u_1} {I : } {M : Type u_2} [] (boxes : Finset ()) (le_of_mem : Jboxes, J I) (pairwise_disjoint : (boxes).Pairwise Disjoint) (f : M) :
J(BoxIntegral.Prepartition.ofWithBot boxes le_of_mem pairwise_disjoint).boxes, f J = Jboxes, Option.elim' 0 f J
def BoxIntegral.Prepartition.restrict {ι : Type u_1} {I : } (π : ) (J : ) :

Restrict a prepartition to a box.

Equations
Instances For
@[simp]
theorem BoxIntegral.Prepartition.mem_restrict {ι : Type u_1} {I : } {J : } {J₁ : } (π : ) :
J₁ π.restrict J J'π, J₁ = J J'
theorem BoxIntegral.Prepartition.mem_restrict' {ι : Type u_1} {I : } {J : } {J₁ : } (π : ) :
J₁ π.restrict J J'π, J₁ = J J'
theorem BoxIntegral.Prepartition.restrict_mono {ι : Type u_1} {I : } {J : } {π₁ : } {π₂ : } (Hle : π₁ π₂) :
π₁.restrict J π₂.restrict J
theorem BoxIntegral.Prepartition.monotone_restrict {ι : Type u_1} {I : } {J : } :
Monotone fun (π : ) => π.restrict J
theorem BoxIntegral.Prepartition.restrict_boxes_of_le {ι : Type u_1} {I : } {J : } (π : ) (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 BoxIntegral.Prepartition.restrict_self {ι : Type u_1} {I : } (π : ) :
π.restrict I = π
@[simp]
theorem BoxIntegral.Prepartition.iUnion_restrict {ι : Type u_1} {I : } {J : } (π : ) :
(π.restrict J).iUnion = J π.iUnion
@[simp]
theorem BoxIntegral.Prepartition.restrict_biUnion {ι : Type u_1} {I : } {J : } (π : ) (πi : (J : ) → ) (hJ : J π) :
(π.biUnion πi).restrict J = πi J
theorem BoxIntegral.Prepartition.biUnion_le_iff {ι : Type u_1} {I : } (π : ) {πi : (J : ) → } {π' : } :
π.biUnion πi π' Jπ, πi J π'.restrict J
theorem BoxIntegral.Prepartition.le_biUnion_iff {ι : Type u_1} {I : } (π : ) {πi : (J : ) → } {π' : } :
π' π.biUnion πi π' π Jπ, π'.restrict J πi J
instance BoxIntegral.Prepartition.inf {ι : Type u_1} {I : } :
Equations
• BoxIntegral.Prepartition.inf = { inf := fun (π₁ π₂ : ) => π₁.biUnion fun (J : ) => π₂.restrict J }
theorem BoxIntegral.Prepartition.inf_def {ι : Type u_1} {I : } (π₁ : ) (π₂ : ) :
π₁ π₂ = π₁.biUnion fun (J : ) => π₂.restrict J
@[simp]
theorem BoxIntegral.Prepartition.mem_inf {ι : Type u_1} {I : } {J : } {π₁ : } {π₂ : } :
J π₁ π₂ J₁π₁, J₂π₂, J = J₁ J₂
@[simp]
theorem BoxIntegral.Prepartition.iUnion_inf {ι : Type u_1} {I : } (π₁ : ) (π₂ : ) :
(π₁ π₂).iUnion = π₁.iUnion π₂.iUnion
Equations
• BoxIntegral.Prepartition.instSemilatticeInf = let __src := BoxIntegral.Prepartition.inf; let __src_1 := BoxIntegral.Prepartition.partialOrder;
@[simp]
theorem BoxIntegral.Prepartition.filter_boxes {ι : Type u_1} {I : } (π : ) (p : ) :
(π.filter p).boxes = Finset.filter p π.boxes
def BoxIntegral.Prepartition.filter {ι : Type u_1} {I : } (π : ) (p : ) :

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

Equations
• π.filter p = { boxes := Finset.filter p π.boxes, le_of_mem' := , pairwiseDisjoint := }
Instances For
@[simp]
theorem BoxIntegral.Prepartition.mem_filter {ι : Type u_1} {I : } {J : } (π : ) {p : } :
J π.filter p J π p J
theorem BoxIntegral.Prepartition.filter_le {ι : Type u_1} {I : } (π : ) (p : ) :
π.filter p π
theorem BoxIntegral.Prepartition.filter_of_true {ι : Type u_1} {I : } (π : ) {p : } (hp : Jπ, p J) :
π.filter p = π
@[simp]
theorem BoxIntegral.Prepartition.filter_true {ι : Type u_1} {I : } (π : ) :
(π.filter fun (x : ) => True) = π
@[simp]
theorem BoxIntegral.Prepartition.iUnion_filter_not {ι : Type u_1} {I : } (π : ) (p : ) :
(π.filter fun (J : ) => ¬p J).iUnion = π.iUnion \ (π.filter p).iUnion
theorem BoxIntegral.Prepartition.sum_fiberwise {ι : Type u_1} {I : } {α : Type u_2} {M : Type u_3} [] (π : ) (f : α) (g : M) :
yFinset.image f π.boxes, J(π.filter fun (J : ) => f J = y).boxes, g J = Jπ.boxes, g J
@[simp]
theorem BoxIntegral.Prepartition.disjUnion_boxes {ι : Type u_1} {I : } (π₁ : ) (π₂ : ) (h : Disjoint π₁.iUnion π₂.iUnion) :
(π₁.disjUnion π₂ h).boxes = π₁.boxes π₂.boxes
def BoxIntegral.Prepartition.disjUnion {ι : Type u_1} {I : } (π₁ : ) (π₂ : ) (h : Disjoint π₁.iUnion π₂.iUnion) :

Union of two disjoint prepartitions.

Equations
• π₁.disjUnion π₂ h = { boxes := π₁.boxes π₂.boxes, le_of_mem' := , pairwiseDisjoint := }
Instances For
@[simp]
theorem BoxIntegral.Prepartition.mem_disjUnion {ι : Type u_1} {I : } {J : } {π₁ : } {π₂ : } (H : Disjoint π₁.iUnion π₂.iUnion) :
J π₁.disjUnion π₂ H J π₁ J π₂
@[simp]
theorem BoxIntegral.Prepartition.iUnion_disjUnion {ι : Type u_1} {I : } {π₁ : } {π₂ : } (h : Disjoint π₁.iUnion π₂.iUnion) :
(π₁.disjUnion π₂ h).iUnion = π₁.iUnion π₂.iUnion
@[simp]
theorem BoxIntegral.Prepartition.sum_disj_union_boxes {ι : Type u_1} {I : } {π₁ : } {π₂ : } {M : Type u_2} [] (h : Disjoint π₁.iUnion π₂.iUnion) (f : M) :
Jπ₁.boxes π₂.boxes, f J = Jπ₁.boxes, f J + Jπ₂.boxes, f J
def BoxIntegral.Prepartition.distortion {ι : Type u_1} {I : } (π : ) [] :

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

Equations
• π.distortion = π.boxes.sup BoxIntegral.Box.distortion
Instances For
theorem BoxIntegral.Prepartition.distortion_le_of_mem {ι : Type u_1} {I : } {J : } (π : ) [] (h : J π) :
J.distortion π.distortion
theorem BoxIntegral.Prepartition.distortion_le_iff {ι : Type u_1} {I : } (π : ) [] {c : NNReal} :
π.distortion c Jπ, J.distortion c
theorem BoxIntegral.Prepartition.distortion_biUnion {ι : Type u_1} {I : } [] (π : ) (πi : (J : ) → ) :
(π.biUnion πi).distortion = π.boxes.sup fun (J : ) => (πi J).distortion
@[simp]
theorem BoxIntegral.Prepartition.distortion_disjUnion {ι : Type u_1} {I : } {π₁ : } {π₂ : } [] (h : Disjoint π₁.iUnion π₂.iUnion) :
(π₁.disjUnion π₂ h).distortion = max π₁.distortion π₂.distortion
theorem BoxIntegral.Prepartition.distortion_of_const {ι : Type u_1} {I : } (π : ) [] {c : NNReal} (h₁ : π.boxes.Nonempty) (h₂ : Jπ, J.distortion = c) :
π.distortion = c
@[simp]
theorem BoxIntegral.Prepartition.distortion_top {ι : Type u_1} [] (I : ) :
.distortion = I.distortion
@[simp]
theorem BoxIntegral.Prepartition.distortion_bot {ι : Type u_1} [] (I : ) :
.distortion = 0
def BoxIntegral.Prepartition.IsPartition {ι : Type u_1} {I : } (π : ) :

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

Equations
• π.IsPartition = xI, Jπ, x J
Instances For
theorem BoxIntegral.Prepartition.isPartition_iff_iUnion_eq {ι : Type u_1} {I : } {π : } :
π.IsPartition π.iUnion = I
@[simp]
theorem BoxIntegral.Prepartition.isPartition_single_iff {ι : Type u_1} {I : } {J : } (h : J I) :
().IsPartition J = I
theorem BoxIntegral.Prepartition.isPartitionTop {ι : Type u_1} (I : ) :
.IsPartition
theorem BoxIntegral.Prepartition.IsPartition.iUnion_eq {ι : Type u_1} {I : } {π : } (h : π.IsPartition) :
π.iUnion = I
theorem BoxIntegral.Prepartition.IsPartition.iUnion_subset {ι : Type u_1} {I : } {π : } (h : π.IsPartition) (π₁ : ) :
π₁.iUnion π.iUnion
theorem BoxIntegral.Prepartition.IsPartition.existsUnique {ι : Type u_1} {I : } {π : } {x : ι} (h : π.IsPartition) (hx : x I) :
∃! J : , J π x J
theorem BoxIntegral.Prepartition.IsPartition.nonempty_boxes {ι : Type u_1} {I : } {π : } (h : π.IsPartition) :
π.boxes.Nonempty
theorem BoxIntegral.Prepartition.IsPartition.eq_of_boxes_subset {ι : Type u_1} {I : } {π₁ : } {π₂ : } (h₁ : π₁.IsPartition) (h₂ : π₁.boxes π₂.boxes) :
π₁ = π₂
theorem BoxIntegral.Prepartition.IsPartition.le_iff {ι : Type u_1} {I : } {π₁ : } {π₂ : } (h : π₂.IsPartition) :
π₁ π₂ Jπ₁, J'π₂, (J J').NonemptyJ J'
theorem BoxIntegral.Prepartition.IsPartition.biUnion {ι : Type u_1} {I : } {π : } {πi : (J : ) → } (h : π.IsPartition) (hi : Jπ, (πi J).IsPartition) :
(π.biUnion πi).IsPartition
theorem BoxIntegral.Prepartition.IsPartition.restrict {ι : Type u_1} {I : } {J : } {π : } (h : π.IsPartition) (hJ : J I) :
(π.restrict J).IsPartition
theorem BoxIntegral.Prepartition.IsPartition.inf {ι : Type u_1} {I : } {π₁ : } {π₂ : } (h₁ : π₁.IsPartition) (h₂ : π₂.IsPartition) :
(π₁ π₂).IsPartition
theorem BoxIntegral.Prepartition.iUnion_biUnion_partition {ι : Type u_1} {I : } (π : ) {πi : (J : ) → } (h : Jπ, (πi J).IsPartition) :
(π.biUnion πi).iUnion = π.iUnion
theorem BoxIntegral.Prepartition.isPartitionDisjUnionOfEqDiff {ι : Type u_1} {I : } {π₁ : } {π₂ : } (h : π₂.iUnion = I \ π₁.iUnion) :
(π₁.disjUnion π₂ ).IsPartition