Tagged partitions

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

Tags

rectangular box, box partition

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

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

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

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

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

  Each tagged point belongs to I

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

Each tagged point belongs to I

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

Equations

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

@[simp]

theorem BoxIntegral.TaggedPrepartition.mem_toPrepartition {ι : Type u_1} {I : BoxIntegral.Box ι} {J : BoxIntegral.Box ι} {π : BoxIntegral.TaggedPrepartition I} : J ∈ π.toPrepartition ↔ J ∈ π

@[simp]

theorem BoxIntegral.TaggedPrepartition.mem_mk {ι : Type u_1} {I : BoxIntegral.Box ι} {J : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I) (f : BoxIntegral.Box ι → ι → ℝ) (h : ∀ (J : BoxIntegral.Box ι), f J ∈ BoxIntegral.Box.Icc I) : J ∈ { toPrepartition := π, tag := f, tag_mem_Icc := h } ↔ J ∈ π

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

Union of all boxes of a tagged prepartition.

Equations

• π.iUnion = π.iUnion

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

@[simp]

theorem BoxIntegral.TaggedPrepartition.iUnion_mk {ι : Type u_1} {I : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I) (f : BoxIntegral.Box ι → ι → ℝ) (h : ∀ (J : BoxIntegral.Box ι), f J ∈ BoxIntegral.Box.Icc I) : { toPrepartition := π, tag := f, tag_mem_Icc := h }.iUnion = π.iUnion

@[simp]

theorem BoxIntegral.TaggedPrepartition.iUnion_toPrepartition {ι : Type u_1} {I : BoxIntegral.Box ι} (π : BoxIntegral.TaggedPrepartition I) : π.iUnion = π.iUnion

@[simp]

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

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

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

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

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

Equations

• π.IsPartition = π.IsPartition

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

@[simp]

theorem BoxIntegral.TaggedPrepartition.filter_tag {ι : Type u_1} {I : BoxIntegral.Box ι} (π : BoxIntegral.TaggedPrepartition I) (p : BoxIntegral.Box ι → Prop) : (π.filter p).tag = π.tag

@[simp]

theorem BoxIntegral.TaggedPrepartition.filter_boxes_val {ι : Type u_1} {I : BoxIntegral.Box ι} (π : BoxIntegral.TaggedPrepartition I) (p : BoxIntegral.Box ι → Prop) : (π.filter p).boxes.val = Multiset.filter p π.boxes.val

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

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

Equations

• π.filter p = { toPrepartition := π.filter p, tag := π.tag, tag_mem_Icc := ⋯ }

@[simp]

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

@[simp]

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

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

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

Equations

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

@[simp]

theorem BoxIntegral.Prepartition.mem_biUnionTagged {ι : Type u_1} {I : BoxIntegral.Box ι} {J : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I) {πi : (J : BoxIntegral.Box ι) → BoxIntegral.TaggedPrepartition J} : J ∈ π.biUnionTagged πi ↔ ∃ J' ∈ π, J ∈ πi J'

theorem BoxIntegral.Prepartition.tag_biUnionTagged {ι : Type u_1} {I : BoxIntegral.Box ι} {J : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I) {πi : (J : BoxIntegral.Box ι) → BoxIntegral.TaggedPrepartition J} (hJ : J ∈ π) {J' : BoxIntegral.Box ι} (hJ' : J' ∈ πi J) : (π.biUnionTagged πi).tag J' = (πi J).tag J'

@[simp]

theorem BoxIntegral.Prepartition.iUnion_biUnionTagged {ι : Type u_1} {I : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I) (πi : (J : BoxIntegral.Box ι) → BoxIntegral.TaggedPrepartition J) : (π.biUnionTagged πi).iUnion = ⋃ J ∈ π, (πi J).iUnion

theorem BoxIntegral.Prepartition.forall_biUnionTagged {ι : Type u_1} {I : BoxIntegral.Box ι} (p : (ι → ℝ) → BoxIntegral.Box ι → Prop) (π : BoxIntegral.Prepartition I) (πi : (J : BoxIntegral.Box ι) → BoxIntegral.TaggedPrepartition J) : (∀ J ∈ π.biUnionTagged πi, p ((π.biUnionTagged πi).tag J) J) ↔ ∀ J ∈ π, ∀ J' ∈ πi J, p ((πi J).tag J') J'

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

@[simp]

theorem BoxIntegral.TaggedPrepartition.biUnionPrepartition_tag {ι : Type u_1} {I : BoxIntegral.Box ι} (π : BoxIntegral.TaggedPrepartition I) (πi : (J : BoxIntegral.Box ι) → BoxIntegral.Prepartition J) : (π.biUnionPrepartition πi).tag = fun (J : BoxIntegral.Box ι) => π.tag (π.biUnionIndex πi J)

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

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

Note that usually the result is not a Henstock partition.

Equations

• π.biUnionPrepartition πi = { toPrepartition := π.biUnion πi, tag := fun (J : BoxIntegral.Box ι) => π.tag (π.biUnionIndex πi J), tag_mem_Icc := ⋯ }

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

def BoxIntegral.TaggedPrepartition.infPrepartition {ι : Type u_1} {I : BoxIntegral.Box ι} (π : BoxIntegral.TaggedPrepartition I) (π' : BoxIntegral.Prepartition I) : BoxIntegral.TaggedPrepartition I

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

Note that usually the result is not a Henstock partition.

Equations

• π.infPrepartition π' = π.biUnionPrepartition fun (J : BoxIntegral.Box ι) => π'.restrict J

@[simp]

theorem BoxIntegral.TaggedPrepartition.infPrepartition_toPrepartition {ι : Type u_1} {I : BoxIntegral.Box ι} (π : BoxIntegral.TaggedPrepartition I) (π' : BoxIntegral.Prepartition I) : (π.infPrepartition π').toPrepartition = π.toPrepartition ⊓ π'

theorem BoxIntegral.TaggedPrepartition.mem_infPrepartition_comm {ι : Type u_1} {I : BoxIntegral.Box ι} {J : BoxIntegral.Box ι} {π₁ : BoxIntegral.TaggedPrepartition I} {π₂ : BoxIntegral.TaggedPrepartition I} : J ∈ π₁.infPrepartition π₂.toPrepartition ↔ J ∈ π₂.infPrepartition π₁.toPrepartition

theorem BoxIntegral.TaggedPrepartition.IsPartition.infPrepartition {ι : Type u_1} {I : BoxIntegral.Box ι} {π₁ : BoxIntegral.TaggedPrepartition I} (h₁ : π₁.IsPartition) {π₂ : BoxIntegral.Prepartition I} (h₂ : π₂.IsPartition) : (π₁.infPrepartition π₂).IsPartition

def BoxIntegral.TaggedPrepartition.IsHenstock {ι : Type u_1} {I : BoxIntegral.Box ι} (π : BoxIntegral.TaggedPrepartition I) : Prop

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

Equations

• π.IsHenstock = ∀ J ∈ π, π.tag J ∈ BoxIntegral.Box.Icc J

@[simp]

theorem BoxIntegral.TaggedPrepartition.isHenstock_biUnionTagged {ι : Type u_1} {I : BoxIntegral.Box ι} {π : BoxIntegral.Prepartition I} {πi : (J : BoxIntegral.Box ι) → BoxIntegral.TaggedPrepartition J} : (π.biUnionTagged πi).IsHenstock ↔ ∀ J ∈ π, (πi J).IsHenstock

theorem BoxIntegral.TaggedPrepartition.IsHenstock.card_filter_tag_eq_le {ι : Type u_1} {I : BoxIntegral.Box ι} {π : BoxIntegral.TaggedPrepartition I} [Fintype ι] (h : π.IsHenstock) (x : ι → ℝ) : (Finset.filter (fun (J : BoxIntegral.Box ι) => π.tag J = x) π.boxes).card ≤ 2 ^ Fintype.card ι

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

def BoxIntegral.TaggedPrepartition.IsSubordinate {ι : Type u_1} {I : BoxIntegral.Box ι} [Fintype ι] (π : BoxIntegral.TaggedPrepartition I) (r : (ι → ℝ) → ↑(Set.Ioi 0)) : Prop

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

Equations

• π.IsSubordinate r = ∀ J ∈ π, BoxIntegral.Box.Icc J ⊆ Metric.closedBall (π.tag J) ↑(r (π.tag J))

@[simp]

theorem BoxIntegral.TaggedPrepartition.isSubordinate_biUnionTagged {ι : Type u_1} {I : BoxIntegral.Box ι} {r : (ι → ℝ) → ↑(Set.Ioi 0)} [Fintype ι] {π : BoxIntegral.Prepartition I} {πi : (J : BoxIntegral.Box ι) → BoxIntegral.TaggedPrepartition J} : (π.biUnionTagged πi).IsSubordinate r ↔ ∀ J ∈ π, (πi J).IsSubordinate r

theorem BoxIntegral.TaggedPrepartition.IsSubordinate.biUnionPrepartition {ι : Type u_1} {I : BoxIntegral.Box ι} {π : BoxIntegral.TaggedPrepartition I} {r : (ι → ℝ) → ↑(Set.Ioi 0)} [Fintype ι] (h : π.IsSubordinate r) (πi : (J : BoxIntegral.Box ι) → BoxIntegral.Prepartition J) : (π.biUnionPrepartition πi).IsSubordinate r

theorem BoxIntegral.TaggedPrepartition.IsSubordinate.infPrepartition {ι : Type u_1} {I : BoxIntegral.Box ι} {π : BoxIntegral.TaggedPrepartition I} {r : (ι → ℝ) → ↑(Set.Ioi 0)} [Fintype ι] (h : π.IsSubordinate r) (π' : BoxIntegral.Prepartition I) : (π.infPrepartition π').IsSubordinate r

theorem BoxIntegral.TaggedPrepartition.IsSubordinate.mono' {ι : Type u_1} {I : BoxIntegral.Box ι} {r₁ : (ι → ℝ) → ↑(Set.Ioi 0)} {r₂ : (ι → ℝ) → ↑(Set.Ioi 0)} [Fintype ι] {π : BoxIntegral.TaggedPrepartition I} (hr₁ : π.IsSubordinate r₁) (h : ∀ J ∈ π, r₁ (π.tag J) ≤ r₂ (π.tag J)) : π.IsSubordinate r₂

theorem BoxIntegral.TaggedPrepartition.IsSubordinate.mono {ι : Type u_1} {I : BoxIntegral.Box ι} {r₁ : (ι → ℝ) → ↑(Set.Ioi 0)} {r₂ : (ι → ℝ) → ↑(Set.Ioi 0)} [Fintype ι] {π : BoxIntegral.TaggedPrepartition I} (hr₁ : π.IsSubordinate r₁) (h : ∀ x ∈ BoxIntegral.Box.Icc I, r₁ x ≤ r₂ x) : π.IsSubordinate r₂

theorem BoxIntegral.TaggedPrepartition.IsSubordinate.diam_le {ι : Type u_1} {I : BoxIntegral.Box ι} {J : BoxIntegral.Box ι} {r : (ι → ℝ) → ↑(Set.Ioi 0)} [Fintype ι] {π : BoxIntegral.TaggedPrepartition I} (h : π.IsSubordinate r) (hJ : J ∈ π.boxes) : Metric.diam (BoxIntegral.Box.Icc J) ≤ 2 * ↑(r (π.tag J))

@[simp]

theorem BoxIntegral.TaggedPrepartition.single_boxes_val {ι : Type u_1} (I : BoxIntegral.Box ι) (J : BoxIntegral.Box ι) (hJ : J ≤ I) (x : ι → ℝ) (h : x ∈ BoxIntegral.Box.Icc I) : (BoxIntegral.TaggedPrepartition.single I J hJ x h).boxes.val = {J}

@[simp]

theorem BoxIntegral.TaggedPrepartition.single_tag {ι : Type u_1} (I : BoxIntegral.Box ι) (J : BoxIntegral.Box ι) (hJ : J ≤ I) (x : ι → ℝ) (h : x ∈ BoxIntegral.Box.Icc I) : (BoxIntegral.TaggedPrepartition.single I J hJ x h).tag = fun (x_1 : BoxIntegral.Box ι) => x

def BoxIntegral.TaggedPrepartition.single {ι : Type u_1} (I : BoxIntegral.Box ι) (J : BoxIntegral.Box ι) (hJ : J ≤ I) (x : ι → ℝ) (h : x ∈ BoxIntegral.Box.Icc I) : BoxIntegral.TaggedPrepartition I

Tagged prepartition with single box and prescribed tag.

Equations

• BoxIntegral.TaggedPrepartition.single I J hJ x h = { toPrepartition := BoxIntegral.Prepartition.single I J hJ, tag := fun (x_1 : BoxIntegral.Box ι) => x, tag_mem_Icc := ⋯ }

@[simp]

theorem BoxIntegral.TaggedPrepartition.mem_single {ι : Type u_1} {I : BoxIntegral.Box ι} {J : BoxIntegral.Box ι} {x : ι → ℝ} {J' : BoxIntegral.Box ι} (hJ : J ≤ I) (h : x ∈ BoxIntegral.Box.Icc I) : J' ∈ BoxIntegral.TaggedPrepartition.single I J hJ x h ↔ J' = J

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

Equations

• BoxIntegral.TaggedPrepartition.instInhabited I = { default := BoxIntegral.TaggedPrepartition.single I I ⋯ I.upper ⋯ }

theorem BoxIntegral.TaggedPrepartition.isPartition_single_iff {ι : Type u_1} {I : BoxIntegral.Box ι} {J : BoxIntegral.Box ι} {x : ι → ℝ} (hJ : J ≤ I) (h : x ∈ BoxIntegral.Box.Icc I) : (BoxIntegral.TaggedPrepartition.single I J hJ x h).IsPartition ↔ J = I

theorem BoxIntegral.TaggedPrepartition.isPartition_single {ι : Type u_1} {I : BoxIntegral.Box ι} {x : ι → ℝ} (h : x ∈ BoxIntegral.Box.Icc I) : (BoxIntegral.TaggedPrepartition.single I I ⋯ x h).IsPartition

theorem BoxIntegral.TaggedPrepartition.forall_mem_single {ι : Type u_1} {I : BoxIntegral.Box ι} {J : BoxIntegral.Box ι} {x : ι → ℝ} (p : (ι → ℝ) → BoxIntegral.Box ι → Prop) (hJ : J ≤ I) (h : x ∈ BoxIntegral.Box.Icc I) : (∀ J' ∈ BoxIntegral.TaggedPrepartition.single I J hJ x h, p ((BoxIntegral.TaggedPrepartition.single I J hJ x h).tag J') J') ↔ p x J

@[simp]

theorem BoxIntegral.TaggedPrepartition.isHenstock_single_iff {ι : Type u_1} {I : BoxIntegral.Box ι} {J : BoxIntegral.Box ι} {x : ι → ℝ} (hJ : J ≤ I) (h : x ∈ BoxIntegral.Box.Icc I) : (BoxIntegral.TaggedPrepartition.single I J hJ x h).IsHenstock ↔ x ∈ BoxIntegral.Box.Icc J

theorem BoxIntegral.TaggedPrepartition.isHenstock_single {ι : Type u_1} {I : BoxIntegral.Box ι} {x : ι → ℝ} (h : x ∈ BoxIntegral.Box.Icc I) : (BoxIntegral.TaggedPrepartition.single I I ⋯ x h).IsHenstock

@[simp]

theorem BoxIntegral.TaggedPrepartition.isSubordinate_single {ι : Type u_1} {I : BoxIntegral.Box ι} {J : BoxIntegral.Box ι} {x : ι → ℝ} {r : (ι → ℝ) → ↑(Set.Ioi 0)} [Fintype ι] (hJ : J ≤ I) (h : x ∈ BoxIntegral.Box.Icc I) : (BoxIntegral.TaggedPrepartition.single I J hJ x h).IsSubordinate r ↔ BoxIntegral.Box.Icc J ⊆ Metric.closedBall x ↑(r x)

@[simp]

theorem BoxIntegral.TaggedPrepartition.iUnion_single {ι : Type u_1} {I : BoxIntegral.Box ι} {J : BoxIntegral.Box ι} {x : ι → ℝ} (hJ : J ≤ I) (h : x ∈ BoxIntegral.Box.Icc I) : (BoxIntegral.TaggedPrepartition.single I J hJ x h).iUnion = ↑J

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

Union of two tagged prepartitions with disjoint unions of boxes.

Equations

• π₁.disjUnion π₂ h = { toPrepartition := π₁.disjUnion π₂.toPrepartition h, tag := π₁.boxes.piecewise π₁.tag π₂.tag, tag_mem_Icc := ⋯ }

@[simp]

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

@[simp]

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

@[simp]

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

theorem BoxIntegral.TaggedPrepartition.disjUnion_tag_of_mem_left {ι : Type u_1} {I : BoxIntegral.Box ι} {J : BoxIntegral.Box ι} {π₁ : BoxIntegral.TaggedPrepartition I} {π₂ : BoxIntegral.TaggedPrepartition I} (h : Disjoint π₁.iUnion π₂.iUnion) (hJ : J ∈ π₁) : (π₁.disjUnion π₂ h).tag J = π₁.tag J

theorem BoxIntegral.TaggedPrepartition.disjUnion_tag_of_mem_right {ι : Type u_1} {I : BoxIntegral.Box ι} {J : BoxIntegral.Box ι} {π₁ : BoxIntegral.TaggedPrepartition I} {π₂ : BoxIntegral.TaggedPrepartition I} (h : Disjoint π₁.iUnion π₂.iUnion) (hJ : J ∈ π₂) : (π₁.disjUnion π₂ h).tag J = π₂.tag J

theorem BoxIntegral.TaggedPrepartition.IsSubordinate.disjUnion {ι : Type u_1} {I : BoxIntegral.Box ι} {π₁ : BoxIntegral.TaggedPrepartition I} {π₂ : BoxIntegral.TaggedPrepartition I} {r : (ι → ℝ) → ↑(Set.Ioi 0)} [Fintype ι] (h₁ : π₁.IsSubordinate r) (h₂ : π₂.IsSubordinate r) (h : Disjoint π₁.iUnion π₂.iUnion) : (π₁.disjUnion π₂ h).IsSubordinate r

theorem BoxIntegral.TaggedPrepartition.IsHenstock.disjUnion {ι : Type u_1} {I : BoxIntegral.Box ι} {π₁ : BoxIntegral.TaggedPrepartition I} {π₂ : BoxIntegral.TaggedPrepartition I} (h₁ : π₁.IsHenstock) (h₂ : π₂.IsHenstock) (h : Disjoint π₁.iUnion π₂.iUnion) : (π₁.disjUnion π₂ h).IsHenstock

def BoxIntegral.TaggedPrepartition.embedBox {ι : Type u_1} (I : BoxIntegral.Box ι) (J : BoxIntegral.Box ι) (h : I ≤ J) : BoxIntegral.TaggedPrepartition I ↪ BoxIntegral.TaggedPrepartition J

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

Equations

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

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

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

Equations

• π.distortion = π.distortion

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

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

@[simp]

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

@[simp]

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

@[simp]

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

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

@[simp]

theorem BoxIntegral.TaggedPrepartition.distortion_single {ι : Type u_1} {I : BoxIntegral.Box ι} {J : BoxIntegral.Box ι} {x : ι → ℝ} [Fintype ι] (hJ : J ≤ I) (h : x ∈ BoxIntegral.Box.Icc I) : (BoxIntegral.TaggedPrepartition.single I J hJ x h).distortion = J.distortion

theorem BoxIntegral.TaggedPrepartition.distortion_filter_le {ι : Type u_1} {I : BoxIntegral.Box ι} (π : BoxIntegral.TaggedPrepartition I) [Fintype ι] (p : BoxIntegral.Box ι → Prop) : (π.filter p).distortion ≤ π.distortion