Documentation

Mathlib.Analysis.BoxIntegral.Partition.Basic

Partitions of rectangular boxes in ℝⁿ #

In this file we define (pre)partitions of rectangular boxes in ℝⁿ. A partition of a box I in ℝⁿ (see BoxIntegral.Prepartition and BoxIntegral.Prepartition.IsPartition) is a finite set of pairwise disjoint boxes such that their union is exactly I. We use boxes : Finset (Box ι) to store the set of boxes.

Many lemmas about box integrals deal with pairwise disjoint collections of subboxes, so we define a structure BoxIntegral.Prepartition (I : BoxIntegral.Box ι) that stores a collection of boxes such that

Then we define a predicate BoxIntegral.Prepartition.IsPartition; π.IsPartition means that the boxes of π actually cover the whole I. We also define some operations on prepartitions:

We also define a SemilatticeInf structure on BoxIntegral.Prepartition I for all I : BoxIntegral.Box ι.

Tags #

rectangular box, partition

structure BoxIntegral.Prepartition {ι : Type u_1} (I : BoxIntegral.Box ι) :
Type u_1

A prepartition of I : BoxIntegral.Box ι is a finite set of pairwise disjoint subboxes of I.

  • boxes : Finset (BoxIntegral.Box ι)

    The underlying set of boxes

  • le_of_mem' : Jself.boxes, J I

    Each box is a sub-box of I

  • pairwiseDisjoint : (↑self.boxes).Pairwise (Disjoint on BoxIntegral.Box.toSet)

    The boxes in a prepartition are pairwise disjoint.

Instances For
    theorem BoxIntegral.Prepartition.le_of_mem' {ι : Type u_1} {I : BoxIntegral.Box ι} (self : BoxIntegral.Prepartition I) (J : BoxIntegral.Box ι) :
    J self.boxesJ I

    Each box is a sub-box of I

    theorem BoxIntegral.Prepartition.pairwiseDisjoint {ι : Type u_1} {I : BoxIntegral.Box ι} (self : BoxIntegral.Prepartition I) :
    (↑self.boxes).Pairwise (Disjoint on BoxIntegral.Box.toSet)

    The boxes in a prepartition are pairwise disjoint.

    Equations
    @[simp]
    theorem BoxIntegral.Prepartition.mem_boxes {ι : Type u_1} {I : BoxIntegral.Box ι} {J : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I) :
    J π.boxes J π
    @[simp]
    theorem BoxIntegral.Prepartition.mem_mk {ι : Type u_1} {I : BoxIntegral.Box ι} {J : BoxIntegral.Box ι} {s : Finset (BoxIntegral.Box ι)} {h₁ : Js, J I} {h₂ : (↑s).Pairwise (Disjoint on BoxIntegral.Box.toSet)} :
    J { boxes := s, le_of_mem' := h₁, pairwiseDisjoint := h₂ } J s
    theorem BoxIntegral.Prepartition.disjoint_coe_of_mem {ι : Type u_1} {I : BoxIntegral.Box ι} {J₁ : BoxIntegral.Box ι} {J₂ : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I) (h₁ : J₁ π) (h₂ : J₂ π) (h : J₁ J₂) :
    Disjoint J₁ J₂
    theorem BoxIntegral.Prepartition.eq_of_mem_of_mem {ι : Type u_1} {I : BoxIntegral.Box ι} {J₁ : BoxIntegral.Box ι} {J₂ : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I) {x : ι} (h₁ : J₁ π) (h₂ : J₂ π) (hx₁ : x J₁) (hx₂ : x J₂) :
    J₁ = J₂
    theorem BoxIntegral.Prepartition.eq_of_le_of_le {ι : Type u_1} {I : BoxIntegral.Box ι} {J : BoxIntegral.Box ι} {J₁ : BoxIntegral.Box ι} {J₂ : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I) (h₁ : J₁ π) (h₂ : J₂ π) (hle₁ : J J₁) (hle₂ : J J₂) :
    J₁ = J₂
    theorem BoxIntegral.Prepartition.eq_of_le {ι : Type u_1} {I : BoxIntegral.Box ι} {J₁ : BoxIntegral.Box ι} {J₂ : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I) (h₁ : J₁ π) (h₂ : J₂ π) (hle : J₁ J₂) :
    J₁ = J₂
    theorem BoxIntegral.Prepartition.lower_le_lower {ι : Type u_1} {I : BoxIntegral.Box ι} {J : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I) (hJ : J π) :
    I.lower J.lower
    theorem BoxIntegral.Prepartition.upper_le_upper {ι : Type u_1} {I : BoxIntegral.Box ι} {J : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I) (hJ : J π) :
    J.upper I.upper
    theorem BoxIntegral.Prepartition.injective_boxes {ι : Type u_1} {I : BoxIntegral.Box ι} :
    Function.Injective BoxIntegral.Prepartition.boxes
    theorem BoxIntegral.Prepartition.ext_iff {ι : Type u_1} {I : BoxIntegral.Box ι} {π₁ : BoxIntegral.Prepartition I} {π₂ : BoxIntegral.Prepartition I} :
    π₁ = π₂ ∀ (J : BoxIntegral.Box ι), J π₁ J π₂
    theorem BoxIntegral.Prepartition.ext {ι : Type u_1} {I : BoxIntegral.Box ι} {π₁ : BoxIntegral.Prepartition I} {π₂ : BoxIntegral.Prepartition I} (h : ∀ (J : BoxIntegral.Box ι), J π₁ J π₂) :
    π₁ = π₂
    @[simp]
    theorem BoxIntegral.Prepartition.single_boxes {ι : Type u_1} (I : BoxIntegral.Box ι) (J : BoxIntegral.Box ι) (h : J I) :

    The singleton prepartition {J}, J ≤ I.

    Equations
    Instances For
      @[simp]

      We say that π ≤ π' if each box of π is a subbox of some box of π'.

      Equations
      Equations
      Equations
      Equations
      Equations
      • BoxIntegral.Prepartition.instInhabited = { default := }
      theorem BoxIntegral.Prepartition.le_def {ι : Type u_1} {I : BoxIntegral.Box ι} {π₁ : BoxIntegral.Prepartition I} {π₂ : BoxIntegral.Prepartition I} :
      π₁ π₂ Jπ₁, J'π₂, J J'
      @[simp]
      theorem BoxIntegral.Prepartition.mem_top {ι : Type u_1} {I : BoxIntegral.Box ι} {J : BoxIntegral.Box ι} :
      J J = I
      @[simp]
      theorem BoxIntegral.Prepartition.top_boxes {ι : Type u_1} {I : BoxIntegral.Box ι} :
      .boxes = {I}
      @[simp]
      @[simp]
      theorem BoxIntegral.Prepartition.bot_boxes {ι : Type u_1} {I : BoxIntegral.Box ι} :
      .boxes =
      theorem BoxIntegral.Prepartition.injOn_setOf_mem_Icc_setOf_lower_eq {ι : Type u_1} {I : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I) (x : ι) :
      Set.InjOn (fun (J : BoxIntegral.Box ι) => {i : ι | J.lower i = x i}) {J : BoxIntegral.Box ι | J π x BoxIntegral.Box.Icc J}

      An auxiliary lemma used to prove that the same point can't belong to more than 2 ^ Fintype.card ι closed boxes of a prepartition.

      theorem BoxIntegral.Prepartition.card_filter_mem_Icc_le {ι : Type u_1} {I : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I) [Fintype ι] (x : ι) :
      (Finset.filter (fun (J : BoxIntegral.Box ι) => x BoxIntegral.Box.Icc J) π.boxes).card 2 ^ Fintype.card ι

      The set of boxes of a prepartition that contain x in their closures has cardinality at most 2 ^ Fintype.card ι.

      Given a prepartition π : BoxIntegral.Prepartition I, π.iUnion is the part of I covered by the boxes of π.

      Equations
      • π.iUnion = Jπ, J
      Instances For
        theorem BoxIntegral.Prepartition.iUnion_def {ι : Type u_1} {I : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I) :
        π.iUnion = Jπ, J
        theorem BoxIntegral.Prepartition.iUnion_def' {ι : Type u_1} {I : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I) :
        π.iUnion = Jπ.boxes, J
        @[simp]
        theorem BoxIntegral.Prepartition.mem_iUnion {ι : Type u_1} {I : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I) {x : ι} :
        x π.iUnion Jπ, x J
        @[simp]
        theorem BoxIntegral.Prepartition.iUnion_single {ι : Type u_1} {I : BoxIntegral.Box ι} {J : BoxIntegral.Box ι} (h : J I) :
        @[simp]
        theorem BoxIntegral.Prepartition.iUnion_top {ι : Type u_1} {I : BoxIntegral.Box ι} :
        .iUnion = I
        @[simp]
        theorem BoxIntegral.Prepartition.iUnion_eq_empty {ι : Type u_1} {I : BoxIntegral.Box ι} {π₁ : BoxIntegral.Prepartition I} :
        π₁.iUnion = π₁ =
        @[simp]
        theorem BoxIntegral.Prepartition.iUnion_bot {ι : Type u_1} {I : BoxIntegral.Box ι} :
        .iUnion =
        theorem BoxIntegral.Prepartition.subset_iUnion {ι : Type u_1} {I : BoxIntegral.Box ι} {J : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I) (h : J π) :
        J π.iUnion
        theorem BoxIntegral.Prepartition.iUnion_mono {ι : Type u_1} {I : BoxIntegral.Box ι} {π₁ : BoxIntegral.Prepartition I} {π₂ : BoxIntegral.Prepartition I} (h : π₁ π₂) :
        π₁.iUnion π₂.iUnion
        theorem BoxIntegral.Prepartition.disjoint_boxes_of_disjoint_iUnion {ι : Type u_1} {I : BoxIntegral.Box ι} {π₁ : BoxIntegral.Prepartition I} {π₂ : BoxIntegral.Prepartition I} (h : Disjoint π₁.iUnion π₂.iUnion) :
        Disjoint π₁.boxes π₂.boxes
        theorem BoxIntegral.Prepartition.le_iff_nonempty_imp_le_and_iUnion_subset {ι : Type u_1} {I : BoxIntegral.Box ι} {π₁ : BoxIntegral.Prepartition I} {π₂ : BoxIntegral.Prepartition I} :
        π₁ π₂ (∀ Jπ₁, J'π₂, (J J').NonemptyJ J') π₁.iUnion π₂.iUnion
        theorem BoxIntegral.Prepartition.eq_of_boxes_subset_iUnion_superset {ι : Type u_1} {I : BoxIntegral.Box ι} {π₁ : BoxIntegral.Prepartition I} {π₂ : BoxIntegral.Prepartition I} (h₁ : π₁.boxes π₂.boxes) (h₂ : π₂.iUnion π₁.iUnion) :
        π₁ = π₂
        @[simp]
        theorem BoxIntegral.Prepartition.biUnion_boxes {ι : Type u_1} {I : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I) (πi : (J : BoxIntegral.Box ι) → BoxIntegral.Prepartition J) :
        (π.biUnion πi).boxes = π.boxes.biUnion fun (J : BoxIntegral.Box ι) => (πi J).boxes

        Given a prepartition π of a box I and a collection of prepartitions πi J of all boxes J ∈ π, returns the prepartition of I into the union of the boxes of all πi J.

        Though we only use the values of πi on the boxes of π, we require πi to be a globally defined function.

        Equations
        • π.biUnion πi = { boxes := π.boxes.biUnion fun (J : BoxIntegral.Box ι) => (πi J).boxes, le_of_mem' := , pairwiseDisjoint := }
        Instances For
          @[simp]
          theorem BoxIntegral.Prepartition.mem_biUnion {ι : Type u_1} {I : BoxIntegral.Box ι} {J : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I) {πi : (J : BoxIntegral.Box ι) → BoxIntegral.Prepartition J} :
          J π.biUnion πi J'π, J πi J'
          theorem BoxIntegral.Prepartition.biUnion_le {ι : Type u_1} {I : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I) (πi : (J : BoxIntegral.Box ι) → BoxIntegral.Prepartition J) :
          π.biUnion πi π
          @[simp]
          theorem BoxIntegral.Prepartition.biUnion_top {ι : Type u_1} {I : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I) :
          (π.biUnion fun (x : BoxIntegral.Box ι) => ) = π
          theorem BoxIntegral.Prepartition.biUnion_congr {ι : Type u_1} {I : BoxIntegral.Box ι} {π₁ : BoxIntegral.Prepartition I} {π₂ : BoxIntegral.Prepartition I} {πi₁ : (J : BoxIntegral.Box ι) → BoxIntegral.Prepartition J} {πi₂ : (J : BoxIntegral.Box ι) → BoxIntegral.Prepartition J} (h : π₁ = π₂) (hi : Jπ₁, πi₁ J = πi₂ J) :
          π₁.biUnion πi₁ = π₂.biUnion πi₂
          theorem BoxIntegral.Prepartition.biUnion_congr_of_le {ι : Type u_1} {I : BoxIntegral.Box ι} {π₁ : BoxIntegral.Prepartition I} {π₂ : BoxIntegral.Prepartition I} {πi₁ : (J : BoxIntegral.Box ι) → BoxIntegral.Prepartition J} {πi₂ : (J : BoxIntegral.Box ι) → BoxIntegral.Prepartition J} (h : π₁ = π₂) (hi : JI, πi₁ J = πi₂ J) :
          π₁.biUnion πi₁ = π₂.biUnion πi₂
          @[simp]
          theorem BoxIntegral.Prepartition.iUnion_biUnion {ι : Type u_1} {I : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I) (πi : (J : BoxIntegral.Box ι) → BoxIntegral.Prepartition J) :
          (π.biUnion πi).iUnion = Jπ, (πi J).iUnion
          @[simp]
          theorem BoxIntegral.Prepartition.sum_biUnion_boxes {ι : Type u_1} {I : BoxIntegral.Box ι} {M : Type u_2} [AddCommMonoid M] (π : BoxIntegral.Prepartition I) (πi : (J : BoxIntegral.Box ι) → BoxIntegral.Prepartition J) (f : BoxIntegral.Box ιM) :
          Jπ.boxes.biUnion fun (J : BoxIntegral.Box ι) => (πi J).boxes, f J = Jπ.boxes, J'(πi J).boxes, f J'

          Given a box J ∈ π.biUnion πi, returns the box J' ∈ π such that J ∈ πi J'. For J ∉ π.biUnion πi, returns I.

          Equations
          • π.biUnionIndex πi J = if hJ : J π.biUnion πi then .choose else I
          Instances For
            theorem BoxIntegral.Prepartition.biUnionIndex_mem {ι : Type u_1} {I : BoxIntegral.Box ι} {J : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I) {πi : (J : BoxIntegral.Box ι) → BoxIntegral.Prepartition J} (hJ : J π.biUnion πi) :
            π.biUnionIndex πi J π
            theorem BoxIntegral.Prepartition.biUnionIndex_le {ι : Type u_1} {I : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I) (πi : (J : BoxIntegral.Box ι) → BoxIntegral.Prepartition J) (J : BoxIntegral.Box ι) :
            π.biUnionIndex πi J I
            theorem BoxIntegral.Prepartition.mem_biUnionIndex {ι : Type u_1} {I : BoxIntegral.Box ι} {J : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I) {πi : (J : BoxIntegral.Box ι) → BoxIntegral.Prepartition J} (hJ : J π.biUnion πi) :
            J πi (π.biUnionIndex πi J)
            theorem BoxIntegral.Prepartition.le_biUnionIndex {ι : Type u_1} {I : BoxIntegral.Box ι} {J : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I) {πi : (J : BoxIntegral.Box ι) → BoxIntegral.Prepartition J} (hJ : J π.biUnion πi) :
            J π.biUnionIndex πi J
            theorem BoxIntegral.Prepartition.biUnionIndex_of_mem {ι : Type u_1} {I : BoxIntegral.Box ι} {J : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I) {πi : (J : BoxIntegral.Box ι) → BoxIntegral.Prepartition J} (hJ : J π) {J' : BoxIntegral.Box ι} (hJ' : J' πi J) :
            π.biUnionIndex πi J' = J

            Uniqueness property of BoxIntegral.Prepartition.biUnionIndex.

            theorem BoxIntegral.Prepartition.biUnion_assoc {ι : Type u_1} {I : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I) (πi : (J : BoxIntegral.Box ι) → BoxIntegral.Prepartition J) (πi' : BoxIntegral.Box ι(J : BoxIntegral.Box ι) → BoxIntegral.Prepartition J) :
            (π.biUnion fun (J : BoxIntegral.Box ι) => (πi J).biUnion (πi' J)) = (π.biUnion πi).biUnion fun (J : BoxIntegral.Box ι) => πi' (π.biUnionIndex πi J) J
            def BoxIntegral.Prepartition.ofWithBot {ι : Type u_1} {I : BoxIntegral.Box ι} (boxes : Finset (WithBot (BoxIntegral.Box ι))) (le_of_mem : Jboxes, J I) (pairwise_disjoint : (↑boxes).Pairwise Disjoint) :

            Create a BoxIntegral.Prepartition from a collection of possibly empty boxes by filtering out the empty one if it exists.

            Equations
            Instances For
              @[simp]
              theorem BoxIntegral.Prepartition.mem_ofWithBot {ι : Type u_1} {I : BoxIntegral.Box ι} {J : BoxIntegral.Box ι} {boxes : Finset (WithBot (BoxIntegral.Box ι))} {h₁ : Jboxes, J I} {h₂ : (↑boxes).Pairwise Disjoint} :
              J BoxIntegral.Prepartition.ofWithBot boxes h₁ h₂ J boxes
              @[simp]
              theorem BoxIntegral.Prepartition.iUnion_ofWithBot {ι : Type u_1} {I : BoxIntegral.Box ι} (boxes : Finset (WithBot (BoxIntegral.Box ι))) (le_of_mem : Jboxes, J I) (pairwise_disjoint : (↑boxes).Pairwise Disjoint) :
              (BoxIntegral.Prepartition.ofWithBot boxes le_of_mem pairwise_disjoint).iUnion = Jboxes, J
              theorem BoxIntegral.Prepartition.ofWithBot_le {ι : Type u_1} {I : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I) {boxes : Finset (WithBot (BoxIntegral.Box ι))} {le_of_mem : Jboxes, J I} {pairwise_disjoint : (↑boxes).Pairwise Disjoint} (H : Jboxes, J J'π, J J') :
              BoxIntegral.Prepartition.ofWithBot boxes le_of_mem pairwise_disjoint π
              theorem BoxIntegral.Prepartition.le_ofWithBot {ι : Type u_1} {I : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I) {boxes : Finset (WithBot (BoxIntegral.Box ι))} {le_of_mem : Jboxes, J I} {pairwise_disjoint : (↑boxes).Pairwise Disjoint} (H : Jπ, J'boxes, J J') :
              π BoxIntegral.Prepartition.ofWithBot boxes le_of_mem pairwise_disjoint
              theorem BoxIntegral.Prepartition.ofWithBot_mono {ι : Type u_1} {I : BoxIntegral.Box ι} {boxes₁ : Finset (WithBot (BoxIntegral.Box ι))} {le_of_mem₁ : Jboxes₁, J I} {pairwise_disjoint₁ : (↑boxes₁).Pairwise Disjoint} {boxes₂ : Finset (WithBot (BoxIntegral.Box ι))} {le_of_mem₂ : Jboxes₂, J I} {pairwise_disjoint₂ : (↑boxes₂).Pairwise Disjoint} (H : Jboxes₁, J J'boxes₂, J J') :
              BoxIntegral.Prepartition.ofWithBot boxes₁ le_of_mem₁ pairwise_disjoint₁ BoxIntegral.Prepartition.ofWithBot boxes₂ le_of_mem₂ pairwise_disjoint₂
              theorem BoxIntegral.Prepartition.sum_ofWithBot {ι : Type u_1} {I : BoxIntegral.Box ι} {M : Type u_2} [AddCommMonoid M] (boxes : Finset (WithBot (BoxIntegral.Box ι))) (le_of_mem : Jboxes, J I) (pairwise_disjoint : (↑boxes).Pairwise Disjoint) (f : BoxIntegral.Box ιM) :
              J(BoxIntegral.Prepartition.ofWithBot boxes le_of_mem pairwise_disjoint).boxes, f J = Jboxes, Option.elim' 0 f J

              Restrict a prepartition to a box.

              Equations
              Instances For
                @[simp]
                theorem BoxIntegral.Prepartition.mem_restrict {ι : Type u_1} {I : BoxIntegral.Box ι} {J : BoxIntegral.Box ι} {J₁ : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I) :
                J₁ π.restrict J J'π, J₁ = J J'
                theorem BoxIntegral.Prepartition.mem_restrict' {ι : Type u_1} {I : BoxIntegral.Box ι} {J : BoxIntegral.Box ι} {J₁ : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I) :
                J₁ π.restrict J J'π, J₁ = J J'
                theorem BoxIntegral.Prepartition.restrict_mono {ι : Type u_1} {I : BoxIntegral.Box ι} {J : BoxIntegral.Box ι} {π₁ : BoxIntegral.Prepartition I} {π₂ : BoxIntegral.Prepartition I} (Hle : π₁ π₂) :
                π₁.restrict J π₂.restrict J
                theorem BoxIntegral.Prepartition.restrict_boxes_of_le {ι : Type u_1} {I : BoxIntegral.Box ι} {J : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I) (h : I J) :
                (π.restrict J).boxes = π.boxes

                Restricting to a larger box does not change the set of boxes. We cannot claim equality of prepartitions because they have different types.

                @[simp]
                theorem BoxIntegral.Prepartition.restrict_self {ι : Type u_1} {I : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I) :
                π.restrict I = π
                @[simp]
                theorem BoxIntegral.Prepartition.iUnion_restrict {ι : Type u_1} {I : BoxIntegral.Box ι} {J : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I) :
                (π.restrict J).iUnion = J π.iUnion
                @[simp]
                theorem BoxIntegral.Prepartition.restrict_biUnion {ι : Type u_1} {I : BoxIntegral.Box ι} {J : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I) (πi : (J : BoxIntegral.Box ι) → BoxIntegral.Prepartition J) (hJ : J π) :
                (π.biUnion πi).restrict J = πi J
                theorem BoxIntegral.Prepartition.biUnion_le_iff {ι : Type u_1} {I : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I) {πi : (J : BoxIntegral.Box ι) → BoxIntegral.Prepartition J} {π' : BoxIntegral.Prepartition I} :
                π.biUnion πi π' Jπ, πi J π'.restrict J
                theorem BoxIntegral.Prepartition.le_biUnion_iff {ι : Type u_1} {I : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I) {πi : (J : BoxIntegral.Box ι) → BoxIntegral.Prepartition J} {π' : BoxIntegral.Prepartition I} :
                π' π.biUnion πi π' π Jπ, π'.restrict J πi J
                Equations
                theorem BoxIntegral.Prepartition.inf_def {ι : Type u_1} {I : BoxIntegral.Box ι} (π₁ : BoxIntegral.Prepartition I) (π₂ : BoxIntegral.Prepartition I) :
                π₁ π₂ = π₁.biUnion fun (J : BoxIntegral.Box ι) => π₂.restrict J
                @[simp]
                theorem BoxIntegral.Prepartition.mem_inf {ι : Type u_1} {I : BoxIntegral.Box ι} {J : BoxIntegral.Box ι} {π₁ : BoxIntegral.Prepartition I} {π₂ : BoxIntegral.Prepartition I} :
                J π₁ π₂ J₁π₁, J₂π₂, J = J₁ J₂
                @[simp]
                theorem BoxIntegral.Prepartition.iUnion_inf {ι : Type u_1} {I : BoxIntegral.Box ι} (π₁ : BoxIntegral.Prepartition I) (π₂ : BoxIntegral.Prepartition I) :
                (π₁ π₂).iUnion = π₁.iUnion π₂.iUnion
                Equations
                @[simp]
                theorem BoxIntegral.Prepartition.filter_boxes {ι : Type u_1} {I : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I) (p : BoxIntegral.Box ιProp) :
                (π.filter p).boxes = Finset.filter (fun (J : BoxIntegral.Box ι) => p J) π.boxes

                The prepartition with boxes {J ∈ π | p J}.

                Equations
                Instances For
                  @[simp]
                  theorem BoxIntegral.Prepartition.mem_filter {ι : Type u_1} {I : BoxIntegral.Box ι} {J : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I) {p : BoxIntegral.Box ιProp} :
                  J π.filter p J π p J
                  theorem BoxIntegral.Prepartition.filter_le {ι : Type u_1} {I : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I) (p : BoxIntegral.Box ιProp) :
                  π.filter p π
                  theorem BoxIntegral.Prepartition.filter_of_true {ι : Type u_1} {I : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I) {p : BoxIntegral.Box ιProp} (hp : Jπ, p J) :
                  π.filter p = π
                  @[simp]
                  theorem BoxIntegral.Prepartition.filter_true {ι : Type u_1} {I : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I) :
                  (π.filter fun (x : BoxIntegral.Box ι) => True) = π
                  @[simp]
                  theorem BoxIntegral.Prepartition.iUnion_filter_not {ι : Type u_1} {I : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I) (p : BoxIntegral.Box ιProp) :
                  (π.filter fun (J : BoxIntegral.Box ι) => ¬p J).iUnion = π.iUnion \ (π.filter p).iUnion
                  theorem BoxIntegral.Prepartition.sum_fiberwise {ι : Type u_1} {I : BoxIntegral.Box ι} {α : Type u_2} {M : Type u_3} [AddCommMonoid M] (π : BoxIntegral.Prepartition I) (f : BoxIntegral.Box ια) (g : BoxIntegral.Box ιM) :
                  yFinset.image f π.boxes, J(π.filter fun (J : BoxIntegral.Box ι) => f J = y).boxes, g J = Jπ.boxes, g J
                  @[simp]
                  theorem BoxIntegral.Prepartition.disjUnion_boxes {ι : Type u_1} {I : BoxIntegral.Box ι} (π₁ : BoxIntegral.Prepartition I) (π₂ : BoxIntegral.Prepartition I) (h : Disjoint π₁.iUnion π₂.iUnion) :
                  (π₁.disjUnion π₂ h).boxes = π₁.boxes π₂.boxes
                  def BoxIntegral.Prepartition.disjUnion {ι : Type u_1} {I : BoxIntegral.Box ι} (π₁ : BoxIntegral.Prepartition I) (π₂ : BoxIntegral.Prepartition I) (h : Disjoint π₁.iUnion π₂.iUnion) :

                  Union of two disjoint prepartitions.

                  Equations
                  • π₁.disjUnion π₂ h = { boxes := π₁.boxes π₂.boxes, le_of_mem' := , pairwiseDisjoint := }
                  Instances For
                    @[simp]
                    theorem BoxIntegral.Prepartition.mem_disjUnion {ι : Type u_1} {I : BoxIntegral.Box ι} {J : BoxIntegral.Box ι} {π₁ : BoxIntegral.Prepartition I} {π₂ : BoxIntegral.Prepartition I} (H : Disjoint π₁.iUnion π₂.iUnion) :
                    J π₁.disjUnion π₂ H J π₁ J π₂
                    @[simp]
                    theorem BoxIntegral.Prepartition.iUnion_disjUnion {ι : Type u_1} {I : BoxIntegral.Box ι} {π₁ : BoxIntegral.Prepartition I} {π₂ : BoxIntegral.Prepartition I} (h : Disjoint π₁.iUnion π₂.iUnion) :
                    (π₁.disjUnion π₂ h).iUnion = π₁.iUnion π₂.iUnion
                    @[simp]
                    theorem BoxIntegral.Prepartition.sum_disj_union_boxes {ι : Type u_1} {I : BoxIntegral.Box ι} {π₁ : BoxIntegral.Prepartition I} {π₂ : BoxIntegral.Prepartition I} {M : Type u_2} [AddCommMonoid M] (h : Disjoint π₁.iUnion π₂.iUnion) (f : BoxIntegral.Box ιM) :
                    Jπ₁.boxes π₂.boxes, f J = Jπ₁.boxes, f J + Jπ₂.boxes, f J

                    The distortion of a prepartition is the maximum of the distortions of the boxes of this prepartition.

                    Equations
                    • π.distortion = π.boxes.sup BoxIntegral.Box.distortion
                    Instances For
                      theorem BoxIntegral.Prepartition.distortion_le_of_mem {ι : Type u_1} {I : BoxIntegral.Box ι} {J : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I) [Fintype ι] (h : J π) :
                      J.distortion π.distortion
                      theorem BoxIntegral.Prepartition.distortion_le_iff {ι : Type u_1} {I : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I) [Fintype ι] {c : NNReal} :
                      π.distortion c Jπ, J.distortion c
                      theorem BoxIntegral.Prepartition.distortion_biUnion {ι : Type u_1} {I : BoxIntegral.Box ι} [Fintype ι] (π : BoxIntegral.Prepartition I) (πi : (J : BoxIntegral.Box ι) → BoxIntegral.Prepartition J) :
                      (π.biUnion πi).distortion = π.boxes.sup fun (J : BoxIntegral.Box ι) => (πi J).distortion
                      @[simp]
                      theorem BoxIntegral.Prepartition.distortion_disjUnion {ι : Type u_1} {I : BoxIntegral.Box ι} {π₁ : BoxIntegral.Prepartition I} {π₂ : BoxIntegral.Prepartition I} [Fintype ι] (h : Disjoint π₁.iUnion π₂.iUnion) :
                      (π₁.disjUnion π₂ h).distortion = max π₁.distortion π₂.distortion
                      theorem BoxIntegral.Prepartition.distortion_of_const {ι : Type u_1} {I : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I) [Fintype ι] {c : NNReal} (h₁ : π.boxes.Nonempty) (h₂ : Jπ, J.distortion = c) :
                      π.distortion = c
                      @[simp]
                      theorem BoxIntegral.Prepartition.distortion_top {ι : Type u_1} [Fintype ι] (I : BoxIntegral.Box ι) :
                      .distortion = I.distortion
                      @[simp]
                      theorem BoxIntegral.Prepartition.distortion_bot {ι : Type u_1} [Fintype ι] (I : BoxIntegral.Box ι) :
                      .distortion = 0

                      A prepartition π of I is a partition if the boxes of π cover the whole I.

                      Equations
                      • π.IsPartition = xI, Jπ, x J
                      Instances For
                        theorem BoxIntegral.Prepartition.isPartition_iff_iUnion_eq {ι : Type u_1} {I : BoxIntegral.Box ι} {π : BoxIntegral.Prepartition I} :
                        π.IsPartition π.iUnion = I
                        @[simp]
                        theorem BoxIntegral.Prepartition.IsPartition.iUnion_eq {ι : Type u_1} {I : BoxIntegral.Box ι} {π : BoxIntegral.Prepartition I} (h : π.IsPartition) :
                        π.iUnion = I
                        theorem BoxIntegral.Prepartition.IsPartition.iUnion_subset {ι : Type u_1} {I : BoxIntegral.Box ι} {π : BoxIntegral.Prepartition I} (h : π.IsPartition) (π₁ : BoxIntegral.Prepartition I) :
                        π₁.iUnion π.iUnion
                        theorem BoxIntegral.Prepartition.IsPartition.existsUnique {ι : Type u_1} {I : BoxIntegral.Box ι} {π : BoxIntegral.Prepartition I} {x : ι} (h : π.IsPartition) (hx : x I) :
                        ∃! J : BoxIntegral.Box ι, J π x J
                        theorem BoxIntegral.Prepartition.IsPartition.nonempty_boxes {ι : Type u_1} {I : BoxIntegral.Box ι} {π : BoxIntegral.Prepartition I} (h : π.IsPartition) :
                        π.boxes.Nonempty
                        theorem BoxIntegral.Prepartition.IsPartition.eq_of_boxes_subset {ι : Type u_1} {I : BoxIntegral.Box ι} {π₁ : BoxIntegral.Prepartition I} {π₂ : BoxIntegral.Prepartition I} (h₁ : π₁.IsPartition) (h₂ : π₁.boxes π₂.boxes) :
                        π₁ = π₂
                        theorem BoxIntegral.Prepartition.IsPartition.le_iff {ι : Type u_1} {I : BoxIntegral.Box ι} {π₁ : BoxIntegral.Prepartition I} {π₂ : BoxIntegral.Prepartition I} (h : π₂.IsPartition) :
                        π₁ π₂ Jπ₁, J'π₂, (J J').NonemptyJ J'
                        theorem BoxIntegral.Prepartition.IsPartition.biUnion {ι : Type u_1} {I : BoxIntegral.Box ι} {π : BoxIntegral.Prepartition I} {πi : (J : BoxIntegral.Box ι) → BoxIntegral.Prepartition J} (h : π.IsPartition) (hi : Jπ, (πi J).IsPartition) :
                        (π.biUnion πi).IsPartition
                        theorem BoxIntegral.Prepartition.IsPartition.restrict {ι : Type u_1} {I : BoxIntegral.Box ι} {J : BoxIntegral.Box ι} {π : BoxIntegral.Prepartition I} (h : π.IsPartition) (hJ : J I) :
                        (π.restrict J).IsPartition
                        theorem BoxIntegral.Prepartition.IsPartition.inf {ι : Type u_1} {I : BoxIntegral.Box ι} {π₁ : BoxIntegral.Prepartition I} {π₂ : BoxIntegral.Prepartition I} (h₁ : π₁.IsPartition) (h₂ : π₂.IsPartition) :
                        (π₁ π₂).IsPartition
                        theorem BoxIntegral.Prepartition.iUnion_biUnion_partition {ι : Type u_1} {I : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I) {πi : (J : BoxIntegral.Box ι) → BoxIntegral.Prepartition J} (h : Jπ, (πi J).IsPartition) :
                        (π.biUnion πi).iUnion = π.iUnion
                        theorem BoxIntegral.Prepartition.isPartitionDisjUnionOfEqDiff {ι : Type u_1} {I : BoxIntegral.Box ι} {π₁ : BoxIntegral.Prepartition I} {π₂ : BoxIntegral.Prepartition I} (h : π₂.iUnion = I \ π₁.iUnion) :
                        (π₁.disjUnion π₂ ).IsPartition