Documentation

Mathlib.Analysis.BoxIntegral.Partition.Basic

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

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:

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 : Box ι) :
Type u_1

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

@[simp]
theorem BoxIntegral.Prepartition.mem_boxes {ι : Type u_1} {I J : Box ι} (π : Prepartition I) :
J π.boxes J π
@[simp]
theorem BoxIntegral.Prepartition.mem_mk {ι : Type u_1} {I J : Box ι} {s : Finset (Box ι)} {h₁ : Js, J I} {h₂ : (↑s).Pairwise (Function.onFun Disjoint 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₂ : Box ι} (π : Prepartition I) (h₁ : J₁ π) (h₂ : J₂ π) (h : J₁ J₂) :
Disjoint J₁ J₂
theorem BoxIntegral.Prepartition.eq_of_mem_of_mem {ι : Type u_1} {I J₁ J₂ : Box ι} (π : Prepartition I) {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₂ : Box ι} (π : Prepartition I) (h₁ : J₁ π) (h₂ : J₂ π) (hle₁ : J J₁) (hle₂ : J J₂) :
J₁ = J₂
theorem BoxIntegral.Prepartition.eq_of_le {ι : Type u_1} {I J₁ J₂ : Box ι} (π : Prepartition I) (h₁ : J₁ π) (h₂ : J₂ π) (hle : J₁ J₂) :
J₁ = J₂
theorem BoxIntegral.Prepartition.le_of_mem {ι : Type u_1} {I J : Box ι} (π : Prepartition I) (hJ : J π) :
J I
theorem BoxIntegral.Prepartition.lower_le_lower {ι : Type u_1} {I J : Box ι} (π : Prepartition I) (hJ : J π) :
theorem BoxIntegral.Prepartition.upper_le_upper {ι : Type u_1} {I J : Box ι} (π : Prepartition I) (hJ : J π) :
theorem BoxIntegral.Prepartition.ext {ι : Type u_1} {I : Box ι} {π₁ π₂ : Prepartition I} (h : ∀ (J : Box ι), J π₁ J π₂) :
π₁ = π₂
theorem BoxIntegral.Prepartition.ext_iff {ι : Type u_1} {I : Box ι} {π₁ π₂ : Prepartition I} :
π₁ = π₂ ∀ (J : Box ι), J π₁ J π₂
def BoxIntegral.Prepartition.single {ι : Type u_1} (I J : Box ι) (h : J I) :

The singleton prepartition {J}, J ≤ I.

Equations
@[simp]
theorem BoxIntegral.Prepartition.single_boxes {ι : Type u_1} (I J : Box ι) (h : J I) :
(single I J h).boxes = {J}
@[simp]
theorem BoxIntegral.Prepartition.mem_single {ι : Type u_1} {I J J' : Box ι} (h : J I) :
J' single I J h J' = J
instance BoxIntegral.Prepartition.instLE {ι : Type u_1} {I : Box ι} :

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

Equations
Equations
Equations
theorem BoxIntegral.Prepartition.le_def {ι : Type u_1} {I : Box ι} {π₁ π₂ : Prepartition I} :
π₁ π₂ Jπ₁, J'π₂, J J'
@[simp]
theorem BoxIntegral.Prepartition.mem_top {ι : Type u_1} {I J : Box ι} :
J J = I
@[simp]
theorem BoxIntegral.Prepartition.top_boxes {ι : Type u_1} {I : Box ι} :
@[simp]
theorem BoxIntegral.Prepartition.notMem_bot {ι : Type u_1} {I J : Box ι} :
J
@[deprecated BoxIntegral.Prepartition.notMem_bot (since := "2025-05-23")]
theorem BoxIntegral.Prepartition.not_mem_bot {ι : Type u_1} {I J : Box ι} :
J

Alias of BoxIntegral.Prepartition.notMem_bot.

@[simp]
theorem BoxIntegral.Prepartition.injOn_setOf_mem_Icc_setOf_lower_eq {ι : Type u_1} {I : Box ι} (π : Prepartition I) (x : ι) :
Set.InjOn (fun (J : Box ι) => {i : ι | J.lower i = x i}) {J : Box ι | J π x 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 : Box ι} (π : Prepartition I) [Fintype ι] (x : ι) :
{Jπ.boxes | x Box.Icc J}.card 2 ^ Fintype.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 : Box ι} (π : Prepartition I) :
Set (ι)

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

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

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

Equations
theorem BoxIntegral.Prepartition.biUnionIndex_mem {ι : Type u_1} {I J : Box ι} (π : Prepartition I) {πi : (J : Box ι) → Prepartition J} (hJ : J π.biUnion πi) :
π.biUnionIndex πi J π
theorem BoxIntegral.Prepartition.biUnionIndex_le {ι : Type u_1} {I : Box ι} (π : Prepartition I) (πi : (J : Box ι) → Prepartition J) (J : Box ι) :
π.biUnionIndex πi J I
theorem BoxIntegral.Prepartition.mem_biUnionIndex {ι : Type u_1} {I J : Box ι} (π : Prepartition I) {πi : (J : Box ι) → Prepartition J} (hJ : J π.biUnion πi) :
J πi (π.biUnionIndex πi J)
theorem BoxIntegral.Prepartition.le_biUnionIndex {ι : Type u_1} {I J : Box ι} (π : Prepartition I) {πi : (J : Box ι) → Prepartition J} (hJ : J π.biUnion πi) :
J π.biUnionIndex πi J
theorem BoxIntegral.Prepartition.biUnionIndex_of_mem {ι : Type u_1} {I J : Box ι} (π : Prepartition I) {πi : (J : Box ι) → Prepartition J} (hJ : J π) {J' : Box ι} (hJ' : J' πi J) :
π.biUnionIndex πi J' = J

Uniqueness property of BoxIntegral.Prepartition.biUnionIndex.

theorem BoxIntegral.Prepartition.biUnion_assoc {ι : Type u_1} {I : Box ι} (π : Prepartition I) (πi : (J : Box ι) → Prepartition J) (πi' : Box ι(J : Box ι) → Prepartition J) :
(π.biUnion fun (J : Box ι) => (πi J).biUnion (πi' J)) = (π.biUnion πi).biUnion fun (J : Box ι) => πi' (π.biUnionIndex πi J) J
def BoxIntegral.Prepartition.ofWithBot {ι : Type u_1} {I : Box ι} (boxes : Finset (WithBot (Box ι))) (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
@[simp]
theorem BoxIntegral.Prepartition.mem_ofWithBot {ι : Type u_1} {I J : Box ι} {boxes : Finset (WithBot (Box ι))} {h₁ : Jboxes, J I} {h₂ : (↑boxes).Pairwise Disjoint} :
J ofWithBot boxes h₁ h₂ J boxes
@[simp]
theorem BoxIntegral.Prepartition.iUnion_ofWithBot {ι : Type u_1} {I : Box ι} (boxes : Finset (WithBot (Box ι))) (le_of_mem : Jboxes, J I) (pairwise_disjoint : (↑boxes).Pairwise Disjoint) :
(ofWithBot boxes le_of_mem pairwise_disjoint).iUnion = Jboxes, J
theorem BoxIntegral.Prepartition.ofWithBot_le {ι : Type u_1} {I : Box ι} (π : Prepartition I) {boxes : Finset (WithBot (Box ι))} {le_of_mem : Jboxes, J I} {pairwise_disjoint : (↑boxes).Pairwise Disjoint} (H : Jboxes, J J'π, J J') :
ofWithBot boxes le_of_mem pairwise_disjoint π
theorem BoxIntegral.Prepartition.le_ofWithBot {ι : Type u_1} {I : Box ι} (π : Prepartition I) {boxes : Finset (WithBot (Box ι))} {le_of_mem : Jboxes, J I} {pairwise_disjoint : (↑boxes).Pairwise Disjoint} (H : Jπ, J'boxes, J J') :
π ofWithBot boxes le_of_mem pairwise_disjoint
theorem BoxIntegral.Prepartition.ofWithBot_mono {ι : Type u_1} {I : Box ι} {boxes₁ : Finset (WithBot (Box ι))} {le_of_mem₁ : Jboxes₁, J I} {pairwise_disjoint₁ : (↑boxes₁).Pairwise Disjoint} {boxes₂ : Finset (WithBot (Box ι))} {le_of_mem₂ : Jboxes₂, J I} {pairwise_disjoint₂ : (↑boxes₂).Pairwise Disjoint} (H : Jboxes₁, J J'boxes₂, J J') :
ofWithBot boxes₁ le_of_mem₁ pairwise_disjoint₁ ofWithBot boxes₂ le_of_mem₂ pairwise_disjoint₂
theorem BoxIntegral.Prepartition.sum_ofWithBot {ι : Type u_1} {I : Box ι} {M : Type u_2} [AddCommMonoid M] (boxes : Finset (WithBot (Box ι))) (le_of_mem : Jboxes, J I) (pairwise_disjoint : (↑boxes).Pairwise Disjoint) (f : Box ιM) :
J(ofWithBot boxes le_of_mem pairwise_disjoint).boxes, f J = Jboxes, Option.elim' 0 f J
def BoxIntegral.Prepartition.restrict {ι : Type u_1} {I : Box ι} (π : Prepartition I) (J : Box ι) :

Restrict a prepartition to a box.

Equations
@[simp]
theorem BoxIntegral.Prepartition.mem_restrict {ι : Type u_1} {I J J₁ : Box ι} (π : Prepartition I) :
J₁ π.restrict J J'π, J₁ = JJ'
theorem BoxIntegral.Prepartition.mem_restrict' {ι : Type u_1} {I J J₁ : Box ι} (π : Prepartition I) :
J₁ π.restrict J J'π, J₁ = J J'
theorem BoxIntegral.Prepartition.restrict_mono {ι : Type u_1} {I J : Box ι} {π₁ π₂ : Prepartition I} (Hle : π₁ π₂) :
π₁.restrict J π₂.restrict J
theorem BoxIntegral.Prepartition.monotone_restrict {ι : Type u_1} {I J : Box ι} :
Monotone fun (π : Prepartition I) => π.restrict J
theorem BoxIntegral.Prepartition.restrict_boxes_of_le {ι : Type u_1} {I J : Box ι} (π : Prepartition I) (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 : Box ι} (π : Prepartition I) :
π.restrict I = π
@[simp]
theorem BoxIntegral.Prepartition.iUnion_restrict {ι : Type u_1} {I J : Box ι} (π : Prepartition I) :
(π.restrict J).iUnion = J π.iUnion
@[simp]
theorem BoxIntegral.Prepartition.restrict_biUnion {ι : Type u_1} {I J : Box ι} (π : Prepartition I) (πi : (J : Box ι) → Prepartition J) (hJ : J π) :
(π.biUnion πi).restrict J = πi J
theorem BoxIntegral.Prepartition.biUnion_le_iff {ι : Type u_1} {I : Box ι} (π : Prepartition I) {πi : (J : Box ι) → Prepartition J} {π' : Prepartition I} :
π.biUnion πi π' Jπ, πi J π'.restrict J
theorem BoxIntegral.Prepartition.le_biUnion_iff {ι : Type u_1} {I : Box ι} (π : Prepartition I) {πi : (J : Box ι) → Prepartition J} {π' : Prepartition I} :
π' π.biUnion πi π' π Jπ, π'.restrict J πi J
Equations
  • One or more equations did not get rendered due to their size.
theorem BoxIntegral.Prepartition.inf_def {ι : Type u_1} {I : Box ι} (π₁ π₂ : Prepartition I) :
π₁π₂ = π₁.biUnion fun (J : Box ι) => π₂.restrict J
@[simp]
theorem BoxIntegral.Prepartition.mem_inf {ι : Type u_1} {I J : Box ι} {π₁ π₂ : Prepartition I} :
J π₁π₂ J₁π₁, J₂π₂, J = J₁J₂
@[simp]
theorem BoxIntegral.Prepartition.iUnion_inf {ι : Type u_1} {I : Box ι} (π₁ π₂ : Prepartition I) :
(π₁π₂).iUnion = π₁.iUnion π₂.iUnion
def BoxIntegral.Prepartition.filter {ι : Type u_1} {I : Box ι} (π : Prepartition I) (p : Box ιProp) :

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

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

Union of two disjoint prepartitions.

Equations
@[simp]
theorem BoxIntegral.Prepartition.disjUnion_boxes {ι : Type u_1} {I : Box ι} (π₁ π₂ : Prepartition I) (h : Disjoint π₁.iUnion π₂.iUnion) :
(π₁.disjUnion π₂ h).boxes = π₁.boxes π₂.boxes
@[simp]
theorem BoxIntegral.Prepartition.mem_disjUnion {ι : Type u_1} {I J : Box ι} {π₁ π₂ : Prepartition I} (H : Disjoint π₁.iUnion π₂.iUnion) :
J π₁.disjUnion π₂ H J π₁ J π₂
@[simp]
theorem BoxIntegral.Prepartition.iUnion_disjUnion {ι : Type u_1} {I : Box ι} {π₁ π₂ : Prepartition I} (h : Disjoint π₁.iUnion π₂.iUnion) :
(π₁.disjUnion π₂ h).iUnion = π₁.iUnion π₂.iUnion
@[simp]
theorem BoxIntegral.Prepartition.sum_disj_union_boxes {ι : Type u_1} {I : Box ι} {π₁ π₂ : Prepartition I} {M : Type u_2} [AddCommMonoid M] (h : Disjoint π₁.iUnion π₂.iUnion) (f : Box ιM) :
Jπ₁.boxes π₂.boxes, f J = Jπ₁.boxes, f J + Jπ₂.boxes, f J

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

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

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

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