# Documentation

Mathlib.Analysis.BoxIntegral.Partition.Tagged

# 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
• boxes :
• le_of_mem' : ∀ (J : ), J s.boxesJ I
• pairwiseDisjoint : Set.Pairwise (s.boxes) (Disjoint on BoxIntegral.Box.toSet)
• tag : ι
• tag_mem_Icc : ∀ (J : ), BoxIntegral.Box.Icc I

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.

Instances For
@[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.

Instances For
theorem BoxIntegral.TaggedPrepartition.iUnion_def {ι : Type u_1} {I : } :
= ⋃ (J : ) (_ : J π), J
@[simp]
theorem BoxIntegral.TaggedPrepartition.iUnion_mk {ι : Type u_1} {I : } (π : ) (f : ι) (h : ∀ (J : ), f J BoxIntegral.Box.Icc I) :
BoxIntegral.TaggedPrepartition.iUnion { toPrepartition := π, tag := f, tag_mem_Icc := h } =
@[simp]
theorem BoxIntegral.TaggedPrepartition.mem_iUnion {ι : Type u_1} {I : } {x : ι} :
J, J π x J
theorem BoxIntegral.TaggedPrepartition.subset_iUnion {ι : Type u_1} {I : } {J : } (h : J π) :

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

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

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

Instances For
@[simp]
theorem BoxIntegral.TaggedPrepartition.mem_filter {ι : Type u_1} {I : } {J : } {p : } :
J π p J
@[simp]
theorem BoxIntegral.TaggedPrepartition.iUnion_filter_not {ι : Type u_1} {I : } (p : ) :
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.

Instances For
@[simp]
theorem BoxIntegral.Prepartition.mem_biUnionTagged {ι : Type u_1} {I : } {J : } (π : ) {πi : } :
J', J' π J πi J'
theorem BoxIntegral.Prepartition.tag_biUnionTagged {ι : Type u_1} {I : } {J : } (π : ) {πi : } (hJ : J π) {J' : } (hJ' : J' πi J) :
@[simp]
theorem BoxIntegral.Prepartition.iUnion_biUnionTagged {ι : Type u_1} {I : } (π : ) (πi : ) :
= ⋃ (J : ) (_ : J π),
theorem BoxIntegral.Prepartition.forall_biUnionTagged {ι : Type u_1} {I : } (p : (ι) → ) (π : ) (πi : ) :
((J : ) → ) (J : ) → J π(J' : ) → J' πi Jp () J'
theorem BoxIntegral.Prepartition.IsPartition.biUnionTagged {ι : Type u_1} {I : } {π : } {πi : } (hi : ∀ (J : ), J π) :
@[simp]
theorem BoxIntegral.TaggedPrepartition.biUnionPrepartition_tag {ι : Type u_1} {I : } (π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.

Instances For
theorem BoxIntegral.TaggedPrepartition.IsPartition.biUnionPrepartition {ι : Type u_1} {I : } {πi : (J : ) → } (hi : ∀ (J : ), J π) :
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.

Instances For
@[simp]
theorem BoxIntegral.TaggedPrepartition.infPrepartition_toPrepartition {ι : Type u_1} {I : } (π' : ) :
().toPrepartition = π.toPrepartition π'
theorem BoxIntegral.TaggedPrepartition.mem_infPrepartition_comm {ι : Type u_1} {I : } {J : } {π₁ : } {π₂ : } :

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

Instances For
@[simp]
theorem BoxIntegral.TaggedPrepartition.isHenstock_biUnionTagged {ι : Type u_1} {I : } {π : } {πi : } :
theorem BoxIntegral.TaggedPrepartition.IsHenstock.card_filter_tag_eq_le {ι : Type u_1} {I : } [] (x : ι) :
Finset.card (Finset.filter (fun J => ) π.boxes)

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

Instances For
@[simp]
theorem BoxIntegral.TaggedPrepartition.isSubordinate_biUnionTagged {ι : Type u_1} {I : } {r : (ι) → ↑()} [] {π : } {πi : } :
∀ (J : ), J π
theorem BoxIntegral.TaggedPrepartition.IsSubordinate.biUnionPrepartition {ι : Type u_1} {I : } {r : (ι) → ↑()} [] (πi : (J : ) → ) :
theorem BoxIntegral.TaggedPrepartition.IsSubordinate.infPrepartition {ι : Type u_1} {I : } {r : (ι) → ↑()} [] (π' : ) :
theorem BoxIntegral.TaggedPrepartition.IsSubordinate.mono' {ι : Type u_1} {I : } {r₁ : (ι) → ↑()} {r₂ : (ι) → ↑()} [] (hr₁ : ) (h : ∀ (J : ), J π ) :
theorem BoxIntegral.TaggedPrepartition.IsSubordinate.mono {ι : Type u_1} {I : } {r₁ : (ι) → ↑()} {r₂ : (ι) → ↑()} [] (hr₁ : ) (h : ∀ (x : ι), x BoxIntegral.Box.Icc Ir₁ x r₂ x) :
theorem BoxIntegral.TaggedPrepartition.IsSubordinate.diam_le {ι : Type u_1} {I : } {J : } {r : (ι) → ↑()} [] (hJ : J π.boxes) :
Metric.diam (BoxIntegral.Box.Icc J) 2 * ↑()
@[simp]
theorem BoxIntegral.TaggedPrepartition.single_tag {ι : Type u_1} (I : ) (J : ) (hJ : J I) (x : ι) (h : x BoxIntegral.Box.Icc I) :
().tag = fun x => x
@[simp]
theorem BoxIntegral.TaggedPrepartition.single_boxes_val {ι : Type u_1} (I : ) (J : ) (hJ : J I) (x : ι) (h : x BoxIntegral.Box.Icc I) :
().toPrepartition.boxes.val = {J}
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.

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
theorem BoxIntegral.TaggedPrepartition.isPartition_single_iff {ι : Type u_1} {I : } {J : } {x : ι} (hJ : J I) (h : x BoxIntegral.Box.Icc I) :
theorem BoxIntegral.TaggedPrepartition.isPartition_single {ι : Type u_1} {I : } {x : ι} (h : x BoxIntegral.Box.Icc I) :
theorem BoxIntegral.TaggedPrepartition.forall_mem_single {ι : Type u_1} {I : } {J : } {x : ι} (p : (ι) → ) (hJ : J I) (h : x BoxIntegral.Box.Icc I) :
((J' : ) → J' p () 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) :
x BoxIntegral.Box.Icc J
theorem BoxIntegral.TaggedPrepartition.isHenstock_single {ι : Type u_1} {I : } {x : ι} (h : x BoxIntegral.Box.Icc I) :
@[simp]
theorem BoxIntegral.TaggedPrepartition.isSubordinate_single {ι : Type u_1} {I : } {J : } {x : ι} {r : (ι) → ↑()} [] (hJ : J I) (h : x BoxIntegral.Box.Icc I) :
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) :
def BoxIntegral.TaggedPrepartition.disjUnion {ι : Type u_1} {I : } (π₁ : ) (π₂ : ) :

Union of two tagged prepartitions with disjoint unions of boxes.

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

Instances For

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

Instances For
theorem BoxIntegral.TaggedPrepartition.distortion_le_of_mem {ι : Type u_1} {I : } {J : } [] (h : J π) :
theorem BoxIntegral.TaggedPrepartition.distortion_le_iff {ι : Type u_1} {I : } [] {c : NNReal} :
∀ (J : ), J π
@[simp]
theorem BoxIntegral.Prepartition.distortion_biUnionTagged {ι : Type u_1} {I : } [] (π : ) (πi : ) :
= Finset.sup π.boxes fun J =>
@[simp]
theorem BoxIntegral.TaggedPrepartition.distortion_biUnionPrepartition {ι : Type u_1} {I : } [] (πi : (J : ) → ) :
@[simp]
theorem BoxIntegral.TaggedPrepartition.distortion_of_const {ι : Type u_1} {I : } [] {c : NNReal} (h₁ : Finset.Nonempty π.boxes) (h₂ : ∀ (J : ), J π) :
@[simp]
theorem BoxIntegral.TaggedPrepartition.distortion_single {ι : Type u_1} {I : } {J : } {x : ι} [] (hJ : J I) (h : x BoxIntegral.Box.Icc I) :