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.

Instances For
    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₂ : Set.Pairwise (s) (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 {ι : 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
      • BoxIntegral.Prepartition.instOrderTopPrepartitionInstLEPrepartition = OrderTop.mk
      Equations
      • BoxIntegral.Prepartition.instOrderBotPrepartitionInstLEPrepartition = OrderBot.mk
      Equations
      • BoxIntegral.Prepartition.instInhabitedPrepartition = { 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
      Instances For
        @[simp]
        theorem BoxIntegral.Prepartition.mem_iUnion {ι : Type u_1} {I : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I) {x : ι} :
        @[simp]
        theorem BoxIntegral.Prepartition.biUnion_boxes {ι : Type u_1} {I : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I) (πi : (J : BoxIntegral.Box ι) → BoxIntegral.Prepartition J) :
        (BoxIntegral.Prepartition.biUnion π πi).boxes = Finset.biUnion π.boxes 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
        Instances For
          @[simp]
          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) :
          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) :
          @[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) :
          (Finset.sum (Finset.biUnion π.boxes fun (J : BoxIntegral.Box ι) => (πi J).boxes) fun (J : BoxIntegral.Box ι) => f J) = Finset.sum π.boxes fun (J : BoxIntegral.Box ι) => Finset.sum (πi J).boxes fun (J' : BoxIntegral.Box ι) => f J'

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

          Equations
          Instances For
            def BoxIntegral.Prepartition.ofWithBot {ι : Type u_1} {I : BoxIntegral.Box ι} (boxes : Finset (WithBot (BoxIntegral.Box ι))) (le_of_mem : Jboxes, J I) (pairwise_disjoint : Set.Pairwise (boxes) 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₂ : Set.Pairwise (boxes) 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 : Set.Pairwise (boxes) Disjoint) :
              BoxIntegral.Prepartition.iUnion (BoxIntegral.Prepartition.ofWithBot boxes le_of_mem pairwise_disjoint) = ⋃ J ∈ boxes, 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 : Set.Pairwise (boxes) 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 : Set.Pairwise (boxes) 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₁ : Set.Pairwise (boxes₁) Disjoint} {boxes₂ : Finset (WithBot (BoxIntegral.Box ι))} {le_of_mem₂ : Jboxes₂, J I} {pairwise_disjoint₂ : Set.Pairwise (boxes₂) 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 : Set.Pairwise (boxes) Disjoint) (f : BoxIntegral.Box ιM) :
              (Finset.sum (BoxIntegral.Prepartition.ofWithBot boxes le_of_mem pairwise_disjoint).boxes fun (J : BoxIntegral.Box ι) => f J) = Finset.sum boxes fun (J : WithBot (BoxIntegral.Box ι)) => 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₁ BoxIntegral.Prepartition.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₁ BoxIntegral.Prepartition.restrict π J ∃ J' ∈ π, J₁ = J J'

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

                Equations
                • One or more equations did not get rendered due to their size.
                @[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₂
                Equations
                • BoxIntegral.Prepartition.instSemilatticeInfPrepartition = let __src := BoxIntegral.Prepartition.inf; let __src_1 := BoxIntegral.Prepartition.partialOrder; SemilatticeInf.mk

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

                Equations
                Instances For
                  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) :
                  (Finset.sum (Finset.image f π.boxes) fun (y : α) => Finset.sum (BoxIntegral.Prepartition.filter π fun (J : BoxIntegral.Box ι) => f J = y).boxes fun (J : BoxIntegral.Box ι) => g J) = Finset.sum π.boxes fun (J : BoxIntegral.Box ι) => g J

                  Union of two disjoint prepartitions.

                  Equations
                  Instances For
                    @[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 (BoxIntegral.Prepartition.iUnion π₁) (BoxIntegral.Prepartition.iUnion π₂)) (f : BoxIntegral.Box ιM) :
                    (Finset.sum (π₁.boxes π₂.boxes) fun (J : BoxIntegral.Box ι) => f J) = (Finset.sum π₁.boxes fun (J : BoxIntegral.Box ι) => f J) + Finset.sum π₂.boxes fun (J : BoxIntegral.Box ι) => f J

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

                    Equations
                    Instances For
                      theorem BoxIntegral.Prepartition.distortion_of_const {ι : Type u_1} {I : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I) [Fintype ι] {c : NNReal} (h₁ : π.boxes.Nonempty) (h₂ : Jπ, BoxIntegral.Box.distortion J = c) :

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

                      Equations
                      Instances For
                        theorem BoxIntegral.Prepartition.IsPartition.existsUnique {ι : Type u_1} {I : BoxIntegral.Box ι} {π : BoxIntegral.Prepartition I} {x : ι} (h : BoxIntegral.Prepartition.IsPartition π) (hx : x I) :
                        ∃! (J : BoxIntegral.Box ι), ∃! (x_1 : J π), x J
                        theorem BoxIntegral.Prepartition.IsPartition.eq_of_boxes_subset {ι : Type u_1} {I : BoxIntegral.Box ι} {π₁ : BoxIntegral.Prepartition I} {π₂ : BoxIntegral.Prepartition I} (h₁ : BoxIntegral.Prepartition.IsPartition π₁) (h₂ : π₁.boxes π₂.boxes) :
                        π₁ = π₂
                        theorem BoxIntegral.Prepartition.IsPartition.le_iff {ι : Type u_1} {I : BoxIntegral.Box ι} {π₁ : BoxIntegral.Prepartition I} {π₂ : BoxIntegral.Prepartition I} (h : BoxIntegral.Prepartition.IsPartition π₂) :
                        π₁ π₂ Jπ₁, J'π₂, Set.Nonempty (J J')J J'