Documentation

Mathlib.Analysis.BoxIntegral.UnitPartition

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 #

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

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

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

Equations
@[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.

Equations
@[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.

Equations
@[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 ι] (ν : ι) :
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.

Equations
theorem BoxIntegral.unitPartition.mem_admissibleIndex_iff {ι : Type u_1} {n : } [NeZero n] [Fintype ι] {B : Box ι} {ν : ι} :
ν admissibleIndex n B box n ν 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 : 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 ι} ( : ν 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_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) :

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

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 ι] (ν : ι) :
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) :
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) :

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 < xx yx s y s) :

A version of tendsto_card_div_pow_atTop_volume for a real variable.