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

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' : ∀ J ∈ self.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.

theorem BoxIntegral.Prepartition.le_of_mem' {ι : Type u_1} {I : BoxIntegral.Box ι} (self : BoxIntegral.Prepartition I) (J : BoxIntegral.Box ι) : J ∈ self.boxes → J ≤ 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.

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

Equations

• BoxIntegral.Prepartition.instMembershipBox = { mem := fun (J : BoxIntegral.Box ι) (π : BoxIntegral.Prepartition I) => J ∈ π.boxes }

@[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 ∈ s, 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.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.

Equations

• BoxIntegral.Prepartition.single I J h = { boxes := {J}, le_of_mem' := ⋯, pairwiseDisjoint := ⋯ }

@[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.instLE {ι : Type u_1} {I : BoxIntegral.Box ι} : LE (BoxIntegral.Prepartition I)

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

Equations

• BoxIntegral.Prepartition.instLE = { le := fun (π π' : BoxIntegral.Prepartition I) => ∀ ⦃I_1 : BoxIntegral.Box ι⦄, I_1 ∈ π → ∃ I' ∈ π', I_1 ≤ I' }

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

Equations

• BoxIntegral.Prepartition.partialOrder = PartialOrder.mk ⋯

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

Equations

• BoxIntegral.Prepartition.instOrderTop = OrderTop.mk ⋯

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

Equations

• BoxIntegral.Prepartition.instOrderBot = OrderBot.mk ⋯

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

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]

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 : 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 ι.

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 π.

Equations

• π.iUnion = ⋃ J ∈ π, ↑J

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) : (BoxIntegral.Prepartition.single I J h).iUnion = ↑J

@[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_subset {ι : Type u_1} {I : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I) : π.iUnion ⊆ ↑I

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').Nonempty → J ≤ 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

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.

Equations

• π.biUnion πi = { boxes := π.boxes.biUnion fun (J : BoxIntegral.Box ι) => (πi J).boxes, le_of_mem' := ⋯, pairwiseDisjoint := ⋯ }

@[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 : ∀ J ≤ I, π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'

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.

Equations

• π.biUnionIndex πi J = if hJ : J ∈ π.biUnion πi then ⋯.choose else 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 ∈ π.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 : ∀ J ∈ boxes, J ≤ ↑I) (pairwise_disjoint : (↑boxes).Pairwise Disjoint) : BoxIntegral.Prepartition I

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

Equations

• BoxIntegral.Prepartition.ofWithBot boxes le_of_mem pairwise_disjoint = { boxes := Finset.eraseNone boxes, le_of_mem' := ⋯, pairwiseDisjoint := ⋯ }

@[simp]

theorem BoxIntegral.Prepartition.mem_ofWithBot {ι : Type u_1} {I : BoxIntegral.Box ι} {J : BoxIntegral.Box ι} {boxes : Finset (WithBot (BoxIntegral.Box ι))} {h₁ : ∀ J ∈ boxes, 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 : ∀ J ∈ boxes, J ≤ ↑I) (pairwise_disjoint : (↑boxes).Pairwise Disjoint) : (BoxIntegral.Prepartition.ofWithBot boxes le_of_mem pairwise_disjoint).iUnion = ⋃ 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 ∈ boxes, J ≤ ↑I} {pairwise_disjoint : (↑boxes).Pairwise Disjoint} (H : ∀ J ∈ boxes, 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 ∈ boxes, 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₁ : ∀ J ∈ boxes₁, J ≤ ↑I} {pairwise_disjoint₁ : (↑boxes₁).Pairwise Disjoint} {boxes₂ : Finset (WithBot (BoxIntegral.Box ι))} {le_of_mem₂ : ∀ J ∈ boxes₂, J ≤ ↑I} {pairwise_disjoint₂ : (↑boxes₂).Pairwise Disjoint} (H : ∀ J ∈ boxes₁, 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 ∈ boxes, J ≤ ↑I) (pairwise_disjoint : (↑boxes).Pairwise Disjoint) (f : BoxIntegral.Box ι → M) : ∑ J ∈ (BoxIntegral.Prepartition.ofWithBot boxes le_of_mem pairwise_disjoint).boxes, f J = ∑ J ∈ boxes, 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.

Equations

• π.restrict J = BoxIntegral.Prepartition.ofWithBot (Finset.image (fun (J' : BoxIntegral.Box ι) => ↑J ⊓ ↑J') π.boxes) ⋯ ⋯

@[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.monotone_restrict {ι : Type u_1} {I : BoxIntegral.Box ι} {J : BoxIntegral.Box ι} : Monotone fun (π : BoxIntegral.Prepartition I) => π.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

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

Equations

• BoxIntegral.Prepartition.inf = { inf := fun (π₁ π₂ : BoxIntegral.Prepartition I) => π₁.biUnion fun (J : BoxIntegral.Box ι) => π₂.restrict J }

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

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

Equations

• BoxIntegral.Prepartition.instSemilatticeInf = let __src := BoxIntegral.Prepartition.inf; let __src_1 := BoxIntegral.Prepartition.partialOrder; SemilatticeInf.mk ⋯ ⋯ ⋯

@[simp]

theorem BoxIntegral.Prepartition.filter_boxes {ι : Type u_1} {I : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I) (p : BoxIntegral.Box ι → Prop) : (π.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}.

Equations

• π.filter p = { boxes := Finset.filter p π.boxes, le_of_mem' := ⋯, pairwiseDisjoint := ⋯ }

@[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) : ∑ y ∈ Finset.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) : BoxIntegral.Prepartition I

Union of two disjoint prepartitions.

Equations

• π₁.disjUnion π₂ h = { boxes := π₁.boxes ∪ π₂.boxes, le_of_mem' := ⋯, pairwiseDisjoint := ⋯ }

@[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

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.

Equations

• π.distortion = π.boxes.sup BoxIntegral.Box.distortion

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

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.

Equations

• π.IsPartition = ∀ x ∈ I, ∃ J ∈ π, x ∈ J

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

@[simp]

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

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

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').Nonempty → J ≤ 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