Documentation

Mathlib.Analysis.BoxIntegral.Partition.Tagged

Tagged partitions #

A tagged (pre)partition is a (pre)partition π enriched with a tagged point for each box of π. For simplicity we require that the function BoxIntegral.TaggedPrepartition.tag is defined on all boxes J : Box ι but use its values only on boxes of the partition. Given π : BoxIntegral.TaggedPrepartition I, we require that each BoxIntegral.TaggedPrepartition π J belongs to BoxIntegral.Box.Icc I. If for every J ∈ π, π.tag J belongs to J.Icc, then π is called a Henstock partition. We do not include this assumption into the definition of a tagged (pre)partition because McShane integral is defined as a limit along tagged partitions without this requirement.

Tags #

rectangular box, box partition

A tagged prepartition is a prepartition enriched with a tagged point for each box of the prepartition. For simplicity we require that tag is defined for all boxes in ι → ℝ but we will use only the values of tag on the boxes of the partition.

  • boxes : Finset (BoxIntegral.Box ι)
  • le_of_mem' : Jself.boxes, J I
  • pairwiseDisjoint : (↑self.boxes).Pairwise (Disjoint on BoxIntegral.Box.toSet)
  • tag : BoxIntegral.Box ιι

    Choice of tagged point of each box in this prepartition: we extend this to a total function, on all boxes in ι → ℝ.

  • tag_mem_Icc : ∀ (J : BoxIntegral.Box ι), self.tag J BoxIntegral.Box.Icc I

    Each tagged point belongs to I

Instances For
    theorem BoxIntegral.TaggedPrepartition.tag_mem_Icc {ι : Type u_1} {I : BoxIntegral.Box ι} (self : BoxIntegral.TaggedPrepartition I) (J : BoxIntegral.Box ι) :
    self.tag J BoxIntegral.Box.Icc I

    Each tagged point belongs to I

    Equations
    @[simp]
    @[simp]
    theorem BoxIntegral.TaggedPrepartition.mem_mk {ι : Type u_1} {I : BoxIntegral.Box ι} {J : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I) (f : BoxIntegral.Box ιι) (h : ∀ (J : BoxIntegral.Box ι), f J BoxIntegral.Box.Icc I) :
    J { toPrepartition := π, tag := f, tag_mem_Icc := h } J π

    Union of all boxes of a tagged prepartition.

    Equations
    • π.iUnion = π.iUnion
    Instances For
      theorem BoxIntegral.TaggedPrepartition.iUnion_def {ι : Type u_1} {I : BoxIntegral.Box ι} (π : BoxIntegral.TaggedPrepartition I) :
      π.iUnion = Jπ, J
      @[simp]
      theorem BoxIntegral.TaggedPrepartition.iUnion_mk {ι : Type u_1} {I : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I) (f : BoxIntegral.Box ιι) (h : ∀ (J : BoxIntegral.Box ι), f J BoxIntegral.Box.Icc I) :
      { toPrepartition := π, tag := f, tag_mem_Icc := h }.iUnion = π.iUnion
      @[simp]
      theorem BoxIntegral.TaggedPrepartition.mem_iUnion {ι : Type u_1} {I : BoxIntegral.Box ι} (π : BoxIntegral.TaggedPrepartition I) {x : ι} :
      x π.iUnion Jπ, x J

      A tagged prepartition is a partition if it covers the whole box.

      Equations
      • π.IsPartition = π.IsPartition
      Instances For
        @[simp]
        theorem BoxIntegral.TaggedPrepartition.filter_tag {ι : Type u_1} {I : BoxIntegral.Box ι} (π : BoxIntegral.TaggedPrepartition I) (p : BoxIntegral.Box ιProp) :
        (π.filter p).tag = π.tag
        @[simp]
        theorem BoxIntegral.TaggedPrepartition.filter_boxes_val {ι : Type u_1} {I : BoxIntegral.Box ι} (π : BoxIntegral.TaggedPrepartition I) (p : BoxIntegral.Box ιProp) :
        (π.filter p).boxes.val = Multiset.filter (fun (J : BoxIntegral.Box ι) => p J) π.boxes.val

        The tagged partition made of boxes of π that satisfy predicate p.

        Equations
        • π.filter p = { toPrepartition := π.filter p, tag := π.tag, tag_mem_Icc := }
        Instances For
          @[simp]
          theorem BoxIntegral.TaggedPrepartition.mem_filter {ι : Type u_1} {I : BoxIntegral.Box ι} {J : BoxIntegral.Box ι} (π : BoxIntegral.TaggedPrepartition I) {p : BoxIntegral.Box ιProp} :
          J π.filter p J π p J
          @[simp]
          theorem BoxIntegral.TaggedPrepartition.iUnion_filter_not {ι : Type u_1} {I : BoxIntegral.Box ι} (π : BoxIntegral.TaggedPrepartition I) (p : BoxIntegral.Box ιProp) :
          (π.filter fun (J : BoxIntegral.Box ι) => ¬p J).iUnion = π.iUnion \ (π.filter p).iUnion

          Given a partition π of I : BoxIntegral.Box ι and a collection of tagged partitions πi J of all boxes J ∈ π, returns the tagged partition of I into all the boxes of πi J with tags coming from (πi J).tag.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            @[simp]
            theorem BoxIntegral.Prepartition.mem_biUnionTagged {ι : Type u_1} {I : BoxIntegral.Box ι} {J : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I) {πi : (J : BoxIntegral.Box ι) → BoxIntegral.TaggedPrepartition J} :
            J π.biUnionTagged πi J'π, J πi J'
            theorem BoxIntegral.Prepartition.tag_biUnionTagged {ι : Type u_1} {I : BoxIntegral.Box ι} {J : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I) {πi : (J : BoxIntegral.Box ι) → BoxIntegral.TaggedPrepartition J} (hJ : J π) {J' : BoxIntegral.Box ι} (hJ' : J' πi J) :
            (π.biUnionTagged πi).tag J' = (πi J).tag J'
            @[simp]
            theorem BoxIntegral.Prepartition.iUnion_biUnionTagged {ι : Type u_1} {I : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I) (πi : (J : BoxIntegral.Box ι) → BoxIntegral.TaggedPrepartition J) :
            (π.biUnionTagged πi).iUnion = Jπ, (πi J).iUnion
            theorem BoxIntegral.Prepartition.forall_biUnionTagged {ι : Type u_1} {I : BoxIntegral.Box ι} (p : (ι)BoxIntegral.Box ιProp) (π : BoxIntegral.Prepartition I) (πi : (J : BoxIntegral.Box ι) → BoxIntegral.TaggedPrepartition J) :
            (∀ Jπ.biUnionTagged πi, p ((π.biUnionTagged πi).tag J) J) Jπ, J'πi J, p ((πi J).tag J') J'
            theorem BoxIntegral.Prepartition.IsPartition.biUnionTagged {ι : Type u_1} {I : BoxIntegral.Box ι} {π : BoxIntegral.Prepartition I} (h : π.IsPartition) {πi : (J : BoxIntegral.Box ι) → BoxIntegral.TaggedPrepartition J} (hi : Jπ, (πi J).IsPartition) :
            (π.biUnionTagged πi).IsPartition
            @[simp]
            theorem BoxIntegral.TaggedPrepartition.biUnionPrepartition_tag {ι : Type u_1} {I : BoxIntegral.Box ι} (π : BoxIntegral.TaggedPrepartition I) (πi : (J : BoxIntegral.Box ι) → BoxIntegral.Prepartition J) :
            (π.biUnionPrepartition πi).tag = fun (J : BoxIntegral.Box ι) => π.tag (π.biUnionIndex πi J)

            Given a tagged partition π of I and a (not tagged) partition πi J hJ of each J ∈ π, returns the tagged partition of I into all the boxes of all πi J hJ. The tag of a box J is defined to be the π.tag of the box of the partition π that includes J.

            Note that usually the result is not a Henstock partition.

            Equations
            • π.biUnionPrepartition πi = { toPrepartition := π.biUnion πi, tag := fun (J : BoxIntegral.Box ι) => π.tag (π.biUnionIndex πi J), tag_mem_Icc := }
            Instances For
              theorem BoxIntegral.TaggedPrepartition.IsPartition.biUnionPrepartition {ι : Type u_1} {I : BoxIntegral.Box ι} {π : BoxIntegral.TaggedPrepartition I} (h : π.IsPartition) {πi : (J : BoxIntegral.Box ι) → BoxIntegral.Prepartition J} (hi : Jπ, (πi J).IsPartition) :
              (π.biUnionPrepartition πi).IsPartition

              Given two partitions π₁ and π₁, one of them tagged and the other is not, returns the tagged partition with toPrepartition = π₁.toPrepartition ⊓ π₂ and tags coming from π₁.

              Note that usually the result is not a Henstock partition.

              Equations
              • π.infPrepartition π' = π.biUnionPrepartition fun (J : BoxIntegral.Box ι) => π'.restrict J
              Instances For
                @[simp]
                theorem BoxIntegral.TaggedPrepartition.infPrepartition_toPrepartition {ι : Type u_1} {I : BoxIntegral.Box ι} (π : BoxIntegral.TaggedPrepartition I) (π' : BoxIntegral.Prepartition I) :
                (π.infPrepartition π').toPrepartition = π.toPrepartition π'
                theorem BoxIntegral.TaggedPrepartition.mem_infPrepartition_comm {ι : Type u_1} {I : BoxIntegral.Box ι} {J : BoxIntegral.Box ι} {π₁ : BoxIntegral.TaggedPrepartition I} {π₂ : BoxIntegral.TaggedPrepartition I} :
                J π₁.infPrepartition π₂.toPrepartition J π₂.infPrepartition π₁.toPrepartition
                theorem BoxIntegral.TaggedPrepartition.IsPartition.infPrepartition {ι : Type u_1} {I : BoxIntegral.Box ι} {π₁ : BoxIntegral.TaggedPrepartition I} (h₁ : π₁.IsPartition) {π₂ : BoxIntegral.Prepartition I} (h₂ : π₂.IsPartition) :
                (π₁.infPrepartition π₂).IsPartition

                A tagged partition is said to be a Henstock partition if for each J ∈ π, the tag of J belongs to J.Icc.

                Equations
                • π.IsHenstock = Jπ, π.tag J BoxIntegral.Box.Icc J
                Instances For
                  @[simp]
                  theorem BoxIntegral.TaggedPrepartition.isHenstock_biUnionTagged {ι : Type u_1} {I : BoxIntegral.Box ι} {π : BoxIntegral.Prepartition I} {πi : (J : BoxIntegral.Box ι) → BoxIntegral.TaggedPrepartition J} :
                  (π.biUnionTagged πi).IsHenstock Jπ, (πi J).IsHenstock
                  theorem BoxIntegral.TaggedPrepartition.IsHenstock.card_filter_tag_eq_le {ι : Type u_1} {I : BoxIntegral.Box ι} {π : BoxIntegral.TaggedPrepartition I} [Fintype ι] (h : π.IsHenstock) (x : ι) :
                  (Finset.filter (fun (J : BoxIntegral.Box ι) => π.tag J = x) π.boxes).card 2 ^ Fintype.card ι

                  In a Henstock prepartition, there are at most 2 ^ Fintype.card ι boxes with a given tag.

                  A tagged partition π is subordinate to r : (ι → ℝ) → ℝ if each box J ∈ π is included in the closed ball with center π.tag J and radius r (π.tag J).

                  Equations
                  • π.IsSubordinate r = Jπ, BoxIntegral.Box.Icc J Metric.closedBall (π.tag J) (r (π.tag J))
                  Instances For
                    @[simp]
                    theorem BoxIntegral.TaggedPrepartition.isSubordinate_biUnionTagged {ι : Type u_1} {I : BoxIntegral.Box ι} {r : (ι)(Set.Ioi 0)} [Fintype ι] {π : BoxIntegral.Prepartition I} {πi : (J : BoxIntegral.Box ι) → BoxIntegral.TaggedPrepartition J} :
                    (π.biUnionTagged πi).IsSubordinate r Jπ, (πi J).IsSubordinate r
                    theorem BoxIntegral.TaggedPrepartition.IsSubordinate.biUnionPrepartition {ι : Type u_1} {I : BoxIntegral.Box ι} {π : BoxIntegral.TaggedPrepartition I} {r : (ι)(Set.Ioi 0)} [Fintype ι] (h : π.IsSubordinate r) (πi : (J : BoxIntegral.Box ι) → BoxIntegral.Prepartition J) :
                    (π.biUnionPrepartition πi).IsSubordinate r
                    theorem BoxIntegral.TaggedPrepartition.IsSubordinate.infPrepartition {ι : Type u_1} {I : BoxIntegral.Box ι} {π : BoxIntegral.TaggedPrepartition I} {r : (ι)(Set.Ioi 0)} [Fintype ι] (h : π.IsSubordinate r) (π' : BoxIntegral.Prepartition I) :
                    (π.infPrepartition π').IsSubordinate r
                    theorem BoxIntegral.TaggedPrepartition.IsSubordinate.mono' {ι : Type u_1} {I : BoxIntegral.Box ι} {r₁ : (ι)(Set.Ioi 0)} {r₂ : (ι)(Set.Ioi 0)} [Fintype ι] {π : BoxIntegral.TaggedPrepartition I} (hr₁ : π.IsSubordinate r₁) (h : Jπ, r₁ (π.tag J) r₂ (π.tag J)) :
                    π.IsSubordinate r₂
                    theorem BoxIntegral.TaggedPrepartition.IsSubordinate.mono {ι : Type u_1} {I : BoxIntegral.Box ι} {r₁ : (ι)(Set.Ioi 0)} {r₂ : (ι)(Set.Ioi 0)} [Fintype ι] {π : BoxIntegral.TaggedPrepartition I} (hr₁ : π.IsSubordinate r₁) (h : xBoxIntegral.Box.Icc I, r₁ x r₂ x) :
                    π.IsSubordinate r₂
                    theorem BoxIntegral.TaggedPrepartition.IsSubordinate.diam_le {ι : Type u_1} {I : BoxIntegral.Box ι} {J : BoxIntegral.Box ι} {r : (ι)(Set.Ioi 0)} [Fintype ι] {π : BoxIntegral.TaggedPrepartition I} (h : π.IsSubordinate r) (hJ : J π.boxes) :
                    Metric.diam (BoxIntegral.Box.Icc J) 2 * (r (π.tag J))
                    @[simp]
                    theorem BoxIntegral.TaggedPrepartition.single_boxes_val {ι : Type u_1} (I : BoxIntegral.Box ι) (J : BoxIntegral.Box ι) (hJ : J I) (x : ι) (h : x BoxIntegral.Box.Icc I) :
                    (BoxIntegral.TaggedPrepartition.single I J hJ x h).boxes.val = {J}
                    @[simp]
                    theorem BoxIntegral.TaggedPrepartition.single_tag {ι : Type u_1} (I : BoxIntegral.Box ι) (J : BoxIntegral.Box ι) (hJ : J I) (x : ι) (h : x BoxIntegral.Box.Icc I) :
                    (BoxIntegral.TaggedPrepartition.single I J hJ x h).tag = fun (x_1 : BoxIntegral.Box ι) => x
                    def BoxIntegral.TaggedPrepartition.single {ι : Type u_1} (I : BoxIntegral.Box ι) (J : BoxIntegral.Box ι) (hJ : J I) (x : ι) (h : x BoxIntegral.Box.Icc I) :

                    Tagged prepartition with single box and prescribed tag.

                    Equations
                    Instances For
                      @[simp]
                      theorem BoxIntegral.TaggedPrepartition.mem_single {ι : Type u_1} {I : BoxIntegral.Box ι} {J : BoxIntegral.Box ι} {x : ι} {J' : BoxIntegral.Box ι} (hJ : J I) (h : x BoxIntegral.Box.Icc I) :
                      theorem BoxIntegral.TaggedPrepartition.isPartition_single_iff {ι : Type u_1} {I : BoxIntegral.Box ι} {J : BoxIntegral.Box ι} {x : ι} (hJ : J I) (h : x BoxIntegral.Box.Icc I) :
                      (BoxIntegral.TaggedPrepartition.single I J hJ x h).IsPartition J = I
                      theorem BoxIntegral.TaggedPrepartition.isPartition_single {ι : Type u_1} {I : BoxIntegral.Box ι} {x : ι} (h : x BoxIntegral.Box.Icc I) :
                      (BoxIntegral.TaggedPrepartition.single I I x h).IsPartition
                      theorem BoxIntegral.TaggedPrepartition.forall_mem_single {ι : Type u_1} {I : BoxIntegral.Box ι} {J : BoxIntegral.Box ι} {x : ι} (p : (ι)BoxIntegral.Box ιProp) (hJ : J I) (h : x BoxIntegral.Box.Icc I) :
                      (∀ J'BoxIntegral.TaggedPrepartition.single I J hJ x h, p ((BoxIntegral.TaggedPrepartition.single I J hJ x h).tag J') J') p x J
                      @[simp]
                      theorem BoxIntegral.TaggedPrepartition.isHenstock_single_iff {ι : Type u_1} {I : BoxIntegral.Box ι} {J : BoxIntegral.Box ι} {x : ι} (hJ : J I) (h : x BoxIntegral.Box.Icc I) :
                      (BoxIntegral.TaggedPrepartition.single I J hJ x h).IsHenstock x BoxIntegral.Box.Icc J
                      theorem BoxIntegral.TaggedPrepartition.isHenstock_single {ι : Type u_1} {I : BoxIntegral.Box ι} {x : ι} (h : x BoxIntegral.Box.Icc I) :
                      (BoxIntegral.TaggedPrepartition.single I I x h).IsHenstock
                      @[simp]
                      theorem BoxIntegral.TaggedPrepartition.isSubordinate_single {ι : Type u_1} {I : BoxIntegral.Box ι} {J : BoxIntegral.Box ι} {x : ι} {r : (ι)(Set.Ioi 0)} [Fintype ι] (hJ : J I) (h : x BoxIntegral.Box.Icc I) :
                      (BoxIntegral.TaggedPrepartition.single I J hJ x h).IsSubordinate r BoxIntegral.Box.Icc J Metric.closedBall x (r x)
                      @[simp]
                      theorem BoxIntegral.TaggedPrepartition.iUnion_single {ι : Type u_1} {I : BoxIntegral.Box ι} {J : BoxIntegral.Box ι} {x : ι} (hJ : J I) (h : x BoxIntegral.Box.Icc I) :
                      (BoxIntegral.TaggedPrepartition.single I J hJ x h).iUnion = J

                      Union of two tagged prepartitions with disjoint unions of boxes.

                      Equations
                      • π₁.disjUnion π₂ h = { toPrepartition := π₁.disjUnion π₂.toPrepartition h, tag := π₁.boxes.piecewise π₁.tag π₂.tag, tag_mem_Icc := }
                      Instances For
                        @[simp]
                        theorem BoxIntegral.TaggedPrepartition.disjUnion_boxes {ι : Type u_1} {I : BoxIntegral.Box ι} {π₁ : BoxIntegral.TaggedPrepartition I} {π₂ : BoxIntegral.TaggedPrepartition I} (h : Disjoint π₁.iUnion π₂.iUnion) :
                        (π₁.disjUnion π₂ h).boxes = π₁.boxes π₂.boxes
                        @[simp]
                        theorem BoxIntegral.TaggedPrepartition.mem_disjUnion {ι : Type u_1} {I : BoxIntegral.Box ι} {J : BoxIntegral.Box ι} {π₁ : BoxIntegral.TaggedPrepartition I} {π₂ : BoxIntegral.TaggedPrepartition I} (h : Disjoint π₁.iUnion π₂.iUnion) :
                        J π₁.disjUnion π₂ h J π₁ J π₂
                        @[simp]
                        theorem BoxIntegral.TaggedPrepartition.iUnion_disjUnion {ι : Type u_1} {I : BoxIntegral.Box ι} {π₁ : BoxIntegral.TaggedPrepartition I} {π₂ : BoxIntegral.TaggedPrepartition I} (h : Disjoint π₁.iUnion π₂.iUnion) :
                        (π₁.disjUnion π₂ h).iUnion = π₁.iUnion π₂.iUnion
                        theorem BoxIntegral.TaggedPrepartition.disjUnion_tag_of_mem_left {ι : Type u_1} {I : BoxIntegral.Box ι} {J : BoxIntegral.Box ι} {π₁ : BoxIntegral.TaggedPrepartition I} {π₂ : BoxIntegral.TaggedPrepartition I} (h : Disjoint π₁.iUnion π₂.iUnion) (hJ : J π₁) :
                        (π₁.disjUnion π₂ h).tag J = π₁.tag J
                        theorem BoxIntegral.TaggedPrepartition.disjUnion_tag_of_mem_right {ι : Type u_1} {I : BoxIntegral.Box ι} {J : BoxIntegral.Box ι} {π₁ : BoxIntegral.TaggedPrepartition I} {π₂ : BoxIntegral.TaggedPrepartition I} (h : Disjoint π₁.iUnion π₂.iUnion) (hJ : J π₂) :
                        (π₁.disjUnion π₂ h).tag J = π₂.tag J
                        theorem BoxIntegral.TaggedPrepartition.IsSubordinate.disjUnion {ι : Type u_1} {I : BoxIntegral.Box ι} {π₁ : BoxIntegral.TaggedPrepartition I} {π₂ : BoxIntegral.TaggedPrepartition I} {r : (ι)(Set.Ioi 0)} [Fintype ι] (h₁ : π₁.IsSubordinate r) (h₂ : π₂.IsSubordinate r) (h : Disjoint π₁.iUnion π₂.iUnion) :
                        (π₁.disjUnion π₂ h).IsSubordinate r
                        theorem BoxIntegral.TaggedPrepartition.IsHenstock.disjUnion {ι : Type u_1} {I : BoxIntegral.Box ι} {π₁ : BoxIntegral.TaggedPrepartition I} {π₂ : BoxIntegral.TaggedPrepartition I} (h₁ : π₁.IsHenstock) (h₂ : π₂.IsHenstock) (h : Disjoint π₁.iUnion π₂.iUnion) :
                        (π₁.disjUnion π₂ h).IsHenstock

                        If I ≤ J, then every tagged prepartition of I is a tagged prepartition of J.

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

                          The distortion of a tagged prepartition is the maximum of distortions of its boxes.

                          Equations
                          • π.distortion = π.distortion
                          Instances For
                            theorem BoxIntegral.TaggedPrepartition.distortion_le_of_mem {ι : Type u_1} {I : BoxIntegral.Box ι} {J : BoxIntegral.Box ι} (π : BoxIntegral.TaggedPrepartition I) [Fintype ι] (h : J π) :
                            J.distortion π.distortion
                            theorem BoxIntegral.TaggedPrepartition.distortion_le_iff {ι : Type u_1} {I : BoxIntegral.Box ι} (π : BoxIntegral.TaggedPrepartition I) [Fintype ι] {c : NNReal} :
                            π.distortion c Jπ, J.distortion c
                            @[simp]
                            theorem BoxIntegral.Prepartition.distortion_biUnionTagged {ι : Type u_1} {I : BoxIntegral.Box ι} [Fintype ι] (π : BoxIntegral.Prepartition I) (πi : (J : BoxIntegral.Box ι) → BoxIntegral.TaggedPrepartition J) :
                            (π.biUnionTagged πi).distortion = π.boxes.sup fun (J : BoxIntegral.Box ι) => (πi J).distortion
                            @[simp]
                            theorem BoxIntegral.TaggedPrepartition.distortion_biUnionPrepartition {ι : Type u_1} {I : BoxIntegral.Box ι} [Fintype ι] (π : BoxIntegral.TaggedPrepartition I) (πi : (J : BoxIntegral.Box ι) → BoxIntegral.Prepartition J) :
                            (π.biUnionPrepartition πi).distortion = π.boxes.sup fun (J : BoxIntegral.Box ι) => (πi J).distortion
                            @[simp]
                            theorem BoxIntegral.TaggedPrepartition.distortion_disjUnion {ι : Type u_1} {I : BoxIntegral.Box ι} {π₁ : BoxIntegral.TaggedPrepartition I} {π₂ : BoxIntegral.TaggedPrepartition I} [Fintype ι] (h : Disjoint π₁.iUnion π₂.iUnion) :
                            (π₁.disjUnion π₂ h).distortion = max π₁.distortion π₂.distortion
                            theorem BoxIntegral.TaggedPrepartition.distortion_of_const {ι : Type u_1} {I : BoxIntegral.Box ι} (π : BoxIntegral.TaggedPrepartition I) [Fintype ι] {c : NNReal} (h₁ : π.boxes.Nonempty) (h₂ : Jπ, J.distortion = c) :
                            π.distortion = c
                            @[simp]
                            theorem BoxIntegral.TaggedPrepartition.distortion_single {ι : Type u_1} {I : BoxIntegral.Box ι} {J : BoxIntegral.Box ι} {x : ι} [Fintype ι] (hJ : J I) (h : x BoxIntegral.Box.Icc I) :
                            (BoxIntegral.TaggedPrepartition.single I J hJ x h).distortion = J.distortion
                            theorem BoxIntegral.TaggedPrepartition.distortion_filter_le {ι : Type u_1} {I : BoxIntegral.Box ι} (π : BoxIntegral.TaggedPrepartition I) [Fintype ι] (p : BoxIntegral.Box ιProp) :
                            (π.filter p).distortion π.distortion