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.

@[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) :
{to_prepartition := «π», tag := f, tag_mem_Icc := h}.Union = «π».Union
@[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
theorem box_integral.tagged_prepartition.subset_Union {ι : Type u_1} {I J : box_integral.box ι} (π : box_integral.tagged_prepartition I) (h : J «π») :
J «π».Union

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'
theorem box_integral.prepartition.is_partition.bUnion_tagged {ι : Type u_1} {I : box_integral.box ι} {π : box_integral.prepartition I} (h : «π».is_partition) {πi : Π (J : box_integral.box ι), box_integral.tagged_prepartition J} (hi : ∀ (J : box_integral.box ι), J «π»(πi J).is_partition) :

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_bUnion_tagged {ι : Type u_1} {I : box_integral.box ι} {r : (ι → )(set.Ioi 0)} [fintype ι] {π : box_integral.prepartition I} {πi : Π (J : box_integral.box ι), box_integral.tagged_prepartition J} :
(«π».bUnion_tagged πi).is_subordinate r ∀ (J : box_integral.box ι), J «π»(πi J).is_subordinate r
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)) :
«π».is_subordinate r₂
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) :
«π».is_subordinate r₂
theorem box_integral.tagged_prepartition.is_subordinate.diam_le {ι : Type u_1} {I J : box_integral.box ι} {r : (ι → )(set.Ioi 0)} [fintype ι] {π : box_integral.tagged_prepartition I} (h : «π».is_subordinate r) (hJ : J «π».to_prepartition.boxes) :

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]
theorem box_integral.tagged_prepartition.distortion_disj_union {ι : Type u_1} {I : box_integral.box ι} {π₁ π₂ : box_integral.tagged_prepartition I} [fintype ι] (h : disjoint π₁.Union π₂.Union) :
(π₁.disj_union π₂ h).distortion = max π₁.distortion π₂.distortion
theorem box_integral.tagged_prepartition.distortion_of_const {ι : Type u_1} {I : box_integral.box ι} (π : box_integral.tagged_prepartition I) [fintype ι] {c : ℝ≥0} (h₁ : «π».to_prepartition.boxes.nonempty) (h₂ : ∀ (J : box_integral.box ι), J «π»J.distortion = c) :
«π».distortion = c