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.

@[protected, instance]
Equations
@[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 «π») :
J «π».Union
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'
theorem box_integral.prepartition.bUnion_le {ι : Type u_1} {I : box_integral.box ι} (π : box_integral.prepartition I) (πi : Π (J : box_integral.box ι), box_integral.prepartition J) :
«π».bUnion πi «π»
@[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) :
∑ (J : box_integral.box ι) in «π».boxes.bUnion (λ (J : box_integral.box ι), (πi J).boxes), f J = ∑ (J : box_integral.box ι) in «π».boxes, ∑ (J' : box_integral.box ι) in (πi J).boxes, 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) :
∑ (J : box_integral.box ι) in (box_integral.prepartition.of_with_bot boxes le_of_mem pairwise_disjoint).boxes, f J = ∑ (J : with_bot (box_integral.box ι)) in boxes, 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.monotone_restrict {ι : Type u_1} {I J : box_integral.box ι} :
monotone (λ («π» : box_integral.prepartition I), «π».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]
theorem box_integral.prepartition.restrict_self {ι : Type u_1} {I : box_integral.box ι} (π : box_integral.prepartition I) :
«π».restrict I = «π»
@[simp]
theorem box_integral.prepartition.Union_restrict {ι : Type u_1} {I J : box_integral.box ι} (π : box_integral.prepartition I) :
(«π».restrict J).Union = J «π».Union
@[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) :
(«π».filter p).boxes = finset.filter p «π».boxes
@[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) :
∑ (y : α) in finset.image f «π».boxes, ∑ (J : box_integral.box ι) in («π».filter (λ (J : box_integral.box ι), f J = y)).boxes, g J = ∑ (J : box_integral.box ι) in «π».boxes, 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) :
∑ (J : box_integral.box ι) in π₁.boxes π₂.boxes, f J = ∑ (J : box_integral.box ι) in π₁.boxes, f J + ∑ (J : box_integral.box ι) in π₂.boxes, 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_of_mem {ι : Type u_1} {I J : box_integral.box ι} (π : box_integral.prepartition I) [fintype ι] (h : J «π») :
theorem box_integral.prepartition.distortion_le_iff {ι : Type u_1} {I : box_integral.box ι} (π : box_integral.prepartition I) [fintype ι] {c : ℝ≥0} :
«π».distortion c ∀ (J : box_integral.box ι), J «π»J.distortion c
theorem box_integral.prepartition.distortion_bUnion {ι : Type u_1} {I : box_integral.box ι} [fintype ι] (π : box_integral.prepartition I) (πi : Π (J : box_integral.box ι), box_integral.prepartition J) :
(«π».bUnion πi).distortion = «π».boxes.sup (λ (J : box_integral.box ι), (πi J).distortion)
@[simp]
theorem box_integral.prepartition.distortion_disj_union {ι : Type u_1} {I : box_integral.box ι} {π₁ π₂ : box_integral.prepartition I} [fintype ι] (h : disjoint π₁.Union π₂.Union) :
(π₁.disj_union π₂ h).distortion = max π₁.distortion π₂.distortion
theorem box_integral.prepartition.distortion_of_const {ι : Type u_1} {I : box_integral.box ι} (π : box_integral.prepartition I) [fintype ι] {c : ℝ≥0} (h₁ : «π».boxes.nonempty) (h₂ : ∀ (J : box_integral.box ι), J «π»J.distortion = c) :
«π».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) :
(«π».bUnion πi).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