mathlib3 documentation

analysis.box_integral.partition.tagged

Tagged partitions #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

Union of all boxes of a tagged prepartition.

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

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.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'
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 πi p ((π.bUnion_tagged πi).tag J) J) (J : box_integral.box ι), J π (J' : box_integral.box ι), J' πi J p ((π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.

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
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 I r₁ x r₂ x) :

Tagged prepartition with single box and prescribed tag.

Equations
@[simp]
@[simp]

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