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 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 corresponding 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.

• tendsto_tsum_div_pow_atTop_integral: let s be a bounded, measurable set of ι → ℝ whose frontier has zero volume and let F be a continuous function. Then the limit as n → ∞ of ∑ F x / n ^ card ι, where the sum is over the points in s ∩ n⁻¹ • (ι → ℤ), tends to the integral of F over s.

• tendsto_card_div_pow_atTop_volume: let s be a bounded, measurable set of ι → ℝ whose frontier has zero volume. Then the limit as n → ∞ of card (s ∩ n⁻¹ • (ι → ℤ)) / n ^ card ι tends to the volume of s.

• tendsto_card_div_pow_atTop_volume': a version of tendsto_card_div_pow_atTop_volume where we assume in addition that x • s ⊆ y • s whenever 0 < x ≤ y. Then we get the same limit card (s ∩ x⁻¹ • (ι → ℤ)) / x ^ card ι → volume s but the limit is over a real variable x.

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

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

theorem BoxIntegral.le_hasIntegralVertices_of_isBounded {ι : Type u_1} [Finite ι] {s : Set (ι → ℝ)} (h : Bornology.IsBounded s) : ∃ (B : Box ι), 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] (ν : ι → ℤ) : Box ι

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

@[simp]

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

@[simp]

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

@[simp]

theorem BoxIntegral.unitPartition.mem_box_iff {ι : Type u_1} {n : ℕ} [NeZero n] {ν : ι → ℤ} {x : ι → ℝ} : x ∈ 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 ∈ 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.

@[simp]

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

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

theorem BoxIntegral.unitPartition.tag_mem {ι : Type u_1} (n : ℕ) [NeZero n] (ν : ι → ℤ) : tag n ν ∈ 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.

@[simp]

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

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

@[simp]

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

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

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

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

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

@[simp]

theorem BoxIntegral.unitPartition.volume_box {ι : Type u_1} (n : ℕ) [NeZero n] [Fintype ι] (ν : ι → ℤ) : MeasureTheory.volume ↑(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 ≠ ⊤) : {ν : ι → ℤ | ↑(box n ν) ⊆ s}.Finite

def BoxIntegral.unitPartition.admissibleIndex {ι : Type u_1} (n : ℕ) [NeZero n] [Fintype ι] (B : 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.

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

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

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

@[simp]

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

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

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

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

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

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

theorem BoxIntegral.unitPartition.mem_admissibleIndex_of_mem_box {ι : Type u_1} (n : ℕ) [NeZero n] [Fintype ι] {B : Box ι} (hB : hasIntegralVertices B) {x : ι → ℝ} (hx : x ∈ B) : index n x ∈ 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 : Box ι} (hB : hasIntegralVertices B) : (prepartition n B).IsPartition

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

theorem BoxIntegral.unitPartition.mem_smul_span_iff {ι : Type u_1} {n : ℕ} [NeZero n] [Fintype ι] {v : ι → ℝ} : v ∈ (↑n)⁻¹ • Submodule.span ℤ (Set.range ⇑(Pi.basisFun ℝ ι)) ↔ ∀ (i : ι), ↑n * v i ∈ Set.range ⇑(algebraMap ℤ ℝ)

theorem BoxIntegral.unitPartition.tag_mem_smul_span {ι : Type u_1} (n : ℕ) [NeZero n] [Fintype ι] (ν : ι → ℤ) : tag n ν ∈ (↑n)⁻¹ • Submodule.span ℤ (Set.range ⇑(Pi.basisFun ℝ ι))

theorem BoxIntegral.unitPartition.tag_index_eq_self_of_mem_smul_span {ι : Type u_1} (n : ℕ) [NeZero n] [Fintype ι] {x : ι → ℝ} (hx : x ∈ (↑n)⁻¹ • Submodule.span ℤ (Set.range ⇑(Pi.basisFun ℝ ι))) : tag n (index n x) = x

theorem BoxIntegral.unitPartition.eq_of_mem_smul_span_of_index_eq_index {ι : Type u_1} (n : ℕ) [NeZero n] [Fintype ι] {x y : ι → ℝ} (hx : x ∈ (↑n)⁻¹ • Submodule.span ℤ (Set.range ⇑(Pi.basisFun ℝ ι))) (hy : y ∈ (↑n)⁻¹ • Submodule.span ℤ (Set.range ⇑(Pi.basisFun ℝ ι))) (h : index n x = index n y) : x = y

theorem BoxIntegral.unitPartition.integralSum_eq_tsum_div {ι : Type u_1} (n : ℕ) [NeZero n] [Fintype ι] (s : Set (ι → ℝ)) (F : (ι → ℝ) → ℝ) {B : Box ι} (hB : hasIntegralVertices B) (hs₀ : s ≤ ↑B) : integralSum (s.indicator F) MeasureTheory.volume.toBoxAdditive.toSMul (prepartition n B) = (∑' (x : ↑(s ∩ (↑n)⁻¹ • ↑(Submodule.span ℤ (Set.range ⇑(Pi.basisFun ℝ ι))))), F ↑x) / ↑n ^ Fintype.card ι

theorem tendsto_tsum_div_pow_atTop_integral {ι : Type u_1} [Fintype ι] (s : Set (ι → ℝ)) (F : (ι → ℝ) → ℝ) (hF : Continuous F) (hs₁ : Bornology.IsBounded s) (hs₂ : MeasurableSet s) (hs₃ : MeasureTheory.volume (frontier s) = 0) : Filter.Tendsto (fun (n : ℕ) => (∑' (x : ↑(s ∩ (↑n)⁻¹ • ↑(Submodule.span ℤ (Set.range ⇑(Pi.basisFun ℝ ι))))), F ↑x) / ↑n ^ Fintype.card ι) Filter.atTop (nhds (∫ (x : ι → ℝ) in s, F x))

Let s be a bounded, measurable set of ι → ℝ whose frontier has zero volume and let F be a continuous function. Then the limit as n → ∞ of ∑ F x / n ^ card ι, where the sum is over the points in s ∩ n⁻¹ • (ι → ℤ), tends to the integral of F over s.

theorem tendsto_card_div_pow_atTop_volume {ι : Type u_1} [Fintype ι] (s : Set (ι → ℝ)) (hs₁ : Bornology.IsBounded s) (hs₂ : MeasurableSet s) (hs₃ : MeasureTheory.volume (frontier s) = 0) : Filter.Tendsto (fun (n : ℕ) => ↑(Nat.card ↑(s ∩ (↑n)⁻¹ • ↑(Submodule.span ℤ (Set.range ⇑(Pi.basisFun ℝ ι))))) / ↑n ^ Fintype.card ι) Filter.atTop (nhds (MeasureTheory.volume.real s))

Let s be a bounded, measurable set of ι → ℝ whose frontier has zero volume. Then the limit as n → ∞ of card (s ∩ n⁻¹ • (ι → ℤ)) / n ^ card ι tends to the volume of s. This is a special case of tendsto_card_div_pow with F = 1.

theorem tendsto_card_div_pow_atTop_volume' {ι : Type u_1} [Fintype ι] (s : Set (ι → ℝ)) (hs₁ : Bornology.IsBounded s) (hs₂ : MeasurableSet s) (hs₃ : MeasureTheory.volume (frontier s) = 0) (hs₄ : ∀ ⦃x y : ℝ⦄, 0 < x → x ≤ y → x • s ⊆ y • s) : Filter.Tendsto (fun (x : ℝ) => ↑(Nat.card ↑(s ∩ x⁻¹ • ↑(Submodule.span ℤ (Set.range ⇑(Pi.basisFun ℝ ι))))) / x ^ Fintype.card ι) Filter.atTop (nhds (MeasureTheory.volume.real s))

A version of tendsto_card_div_pow_atTop_volume for a real variable.