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 ofI
; - 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
- boxes : Finset (BoxIntegral.Box ι)
- le_of_mem' : ∀ (J : BoxIntegral.Box ι), J ∈ s.boxes → J ≤ I
- pairwiseDisjoint : Set.Pairwise (↑s.boxes) (Disjoint on BoxIntegral.Box.toSet)
A prepartition of I : BoxIntegral.Box ι
is a finite set of pairwise disjoint subboxes of
I
.
Instances For
The singleton prepartition {J}
, J ≤ I
.
Instances For
We say that π ≤ π'
if each box of π
is a subbox of some box of π'
.
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 ι
.
Given a prepartition π : BoxIntegral.Prepartition I
, π.iUnion
is the part of I
covered by
the boxes of π
.
Instances For
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.
Instances For
Given a box J ∈ π.biUnion πi
, returns the box J' ∈ π
such that J ∈ πi J'
.
For J ∉ π.biUnion πi
, returns I
.
Instances For
Uniqueness property of BoxIntegral.Prepartition.biUnionIndex
.
Create a BoxIntegral.Prepartition
from a collection of possibly empty boxes by filtering out
the empty one if it exists.
Instances For
Restrict a prepartition to a box.
Instances For
Restricting to a larger box does not change the set of boxes. We cannot claim equality of prepartitions because they have different types.
The prepartition with boxes {J ∈ π | p J}
.
Instances For
Union of two disjoint prepartitions.
Instances For
The distortion of a prepartition is the maximum of the distortions of the boxes of this prepartition.
Instances For
A prepartition π
of I
is a partition if the boxes of π
cover the whole I
.