mathlib documentation

analysis.box_integral.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 functionbox_integral.tagged_prepartition.tagis defined on all boxesJ : box ιbut use its values only on boxes of the partition. Givenπ : box_integral.tagged_partition I, we require that eachbox_integral.tagged_partition π Jbelongs tobox_integral.box.Icc I. If for everyJ ∈ π,π.tag Jbelongs toJ.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 box_integral.tagged_prepartition {ι : Type u_1} (I : box_integral.box ι) :
Type u_1

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

Instances for box_integral.tagged_prepartition
@[simp]
theorem box_integral.tagged_prepartition.mem_mk {ι : Type u_1} {I J : box_integral.box ι} (π : box_integral.prepartition I) (f : box_integral.box ιι → ) (h : ∀ (J : box_integral.box ι), f J box_integral.box.Icc I) :
J {to_prepartition := π, tag := f, tag_mem_Icc := h} J π

Union of all boxes of a tagged prepartition.

Equations
theorem box_integral.tagged_prepartition.Union_def {ι : Type u_1} {I : box_integral.box ι} (π : box_integral.tagged_prepartition I) :
π.Union = ⋃ (J : box_integral.box ι) (H : J π), J
@[simp]
theorem box_integral.tagged_prepartition.Union_mk {ι : Type u_1} {I : box_integral.box ι} (π : box_integral.prepartition I) (f : box_integral.box ιι → ) (h : ∀ (J : box_integral.box ι), f J box_integral.box.Icc I) :
@[simp]
theorem box_integral.tagged_prepartition.mem_Union {ι : Type u_1} {I : box_integral.box ι} (π : box_integral.tagged_prepartition I) {x : ι → } :
x π.Union ∃ (J : box_integral.box ι) (H : J π), x J

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

Equations

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

Equations
@[simp]
theorem box_integral.tagged_prepartition.filter_tag {ι : Type u_1} {I : box_integral.box ι} (π : box_integral.tagged_prepartition I) (p : box_integral.box ι → Prop) :
(π.filter p).tag = π.tag
@[simp]
theorem box_integral.tagged_prepartition.mem_filter {ι : Type u_1} {I J : box_integral.box ι} (π : box_integral.tagged_prepartition I) {p : box_integral.box ι → Prop} :
J π.filter p J π p J
@[simp]
theorem box_integral.tagged_prepartition.Union_filter_not {ι : Type u_1} {I : box_integral.box ι} (π : box_integral.tagged_prepartition I) (p : box_integral.box ι → Prop) :
(π.filter (λ (J : box_integral.box ι), ¬p J)).Union = π.Union \ (π.filter p).Union

Given a partition π of I : box_integral.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
@[simp]
theorem box_integral.prepartition.mem_bUnion_tagged {ι : Type u_1} {I J : box_integral.box ι} (π : box_integral.prepartition I) {πi : Π (J : box_integral.box ι), box_integral.tagged_prepartition J} :
J π.bUnion_tagged πi ∃ (J' : box_integral.box ι) (H : J' π), J πi J'
theorem box_integral.prepartition.tag_bUnion_tagged {ι : Type u_1} {I J : box_integral.box ι} (π : box_integral.prepartition I) {πi : Π (J : box_integral.box ι), box_integral.tagged_prepartition J} (hJ : J π) {J' : box_integral.box ι} (hJ' : J' πi J) :
(π.bUnion_tagged πi).tag J' = (πi J).tag J'
@[simp]
theorem box_integral.prepartition.Union_bUnion_tagged {ι : Type u_1} {I : box_integral.box ι} (π : box_integral.prepartition I) (πi : Π (J : box_integral.box ι), box_integral.tagged_prepartition J) :
(π.bUnion_tagged πi).Union = ⋃ (J : box_integral.box ι) (H : J π), (πi J).Union
theorem box_integral.prepartition.forall_bUnion_tagged {ι : Type u_1} {I : box_integral.box ι} (p : (ι → )box_integral.box ι → Prop) (π : box_integral.prepartition I) (πi : Π (J : box_integral.box ι), box_integral.tagged_prepartition J) :
(∀ (J : box_integral.box ι), J π.bUnion_tagged πip ((π.bUnion_tagged πi).tag J) J) ∀ (J : box_integral.box ι), J π∀ (J' : box_integral.box ι), J' πi Jp ((πi J).tag J') 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

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

Note that usually the result is not a Henstock partition.

Equations

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

Equations

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

def box_integral.tagged_prepartition.is_subordinate {ι : Type u_1} {I : box_integral.box ι} [fintype ι] (π : box_integral.tagged_prepartition 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
@[simp]
theorem box_integral.tagged_prepartition.is_subordinate.mono' {ι : Type u_1} {I : box_integral.box ι} {r₁ r₂ : (ι → )(set.Ioi 0)} [fintype ι] {π : box_integral.tagged_prepartition I} (hr₁ : π.is_subordinate r₁) (h : ∀ (J : box_integral.box ι), J πr₁ (π.tag J) r₂ (π.tag J)) :
theorem box_integral.tagged_prepartition.is_subordinate.mono {ι : Type u_1} {I : box_integral.box ι} {r₁ r₂ : (ι → )(set.Ioi 0)} [fintype ι] {π : box_integral.tagged_prepartition I} (hr₁ : π.is_subordinate r₁) (h : ∀ (x : ι → ), x box_integral.box.Icc Ir₁ x r₂ x) :

Tagged prepartition with single box and prescribed tag.

Equations
@[simp]
theorem box_integral.tagged_prepartition.single_tag {ι : Type u_1} (I J : box_integral.box ι) (hJ : J I) (x : ι → ) (h : x box_integral.box.Icc I) :
@[simp]
theorem box_integral.tagged_prepartition.mem_single {ι : Type u_1} {I J : box_integral.box ι} {x : ι → } {J' : box_integral.box ι} (hJ : J I) (h : x box_integral.box.Icc I) :
theorem box_integral.tagged_prepartition.forall_mem_single {ι : Type u_1} {I J : box_integral.box ι} {x : ι → } (p : (ι → )box_integral.box ι → Prop) (hJ : J I) (h : x box_integral.box.Icc I) :
(∀ (J' : box_integral.box ι), J' box_integral.tagged_prepartition.single I J hJ x hp ((box_integral.tagged_prepartition.single I J hJ x h).tag J') J') p x J
@[simp]
theorem box_integral.tagged_prepartition.Union_single {ι : Type u_1} {I J : box_integral.box ι} {x : ι → } (hJ : J I) (h : x box_integral.box.Icc I) :

Union of two tagged prepartitions with disjoint unions of boxes.

Equations
@[simp]
theorem box_integral.tagged_prepartition.mem_disj_union {ι : Type u_1} {I J : box_integral.box ι} {π₁ π₂ : box_integral.tagged_prepartition I} (h : disjoint π₁.Union π₂.Union) :
J π₁.disj_union π₂ h J π₁ J π₂
@[simp]
theorem box_integral.tagged_prepartition.Union_disj_union {ι : Type u_1} {I : box_integral.box ι} {π₁ π₂ : box_integral.tagged_prepartition I} (h : disjoint π₁.Union π₂.Union) :
(π₁.disj_union π₂ h).Union = π₁.Union π₂.Union
theorem box_integral.tagged_prepartition.disj_union_tag_of_mem_left {ι : Type u_1} {I J : box_integral.box ι} {π₁ π₂ : box_integral.tagged_prepartition I} (h : disjoint π₁.Union π₂.Union) (hJ : J π₁) :
(π₁.disj_union π₂ h).tag J = π₁.tag J
theorem box_integral.tagged_prepartition.disj_union_tag_of_mem_right {ι : Type u_1} {I J : box_integral.box ι} {π₁ π₂ : box_integral.tagged_prepartition I} (h : disjoint π₁.Union π₂.Union) (hJ : J π₂) :
(π₁.disj_union π₂ h).tag J = π₂.tag J
theorem box_integral.tagged_prepartition.is_subordinate.disj_union {ι : Type u_1} {I : box_integral.box ι} {π₁ π₂ : box_integral.tagged_prepartition I} {r : (ι → )(set.Ioi 0)} [fintype ι] (h₁ : π₁.is_subordinate r) (h₂ : π₂.is_subordinate r) (h : disjoint π₁.Union π₂.Union) :
(π₁.disj_union π₂ h).is_subordinate r
theorem box_integral.tagged_prepartition.is_Henstock.disj_union {ι : Type u_1} {I : box_integral.box ι} {π₁ π₂ : box_integral.tagged_prepartition I} (h₁ : π₁.is_Henstock) (h₂ : π₂.is_Henstock) (h : disjoint π₁.Union π₂.Union) :
(π₁.disj_union π₂ h).is_Henstock

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

Equations

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

Equations
@[simp]