mathlib3 documentation

analysis.box_integral.box.basic

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 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 box_integral.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 has_mem (ι → ℝ) (box ι) and has_coe_t (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 ⊥ : with_bot (box_integral.box ι).

We define the following operations on boxes:

coercion to set (ι → ℝ) and has_mem (ι → ℝ) (box_integral.box ι) as described above;
partial_order and semilattice_sup instances such that I ≤ J is equivalent to (I : set (ι → ℝ)) ⊆ J;
lattice instances on with_bot (box_integral.box ι);
box_integral.box.Icc: the closed box set.Icc I.lower I.upper; defined as a bundled monotone map from box ι to set (ι → ℝ);
box_integral.box.face I i : box (fin n): a hyperface of I : box_integral.box (fin (n + 1));
box_integral.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 box_integral.box.mk' (l u : ι → ℝ) : with_bot (box ι) that returns the box ⟨l, u, _⟩ if it is nonempty and ⊥ otherwise.

Tags #

rectangular box

Rectangular box: definition and partial order #

structure box_integral.box (ι : Type u_2) :

Type u_2

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

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

Instances for box_integral.box

box_integral.box.has_sizeof_inst
box_integral.box.inhabited
box_integral.box.has_mem
box_integral.box.set.has_coe_t
box_integral.box.has_le
box_integral.box.partial_order
box_integral.box.has_sup
box_integral.box.semilattice_sup
box_integral.prepartition.has_mem
box_integral.tagged_prepartition.has_mem

@[protected, instance]

def box_integral.box.inhabited {ι : Type u_1} :

inhabited (box_integral.box ι)

Equations

box_integral.box.inhabited = {default := {lower := 0, upper := 1, lower_lt_upper := _}}

theorem box_integral.box.lower_le_upper {ι : Type u_1} (I : box_integral.box ι) :

I.lower ≤ I.upper

theorem box_integral.box.lower_ne_upper {ι : Type u_1} (I : box_integral.box ι) (i : ι) :

I.lower i ≠ I.upper i

@[protected, instance]

def box_integral.box.has_mem {ι : Type u_1} :

has_mem (ι → ℝ) (box_integral.box ι)

Equations

box_integral.box.has_mem = {mem := λ (x : ι → ℝ) (I : box_integral.box ι), ∀ (i : ι), x i ∈ set.Ioc (I.lower i) (I.upper i)}

@[protected, instance]

def box_integral.box.set.has_coe_t {ι : Type u_1} :

has_coe_t (box_integral.box ι) (set (ι → ℝ))

Equations

box_integral.box.set.has_coe_t = {coe := λ (I : box_integral.box ι), {x : ι → ℝ | x ∈ I}}

@[simp]

theorem box_integral.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, norm_cast]

theorem box_integral.box.mem_coe {ι : Type u_1} (I : box_integral.box ι) {x : ι → ℝ} :

x ∈ ↑I ↔ x ∈ I

theorem box_integral.box.mem_def {ι : Type u_1} (I : box_integral.box ι) {x : ι → ℝ} :

x ∈ I ↔ ∀ (i : ι), x i ∈ set.Ioc (I.lower i) (I.upper i)

theorem box_integral.box.mem_univ_Ioc {ι : Type u_1} {x : ι → ℝ} {I : box_integral.box ι} :

x ∈ set.univ.pi (λ (i : ι), set.Ioc (I.lower i) (I.upper i)) ↔ x ∈ I

theorem box_integral.box.coe_eq_pi {ι : Type u_1} (I : box_integral.box ι) :

↑I = set.univ.pi (λ (i : ι), set.Ioc (I.lower i) (I.upper i))

@[simp]

theorem box_integral.box.upper_mem {ι : Type u_1} (I : box_integral.box ι) :

theorem box_integral.box.exists_mem {ι : Type u_1} (I : box_integral.box ι) :

∃ (x : ι → ℝ), x ∈ I

theorem box_integral.box.nonempty_coe {ι : Type u_1} (I : box_integral.box ι) :

@[simp]

theorem box_integral.box.coe_ne_empty {ι : Type u_1} (I : box_integral.box ι) :

@[simp]

theorem box_integral.box.empty_ne_coe {ι : Type u_1} (I : box_integral.box ι) :

@[protected, instance]

def box_integral.box.has_le {ι : Type u_1} :

has_le (box_integral.box ι)

Equations

box_integral.box.has_le = {le := λ (I J : box_integral.box ι), ∀ ⦃x : ι → ℝ⦄, x ∈ I → x ∈ J}

theorem box_integral.box.le_def {ι : Type u_1} (I J : box_integral.box ι) :

I ≤ J ↔ ∀ (x : ι → ℝ), x ∈ I → x ∈ J

theorem box_integral.box.le_tfae {ι : Type u_1} (I J : box_integral.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, norm_cast]

theorem box_integral.box.coe_subset_coe {ι : Type u_1} {I J : box_integral.box ι} :

↑I ⊆ ↑J ↔ I ≤ J

theorem box_integral.box.le_iff_bounds {ι : Type u_1} {I J : box_integral.box ι} :

I ≤ J ↔ J.lower ≤ I.lower ∧ I.upper ≤ J.upper

theorem box_integral.box.injective_coe {ι : Type u_1} :

function.injective coe

@[simp, norm_cast]

theorem box_integral.box.coe_inj {ι : Type u_1} {I J : box_integral.box ι} :

↑I = ↑J ↔ I = J

@[ext]

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

I = J

theorem box_integral.box.ne_of_disjoint_coe {ι : Type u_1} {I J : box_integral.box ι} (h : disjoint ↑I ↑J) :

I ≠ J

@[protected, instance]

def box_integral.box.partial_order {ι : Type u_1} :

partial_order (box_integral.box ι)

Equations

box_integral.box.partial_order = {le := has_le.le box_integral.box.has_le, lt := partial_order.lt (partial_order.lift coe box_integral.box.injective_coe), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _}

@[protected]

def box_integral.box.Icc {ι : Type u_1} :

box_integral.box ι ↪o set (ι → ℝ)

Closed box corresponding to I : box_integral.box ι.

Equations

box_integral.box.Icc = order_embedding.of_map_le_iff (λ (I : box_integral.box ι), set.Icc I.lower I.upper) box_integral.box.Icc._proof_1

theorem box_integral.box.Icc_def {ι : Type u_1} {I : box_integral.box ι} :

⇑box_integral.box.Icc I = set.Icc I.lower I.upper

@[simp]

theorem box_integral.box.upper_mem_Icc {ι : Type u_1} (I : box_integral.box ι) :

I.upper ∈ ⇑box_integral.box.Icc I

@[simp]

theorem box_integral.box.lower_mem_Icc {ι : Type u_1} (I : box_integral.box ι) :

I.lower ∈ ⇑box_integral.box.Icc I

@[protected]

theorem box_integral.box.is_compact_Icc {ι : Type u_1} (I : box_integral.box ι) :

is_compact (⇑box_integral.box.Icc I)

theorem box_integral.box.Icc_eq_pi {ι : Type u_1} {I : box_integral.box ι} :

⇑box_integral.box.Icc I = set.univ.pi (λ (i : ι), set.Icc (I.lower i) (I.upper i))

theorem box_integral.box.le_iff_Icc {ι : Type u_1} {I J : box_integral.box ι} :

I ≤ J ↔ ⇑box_integral.box.Icc I ⊆ ⇑box_integral.box.Icc J

theorem box_integral.box.antitone_lower {ι : Type u_1} :

antitone (λ (I : box_integral.box ι), I.lower)

theorem box_integral.box.monotone_upper {ι : Type u_1} :

monotone (λ (I : box_integral.box ι), I.upper)

theorem box_integral.box.coe_subset_Icc {ι : Type u_1} {I : box_integral.box ι} :

↑I ⊆ ⇑box_integral.box.Icc I

Supremum of two boxes #

@[protected, instance]

def box_integral.box.has_sup {ι : Type u_1} :

has_sup (box_integral.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

box_integral.box.has_sup = {sup := λ (I J : box_integral.box ι), {lower := I.lower ⊓ J.lower, upper := I.upper ⊔ J.upper, lower_lt_upper := _}}

@[protected, instance]

def box_integral.box.semilattice_sup {ι : Type u_1} :

semilattice_sup (box_integral.box ι)

Equations

box_integral.box.semilattice_sup = {sup := has_sup.sup box_integral.box.has_sup, le := partial_order.le box_integral.box.partial_order, lt := partial_order.lt box_integral.box.partial_order, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _}

`with_bot (box ι)` #

In this section we define coercion from with_bot (box ι) to set (ι → ℝ) by sending ⊥ to ∅.

@[protected, instance]

def box_integral.box.with_bot_coe {ι : Type u_1} :

has_coe_t (with_bot (box_integral.box ι)) (set (ι → ℝ))

Equations

box_integral.box.with_bot_coe = {coe := λ (o : with_bot (box_integral.box ι)), option.elim ∅ coe o}

@[simp, norm_cast]

theorem box_integral.box.coe_bot {ι : Type u_1} :

@[simp, norm_cast]

theorem box_integral.box.coe_coe {ι : Type u_1} {I : box_integral.box ι} :

theorem box_integral.box.is_some_iff {ι : Type u_1} {I : with_bot (box_integral.box ι)} :

↥(option.is_some I) ↔ ↑I.nonempty

theorem box_integral.box.bUnion_coe_eq_coe {ι : Type u_1} (I : with_bot (box_integral.box ι)) :

(⋃ (J : box_integral.box ι) (hJ : ↑J = I), ↑J) = ↑I

@[simp, norm_cast]

theorem box_integral.box.with_bot_coe_subset_iff {ι : Type u_1} {I J : with_bot (box_integral.box ι)} :

↑I ⊆ ↑J ↔ I ≤ J

@[simp, norm_cast]

theorem box_integral.box.with_bot_coe_inj {ι : Type u_1} {I J : with_bot (box_integral.box ι)} :

↑I = ↑J ↔ I = J

noncomputable def box_integral.box.mk' {ι : Type u_1} (l u : ι → ℝ) :

with_bot (box_integral.box ι)

Make a with_bot (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

box_integral.box.mk' l u = dite (∀ (i : ι), l i < u i) (λ (h : ∀ (i : ι), l i < u i), ↑{lower := l, upper := u, lower_lt_upper := h}) (λ (h : ¬∀ (i : ι), l i < u i), ⊥)

@[simp]

theorem box_integral.box.mk'_eq_bot {ι : Type u_1} {l u : ι → ℝ} :

box_integral.box.mk' l u = ⊥ ↔ ∃ (i : ι), u i ≤ l i

@[simp]

theorem box_integral.box.mk'_eq_coe {ι : Type u_1} {I : box_integral.box ι} {l u : ι → ℝ} :

box_integral.box.mk' l u = ↑I ↔ l = I.lower ∧ u = I.upper

@[simp]

theorem box_integral.box.coe_mk' {ι : Type u_1} (l u : ι → ℝ) :

↑(box_integral.box.mk' l u) = set.univ.pi (λ (i : ι), set.Ioc (l i) (u i))

@[protected, instance]

noncomputable def box_integral.box.with_bot.has_inf {ι : Type u_1} :

has_inf (with_bot (box_integral.box ι))

Equations

box_integral.box.with_bot.has_inf = {inf := λ (I : with_bot (box_integral.box ι)), with_bot.rec_bot_coe (λ (J : with_bot (box_integral.box ι)), ⊥) (λ (I : box_integral.box ι) (J : with_bot (box_integral.box ι)), with_bot.rec_bot_coe ⊥ (λ (J : box_integral.box ι), box_integral.box.mk' (I.lower ⊔ J.lower) (I.upper ⊓ J.upper)) J) I}

@[simp]

theorem box_integral.box.coe_inf {ι : Type u_1} (I J : with_bot (box_integral.box ι)) :

↑(I ⊓ J) = ↑I ∩ ↑J

@[protected, instance]

noncomputable def box_integral.box.with_bot.lattice {ι : Type u_1} :

lattice (with_bot (box_integral.box ι))

Equations

box_integral.box.with_bot.lattice = {sup := semilattice_sup.sup with_bot.semilattice_sup, le := semilattice_sup.le with_bot.semilattice_sup, lt := semilattice_sup.lt with_bot.semilattice_sup, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := has_inf.inf box_integral.box.with_bot.has_inf, inf_le_left := _, inf_le_right := _, le_inf := _}

@[simp, norm_cast]

theorem box_integral.box.disjoint_with_bot_coe {ι : Type u_1} {I J : with_bot (box_integral.box ι)} :

disjoint ↑I ↑J ↔ disjoint I J

theorem box_integral.box.disjoint_coe {ι : Type u_1} {I J : box_integral.box ι} :

disjoint ↑I ↑J ↔ disjoint ↑I ↑J

theorem box_integral.box.not_disjoint_coe_iff_nonempty_inter {ι : Type u_1} {I J : box_integral.box ι} :

¬disjoint ↑I ↑J ↔ (↑I ∩ ↑J).nonempty

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

def box_integral.box.face {n : ℕ} (I : box_integral.box (fin (n + 1))) (i : fin (n + 1)) :

box_integral.box (fin n)

Face of a box in ℝⁿ⁺¹ = fin (n + 1) → ℝ: the box in ℝⁿ = fin n → ℝ with corners at I.lower ∘ fin.succ_above i and I.upper ∘ fin.succ_above i.

Equations

I.face i = {lower := I.lower ∘ ⇑(i.succ_above), upper := I.upper ∘ ⇑(i.succ_above), lower_lt_upper := _}

@[simp]

theorem box_integral.box.face_upper {n : ℕ} (I : box_integral.box (fin (n + 1))) (i : fin (n + 1)) (ᾰ : fin n) :

(I.face i).upper ᾰ = I.upper (⇑(i.succ_above) ᾰ)

@[simp]

theorem box_integral.box.face_lower {n : ℕ} (I : box_integral.box (fin (n + 1))) (i : fin (n + 1)) (ᾰ : fin n) :

(I.face i).lower ᾰ = I.lower (⇑(i.succ_above) ᾰ)

@[simp]

theorem box_integral.box.face_mk {n : ℕ} (l 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.succ_above), upper := u ∘ ⇑(i.succ_above), lower_lt_upper := _}

theorem box_integral.box.face_mono {n : ℕ} {I J : box_integral.box (fin (n + 1))} (h : I ≤ J) (i : fin (n + 1)) :

I.face i ≤ J.face i

theorem box_integral.box.monotone_face {n : ℕ} (i : fin (n + 1)) :

monotone (λ (I : box_integral.box (fin (n + 1))), I.face i)

theorem box_integral.box.maps_to_insert_nth_face_Icc {n : ℕ} (I : box_integral.box (fin (n + 1))) {i : fin (n + 1)} {x : ℝ} (hx : x ∈ set.Icc (I.lower i) (I.upper i)) :

set.maps_to (i.insert_nth x) (⇑box_integral.box.Icc (I.face i)) (⇑box_integral.box.Icc I)

theorem box_integral.box.maps_to_insert_nth_face {n : ℕ} (I : box_integral.box (fin (n + 1))) {i : fin (n + 1)} {x : ℝ} (hx : x ∈ set.Ioc (I.lower i) (I.upper i)) :

set.maps_to (i.insert_nth x) ↑(I.face i) ↑I

theorem box_integral.box.continuous_on_face_Icc {X : Type u_1} [topological_space X] {n : ℕ} {f : (fin (n + 1) → ℝ) → X} {I : box_integral.box (fin (n + 1))} (h : continuous_on f (⇑box_integral.box.Icc I)) {i : fin (n + 1)} {x : ℝ} (hx : x ∈ set.Icc (I.lower i) (I.upper i)) :

continuous_on (f ∘ i.insert_nth x) (⇑box_integral.box.Icc (I.face i))

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

@[protected]

def box_integral.box.Ioo {ι : Type u_1} :

box_integral.box ι →o set (ι → ℝ)

The interior of a box.

Equations

box_integral.box.Ioo = {to_fun := λ (I : box_integral.box ι), set.univ.pi (λ (i : ι), set.Ioo (I.lower i) (I.upper i)), monotone' := _}

theorem box_integral.box.Ioo_subset_coe {ι : Type u_1} (I : box_integral.box ι) :

⇑box_integral.box.Ioo I ⊆ ↑I

@[protected]

theorem box_integral.box.Ioo_subset_Icc {ι : Type u_1} (I : box_integral.box ι) :

⇑box_integral.box.Ioo I ⊆ ⇑box_integral.box.Icc I

theorem box_integral.box.Union_Ioo_of_tendsto {ι : Type u_1} [finite ι] {I : box_integral.box ι} {J : ℕ → box_integral.box ι} (hJ : monotone J) (hl : filter.tendsto (box_integral.box.lower ∘ J) filter.at_top (nhds I.lower)) (hu : filter.tendsto (box_integral.box.upper ∘ J) filter.at_top (nhds I.upper)) :

(⋃ (n : ℕ), ⇑box_integral.box.Ioo (J n)) = ⇑box_integral.box.Ioo I

theorem box_integral.box.exists_seq_mono_tendsto {ι : Type u_1} (I : box_integral.box ι) :

∃ (J : ℕ →o box_integral.box ι), (∀ (n : ℕ), ⇑box_integral.box.Icc (⇑J n) ⊆ ⇑box_integral.box.Ioo I) ∧ filter.tendsto (box_integral.box.lower ∘ ⇑J) filter.at_top (nhds I.lower) ∧ filter.tendsto (box_integral.box.upper ∘ ⇑J) filter.at_top (nhds I.upper)

noncomputable def box_integral.box.distortion {ι : Type u_1} [fintype ι] (I : box_integral.box ι) :

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 (λ (i : ι), has_nndist.nndist I.lower I.upper / has_nndist.nndist (I.lower i) (I.upper i))

theorem box_integral.box.distortion_eq_of_sub_eq_div {ι : Type u_1} [fintype ι] {I J : box_integral.box ι} {r : ℝ} (h : ∀ (i : ι), I.upper i - I.lower i = (J.upper i - J.lower i) / r) :

I.distortion = J.distortion

theorem box_integral.box.nndist_le_distortion_mul {ι : Type u_1} [fintype ι] (I : box_integral.box ι) (i : ι) :

has_nndist.nndist I.lower I.upper ≤ I.distortion * has_nndist.nndist (I.lower i) (I.upper i)

theorem box_integral.box.dist_le_distortion_mul {ι : Type u_1} [fintype ι] (I : box_integral.box ι) (i : ι) :

has_dist.dist I.lower I.upper ≤ ↑(I.distortion) * (I.upper i - I.lower i)

theorem box_integral.box.diam_Icc_le_of_distortion_le {ι : Type u_1} [fintype ι] (I : box_integral.box ι) (i : ι) {c : nnreal} (h : I.distortion ≤ c) :

metric.diam (⇑box_integral.box.Icc I) ≤ ↑c * (I.upper i - I.lower i)