Unit Partition

Fix n a positive integer. BoxIntegral.unitPartition.box are boxes in ι → ℝ obtained by dividing the unit box uniformly into boxes of side length 1 / n and translating the boxes by the lattice ι → ℤ so that they cover the whole space. For fixed n, there are indexed by vectors ν : ι → ℤ.

Let B be a BoxIntegral. A unitPartition.box is admissible for B (more precisely its index is admissible) if it is contained in B. There are finitely many admissible unitPartition.box for B and thus we can form the corresponing tagged prepartition, see BoxIntegral.unitPartition.prepartition (note that each unitPartition.Box comes with its tag situated at its "upper most" vertex). If B satisfies hasIntegralVertices, that is its vertices are in ι → ℤ, then the corresponding prepartition is actually a partition.

Main definitions and results

• BoxIntegral.hasIntegralVertices: a Prop that states that the vertices of the box have coordinates in ℤ

• BoxIntegral.unitPartition.box: a BoxIntegral, indexed by ν : ι → ℤ, with vertices ν i / n and of side length 1 / n.

• BoxIntegral.unitPartition.admissibleIndex: For B : BoxIntegral.Box, the set of indices of unitPartition.box that are subsets of B. This is a finite set.

• BoxIntegral.unitPartition.prepartition_isPartition: For B : BoxIntegral.Box, if B has integral vertices, then the prepartition of unitPartition.box admissible for B is a partition of B.

def BoxIntegral.hasIntegralVertices {ι : Type u_1} (B : BoxIntegral.Box ι) : Prop

A BoxIntegral.Box has integral vertices if its vertices have coordinates in ℤ.

Equations

• BoxIntegral.hasIntegralVertices B = ∃ (l : ι → ℤ) (u : ι → ℤ), (∀ (i : ι), B.lower i = ↑(l i)) ∧ ∀ (i : ι), B.upper i = ↑(u i)

theorem BoxIntegral.le_hasIntegralVertices_of_isBounded {ι : Type u_1} [Finite ι] {s : Set (ι → ℝ)} (h : Bornology.IsBounded s) : ∃ (B : BoxIntegral.Box ι), BoxIntegral.hasIntegralVertices B ∧ s ≤ ↑B

Any bounded set is contained in a BoxIntegral.Box with integral vertices.

def BoxIntegral.unitPartition.box {ι : Type u_1} (n : ℕ) [NeZero n] (ν : ι → ℤ) : BoxIntegral.Box ι

A BoxIntegral, indexed by a positive integer n and ν : ι → ℤ, with corners ν i / n and of side length 1 / n.

Equations

• BoxIntegral.unitPartition.box n ν = { lower := fun (i : ι) => ↑(ν i) / ↑n, upper := fun (i : ι) => (↑(ν i) + 1) / ↑n, lower_lt_upper := ⋯ }

@[simp]

theorem BoxIntegral.unitPartition.box_lower {ι : Type u_1} (n : ℕ) [NeZero n] (ν : ι → ℤ) : (BoxIntegral.unitPartition.box n ν).lower = fun (i : ι) => ↑(ν i) / ↑n

@[simp]

theorem BoxIntegral.unitPartition.box_upper {ι : Type u_1} (n : ℕ) [NeZero n] (ν : ι → ℤ) : (BoxIntegral.unitPartition.box n ν).upper = fun (i : ι) => (↑(ν i) + 1) / ↑n

@[simp]

theorem BoxIntegral.unitPartition.mem_box_iff {ι : Type u_1} {n : ℕ} [NeZero n] {ν : ι → ℤ} {x : ι → ℝ} : x ∈ BoxIntegral.unitPartition.box n ν ↔ ∀ (i : ι), ↑(ν i) / ↑n < x i ∧ x i ≤ (↑(ν i) + 1) / ↑n

theorem BoxIntegral.unitPartition.mem_box_iff' {ι : Type u_1} {n : ℕ} [NeZero n] {ν : ι → ℤ} {x : ι → ℝ} : x ∈ BoxIntegral.unitPartition.box n ν ↔ ∀ (i : ι), ↑(ν i) < ↑n * x i ∧ ↑n * x i ≤ ↑(ν i) + 1

@[reducible, inline]

abbrev BoxIntegral.unitPartition.tag {ι : Type u_1} (n : ℕ) (ν : ι → ℤ) : ι → ℝ

The tag of (the index of) a unitPartition.box.

Equations

• BoxIntegral.unitPartition.tag n ν i = (↑(ν i) + 1) / ↑n

@[simp]

theorem BoxIntegral.unitPartition.tag_apply {ι : Type u_1} (n : ℕ) (ν : ι → ℤ) (i : ι) : BoxIntegral.unitPartition.tag n ν i = (↑(ν i) + 1) / ↑n

theorem BoxIntegral.unitPartition.tag_injective {ι : Type u_1} (n : ℕ) [NeZero n] : Function.Injective fun (ν : ι → ℤ) => BoxIntegral.unitPartition.tag n ν

theorem BoxIntegral.unitPartition.tag_mem {ι : Type u_1} (n : ℕ) [NeZero n] (ν : ι → ℤ) : BoxIntegral.unitPartition.tag n ν ∈ BoxIntegral.unitPartition.box n ν

def BoxIntegral.unitPartition.index {ι : Type u_1} (n : ℕ) (x : ι → ℝ) (i : ι) : ℤ

For x : ι → ℝ, its index is the index of the unique unitPartition.box to which it belongs.

Equations

• BoxIntegral.unitPartition.index n x i = ⌈↑n * x i⌉ - 1

@[simp]

theorem BoxIntegral.unitPartition.index_apply {ι : Type u_1} (m : ℕ) {x : ι → ℝ} (i : ι) : BoxIntegral.unitPartition.index m x i = ⌈↑m * x i⌉ - 1

theorem BoxIntegral.unitPartition.mem_box_iff_index {ι : Type u_1} {n : ℕ} [NeZero n] {x : ι → ℝ} {ν : ι → ℤ} : x ∈ BoxIntegral.unitPartition.box n ν ↔ BoxIntegral.unitPartition.index n x = ν

@[simp]

theorem BoxIntegral.unitPartition.index_tag {ι : Type u_1} (n : ℕ) [NeZero n] (ν : ι → ℤ) : BoxIntegral.unitPartition.index n (BoxIntegral.unitPartition.tag n ν) = ν

theorem BoxIntegral.unitPartition.disjoint {ι : Type u_1} {n : ℕ} [NeZero n] {ν ν' : ι → ℤ} : ν ≠ ν' ↔ Disjoint ↑(BoxIntegral.unitPartition.box n ν) ↑(BoxIntegral.unitPartition.box n ν')

theorem BoxIntegral.unitPartition.box_injective {ι : Type u_1} (n : ℕ) [NeZero n] : Function.Injective fun (ν : ι → ℤ) => BoxIntegral.unitPartition.box n ν

theorem BoxIntegral.unitPartition.box.upper_sub_lower {ι : Type u_1} (n : ℕ) [NeZero n] (ν : ι → ℤ) (i : ι) : (BoxIntegral.unitPartition.box n ν).upper i - (BoxIntegral.unitPartition.box n ν).lower i = 1 / ↑n

theorem BoxIntegral.unitPartition.diam_boxIcc {ι : Type u_1} (n : ℕ) [NeZero n] [Fintype ι] (ν : ι → ℤ) : Metric.diam (BoxIntegral.Box.Icc (BoxIntegral.unitPartition.box n ν)) ≤ 1 / ↑n

@[simp]

theorem BoxIntegral.unitPartition.volume_box {ι : Type u_1} (n : ℕ) [NeZero n] [Fintype ι] (ν : ι → ℤ) : MeasureTheory.volume ↑(BoxIntegral.unitPartition.box n ν) = 1 / ↑n ^ Fintype.card ι

theorem BoxIntegral.unitPartition.setFinite_index {ι : Type u_1} (n : ℕ) [NeZero n] [Fintype ι] {s : Set (ι → ℝ)} (hs₁ : MeasureTheory.NullMeasurableSet s MeasureTheory.volume) (hs₂ : MeasureTheory.volume s ≠ ⊤) : {ν : ι → ℤ | ↑(BoxIntegral.unitPartition.box n ν) ⊆ s}.Finite

def BoxIntegral.unitPartition.admissibleIndex {ι : Type u_1} (n : ℕ) [NeZero n] [Fintype ι] (B : BoxIntegral.Box ι) : Finset (ι → ℤ)

For B : BoxIntegral.Box, the set of indices of unitPartition.Box that are subsets of B. This is a finite set. These boxes cover B if it has integral vertices, see unitPartition.prepartition_isPartition.

Equations

• BoxIntegral.unitPartition.admissibleIndex n B = ⋯.toFinset

theorem BoxIntegral.unitPartition.mem_admissibleIndex_iff {ι : Type u_1} {n : ℕ} [NeZero n] [Fintype ι] {B : BoxIntegral.Box ι} {ν : ι → ℤ} : ν ∈ BoxIntegral.unitPartition.admissibleIndex n B ↔ BoxIntegral.unitPartition.box n ν ≤ B

def BoxIntegral.unitPartition.prepartition {ι : Type u_1} (n : ℕ) [NeZero n] [Fintype ι] (B : BoxIntegral.Box ι) : BoxIntegral.TaggedPrepartition B

For B : BoxIntegral.Box, the TaggedPrepartition formed by the set of all unitPartition.box whose index is B-admissible.

Equations

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

@[simp]

theorem BoxIntegral.unitPartition.mem_prepartition_iff {ι : Type u_1} {n : ℕ} [NeZero n] [Fintype ι] {B I : BoxIntegral.Box ι} : I ∈ BoxIntegral.unitPartition.prepartition n B ↔ ∃ ν ∈ BoxIntegral.unitPartition.admissibleIndex n B, BoxIntegral.unitPartition.box n ν = I

theorem BoxIntegral.unitPartition.mem_prepartition_boxes_iff {ι : Type u_1} {n : ℕ} [NeZero n] [Fintype ι] {B I : BoxIntegral.Box ι} : I ∈ (BoxIntegral.unitPartition.prepartition n B).boxes ↔ ∃ ν ∈ BoxIntegral.unitPartition.admissibleIndex n B, BoxIntegral.unitPartition.box n ν = I

theorem BoxIntegral.unitPartition.prepartition_tag {ι : Type u_1} (n : ℕ) [NeZero n] [Fintype ι] {ν : ι → ℤ} {B : BoxIntegral.Box ι} (hν : ν ∈ BoxIntegral.unitPartition.admissibleIndex n B) : (BoxIntegral.unitPartition.prepartition n B).tag (BoxIntegral.unitPartition.box n ν) = BoxIntegral.unitPartition.tag n ν

theorem BoxIntegral.unitPartition.box_index_tag_eq_self {ι : Type u_1} (n : ℕ) [NeZero n] [Fintype ι] {B I : BoxIntegral.Box ι} (hI : I ∈ (BoxIntegral.unitPartition.prepartition n B).boxes) : BoxIntegral.unitPartition.box n (BoxIntegral.unitPartition.index n ((BoxIntegral.unitPartition.prepartition n B).tag I)) = I

theorem BoxIntegral.unitPartition.prepartition_isHenstock {ι : Type u_1} (n : ℕ) [NeZero n] [Fintype ι] (B : BoxIntegral.Box ι) : (BoxIntegral.unitPartition.prepartition n B).IsHenstock

theorem BoxIntegral.unitPartition.prepartition_isSubordinate {ι : Type u_1} (n : ℕ) [NeZero n] [Fintype ι] (B : BoxIntegral.Box ι) {r : ℝ} (hr : 0 < r) (hn : 1 / ↑n ≤ r) : (BoxIntegral.unitPartition.prepartition n B).IsSubordinate fun (x : ι → ℝ) => ⟨r, hr⟩

theorem BoxIntegral.unitPartition.mem_admissibleIndex_of_mem_box {ι : Type u_1} (n : ℕ) [NeZero n] [Fintype ι] {B : BoxIntegral.Box ι} (hB : BoxIntegral.hasIntegralVertices B) {x : ι → ℝ} (hx : x ∈ B) : BoxIntegral.unitPartition.index n x ∈ BoxIntegral.unitPartition.admissibleIndex n B

If B : BoxIntegral.Box has integral vertices and contains the point x, then the index of x is admissible for B.

theorem BoxIntegral.unitPartition.prepartition_isPartition {ι : Type u_1} (n : ℕ) [NeZero n] [Fintype ι] {B : BoxIntegral.Box ι} (hB : BoxIntegral.hasIntegralVertices B) : (BoxIntegral.unitPartition.prepartition n B).IsPartition

If B : BoxIntegral.Box has integral vertices, then prepartition n B is a partition of B.