Rectangular boxes in ℝⁿ
#
In this file we define rectangular boxes in ℝⁿ
. As usual, we represent ℝⁿ
as the type of
functions ι → ℝ
(usually ι = Fin n
for some n
). When we need to interpret a box [l, u]
as a
set, we use the product {x | ∀ i, l i < x i ∧ x i ≤ u i}
of half-open intervals (l i, u i]
. We
exclude l i
because this way boxes of a partition are disjoint as sets in ℝⁿ
.
Currently, the only use cases for these constructions are the definitions of Riemann-style integrals (Riemann, Henstock-Kurzweil, McShane).
Main definitions #
We use the same structure BoxIntegral.Box
both for ambient boxes and for elements of a partition.
Each box is stored as two points lower upper : ι → ℝ
and a proof of ∀ i, lower i < upper i
. We
define instances Membership (ι → ℝ) (Box ι)
and CoeTC (Box ι) (Set <| ι → ℝ)
so that each box is
interpreted as the set {x | ∀ i, x i ∈ Set.Ioc (I.lower i) (I.upper i)}
. This way boxes of a
partition are pairwise disjoint and their union is exactly the original box.
We require boxes to be nonempty, because this way coercion to sets is injective. The empty box can
be represented as ⊥ : WithBot (BoxIntegral.Box ι)
.
We define the following operations on boxes:
- coercion to
Set (ι → ℝ)
andMembership (ι → ℝ) (BoxIntegral.Box ι)
as described above; PartialOrder
andSemilatticeSup
instances such thatI ≤ J
is equivalent to(I : Set (ι → ℝ)) ⊆ J
;Lattice
instances onWithBot (BoxIntegral.Box ι)
;BoxIntegral.Box.Icc
: the closed boxSet.Icc I.lower I.upper
; defined as a bundled monotone map fromBox ι
toSet (ι → ℝ)
;BoxIntegral.Box.face I i : Box (Fin n)
: a hyperface ofI : BoxIntegral.Box (Fin (n + 1))
;BoxIntegral.Box.distortion
: the maximal ratio of two lengths of edges of a box; defined as the supremum ofnndist I.lower I.upper / nndist (I.lower i) (I.upper i)
.
We also provide a convenience constructor BoxIntegral.Box.mk' (l u : ι → ℝ) : WithBot (Box ι)
that returns the box ⟨l, u, _⟩
if it is nonempty and ⊥
otherwise.
Tags #
rectangular box
Rectangular box: definition and partial order #
- lower : ι → ℝ
- upper : ι → ℝ
- lower_lt_upper : ∀ (i : ι), BoxIntegral.Box.lower s i < BoxIntegral.Box.upper s i
A nontrivial rectangular box in ι → ℝ
with corners lower
and upper
. Represents the product
of half-open intervals (lower i, upper i]
.
Instances For
Closed box corresponding to I : BoxIntegral.Box ι
.
Instances For
Supremum of two boxes #
I ⊔ J
is the least box that includes both I
and J
. Since ↑I ∪ ↑J
is usually not a box,
↑(I ⊔ J)
is larger than ↑I ∪ ↑J
.
WithBot (Box ι)
#
In this section we define coercion from WithBot (Box ι)
to Set (ι → ℝ)
by sending ⊥
to ∅
.
Instances For
Face of a box in ℝⁿ⁺¹ = Fin (n + 1) → ℝ
: the box in ℝⁿ = Fin n → ℝ
with corners at
I.lower ∘ Fin.succAbove i
and I.upper ∘ Fin.succAbove i
.
Instances For
Covering of the interior of a box by a monotone sequence of smaller boxes #
The interior of a box.