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
- each box
J ∈ boxesis a subbox ofI; - the boxes are pairwise disjoint as sets in
ℝⁿ.
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:
box_integral.partition.bUnion: split each box of a partition into smaller boxes;box_integral.partition.restrict: restrict a partition to a smaller box.
We also define a semilattice_inf structure on box_integral.partition I for all
I : box_integral.box ι.
Tags #
rectangular box, partition
- boxes : finset (box_integral.box ι)
- le_of_mem' : ∀ (J : box_integral.box ι), J ∈ self.boxes → J ≤ I
- pairwise_disjoint : ↑(self.boxes).pairwise (disjoint on coe)
A prepartition of I : box_integral.box ι is a finite set of pairwise disjoint subboxes of
I.
Instances for box_integral.prepartition
- box_integral.prepartition.has_sizeof_inst
- box_integral.prepartition.has_mem
- box_integral.prepartition.has_le
- box_integral.prepartition.partial_order
- box_integral.prepartition.order_top
- box_integral.prepartition.order_bot
- box_integral.prepartition.inhabited
- box_integral.prepartition.has_inf
- box_integral.prepartition.semilattice_inf
@[protected, instance]
Equations
- box_integral.prepartition.has_mem = {mem := λ (J : box_integral.box ι) (π : box_integral.prepartition I), J ∈ π.boxes}
@[simp]
theorem
box_integral.prepartition.mem_boxes
{ι : Type u_1}
{I J : box_integral.box ι}
(π : box_integral.prepartition I) :
@[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₂) :
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 ∈ π₂) :
π₁ = π₂
The singleton prepartition {J}, J ≤ I.
Equations
- box_integral.prepartition.single I J h = {boxes := {J}, le_of_mem' := _, pairwise_disjoint := _}
@[simp]
theorem
box_integral.prepartition.single_boxes
{ι : Type u_1}
(I J : box_integral.box ι)
(h : J ≤ I) :
(box_integral.prepartition.single I J h).boxes = {J}
@[simp]
theorem
box_integral.prepartition.mem_single
{ι : Type u_1}
{I J J' : box_integral.box ι}
(h : J ≤ I) :
J' ∈ box_integral.prepartition.single I J h ↔ J' = J
@[protected, instance]
We say that π ≤ π' if each box of π is a subbox of some box of π'.
Equations
- box_integral.prepartition.has_le = {le := λ (π π' : box_integral.prepartition I), ∀ ⦃I_1 : box_integral.box ι⦄, I_1 ∈ π → (∃ (I' : box_integral.box ι) (H : I' ∈ π'), I_1 ≤ I')}
@[protected, instance]
Equations
- box_integral.prepartition.partial_order = {le := has_le.le box_integral.prepartition.has_le, lt := preorder.lt._default has_le.le, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _}
@[protected, instance]
Equations
- box_integral.prepartition.order_top = {top := box_integral.prepartition.single I I box_integral.prepartition.order_top._proof_1, le_top := _}
@[protected, instance]
Equations
- box_integral.prepartition.order_bot = {bot := {boxes := ∅, le_of_mem' := _, pairwise_disjoint := _}, bot_le := _}
@[protected, instance]
Equations
theorem
box_integral.prepartition.le_def
{ι : Type u_1}
{I : box_integral.box ι}
{π₁ π₂ : box_integral.prepartition I} :
@[simp]
@[simp]
@[simp]
@[simp]
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.
theorem
box_integral.prepartition.card_filter_mem_Icc_le
{ι : Type u_1}
{I : box_integral.box ι}
(π : box_integral.prepartition I)
[fintype ι]
(x : ι → ℝ) :
(finset.filter (λ (J : box_integral.box ι), x ∈ ⇑box_integral.box.Icc J) π.boxes).card ≤ 2 ^ fintype.card ι
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) :
Given a prepartition π : box_integral.prepartition I, π.Union is the part of I covered by
the boxes of π.
theorem
box_integral.prepartition.Union_def
{ι : Type u_1}
{I : box_integral.box ι}
(π : box_integral.prepartition I) :
theorem
box_integral.prepartition.Union_def'
{ι : Type u_1}
{I : box_integral.box ι}
(π : box_integral.prepartition I) :
@[simp]
theorem
box_integral.prepartition.mem_Union
{ι : Type u_1}
{I : box_integral.box ι}
(π : box_integral.prepartition I)
{x : ι → ℝ} :
@[simp]
theorem
box_integral.prepartition.Union_single
{ι : Type u_1}
{I J : box_integral.box ι}
(h : J ≤ I) :
(box_integral.prepartition.single I J h).Union = ↑J
@[simp]
@[simp]
theorem
box_integral.prepartition.Union_eq_empty
{ι : Type u_1}
{I : box_integral.box ι}
{π₁ : box_integral.prepartition I} :
@[simp]
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_subset
{ι : Type u_1}
{I : box_integral.box ι}
(π : box_integral.prepartition I) :
theorem
box_integral.prepartition.Union_mono
{ι : Type u_1}
{I : box_integral.box ι}
{π₁ π₂ : box_integral.prepartition I}
(h : π₁ ≤ π₂) :
theorem
box_integral.prepartition.disjoint_boxes_of_disjoint_Union
{ι : Type u_1}
{I : box_integral.box ι}
{π₁ π₂ : box_integral.prepartition I}
(h : disjoint π₁.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} :
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) :
π₁ = π₂
noncomputable
def
box_integral.prepartition.bUnion
{ι : Type u_1}
{I : box_integral.box ι}
(π : box_integral.prepartition I)
(πi : Π (J : box_integral.box ι), box_integral.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
- π.bUnion πi = {boxes := π.boxes.bUnion (λ (J : box_integral.box ι), (πi J).boxes), le_of_mem' := _, pairwise_disjoint := _}
@[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) :
@[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} :
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) :
@[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) :
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) :
@[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) :
@[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'))
noncomputable
def
box_integral.prepartition.bUnion_index
{ι : Type u_1}
{I : box_integral.box ι}
(π : box_integral.prepartition I)
(πi : Π (J : box_integral.box ι), box_integral.prepartition J)
(J : box_integral.box ι) :
Given a box J ∈ π.bUnion πi, returns the box J' ∈ π such that J ∈ πi J'.
For J ∉ π.bUnion πi, returns I.
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.bUnion_index_le
{ι : Type u_1}
{I : box_integral.box ι}
(π : box_integral.prepartition I)
(πi : Π (J : box_integral.box ι), box_integral.prepartition J)
(J : box_integral.box ι) :
π.bUnion_index πi J ≤ I
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 ∈ 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
- box_integral.prepartition.of_with_bot boxes le_of_mem pairwise_disjoint = {boxes := ⇑finset.erase_none boxes, le_of_mem' := _, pairwise_disjoint := _}
@[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} :
J ∈ box_integral.prepartition.of_with_bot boxes h₁ h₂ ↔ ↑J ∈ boxes
@[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)
noncomputable
def
box_integral.prepartition.restrict
{ι : Type u_1}
{I : box_integral.box ι}
(π : box_integral.prepartition I)
(J : box_integral.box ι) :
Restrict a prepartition to a box.
Equations
- π.restrict J = box_integral.prepartition.of_with_bot (finset.image (λ (J' : box_integral.box ι), ↑J ⊓ ↑J') π.boxes) _ _
@[simp]
theorem
box_integral.prepartition.mem_restrict
{ι : Type u_1}
{I J J₁ : box_integral.box ι}
(π : box_integral.prepartition I) :
theorem
box_integral.prepartition.mem_restrict'
{ι : Type u_1}
{I J J₁ : box_integral.box ι}
(π : box_integral.prepartition I) :
theorem
box_integral.prepartition.restrict_mono
{ι : Type u_1}
{I J : box_integral.box ι}
{π₁ π₂ : box_integral.prepartition I}
(Hle : π₁ ≤ π₂) :
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) :
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) :
@[simp]
theorem
box_integral.prepartition.Union_restrict
{ι : Type u_1}
{I J : box_integral.box ι}
(π : box_integral.prepartition I) :
@[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 ∈ π) :
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} :
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} :
@[protected, instance]
Equations
- box_integral.prepartition.has_inf = {inf := λ (π₁ π₂ : box_integral.prepartition I), π₁.bUnion (λ (J : box_integral.box ι), π₂.restrict J)}
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} :
@[simp]
theorem
box_integral.prepartition.Union_inf
{ι : Type u_1}
{I : box_integral.box ι}
(π₁ π₂ : box_integral.prepartition I) :
@[protected, instance]
noncomputable
def
box_integral.prepartition.semilattice_inf
{ι : Type u_1}
{I : box_integral.box ι} :
Equations
- box_integral.prepartition.semilattice_inf = {inf := has_inf.inf box_integral.prepartition.has_inf, le := partial_order.le box_integral.prepartition.partial_order, lt := partial_order.lt box_integral.prepartition.partial_order, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, inf_le_left := _, inf_le_right := _, le_inf := _}
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
- π.filter p = {boxes := finset.filter p π.boxes, le_of_mem' := _, pairwise_disjoint := _}
@[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} :
theorem
box_integral.prepartition.filter_le
{ι : Type u_1}
{I : box_integral.box ι}
(π : box_integral.prepartition I)
(p : box_integral.box ι → Prop) :
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) :
@[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) :
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
- π₁.disj_union π₂ h = {boxes := π₁.boxes ∪ π₂.boxes, le_of_mem' := _, pairwise_disjoint := _}
@[simp]
theorem
box_integral.prepartition.disj_union_boxes
{ι : Type u_1}
{I : box_integral.box ι}
(π₁ π₂ : box_integral.prepartition I)
(h : disjoint π₁.Union π₂.Union) :
@[simp]
theorem
box_integral.prepartition.mem_disj_union
{ι : Type u_1}
{I J : box_integral.box ι}
{π₁ π₂ : box_integral.prepartition I}
(H : disjoint π₁.Union π₂.Union) :
@[simp]
theorem
box_integral.prepartition.Union_disj_union
{ι : Type u_1}
{I : box_integral.box ι}
{π₁ π₂ : box_integral.prepartition I}
(h : disjoint π₁.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_of_mem
{ι : Type u_1}
{I J : box_integral.box ι}
(π : box_integral.prepartition I)
[fintype ι]
(h : J ∈ π) :
J.distortion ≤ π.distortion
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
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 = linear_order.max π₁.distortion π₂.distortion
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) :
π.distortion = c
@[simp]
theorem
box_integral.prepartition.distortion_top
{ι : Type u_1}
[fintype ι]
(I : box_integral.box ι) :
@[simp]
theorem
box_integral.prepartition.distortion_bot
{ι : Type u_1}
[fintype ι]
(I : box_integral.box ι) :
⊥.distortion = 0
def
box_integral.prepartition.is_partition
{ι : Type u_1}
{I : box_integral.box ι}
(π : box_integral.prepartition I) :
Prop
A prepartition π of I is a partition if the boxes of π cover the whole I.
theorem
box_integral.prepartition.is_partition_iff_Union_eq
{ι : Type u_1}
{I : box_integral.box ι}
{π : box_integral.prepartition I} :
π.is_partition ↔ π.Union = ↑I
@[simp]
theorem
box_integral.prepartition.is_partition_single_iff
{ι : Type u_1}
{I J : box_integral.box ι}
(h : J ≤ I) :
(box_integral.prepartition.single I J h).is_partition ↔ J = I
theorem
box_integral.prepartition.is_partition.Union_eq
{ι : Type u_1}
{I : box_integral.box ι}
{π : box_integral.prepartition I}
(h : π.is_partition) :
theorem
box_integral.prepartition.is_partition.Union_subset
{ι : Type u_1}
{I : box_integral.box ι}
{π : box_integral.prepartition I}
(h : π.is_partition)
(π₁ : box_integral.prepartition I) :
@[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.nonempty_boxes
{ι : Type u_1}
{I : box_integral.box ι}
{π : box_integral.prepartition I}
(h : π.is_partition) :
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) :
@[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) :
(π.restrict J).is_partition
@[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) :
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