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
Instances For
    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
    Instances For
      @[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
      Instances For
        @[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
        Instances For
          @[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.

          Equations
          Instances For
            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.
            Instances For
              @[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) :

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

              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) :
              Filter.Tendsto (fun (x : ) => (Nat.card (s x⁻¹ (Submodule.span (Set.range (Pi.basisFun ι))))) / x ^ Fintype.card ι) Filter.atTop (nhds (MeasureTheory.volume s).toReal)

              A version of tendsto_card_div_pow_atTop_volume for a real variable.