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

• each box J ∈ boxes is a subbox of I;
• the boxes are pairwise disjoint as sets in ℝⁿ.

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:

• BoxIntegral.Prepartition.biUnion: split each box of a partition into smaller boxes;
• BoxIntegral.Prepartition.restrict: restrict a partition to a smaller box.

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

• boxes : Finset (BoxIntegral.Box ι)
• le_of_mem' : ∀ (J : BoxIntegral.Box ι), J ∈ s.boxes → J ≤ I
• pairwiseDisjoint : Set.Pairwise (↑s.boxes) (Disjoint on BoxIntegral.Box.toSet)

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

instance BoxIntegral.Prepartition.instMembershipBoxPrepartition {ι : Type u_1} {I : BoxIntegral.Box ι} : Membership (BoxIntegral.Box ι) (BoxIntegral.Prepartition I)

@[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₁ : ∀ (J : BoxIntegral.Box ι), J ∈ s → 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.le_of_mem {ι : Type u_1} {I : BoxIntegral.Box ι} {J : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I) (hJ : J ∈ π) : J ≤ I

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) : (BoxIntegral.Prepartition.single I J h).boxes = {J}

def BoxIntegral.Prepartition.single {ι : Type u_1} (I : BoxIntegral.Box ι) (J : BoxIntegral.Box ι) (h : J ≤ I) : BoxIntegral.Prepartition I

The singleton prepartition {J}, J ≤ I.

@[simp]

theorem BoxIntegral.Prepartition.mem_single {ι : Type u_1} {I : BoxIntegral.Box ι} {J : BoxIntegral.Box ι} {J' : BoxIntegral.Box ι} (h : J ≤ I) : J' ∈ BoxIntegral.Prepartition.single I J h ↔ J' = J

instance BoxIntegral.Prepartition.instLEPrepartition {ι : Type u_1} {I : BoxIntegral.Box ι} : LE (BoxIntegral.Prepartition I)

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

instance BoxIntegral.Prepartition.partialOrder {ι : Type u_1} {I : BoxIntegral.Box ι} : PartialOrder (BoxIntegral.Prepartition I)

instance BoxIntegral.Prepartition.instOrderTopPrepartitionInstLEPrepartition {ι : Type u_1} {I : BoxIntegral.Box ι} : OrderTop (BoxIntegral.Prepartition I)

instance BoxIntegral.Prepartition.instOrderBotPrepartitionInstLEPrepartition {ι : Type u_1} {I : BoxIntegral.Box ι} : OrderBot (BoxIntegral.Prepartition I)

instance BoxIntegral.Prepartition.instInhabitedPrepartition {ι : Type u_1} {I : BoxIntegral.Box ι} : Inhabited (BoxIntegral.Prepartition I)

theorem BoxIntegral.Prepartition.le_def {ι : Type u_1} {I : BoxIntegral.Box ι} {π₁ : BoxIntegral.Prepartition I} {π₂ : BoxIntegral.Prepartition I} : π₁ ≤ π₂ ↔ ∀ (J : BoxIntegral.Box ι), J ∈ π₁ → ∃ 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]

theorem BoxIntegral.Prepartition.not_mem_bot {ι : Type u_1} {I : BoxIntegral.Box ι} {J : BoxIntegral.Box ι} : ¬J ∈ ⊥

@[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 => {i | BoxIntegral.Box.lower J i = x i}) {J | 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.card (Finset.filter (fun J => x ∈ ↑BoxIntegral.Box.Icc J) π.boxes) ≤ 2 ^ Fintype.card ι

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

def BoxIntegral.Prepartition.iUnion {ι : Type u_1} {I : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I) : Set (ι → ℝ)

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

theorem BoxIntegral.Prepartition.iUnion_def {ι : Type u_1} {I : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I) : BoxIntegral.Prepartition.iUnion π = ⋃ (J : BoxIntegral.Box ι) (_ : J ∈ π), ↑J

theorem BoxIntegral.Prepartition.iUnion_def' {ι : Type u_1} {I : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I) : BoxIntegral.Prepartition.iUnion π = ⋃ (J : BoxIntegral.Box ι) (_ : J ∈ π.boxes), ↑J

@[simp]

theorem BoxIntegral.Prepartition.mem_iUnion {ι : Type u_1} {I : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I) {x : ι → ℝ} : x ∈ BoxIntegral.Prepartition.iUnion π ↔ ∃ J, J ∈ π ∧ x ∈ J

@[simp]

theorem BoxIntegral.Prepartition.iUnion_single {ι : Type u_1} {I : BoxIntegral.Box ι} {J : BoxIntegral.Box ι} (h : J ≤ I) : BoxIntegral.Prepartition.iUnion (BoxIntegral.Prepartition.single I J h) = ↑J

@[simp]

theorem BoxIntegral.Prepartition.iUnion_top {ι : Type u_1} {I : BoxIntegral.Box ι} : BoxIntegral.Prepartition.iUnion ⊤ = ↑I

@[simp]

theorem BoxIntegral.Prepartition.iUnion_eq_empty {ι : Type u_1} {I : BoxIntegral.Box ι} {π₁ : BoxIntegral.Prepartition I} : BoxIntegral.Prepartition.iUnion π₁ = ∅ ↔ π₁ = ⊥

@[simp]

theorem BoxIntegral.Prepartition.iUnion_bot {ι : Type u_1} {I : BoxIntegral.Box ι} : BoxIntegral.Prepartition.iUnion ⊥ = ∅

theorem BoxIntegral.Prepartition.subset_iUnion {ι : Type u_1} {I : BoxIntegral.Box ι} {J : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I) (h : J ∈ π) : ↑J ⊆ BoxIntegral.Prepartition.iUnion π

theorem BoxIntegral.Prepartition.iUnion_subset {ι : Type u_1} {I : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I) : BoxIntegral.Prepartition.iUnion π ⊆ ↑I

theorem BoxIntegral.Prepartition.iUnion_mono {ι : Type u_1} {I : BoxIntegral.Box ι} {π₁ : BoxIntegral.Prepartition I} {π₂ : BoxIntegral.Prepartition I} (h : π₁ ≤ π₂) : BoxIntegral.Prepartition.iUnion π₁ ⊆ BoxIntegral.Prepartition.iUnion π₂

theorem BoxIntegral.Prepartition.disjoint_boxes_of_disjoint_iUnion {ι : Type u_1} {I : BoxIntegral.Box ι} {π₁ : BoxIntegral.Prepartition I} {π₂ : BoxIntegral.Prepartition I} (h : Disjoint (BoxIntegral.Prepartition.iUnion π₁) (BoxIntegral.Prepartition.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 : BoxIntegral.Box ι), J ∈ π₁ → ∀ (J' : BoxIntegral.Box ι), J' ∈ π₂ → Set.Nonempty (↑J ∩ ↑J') → J ≤ J') ∧ BoxIntegral.Prepartition.iUnion π₁ ⊆ BoxIntegral.Prepartition.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₂ : BoxIntegral.Prepartition.iUnion π₂ ⊆ BoxIntegral.Prepartition.iUnion π₁) : π₁ = π₂

@[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 => (πi J).boxes

def BoxIntegral.Prepartition.biUnion {ι : Type u_1} {I : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I) (πi : (J : BoxIntegral.Box ι) → BoxIntegral.Prepartition J) : BoxIntegral.Prepartition I

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.

@[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 ∈ BoxIntegral.Prepartition.biUnion π πi ↔ ∃ J', 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) : BoxIntegral.Prepartition.biUnion π πi ≤ π

@[simp]

theorem BoxIntegral.Prepartition.biUnion_top {ι : Type u_1} {I : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I) : (BoxIntegral.Prepartition.biUnion π fun x => ⊤) = π

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 : BoxIntegral.Box ι), J ∈ π₁ → πi₁ J = πi₂ J) : BoxIntegral.Prepartition.biUnion π₁ πi₁ = BoxIntegral.Prepartition.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 : ∀ (J : BoxIntegral.Box ι), J ≤ I → πi₁ J = πi₂ J) : BoxIntegral.Prepartition.biUnion π₁ πi₁ = BoxIntegral.Prepartition.biUnion π₂ πi₂

@[simp]

theorem BoxIntegral.Prepartition.iUnion_biUnion {ι : Type u_1} {I : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I) (πi : (J : BoxIntegral.Box ι) → BoxIntegral.Prepartition J) : BoxIntegral.Prepartition.iUnion (BoxIntegral.Prepartition.biUnion π πi) = ⋃ (J : BoxIntegral.Box ι) (_ : J ∈ π), BoxIntegral.Prepartition.iUnion (π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 => (πi J).boxes) fun J => f J) = Finset.sum π.boxes fun J => Finset.sum (πi J).boxes fun J' => f J'

def BoxIntegral.Prepartition.biUnionIndex {ι : Type u_1} {I : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I) (πi : (J : BoxIntegral.Box ι) → BoxIntegral.Prepartition J) (J : BoxIntegral.Box ι) : BoxIntegral.Box ι

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

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 ∈ BoxIntegral.Prepartition.biUnion π πi) : BoxIntegral.Prepartition.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 ι) : BoxIntegral.Prepartition.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 ∈ BoxIntegral.Prepartition.biUnion π πi) : J ∈ πi (BoxIntegral.Prepartition.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 ∈ BoxIntegral.Prepartition.biUnion π πi) : J ≤ BoxIntegral.Prepartition.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) : BoxIntegral.Prepartition.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) : (BoxIntegral.Prepartition.biUnion π fun J => BoxIntegral.Prepartition.biUnion (πi J) (πi' J)) = BoxIntegral.Prepartition.biUnion (BoxIntegral.Prepartition.biUnion π πi) fun J => πi' (BoxIntegral.Prepartition.biUnionIndex π πi J) J

def BoxIntegral.Prepartition.ofWithBot {ι : Type u_1} {I : BoxIntegral.Box ι} (boxes : Finset (WithBot (BoxIntegral.Box ι))) (le_of_mem : ∀ (J : WithBot (BoxIntegral.Box ι)), J ∈ boxes → J ≤ ↑I) (pairwise_disjoint : Set.Pairwise (↑boxes) Disjoint) : BoxIntegral.Prepartition I

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

@[simp]

theorem BoxIntegral.Prepartition.mem_ofWithBot {ι : Type u_1} {I : BoxIntegral.Box ι} {J : BoxIntegral.Box ι} {boxes : Finset (WithBot (BoxIntegral.Box ι))} {h₁ : ∀ (J : WithBot (BoxIntegral.Box ι)), J ∈ boxes → 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 : ∀ (J : WithBot (BoxIntegral.Box ι)), J ∈ boxes → J ≤ ↑I) (pairwise_disjoint : Set.Pairwise (↑boxes) Disjoint) : BoxIntegral.Prepartition.iUnion (BoxIntegral.Prepartition.ofWithBot boxes le_of_mem pairwise_disjoint) = ⋃ (J : WithBot (BoxIntegral.Box ι)) (_ : 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 : ∀ (J : WithBot (BoxIntegral.Box ι)), J ∈ boxes → J ≤ ↑I} {pairwise_disjoint : Set.Pairwise (↑boxes) Disjoint} (H : ∀ (J : WithBot (BoxIntegral.Box ι)), J ∈ boxes → J ≠ ⊥ → ∃ 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 : ∀ (J : WithBot (BoxIntegral.Box ι)), J ∈ boxes → J ≤ ↑I} {pairwise_disjoint : Set.Pairwise (↑boxes) Disjoint} (H : ∀ (J : BoxIntegral.Box ι), J ∈ π → ∃ 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₁ : ∀ (J : WithBot (BoxIntegral.Box ι)), J ∈ boxes₁ → J ≤ ↑I} {pairwise_disjoint₁ : Set.Pairwise (↑boxes₁) Disjoint} {boxes₂ : Finset (WithBot (BoxIntegral.Box ι))} {le_of_mem₂ : ∀ (J : WithBot (BoxIntegral.Box ι)), J ∈ boxes₂ → J ≤ ↑I} {pairwise_disjoint₂ : Set.Pairwise (↑boxes₂) Disjoint} (H : ∀ (J : WithBot (BoxIntegral.Box ι)), J ∈ boxes₁ → J ≠ ⊥ → ∃ 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 : ∀ (J : WithBot (BoxIntegral.Box ι)), J ∈ boxes → 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 => f J) = Finset.sum boxes fun J => Option.elim' 0 f J

def BoxIntegral.Prepartition.restrict {ι : Type u_1} {I : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I) (J : BoxIntegral.Box ι) : BoxIntegral.Prepartition J

Restrict a prepartition to a box.

@[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 ⊓ ↑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 ∩ ↑J'

theorem BoxIntegral.Prepartition.restrict_mono {ι : Type u_1} {I : BoxIntegral.Box ι} {J : BoxIntegral.Box ι} {π₁ : BoxIntegral.Prepartition I} {π₂ : BoxIntegral.Prepartition I} (Hle : π₁ ≤ π₂) : BoxIntegral.Prepartition.restrict π₁ J ≤ BoxIntegral.Prepartition.restrict π₂ J

theorem BoxIntegral.Prepartition.monotone_restrict {ι : Type u_1} {I : BoxIntegral.Box ι} {J : BoxIntegral.Box ι} : Monotone fun π => BoxIntegral.Prepartition.restrict π J

theorem BoxIntegral.Prepartition.restrict_boxes_of_le {ι : Type u_1} {I : BoxIntegral.Box ι} {J : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I) (h : I ≤ J) : (BoxIntegral.Prepartition.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) : BoxIntegral.Prepartition.restrict π I = π

@[simp]

theorem BoxIntegral.Prepartition.iUnion_restrict {ι : Type u_1} {I : BoxIntegral.Box ι} {J : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I) : BoxIntegral.Prepartition.iUnion (BoxIntegral.Prepartition.restrict π J) = ↑J ∩ BoxIntegral.Prepartition.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 ∈ π) : BoxIntegral.Prepartition.restrict (BoxIntegral.Prepartition.biUnion π πi) 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} : BoxIntegral.Prepartition.biUnion π πi ≤ π' ↔ ∀ (J : BoxIntegral.Box ι), J ∈ π → πi J ≤ BoxIntegral.Prepartition.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} : π' ≤ BoxIntegral.Prepartition.biUnion π πi ↔ π' ≤ π ∧ ∀ (J : BoxIntegral.Box ι), J ∈ π → BoxIntegral.Prepartition.restrict π' J ≤ πi J

instance BoxIntegral.Prepartition.inf {ι : Type u_1} {I : BoxIntegral.Box ι} : Inf (BoxIntegral.Prepartition I)

theorem BoxIntegral.Prepartition.inf_def {ι : Type u_1} {I : BoxIntegral.Box ι} (π₁ : BoxIntegral.Prepartition I) (π₂ : BoxIntegral.Prepartition I) : π₁ ⊓ π₂ = BoxIntegral.Prepartition.biUnion π₁ fun J => BoxIntegral.Prepartition.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 = ↑J₁ ⊓ ↑J₂

@[simp]

theorem BoxIntegral.Prepartition.iUnion_inf {ι : Type u_1} {I : BoxIntegral.Box ι} (π₁ : BoxIntegral.Prepartition I) (π₂ : BoxIntegral.Prepartition I) : BoxIntegral.Prepartition.iUnion (π₁ ⊓ π₂) = BoxIntegral.Prepartition.iUnion π₁ ∩ BoxIntegral.Prepartition.iUnion π₂

instance BoxIntegral.Prepartition.instSemilatticeInfPrepartition {ι : Type u_1} {I : BoxIntegral.Box ι} : SemilatticeInf (BoxIntegral.Prepartition I)

@[simp]

theorem BoxIntegral.Prepartition.filter_boxes {ι : Type u_1} {I : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I) (p : BoxIntegral.Box ι → Prop) : (BoxIntegral.Prepartition.filter π p).boxes = Finset.filter p π.boxes

def BoxIntegral.Prepartition.filter {ι : Type u_1} {I : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I) (p : BoxIntegral.Box ι → Prop) : BoxIntegral.Prepartition I

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

@[simp]

theorem BoxIntegral.Prepartition.mem_filter {ι : Type u_1} {I : BoxIntegral.Box ι} {J : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I) {p : BoxIntegral.Box ι → Prop} : J ∈ BoxIntegral.Prepartition.filter π p ↔ J ∈ π ∧ p J

theorem BoxIntegral.Prepartition.filter_le {ι : Type u_1} {I : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I) (p : BoxIntegral.Box ι → Prop) : BoxIntegral.Prepartition.filter π p ≤ π

theorem BoxIntegral.Prepartition.filter_of_true {ι : Type u_1} {I : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I) {p : BoxIntegral.Box ι → Prop} (hp : (J : BoxIntegral.Box ι) → J ∈ π → p J) : BoxIntegral.Prepartition.filter π p = π

@[simp]

theorem BoxIntegral.Prepartition.filter_true {ι : Type u_1} {I : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I) : (BoxIntegral.Prepartition.filter π fun x => True) = π

@[simp]

theorem BoxIntegral.Prepartition.iUnion_filter_not {ι : Type u_1} {I : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I) (p : BoxIntegral.Box ι → Prop) : BoxIntegral.Prepartition.iUnion (BoxIntegral.Prepartition.filter π fun J => ¬p J) = BoxIntegral.Prepartition.iUnion π \ BoxIntegral.Prepartition.iUnion (BoxIntegral.Prepartition.filter π p)

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 => f J = y).boxes fun J => g J) = Finset.sum π.boxes fun J => g J

@[simp]

theorem BoxIntegral.Prepartition.disjUnion_boxes {ι : Type u_1} {I : BoxIntegral.Box ι} (π₁ : BoxIntegral.Prepartition I) (π₂ : BoxIntegral.Prepartition I) (h : Disjoint (BoxIntegral.Prepartition.iUnion π₁) (BoxIntegral.Prepartition.iUnion π₂)) : (BoxIntegral.Prepartition.disjUnion π₁ π₂ h).boxes = π₁.boxes ∪ π₂.boxes

def BoxIntegral.Prepartition.disjUnion {ι : Type u_1} {I : BoxIntegral.Box ι} (π₁ : BoxIntegral.Prepartition I) (π₂ : BoxIntegral.Prepartition I) (h : Disjoint (BoxIntegral.Prepartition.iUnion π₁) (BoxIntegral.Prepartition.iUnion π₂)) : BoxIntegral.Prepartition I

Union of two disjoint prepartitions.

@[simp]

theorem BoxIntegral.Prepartition.mem_disjUnion {ι : Type u_1} {I : BoxIntegral.Box ι} {J : BoxIntegral.Box ι} {π₁ : BoxIntegral.Prepartition I} {π₂ : BoxIntegral.Prepartition I} (H : Disjoint (BoxIntegral.Prepartition.iUnion π₁) (BoxIntegral.Prepartition.iUnion π₂)) : J ∈ BoxIntegral.Prepartition.disjUnion π₁ π₂ H ↔ J ∈ π₁ ∨ J ∈ π₂

@[simp]

theorem BoxIntegral.Prepartition.iUnion_disjUnion {ι : Type u_1} {I : BoxIntegral.Box ι} {π₁ : BoxIntegral.Prepartition I} {π₂ : BoxIntegral.Prepartition I} (h : Disjoint (BoxIntegral.Prepartition.iUnion π₁) (BoxIntegral.Prepartition.iUnion π₂)) : BoxIntegral.Prepartition.iUnion (BoxIntegral.Prepartition.disjUnion π₁ π₂ h) = BoxIntegral.Prepartition.iUnion π₁ ∪ BoxIntegral.Prepartition.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 (BoxIntegral.Prepartition.iUnion π₁) (BoxIntegral.Prepartition.iUnion π₂)) (f : BoxIntegral.Box ι → M) : (Finset.sum (π₁.boxes ∪ π₂.boxes) fun J => f J) = (Finset.sum π₁.boxes fun J => f J) + Finset.sum π₂.boxes fun J => f J

def BoxIntegral.Prepartition.distortion {ι : Type u_1} {I : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I) [Fintype ι] : NNReal

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

theorem BoxIntegral.Prepartition.distortion_le_of_mem {ι : Type u_1} {I : BoxIntegral.Box ι} {J : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I) [Fintype ι] (h : J ∈ π) : BoxIntegral.Box.distortion J ≤ BoxIntegral.Prepartition.distortion π

theorem BoxIntegral.Prepartition.distortion_le_iff {ι : Type u_1} {I : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I) [Fintype ι] {c : NNReal} : BoxIntegral.Prepartition.distortion π ≤ c ↔ ∀ (J : BoxIntegral.Box ι), J ∈ π → BoxIntegral.Box.distortion J ≤ c

theorem BoxIntegral.Prepartition.distortion_biUnion {ι : Type u_1} {I : BoxIntegral.Box ι} [Fintype ι] (π : BoxIntegral.Prepartition I) (πi : (J : BoxIntegral.Box ι) → BoxIntegral.Prepartition J) : BoxIntegral.Prepartition.distortion (BoxIntegral.Prepartition.biUnion π πi) = Finset.sup π.boxes fun J => BoxIntegral.Prepartition.distortion (πi J)

@[simp]

theorem BoxIntegral.Prepartition.distortion_disjUnion {ι : Type u_1} {I : BoxIntegral.Box ι} {π₁ : BoxIntegral.Prepartition I} {π₂ : BoxIntegral.Prepartition I} [Fintype ι] (h : Disjoint (BoxIntegral.Prepartition.iUnion π₁) (BoxIntegral.Prepartition.iUnion π₂)) : BoxIntegral.Prepartition.distortion (BoxIntegral.Prepartition.disjUnion π₁ π₂ h) = max (BoxIntegral.Prepartition.distortion π₁) (BoxIntegral.Prepartition.distortion π₂)

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

@[simp]

theorem BoxIntegral.Prepartition.distortion_top {ι : Type u_1} [Fintype ι] (I : BoxIntegral.Box ι) : BoxIntegral.Prepartition.distortion ⊤ = BoxIntegral.Box.distortion I

@[simp]

theorem BoxIntegral.Prepartition.distortion_bot {ι : Type u_1} [Fintype ι] (I : BoxIntegral.Box ι) : BoxIntegral.Prepartition.distortion ⊥ = 0

def BoxIntegral.Prepartition.IsPartition {ι : Type u_1} {I : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I) : Prop

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

theorem BoxIntegral.Prepartition.isPartition_iff_iUnion_eq {ι : Type u_1} {I : BoxIntegral.Box ι} {π : BoxIntegral.Prepartition I} : BoxIntegral.Prepartition.IsPartition π ↔ BoxIntegral.Prepartition.iUnion π = ↑I

@[simp]

theorem BoxIntegral.Prepartition.isPartition_single_iff {ι : Type u_1} {I : BoxIntegral.Box ι} {J : BoxIntegral.Box ι} (h : J ≤ I) : BoxIntegral.Prepartition.IsPartition (BoxIntegral.Prepartition.single I J h) ↔ J = I

theorem BoxIntegral.Prepartition.isPartitionTop {ι : Type u_1} (I : BoxIntegral.Box ι) : BoxIntegral.Prepartition.IsPartition ⊤

theorem BoxIntegral.Prepartition.IsPartition.iUnion_eq {ι : Type u_1} {I : BoxIntegral.Box ι} {π : BoxIntegral.Prepartition I} (h : BoxIntegral.Prepartition.IsPartition π) : BoxIntegral.Prepartition.iUnion π = ↑I

theorem BoxIntegral.Prepartition.IsPartition.iUnion_subset {ι : Type u_1} {I : BoxIntegral.Box ι} {π : BoxIntegral.Prepartition I} (h : BoxIntegral.Prepartition.IsPartition π) (π₁ : BoxIntegral.Prepartition I) : BoxIntegral.Prepartition.iUnion π₁ ⊆ BoxIntegral.Prepartition.iUnion π

theorem BoxIntegral.Prepartition.IsPartition.existsUnique {ι : Type u_1} {I : BoxIntegral.Box ι} {π : BoxIntegral.Prepartition I} {x : ι → ℝ} (h : BoxIntegral.Prepartition.IsPartition π) (hx : x ∈ I) : ∃! J x, x ∈ J

theorem BoxIntegral.Prepartition.IsPartition.nonempty_boxes {ι : Type u_1} {I : BoxIntegral.Box ι} {π : BoxIntegral.Prepartition I} (h : BoxIntegral.Prepartition.IsPartition π) : Finset.Nonempty π.boxes

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 : BoxIntegral.Box ι), J ∈ π₁ → ∀ (J' : BoxIntegral.Box ι), J' ∈ π₂ → Set.Nonempty (↑J ∩ ↑J') → J ≤ J'

theorem BoxIntegral.Prepartition.IsPartition.biUnion {ι : Type u_1} {I : BoxIntegral.Box ι} {π : BoxIntegral.Prepartition I} {πi : (J : BoxIntegral.Box ι) → BoxIntegral.Prepartition J} (h : BoxIntegral.Prepartition.IsPartition π) (hi : ∀ (J : BoxIntegral.Box ι), J ∈ π → BoxIntegral.Prepartition.IsPartition (πi J)) : BoxIntegral.Prepartition.IsPartition (BoxIntegral.Prepartition.biUnion π πi)

theorem BoxIntegral.Prepartition.IsPartition.restrict {ι : Type u_1} {I : BoxIntegral.Box ι} {J : BoxIntegral.Box ι} {π : BoxIntegral.Prepartition I} (h : BoxIntegral.Prepartition.IsPartition π) (hJ : J ≤ I) : BoxIntegral.Prepartition.IsPartition (BoxIntegral.Prepartition.restrict π J)

theorem BoxIntegral.Prepartition.IsPartition.inf {ι : Type u_1} {I : BoxIntegral.Box ι} {π₁ : BoxIntegral.Prepartition I} {π₂ : BoxIntegral.Prepartition I} (h₁ : BoxIntegral.Prepartition.IsPartition π₁) (h₂ : BoxIntegral.Prepartition.IsPartition π₂) : BoxIntegral.Prepartition.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 : BoxIntegral.Box ι), J ∈ π → BoxIntegral.Prepartition.IsPartition (πi J)) : BoxIntegral.Prepartition.iUnion (BoxIntegral.Prepartition.biUnion π πi) = BoxIntegral.Prepartition.iUnion π

theorem BoxIntegral.Prepartition.isPartitionDisjUnionOfEqDiff {ι : Type u_1} {I : BoxIntegral.Box ι} {π₁ : BoxIntegral.Prepartition I} {π₂ : BoxIntegral.Prepartition I} (h : BoxIntegral.Prepartition.iUnion π₂ = ↑I \ BoxIntegral.Prepartition.iUnion π₁) : BoxIntegral.Prepartition.IsPartition (BoxIntegral.Prepartition.disjUnion π₁ π₂ (_ : Disjoint (BoxIntegral.Prepartition.iUnion π₁) (BoxIntegral.Prepartition.iUnion π₂)))