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 (ι → ℝ) and Membership (ι → ℝ) (BoxIntegral.Box ι) as described above;
• PartialOrder and SemilatticeSup instances such that I ≤ J is equivalent to (I : Set (ι → ℝ)) ⊆ J;
• Lattice instances on WithBot (BoxIntegral.Box ι);
• BoxIntegral.Box.Icc: the closed box Set.Icc I.lower I.upper; defined as a bundled monotone map from Box ι to Set (ι → ℝ);
• BoxIntegral.Box.face I i : Box (Fin n): a hyperface of I : BoxIntegral.Box (Fin (n + 1));
• BoxIntegral.Box.distortion: the maximal ratio of two lengths of edges of a box; defined as the supremum of nndist 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

structure BoxIntegral.Box (ι : Type u_2) : Type u_2

A nontrivial rectangular box in ι → ℝ with corners lower and upper. Represents the product of half-open intervals (lower i, upper i].

• lower : ι → ℝ

  coordinates of the lower and upper corners of the box

• upper : ι → ℝ

  coordinates of the lower and upper corners of the box

• lower_lt_upper : ∀ (i : ι), self.lower i < self.upper i

  Each lower coordinate is less than its upper coordinate: i.e., the box is non-empty

@[simp]

theorem BoxIntegral.Box.lower_lt_upper {ι : Type u_2} (self : BoxIntegral.Box ι) (i : ι) : self.lower i < self.upper i

Each lower coordinate is less than its upper coordinate: i.e., the box is non-empty

instance BoxIntegral.Box.instInhabited {ι : Type u_1} : Inhabited (BoxIntegral.Box ι)

Equations

• BoxIntegral.Box.instInhabited = { default := { lower := 0, upper := 1, lower_lt_upper := ⋯ } }

theorem BoxIntegral.Box.lower_le_upper {ι : Type u_1} (I : BoxIntegral.Box ι) : I.lower ≤ I.upper

theorem BoxIntegral.Box.lower_ne_upper {ι : Type u_1} (I : BoxIntegral.Box ι) (i : ι) : I.lower i ≠ I.upper i

instance BoxIntegral.Box.instMembershipForallReal {ι : Type u_1} : Membership (ι → ℝ) (BoxIntegral.Box ι)

Equations

• BoxIntegral.Box.instMembershipForallReal = { mem := fun (x : ι → ℝ) (I : BoxIntegral.Box ι) => ∀ (i : ι), x i ∈ Set.Ioc (I.lower i) (I.upper i) }

def BoxIntegral.Box.toSet {ι : Type u_1} (I : BoxIntegral.Box ι) : Set (ι → ℝ)

The set of points in this box: this is the product of half-open intervals (lower i, upper i], where lower and upper are this box' corners.

Equations

• ↑I = {x : ι → ℝ | x ∈ I}

instance BoxIntegral.Box.instCoeTCSetForallReal {ι : Type u_1} : CoeTC (BoxIntegral.Box ι) (Set (ι → ℝ))

Equations

• BoxIntegral.Box.instCoeTCSetForallReal = { coe := BoxIntegral.Box.toSet }

@[simp]

theorem BoxIntegral.Box.mem_mk {ι : Type u_1} {l : ι → ℝ} {u : ι → ℝ} {x : ι → ℝ} {H : ∀ (i : ι), l i < u i} : x ∈ { lower := l, upper := u, lower_lt_upper := H } ↔ ∀ (i : ι), x i ∈ Set.Ioc (l i) (u i)

@[simp]

theorem BoxIntegral.Box.mem_coe {ι : Type u_1} (I : BoxIntegral.Box ι) {x : ι → ℝ} : x ∈ ↑I ↔ x ∈ I

theorem BoxIntegral.Box.mem_def {ι : Type u_1} (I : BoxIntegral.Box ι) {x : ι → ℝ} : x ∈ I ↔ ∀ (i : ι), x i ∈ Set.Ioc (I.lower i) (I.upper i)

theorem BoxIntegral.Box.mem_univ_Ioc {ι : Type u_1} {x : ι → ℝ} {I : BoxIntegral.Box ι} : (x ∈ Set.univ.pi fun (i : ι) => Set.Ioc (I.lower i) (I.upper i)) ↔ x ∈ I

theorem BoxIntegral.Box.coe_eq_pi {ι : Type u_1} (I : BoxIntegral.Box ι) : ↑I = Set.univ.pi fun (i : ι) => Set.Ioc (I.lower i) (I.upper i)

@[simp]

theorem BoxIntegral.Box.upper_mem {ι : Type u_1} (I : BoxIntegral.Box ι) : I.upper ∈ I

theorem BoxIntegral.Box.exists_mem {ι : Type u_1} (I : BoxIntegral.Box ι) : ∃ (x : ι → ℝ), x ∈ I

theorem BoxIntegral.Box.nonempty_coe {ι : Type u_1} (I : BoxIntegral.Box ι) : (↑I).Nonempty

@[simp]

theorem BoxIntegral.Box.coe_ne_empty {ι : Type u_1} (I : BoxIntegral.Box ι) : ↑I ≠ ∅

@[simp]

theorem BoxIntegral.Box.empty_ne_coe {ι : Type u_1} (I : BoxIntegral.Box ι) : ∅ ≠ ↑I

instance BoxIntegral.Box.instLE {ι : Type u_1} : LE (BoxIntegral.Box ι)

Equations

• BoxIntegral.Box.instLE = { le := fun (I J : BoxIntegral.Box ι) => ∀ ⦃x : ι → ℝ⦄, x ∈ I → x ∈ J }

theorem BoxIntegral.Box.le_def {ι : Type u_1} (I : BoxIntegral.Box ι) (J : BoxIntegral.Box ι) : I ≤ J ↔ ∀ x ∈ I, x ∈ J

theorem BoxIntegral.Box.le_TFAE {ι : Type u_1} (I : BoxIntegral.Box ι) (J : BoxIntegral.Box ι) : [I ≤ J, ↑I ⊆ ↑J, Set.Icc I.lower I.upper ⊆ Set.Icc J.lower J.upper, J.lower ≤ I.lower ∧ I.upper ≤ J.upper].TFAE

@[simp]

theorem BoxIntegral.Box.coe_subset_coe {ι : Type u_1} {I : BoxIntegral.Box ι} {J : BoxIntegral.Box ι} : ↑I ⊆ ↑J ↔ I ≤ J

theorem BoxIntegral.Box.le_iff_bounds {ι : Type u_1} {I : BoxIntegral.Box ι} {J : BoxIntegral.Box ι} : I ≤ J ↔ J.lower ≤ I.lower ∧ I.upper ≤ J.upper

theorem BoxIntegral.Box.injective_coe {ι : Type u_1} : Function.Injective BoxIntegral.Box.toSet

@[simp]

theorem BoxIntegral.Box.coe_inj {ι : Type u_1} {I : BoxIntegral.Box ι} {J : BoxIntegral.Box ι} : ↑I = ↑J ↔ I = J

theorem BoxIntegral.Box.ext {ι : Type u_1} {I : BoxIntegral.Box ι} {J : BoxIntegral.Box ι} (H : ∀ (x : ι → ℝ), x ∈ I ↔ x ∈ J) : I = J

theorem BoxIntegral.Box.ne_of_disjoint_coe {ι : Type u_1} {I : BoxIntegral.Box ι} {J : BoxIntegral.Box ι} (h : Disjoint ↑I ↑J) : I ≠ J

instance BoxIntegral.Box.instPartialOrder {ι : Type u_1} : PartialOrder (BoxIntegral.Box ι)

Equations

• BoxIntegral.Box.instPartialOrder = let __src := PartialOrder.lift BoxIntegral.Box.toSet ⋯; PartialOrder.mk ⋯

def BoxIntegral.Box.Icc {ι : Type u_1} : BoxIntegral.Box ι ↪o Set (ι → ℝ)

Closed box corresponding to I : BoxIntegral.Box ι.

Equations

• BoxIntegral.Box.Icc = OrderEmbedding.ofMapLEIff (fun (I : BoxIntegral.Box ι) => Set.Icc I.lower I.upper) ⋯

theorem BoxIntegral.Box.Icc_def {ι : Type u_1} {I : BoxIntegral.Box ι} : BoxIntegral.Box.Icc I = Set.Icc I.lower I.upper

@[simp]

theorem BoxIntegral.Box.upper_mem_Icc {ι : Type u_1} (I : BoxIntegral.Box ι) : I.upper ∈ BoxIntegral.Box.Icc I

@[simp]

theorem BoxIntegral.Box.lower_mem_Icc {ι : Type u_1} (I : BoxIntegral.Box ι) : I.lower ∈ BoxIntegral.Box.Icc I

theorem BoxIntegral.Box.isCompact_Icc {ι : Type u_1} (I : BoxIntegral.Box ι) : IsCompact (BoxIntegral.Box.Icc I)

theorem BoxIntegral.Box.Icc_eq_pi {ι : Type u_1} {I : BoxIntegral.Box ι} : BoxIntegral.Box.Icc I = Set.univ.pi fun (i : ι) => Set.Icc (I.lower i) (I.upper i)

theorem BoxIntegral.Box.le_iff_Icc {ι : Type u_1} {I : BoxIntegral.Box ι} {J : BoxIntegral.Box ι} : I ≤ J ↔ BoxIntegral.Box.Icc I ⊆ BoxIntegral.Box.Icc J

theorem BoxIntegral.Box.antitone_lower {ι : Type u_1} : Antitone fun (I : BoxIntegral.Box ι) => I.lower

theorem BoxIntegral.Box.monotone_upper {ι : Type u_1} : Monotone fun (I : BoxIntegral.Box ι) => I.upper

theorem BoxIntegral.Box.coe_subset_Icc {ι : Type u_1} {I : BoxIntegral.Box ι} : ↑I ⊆ BoxIntegral.Box.Icc I

Supremum of two boxes

instance BoxIntegral.Box.instSup {ι : Type u_1} : Sup (BoxIntegral.Box ι)

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.

Equations

• BoxIntegral.Box.instSup = { sup := fun (I J : BoxIntegral.Box ι) => { lower := I.lower ⊓ J.lower, upper := I.upper ⊔ J.upper, lower_lt_upper := ⋯ } }

instance BoxIntegral.Box.instSemilatticeSup {ι : Type u_1} : SemilatticeSup (BoxIntegral.Box ι)

Equations

• BoxIntegral.Box.instSemilatticeSup = let __src := inferInstance; let __src_1 := inferInstance; SemilatticeSup.mk ⋯ ⋯ ⋯

WithBot (Box ι)

In this section we define coercion from WithBot (Box ι) to Set (ι → ℝ) by sending ⊥ to ∅.

def BoxIntegral.Box.withBotToSet {ι : Type u_1} (o : WithBot (BoxIntegral.Box ι)) : Set (ι → ℝ)

The set underlying this box: ⊥ is mapped to ∅.

Equations

• ↑o = Option.elim o ∅ BoxIntegral.Box.toSet

instance BoxIntegral.Box.withBotCoe {ι : Type u_1} : CoeTC (WithBot (BoxIntegral.Box ι)) (Set (ι → ℝ))

Equations

• BoxIntegral.Box.withBotCoe = { coe := BoxIntegral.Box.withBotToSet }

@[simp]

theorem BoxIntegral.Box.coe_bot {ι : Type u_1} : ↑⊥ = ∅

@[simp]

theorem BoxIntegral.Box.coe_coe {ι : Type u_1} {I : BoxIntegral.Box ι} : ↑↑I = ↑I

theorem BoxIntegral.Box.isSome_iff {ι : Type u_1} {I : WithBot (BoxIntegral.Box ι)} : Option.isSome I = true ↔ (↑I).Nonempty

theorem BoxIntegral.Box.biUnion_coe_eq_coe {ι : Type u_1} (I : WithBot (BoxIntegral.Box ι)) : ⋃ (J : BoxIntegral.Box ι), ⋃ (_ : ↑J = I), ↑J = ↑I

@[simp]

theorem BoxIntegral.Box.withBotCoe_subset_iff {ι : Type u_1} {I : WithBot (BoxIntegral.Box ι)} {J : WithBot (BoxIntegral.Box ι)} : ↑I ⊆ ↑J ↔ I ≤ J

@[simp]

theorem BoxIntegral.Box.withBotCoe_inj {ι : Type u_1} {I : WithBot (BoxIntegral.Box ι)} {J : WithBot (BoxIntegral.Box ι)} : ↑I = ↑J ↔ I = J

def BoxIntegral.Box.mk' {ι : Type u_1} (l : ι → ℝ) (u : ι → ℝ) : WithBot (BoxIntegral.Box ι)

Make a WithBot (Box ι) from a pair of corners l u : ι → ℝ. If l i < u i for all i, then the result is ⟨l, u, _⟩ : Box ι, otherwise it is ⊥. In any case, the result interpreted as a set in ι → ℝ is the set {x : ι → ℝ | ∀ i, x i ∈ Ioc (l i) (u i)}.

Equations

• BoxIntegral.Box.mk' l u = if h : ∀ (i : ι), l i < u i then ↑{ lower := l, upper := u, lower_lt_upper := h } else ⊥

@[simp]

theorem BoxIntegral.Box.mk'_eq_bot {ι : Type u_1} {l : ι → ℝ} {u : ι → ℝ} : BoxIntegral.Box.mk' l u = ⊥ ↔ ∃ (i : ι), u i ≤ l i

@[simp]

theorem BoxIntegral.Box.mk'_eq_coe {ι : Type u_1} {I : BoxIntegral.Box ι} {l : ι → ℝ} {u : ι → ℝ} : BoxIntegral.Box.mk' l u = ↑I ↔ l = I.lower ∧ u = I.upper

@[simp]

theorem BoxIntegral.Box.coe_mk' {ι : Type u_1} (l : ι → ℝ) (u : ι → ℝ) : ↑(BoxIntegral.Box.mk' l u) = Set.univ.pi fun (i : ι) => Set.Ioc (l i) (u i)

instance BoxIntegral.Box.WithBot.inf {ι : Type u_1} : Inf (WithBot (BoxIntegral.Box ι))

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem BoxIntegral.Box.coe_inf {ι : Type u_1} (I : WithBot (BoxIntegral.Box ι)) (J : WithBot (BoxIntegral.Box ι)) : ↑(I ⊓ J) = ↑I ∩ ↑J

instance BoxIntegral.Box.instLatticeWithBot {ι : Type u_1} : Lattice (WithBot (BoxIntegral.Box ι))

Equations

• BoxIntegral.Box.instLatticeWithBot = let __src := WithBot.semilatticeSup; let __src_1 := BoxIntegral.Box.WithBot.inf; Lattice.mk ⋯ ⋯ ⋯

@[simp]

theorem BoxIntegral.Box.disjoint_withBotCoe {ι : Type u_1} {I : WithBot (BoxIntegral.Box ι)} {J : WithBot (BoxIntegral.Box ι)} : Disjoint ↑I ↑J ↔ Disjoint I J

theorem BoxIntegral.Box.disjoint_coe {ι : Type u_1} {I : BoxIntegral.Box ι} {J : BoxIntegral.Box ι} : Disjoint ↑I ↑J ↔ Disjoint ↑I ↑J

theorem BoxIntegral.Box.not_disjoint_coe_iff_nonempty_inter {ι : Type u_1} {I : BoxIntegral.Box ι} {J : BoxIntegral.Box ι} : ¬Disjoint ↑I ↑J ↔ (↑I ∩ ↑J).Nonempty

Hyperface of a box in ℝⁿ⁺¹ = Fin (n + 1) → ℝ

@[simp]

theorem BoxIntegral.Box.face_upper {n : ℕ} (I : BoxIntegral.Box (Fin (n + 1))) (i : Fin (n + 1)) : ∀ (a : Fin n), (I.face i).upper a = I.upper (i.succAbove a)

@[simp]

theorem BoxIntegral.Box.face_lower {n : ℕ} (I : BoxIntegral.Box (Fin (n + 1))) (i : Fin (n + 1)) : ∀ (a : Fin n), (I.face i).lower a = I.lower (i.succAbove a)

def BoxIntegral.Box.face {n : ℕ} (I : BoxIntegral.Box (Fin (n + 1))) (i : Fin (n + 1)) : BoxIntegral.Box (Fin n)

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.

Equations

• I.face i = { lower := I.lower ∘ i.succAbove, upper := I.upper ∘ i.succAbove, lower_lt_upper := ⋯ }

@[simp]

theorem BoxIntegral.Box.face_mk {n : ℕ} (l : Fin (n + 1) → ℝ) (u : Fin (n + 1) → ℝ) (h : ∀ (i : Fin (n + 1)), l i < u i) (i : Fin (n + 1)) : { lower := l, upper := u, lower_lt_upper := h }.face i = { lower := l ∘ i.succAbove, upper := u ∘ i.succAbove, lower_lt_upper := ⋯ }

theorem BoxIntegral.Box.face_mono {n : ℕ} {I : BoxIntegral.Box (Fin (n + 1))} {J : BoxIntegral.Box (Fin (n + 1))} (h : I ≤ J) (i : Fin (n + 1)) : I.face i ≤ J.face i

theorem BoxIntegral.Box.monotone_face {n : ℕ} (i : Fin (n + 1)) : Monotone fun (I : BoxIntegral.Box (Fin (n + 1))) => I.face i

theorem BoxIntegral.Box.mapsTo_insertNth_face_Icc {n : ℕ} (I : BoxIntegral.Box (Fin (n + 1))) {i : Fin (n + 1)} {x : ℝ} (hx : x ∈ Set.Icc (I.lower i) (I.upper i)) : Set.MapsTo (i.insertNth x) (BoxIntegral.Box.Icc (I.face i)) (BoxIntegral.Box.Icc I)

theorem BoxIntegral.Box.mapsTo_insertNth_face {n : ℕ} (I : BoxIntegral.Box (Fin (n + 1))) {i : Fin (n + 1)} {x : ℝ} (hx : x ∈ Set.Ioc (I.lower i) (I.upper i)) : Set.MapsTo (i.insertNth x) ↑(I.face i) ↑I

theorem BoxIntegral.Box.continuousOn_face_Icc {X : Type u_2} [TopologicalSpace X] {n : ℕ} {f : (Fin (n + 1) → ℝ) → X} {I : BoxIntegral.Box (Fin (n + 1))} (h : ContinuousOn f (BoxIntegral.Box.Icc I)) {i : Fin (n + 1)} {x : ℝ} (hx : x ∈ Set.Icc (I.lower i) (I.upper i)) : ContinuousOn (f ∘ i.insertNth x) (BoxIntegral.Box.Icc (I.face i))

Covering of the interior of a box by a monotone sequence of smaller boxes

def BoxIntegral.Box.Ioo {ι : Type u_1} : BoxIntegral.Box ι →o Set (ι → ℝ)

The interior of a box.

Equations

• BoxIntegral.Box.Ioo = { toFun := fun (I : BoxIntegral.Box ι) => Set.univ.pi fun (i : ι) => Set.Ioo (I.lower i) (I.upper i), monotone' := ⋯ }

theorem BoxIntegral.Box.Ioo_subset_coe {ι : Type u_1} (I : BoxIntegral.Box ι) : BoxIntegral.Box.Ioo I ⊆ ↑I

theorem BoxIntegral.Box.Ioo_subset_Icc {ι : Type u_1} (I : BoxIntegral.Box ι) : BoxIntegral.Box.Ioo I ⊆ BoxIntegral.Box.Icc I

theorem BoxIntegral.Box.iUnion_Ioo_of_tendsto {ι : Type u_1} [Finite ι] {I : BoxIntegral.Box ι} {J : ℕ → BoxIntegral.Box ι} (hJ : Monotone J) (hl : Filter.Tendsto (BoxIntegral.Box.lower ∘ J) Filter.atTop (nhds I.lower)) (hu : Filter.Tendsto (BoxIntegral.Box.upper ∘ J) Filter.atTop (nhds I.upper)) : ⋃ (n : ℕ), BoxIntegral.Box.Ioo (J n) = BoxIntegral.Box.Ioo I

theorem BoxIntegral.Box.exists_seq_mono_tendsto {ι : Type u_1} (I : BoxIntegral.Box ι) : ∃ (J : ℕ →o BoxIntegral.Box ι), (∀ (n : ℕ), BoxIntegral.Box.Icc (J n) ⊆ BoxIntegral.Box.Ioo I) ∧ Filter.Tendsto (BoxIntegral.Box.lower ∘ ⇑J) Filter.atTop (nhds I.lower) ∧ Filter.Tendsto (BoxIntegral.Box.upper ∘ ⇑J) Filter.atTop (nhds I.upper)

def BoxIntegral.Box.distortion {ι : Type u_1} [Fintype ι] (I : BoxIntegral.Box ι) : NNReal

The distortion of a box I is the maximum of the ratios of the lengths of its edges. It is defined as the maximum of the ratios nndist I.lower I.upper / nndist (I.lower i) (I.upper i).

Equations

• I.distortion = Finset.univ.sup fun (i : ι) => nndist I.lower I.upper / nndist (I.lower i) (I.upper i)

theorem BoxIntegral.Box.distortion_eq_of_sub_eq_div {ι : Type u_1} [Fintype ι] {I : BoxIntegral.Box ι} {J : BoxIntegral.Box ι} {r : ℝ} (h : ∀ (i : ι), I.upper i - I.lower i = (J.upper i - J.lower i) / r) : I.distortion = J.distortion

theorem BoxIntegral.Box.nndist_le_distortion_mul {ι : Type u_1} [Fintype ι] (I : BoxIntegral.Box ι) (i : ι) : nndist I.lower I.upper ≤ I.distortion * nndist (I.lower i) (I.upper i)

theorem BoxIntegral.Box.dist_le_distortion_mul {ι : Type u_1} [Fintype ι] (I : BoxIntegral.Box ι) (i : ι) : dist I.lower I.upper ≤ ↑I.distortion * (I.upper i - I.lower i)

theorem BoxIntegral.Box.diam_Icc_le_of_distortion_le {ι : Type u_1} [Fintype ι] (I : BoxIntegral.Box ι) (i : ι) {c : NNReal} (h : I.distortion ≤ c) : Metric.diam (BoxIntegral.Box.Icc I) ≤ ↑c * (I.upper i - I.lower i)