mathlib documentation

analysis.box_integral.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 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]
theorem box_integral.prepartition.mem_boxes {ι : Type u_1} {I J : box_integral.box ι} (π : box_integral.prepartition I) :
J π.boxes J π
@[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 sJ 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
theorem box_integral.prepartition.lower_le_lower {ι : Type u_1} {I J : box_integral.box ι} (π : box_integral.prepartition I) (hJ : J π) :
theorem box_integral.prepartition.upper_le_upper {ι : Type u_1} {I J : box_integral.box ι} (π : box_integral.prepartition I) (hJ : J π) :
@[ext]
theorem box_integral.prepartition.ext {ι : Type u_1} {I : box_integral.box ι} {π₁ π₂ : box_integral.prepartition I} (h : ∀ (J : box_integral.box ι), 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) :
@[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]
theorem box_integral.prepartition.top_boxes {ι : Type u_1} {I : box_integral.box ι} :
.boxes = {I}
@[simp]
theorem box_integral.prepartition.not_mem_bot {ι : Type u_1} {I J : box_integral.box ι} :
@[simp]
theorem box_integral.prepartition.bot_boxes {ι : Type u_1} {I : box_integral.box ι} :
theorem box_integral.prepartition.inj_on_set_of_mem_Icc_set_of_lower_eq {ι : Type u_1} {I : box_integral.box ι} (π : box_integral.prepartition I) (x : ι → ) :
set.inj_on (λ (J : box_integral.box ι), {i : ι | J.lower i = x i}) {J : box_integral.box ι | J π x box_integral.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.

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 ι} (π : box_integral.prepartition I) :
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 ι} (π : box_integral.prepartition I) :
π.Union = ⋃ (J : box_integral.box ι) (H : J π), J
theorem box_integral.prepartition.Union_def' {ι : Type u_1} {I : box_integral.box ι} (π : box_integral.prepartition I) :
π.Union = ⋃ (J : box_integral.box ι) (H : J π.boxes), J
@[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_top {ι : Type u_1} {I : box_integral.box ι} :
@[simp]
theorem box_integral.prepartition.Union_eq_empty {ι : Type u_1} {I : box_integral.box ι} {π₁ : box_integral.prepartition I} :
π₁.Union = π₁ =
@[simp]
theorem box_integral.prepartition.Union_bot {ι : Type u_1} {I : box_integral.box ι} :
theorem box_integral.prepartition.subset_Union {ι : Type u_1} {I J : box_integral.box ι} (π : box_integral.prepartition I) (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.disjoint_boxes_of_disjoint_Union {ι : Type u_1} {I : box_integral.box ι} {π₁ π₂ : box_integral.prepartition I} (h : disjoint π₁.Union π₂.Union) :
disjoint π₁.boxes π₂.boxes
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').nonemptyJ 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]
theorem box_integral.prepartition.bUnion_boxes {ι : Type u_1} {I : box_integral.box ι} (π : box_integral.prepartition I) (πi : Π (J : box_integral.box ι), box_integral.prepartition J) :
(π.bUnion πi).boxes = π.boxes.bUnion (λ (J : box_integral.box ι), (πi J).boxes)
@[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_top {ι : Type u_1} {I : box_integral.box ι} (π : box_integral.prepartition I) :
π.bUnion (λ (_x : box_integral.box ι), ) = π
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.bUnion_index_mem {ι : 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) :
π.bUnion_index πi J π
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.le_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 π.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 boxesJ 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 boxesJ 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 boxesJ 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 boxesJ I} {pairwise_disjoint : boxes.pairwise disjoint} (H : ∀ (J : with_bot (box_integral.box ι)), J boxesJ (∃ (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 boxesJ 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 boxesJ 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 J 0 f)

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
theorem box_integral.prepartition.restrict_boxes_of_le {ι : Type u_1} {I J : box_integral.box ι} (π : box_integral.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]
@[simp]
@[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
theorem box_integral.prepartition.bUnion_le_iff {ι : Type u_1} {I : box_integral.box ι} (π : box_integral.prepartition I) {πi : Π (J : box_integral.box ι), box_integral.prepartition J} {π' : box_integral.prepartition I} :
π.bUnion πi π' ∀ (J : box_integral.box ι), J ππi J π'.restrict J
theorem box_integral.prepartition.le_bUnion_iff {ι : Type u_1} {I : box_integral.box ι} (π : box_integral.prepartition I) {πi : Π (J : box_integral.box ι), box_integral.prepartition J} {π' : box_integral.prepartition I} :
π' π.bUnion πi π' π ∀ (J : box_integral.box ι), 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 : 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
noncomputable def box_integral.prepartition.filter {ι : Type u_1} {I : box_integral.box ι} (π : box_integral.prepartition I) (p : box_integral.box ι → Prop) :

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

Equations
@[simp]
theorem box_integral.prepartition.filter_boxes {ι : Type u_1} {I : box_integral.box ι} (π : box_integral.prepartition I) (p : box_integral.box ι → Prop) :
@[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_le {ι : Type u_1} {I : box_integral.box ι} (π : box_integral.prepartition I) (p : box_integral.box ι → Prop) :
π.filter p π
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]
theorem box_integral.prepartition.filter_true {ι : Type u_1} {I : box_integral.box ι} (π : box_integral.prepartition I) :
π.filter (λ (_x : box_integral.box ι), true) = π
@[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)
noncomputable def box_integral.prepartition.distortion {ι : Type u_1} {I : box_integral.box ι} (π : box_integral.prepartition I) [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_iff {ι : Type u_1} {I : box_integral.box ι} (π : box_integral.prepartition I) [fintype ι] {c : nnreal} :
π.distortion c ∀ (J : box_integral.box ι), J πJ.distortion c
@[simp]
theorem box_integral.prepartition.distortion_disj_union {ι : Type u_1} {I : box_integral.box ι} {π₁ π₂ : box_integral.prepartition I} [fintype ι] (h : disjoint π₁.Union π₂.Union) :
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) :
@[simp]

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').nonemptyJ J'
@[protected]
theorem box_integral.prepartition.is_partition.bUnion {ι : Type u_1} {I : box_integral.box ι} {π : box_integral.prepartition I} {πi : Π (J : box_integral.box ι), box_integral.prepartition J} (h : π.is_partition) (hi : ∀ (J : box_integral.box ι), J π(πi J).is_partition) :
@[protected]
theorem box_integral.prepartition.is_partition.restrict {ι : Type u_1} {I J : box_integral.box ι} {π : box_integral.prepartition I} (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 ι} (π : box_integral.prepartition I) {πi : Π (J : box_integral.box ι), box_integral.prepartition J} (h : ∀ (J : box_integral.box ι), J π(πi J).is_partition) :
(π.bUnion πi).Union = π.Union
theorem box_integral.prepartition.is_partition_disj_union_of_eq_diff {ι : Type u_1} {I : box_integral.box ι} {π₁ π₂ : box_integral.prepartition I} (h : π₂.Union = I \ π₁.Union) :
(π₁.disj_union π₂ _).is_partition