# 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 : ) extends :
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 :
• le_of_mem' : Jself.boxes, J I
• pairwiseDisjoint : (self.boxes).Pairwise (Disjoint on BoxIntegral.Box.toSet)
• tag : ι

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 : ), self.tag J BoxIntegral.Box.Icc I

Each tagged point belongs to I

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

Each tagged point belongs to I

Equations
• BoxIntegral.TaggedPrepartition.instMembershipBox = { mem := fun (J : ) (π : ) => J π.boxes }
@[simp]
theorem BoxIntegral.TaggedPrepartition.mem_toPrepartition {ι : Type u_1} {I : } {J : } :
J π.toPrepartition J π
@[simp]
theorem BoxIntegral.TaggedPrepartition.mem_mk {ι : Type u_1} {I : } {J : } (π : ) (f : ι) (h : ∀ (J : ), f J BoxIntegral.Box.Icc I) :
J { toPrepartition := π, tag := f, tag_mem_Icc := h } J π
def BoxIntegral.TaggedPrepartition.iUnion {ι : Type u_1} {I : } :
Set (ι)

Union of all boxes of a tagged prepartition.

Equations
• π.iUnion = π.iUnion
Instances For
theorem BoxIntegral.TaggedPrepartition.iUnion_def {ι : Type u_1} {I : } :
π.iUnion = Jπ, J
@[simp]
theorem BoxIntegral.TaggedPrepartition.iUnion_mk {ι : Type u_1} {I : } (π : ) (f : ι) (h : ∀ (J : ), 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 : } :
π.iUnion = π.iUnion
@[simp]
theorem BoxIntegral.TaggedPrepartition.mem_iUnion {ι : Type u_1} {I : } {x : ι} :
x π.iUnion Jπ, x J
theorem BoxIntegral.TaggedPrepartition.subset_iUnion {ι : Type u_1} {I : } {J : } (h : J π) :
J π.iUnion
theorem BoxIntegral.TaggedPrepartition.iUnion_subset {ι : Type u_1} {I : } :
π.iUnion I

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

Equations
• π.IsPartition = π.IsPartition
Instances For
theorem BoxIntegral.TaggedPrepartition.isPartition_iff_iUnion_eq {ι : Type u_1} {I : } :
π.IsPartition π.iUnion = I
@[simp]
theorem BoxIntegral.TaggedPrepartition.filter_tag {ι : Type u_1} {I : } (p : ) :
(π.filter p).tag = π.tag
@[simp]
theorem BoxIntegral.TaggedPrepartition.filter_boxes_val {ι : Type u_1} {I : } (p : ) :
(π.filter p).boxes.val = Multiset.filter p π.boxes.val
def BoxIntegral.TaggedPrepartition.filter {ι : Type u_1} {I : } (p : ) :

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

Equations
• π.filter p = { toPrepartition := π.filter p, tag := π.tag, tag_mem_Icc := }
Instances For
@[simp]
theorem BoxIntegral.TaggedPrepartition.mem_filter {ι : Type u_1} {I : } {J : } {p : } :
J π.filter p J π p J
@[simp]
theorem BoxIntegral.TaggedPrepartition.iUnion_filter_not {ι : Type u_1} {I : } (p : ) :
(π.filter fun (J : ) => ¬p J).iUnion = π.iUnion \ (π.filter p).iUnion
def BoxIntegral.Prepartition.biUnionTagged {ι : Type u_1} {I : } (π : ) (π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.
Instances For
@[simp]
theorem BoxIntegral.Prepartition.mem_biUnionTagged {ι : Type u_1} {I : } {J : } (π : ) {πi : } :
J π.biUnionTagged πi J'π, J πi J'
theorem BoxIntegral.Prepartition.tag_biUnionTagged {ι : Type u_1} {I : } {J : } (π : ) {πi : } (hJ : J π) {J' : } (hJ' : J' πi J) :
(π.biUnionTagged πi).tag J' = (πi J).tag J'
@[simp]
theorem BoxIntegral.Prepartition.iUnion_biUnionTagged {ι : Type u_1} {I : } (π : ) (πi : ) :
(π.biUnionTagged πi).iUnion = Jπ, (πi J).iUnion
theorem BoxIntegral.Prepartition.forall_biUnionTagged {ι : Type u_1} {I : } (p : (ι)) (π : ) (πi : ) :
(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 : } {π : } (h : π.IsPartition) {πi : } (hi : Jπ, (πi J).IsPartition) :
(π.biUnionTagged πi).IsPartition
@[simp]
theorem BoxIntegral.TaggedPrepartition.biUnionPrepartition_tag {ι : Type u_1} {I : } (πi : (J : ) → ) :
(π.biUnionPrepartition πi).tag = fun (J : ) => π.tag (π.biUnionIndex πi J)
def BoxIntegral.TaggedPrepartition.biUnionPrepartition {ι : Type u_1} {I : } (πi : (J : ) → ) :

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 : ) => π.tag (π.biUnionIndex πi J), tag_mem_Icc := }
Instances For
theorem BoxIntegral.TaggedPrepartition.IsPartition.biUnionPrepartition {ι : Type u_1} {I : } (h : π.IsPartition) {πi : (J : ) → } (hi : Jπ, (πi J).IsPartition) :
(π.biUnionPrepartition πi).IsPartition
def BoxIntegral.TaggedPrepartition.infPrepartition {ι : Type u_1} {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 : ) => π'.restrict J
Instances For
@[simp]
theorem BoxIntegral.TaggedPrepartition.infPrepartition_toPrepartition {ι : Type u_1} {I : } (π' : ) :
(π.infPrepartition π').toPrepartition = π.toPrepartition π'
theorem BoxIntegral.TaggedPrepartition.mem_infPrepartition_comm {ι : Type u_1} {I : } {J : } {π₁ : } {π₂ : } :
J π₁.infPrepartition π₂.toPrepartition J π₂.infPrepartition π₁.toPrepartition
theorem BoxIntegral.TaggedPrepartition.IsPartition.infPrepartition {ι : Type u_1} {I : } {π₁ : } (h₁ : π₁.IsPartition) {π₂ : } (h₂ : π₂.IsPartition) :
(π₁.infPrepartition π₂).IsPartition

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
Instances For
@[simp]
theorem BoxIntegral.TaggedPrepartition.isHenstock_biUnionTagged {ι : Type u_1} {I : } {π : } {πi : } :
(π.biUnionTagged πi).IsHenstock Jπ, (πi J).IsHenstock
theorem BoxIntegral.TaggedPrepartition.IsHenstock.card_filter_tag_eq_le {ι : Type u_1} {I : } [] (h : π.IsHenstock) (x : ι) :
(Finset.filter (fun (J : ) => π.tag J = x) π.boxes).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 : } [] (r : (ι)()) :

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))
Instances For
@[simp]
theorem BoxIntegral.TaggedPrepartition.isSubordinate_biUnionTagged {ι : Type u_1} {I : } {r : (ι)()} [] {π : } {πi : } :
(π.biUnionTagged πi).IsSubordinate r Jπ, (πi J).IsSubordinate r
theorem BoxIntegral.TaggedPrepartition.IsSubordinate.biUnionPrepartition {ι : Type u_1} {I : } {r : (ι)()} [] (h : π.IsSubordinate r) (πi : (J : ) → ) :
(π.biUnionPrepartition πi).IsSubordinate r
theorem BoxIntegral.TaggedPrepartition.IsSubordinate.infPrepartition {ι : Type u_1} {I : } {r : (ι)()} [] (h : π.IsSubordinate r) (π' : ) :
(π.infPrepartition π').IsSubordinate r
theorem BoxIntegral.TaggedPrepartition.IsSubordinate.mono' {ι : Type u_1} {I : } {r₁ : (ι)()} {r₂ : (ι)()} [] (hr₁ : π.IsSubordinate r₁) (h : Jπ, r₁ (π.tag J) r₂ (π.tag J)) :
π.IsSubordinate r₂
theorem BoxIntegral.TaggedPrepartition.IsSubordinate.mono {ι : Type u_1} {I : } {r₁ : (ι)()} {r₂ : (ι)()} [] (hr₁ : π.IsSubordinate r₁) (h : xBoxIntegral.Box.Icc I, r₁ x r₂ x) :
π.IsSubordinate r₂
theorem BoxIntegral.TaggedPrepartition.IsSubordinate.diam_le {ι : Type u_1} {I : } {J : } {r : (ι)()} [] (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 : ) (J : ) (hJ : J I) (x : ι) (h : x BoxIntegral.Box.Icc I) :
().boxes.val = {J}
@[simp]
theorem BoxIntegral.TaggedPrepartition.single_tag {ι : Type u_1} (I : ) (J : ) (hJ : J I) (x : ι) (h : x BoxIntegral.Box.Icc I) :
().tag = fun (x_1 : ) => x
def BoxIntegral.TaggedPrepartition.single {ι : Type u_1} (I : ) (J : ) (hJ : J I) (x : ι) (h : x BoxIntegral.Box.Icc I) :

Tagged prepartition with single box and prescribed tag.

Equations
• = { toPrepartition := , tag := fun (x_1 : ) => x, tag_mem_Icc := }
Instances For
@[simp]
theorem BoxIntegral.TaggedPrepartition.mem_single {ι : Type u_1} {I : } {J : } {x : ι} {J' : } (hJ : J I) (h : x BoxIntegral.Box.Icc I) :
J' J' = J
Equations
theorem BoxIntegral.TaggedPrepartition.isPartition_single_iff {ι : Type u_1} {I : } {J : } {x : ι} (hJ : J I) (h : x BoxIntegral.Box.Icc I) :
().IsPartition J = I
theorem BoxIntegral.TaggedPrepartition.isPartition_single {ι : Type u_1} {I : } {x : ι} (h : x BoxIntegral.Box.Icc I) :
().IsPartition
theorem BoxIntegral.TaggedPrepartition.forall_mem_single {ι : Type u_1} {I : } {J : } {x : ι} (p : (ι)) (hJ : J I) (h : x BoxIntegral.Box.Icc I) :
(J', p (().tag J') J') p x J
@[simp]
theorem BoxIntegral.TaggedPrepartition.isHenstock_single_iff {ι : Type u_1} {I : } {J : } {x : ι} (hJ : J I) (h : x BoxIntegral.Box.Icc I) :
().IsHenstock x BoxIntegral.Box.Icc J
theorem BoxIntegral.TaggedPrepartition.isHenstock_single {ι : Type u_1} {I : } {x : ι} (h : x BoxIntegral.Box.Icc I) :
().IsHenstock
@[simp]
theorem BoxIntegral.TaggedPrepartition.isSubordinate_single {ι : Type u_1} {I : } {J : } {x : ι} {r : (ι)()} [] (hJ : J I) (h : x BoxIntegral.Box.Icc I) :
().IsSubordinate r BoxIntegral.Box.Icc J Metric.closedBall x (r x)
@[simp]
theorem BoxIntegral.TaggedPrepartition.iUnion_single {ι : Type u_1} {I : } {J : } {x : ι} (hJ : J I) (h : x BoxIntegral.Box.Icc I) :
().iUnion = J
def BoxIntegral.TaggedPrepartition.disjUnion {ι : Type u_1} {I : } (π₁ : ) (π₂ : ) (h : Disjoint π₁.iUnion π₂.iUnion) :

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 := }
Instances For
@[simp]
theorem BoxIntegral.TaggedPrepartition.disjUnion_boxes {ι : Type u_1} {I : } {π₁ : } {π₂ : } (h : Disjoint π₁.iUnion π₂.iUnion) :
(π₁.disjUnion π₂ h).boxes = π₁.boxes π₂.boxes
@[simp]
theorem BoxIntegral.TaggedPrepartition.mem_disjUnion {ι : Type u_1} {I : } {J : } {π₁ : } {π₂ : } (h : Disjoint π₁.iUnion π₂.iUnion) :
J π₁.disjUnion π₂ h J π₁ J π₂
@[simp]
theorem BoxIntegral.TaggedPrepartition.iUnion_disjUnion {ι : Type u_1} {I : } {π₁ : } {π₂ : } (h : Disjoint π₁.iUnion π₂.iUnion) :
(π₁.disjUnion π₂ h).iUnion = π₁.iUnion π₂.iUnion
theorem BoxIntegral.TaggedPrepartition.disjUnion_tag_of_mem_left {ι : Type u_1} {I : } {J : } {π₁ : } {π₂ : } (h : Disjoint π₁.iUnion π₂.iUnion) (hJ : J π₁) :
(π₁.disjUnion π₂ h).tag J = π₁.tag J
theorem BoxIntegral.TaggedPrepartition.disjUnion_tag_of_mem_right {ι : Type u_1} {I : } {J : } {π₁ : } {π₂ : } (h : Disjoint π₁.iUnion π₂.iUnion) (hJ : J π₂) :
(π₁.disjUnion π₂ h).tag J = π₂.tag J
theorem BoxIntegral.TaggedPrepartition.IsSubordinate.disjUnion {ι : Type u_1} {I : } {π₁ : } {π₂ : } {r : (ι)()} [] (h₁ : π₁.IsSubordinate r) (h₂ : π₂.IsSubordinate r) (h : Disjoint π₁.iUnion π₂.iUnion) :
(π₁.disjUnion π₂ h).IsSubordinate r
theorem BoxIntegral.TaggedPrepartition.IsHenstock.disjUnion {ι : Type u_1} {I : } {π₁ : } {π₂ : } (h₁ : π₁.IsHenstock) (h₂ : π₂.IsHenstock) (h : Disjoint π₁.iUnion π₂.iUnion) :
(π₁.disjUnion π₂ h).IsHenstock
def BoxIntegral.TaggedPrepartition.embedBox {ι : Type u_1} (I : ) (J : ) (h : I 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.
Instances For

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

Equations
• π.distortion = π.distortion
Instances For
theorem BoxIntegral.TaggedPrepartition.distortion_le_of_mem {ι : Type u_1} {I : } {J : } [] (h : J π) :
J.distortion π.distortion
theorem BoxIntegral.TaggedPrepartition.distortion_le_iff {ι : Type u_1} {I : } [] {c : NNReal} :
π.distortion c Jπ, J.distortion c
@[simp]
theorem BoxIntegral.Prepartition.distortion_biUnionTagged {ι : Type u_1} {I : } [] (π : ) (πi : ) :
(π.biUnionTagged πi).distortion = π.boxes.sup fun (J : ) => (πi J).distortion
@[simp]
theorem BoxIntegral.TaggedPrepartition.distortion_biUnionPrepartition {ι : Type u_1} {I : } [] (πi : (J : ) → ) :
(π.biUnionPrepartition πi).distortion = π.boxes.sup fun (J : ) => (πi J).distortion
@[simp]
theorem BoxIntegral.TaggedPrepartition.distortion_disjUnion {ι : Type u_1} {I : } {π₁ : } {π₂ : } [] (h : Disjoint π₁.iUnion π₂.iUnion) :
(π₁.disjUnion π₂ h).distortion = max π₁.distortion π₂.distortion
theorem BoxIntegral.TaggedPrepartition.distortion_of_const {ι : Type u_1} {I : } [] {c : NNReal} (h₁ : π.boxes.Nonempty) (h₂ : Jπ, J.distortion = c) :
π.distortion = c
@[simp]
theorem BoxIntegral.TaggedPrepartition.distortion_single {ι : Type u_1} {I : } {J : } {x : ι} [] (hJ : J I) (h : x BoxIntegral.Box.Icc I) :
().distortion = J.distortion
theorem BoxIntegral.TaggedPrepartition.distortion_filter_le {ι : Type u_1} {I : } [] (p : ) :
(π.filter p).distortion π.distortion