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

to_prepartition : box_integral.prepartition I
tag : box_integral.box ι → ι → ℝ
tag_mem_Icc : ∀ (J : box_integral.box ι), self.tag J ∈ ⇑box_integral.box.Icc I

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

box_integral.tagged_prepartition.has_sizeof_inst
box_integral.tagged_prepartition.has_mem
box_integral.tagged_prepartition.inhabited

@[protected, instance]

def box_integral.tagged_prepartition.has_mem {ι : Type u_1} {I : box_integral.box ι} :

has_mem (box_integral.box ι) (box_integral.tagged_prepartition I)

Equations

box_integral.tagged_prepartition.has_mem = {mem := λ (J : box_integral.box ι) (π : box_integral.tagged_prepartition I), J ∈ π.to_prepartition.boxes}

@[simp]

theorem box_integral.tagged_prepartition.mem_to_prepartition {ι : Type u_1} {I J : box_integral.box ι} {π : box_integral.tagged_prepartition I} :

J ∈ π.to_prepartition ↔ J ∈ π

@[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 ∈ π

def box_integral.tagged_prepartition.Union {ι : Type u_1} {I : box_integral.box ι} (π : box_integral.tagged_prepartition I) :

set (ι → ℝ)

Union of all boxes of a tagged prepartition.

Equations

π.Union = π.to_prepartition.Union

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.Union_to_prepartition {ι : Type u_1} {I : box_integral.box ι} (π : box_integral.tagged_prepartition I) :

π.to_prepartition.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

theorem box_integral.tagged_prepartition.Union_subset {ι : Type u_1} {I : box_integral.box ι} (π : box_integral.tagged_prepartition I) :

π.Union ⊆ ↑I

def box_integral.tagged_prepartition.is_partition {ι : Type u_1} {I : box_integral.box ι} (π : box_integral.tagged_prepartition I) :

Prop

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

Equations

π.is_partition = π.to_prepartition.is_partition

theorem box_integral.tagged_prepartition.is_partition_iff_Union_eq {ι : Type u_1} {I : box_integral.box ι} (π : box_integral.tagged_prepartition I) :

π.is_partition ↔ π.Union = ↑I

noncomputable def box_integral.tagged_prepartition.filter {ι : Type u_1} {I : box_integral.box ι} (π : box_integral.tagged_prepartition I) (p : box_integral.box ι → Prop) :

box_integral.tagged_prepartition I

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

Equations

π.filter p = {to_prepartition := π.to_prepartition.filter p, tag := π.tag, tag_mem_Icc := _}

@[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.filter_to_prepartition {ι : Type u_1} {I : box_integral.box ι} (π : box_integral.tagged_prepartition I) (p : box_integral.box ι → Prop) :

(π.filter p).to_prepartition = π.to_prepartition.filter p

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

noncomputable def box_integral.prepartition.bUnion_tagged {ι : Type u_1} {I : box_integral.box ι} (π : box_integral.prepartition I) (πi : Π (J : box_integral.box ι), box_integral.tagged_prepartition J) :

box_integral.tagged_prepartition I

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

π.bUnion_tagged πi = {to_prepartition := π.bUnion (λ (J : box_integral.box ι), (πi J).to_prepartition), tag := λ (J : box_integral.box ι), (πi (π.bUnion_index (λ (J : box_integral.box ι), (πi J).to_prepartition) J)).tag J, tag_mem_Icc := _}

@[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 π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'

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

(π.bUnion_tagged πi).is_partition

noncomputable def box_integral.tagged_prepartition.bUnion_prepartition {ι : Type u_1} {I : box_integral.box ι} (π : box_integral.tagged_prepartition I) (πi : Π (J : box_integral.box ι), box_integral.prepartition J) :

box_integral.tagged_prepartition I

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

π.bUnion_prepartition πi = {to_prepartition := π.to_prepartition.bUnion πi, tag := λ (J : box_integral.box ι), π.tag (π.to_prepartition.bUnion_index πi J), tag_mem_Icc := _}

@[simp]

theorem box_integral.tagged_prepartition.bUnion_prepartition_tag {ι : Type u_1} {I : box_integral.box ι} (π : box_integral.tagged_prepartition I) (πi : Π (J : box_integral.box ι), box_integral.prepartition J) :

(π.bUnion_prepartition πi).tag = λ (J : box_integral.box ι), π.tag (π.to_prepartition.bUnion_index πi J)

theorem box_integral.tagged_prepartition.is_partition.bUnion_prepartition {ι : Type u_1} {I : box_integral.box ι} {π : box_integral.tagged_prepartition I} (h : π.is_partition) {πi : Π (J : box_integral.box ι), box_integral.prepartition J} (hi : ∀ (J : box_integral.box ι), J ∈ π → (πi J).is_partition) :

(π.bUnion_prepartition πi).is_partition

noncomputable def box_integral.tagged_prepartition.inf_prepartition {ι : Type u_1} {I : box_integral.box ι} (π : box_integral.tagged_prepartition I) (π' : box_integral.prepartition I) :

box_integral.tagged_prepartition I

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

π.inf_prepartition π' = π.bUnion_prepartition (λ (J : box_integral.box ι), π'.restrict J)

@[simp]

theorem box_integral.tagged_prepartition.inf_prepartition_to_prepartition {ι : Type u_1} {I : box_integral.box ι} (π : box_integral.tagged_prepartition I) (π' : box_integral.prepartition I) :

(π.inf_prepartition π').to_prepartition = π.to_prepartition ⊓ π'

theorem box_integral.tagged_prepartition.mem_inf_prepartition_comm {ι : Type u_1} {I J : box_integral.box ι} {π₁ π₂ : box_integral.tagged_prepartition I} :

J ∈ π₁.inf_prepartition π₂.to_prepartition ↔ J ∈ π₂.inf_prepartition π₁.to_prepartition

theorem box_integral.tagged_prepartition.is_partition.inf_prepartition {ι : Type u_1} {I : box_integral.box ι} {π₁ : box_integral.tagged_prepartition I} (h₁ : π₁.is_partition) {π₂ : box_integral.prepartition I} (h₂ : π₂.is_partition) :

(π₁.inf_prepartition π₂).is_partition

def box_integral.tagged_prepartition.is_Henstock {ι : Type u_1} {I : box_integral.box ι} (π : box_integral.tagged_prepartition I) :

Prop

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

Equations

π.is_Henstock = ∀ (J : box_integral.box ι), J ∈ π → π.tag J ∈ ⇑box_integral.box.Icc J

@[simp]

theorem box_integral.tagged_prepartition.is_Henstock_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).is_Henstock ↔ ∀ (J : box_integral.box ι), J ∈ π → (πi J).is_Henstock

theorem box_integral.tagged_prepartition.is_Henstock.card_filter_tag_eq_le {ι : Type u_1} {I : box_integral.box ι} {π : box_integral.tagged_prepartition I} [fintype ι] (h : π.is_Henstock) (x : ι → ℝ) :

(finset.filter (λ (J : box_integral.box ι), π.tag J = x) π.to_prepartition.boxes).card ≤ 2 ^ fintype.card ι

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

π.is_subordinate r = ∀ (J : box_integral.box ι), J ∈ π → ⇑box_integral.box.Icc J ⊆ metric.closed_ball (π.tag J) ↑(r (π.tag J))

@[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.bUnion_prepartition {ι : Type u_1} {I : box_integral.box ι} {π : box_integral.tagged_prepartition I} {r : (ι → ℝ) → ↥(set.Ioi 0)} [fintype ι] (h : π.is_subordinate r) (πi : Π (J : box_integral.box ι), box_integral.prepartition J) :

(π.bUnion_prepartition πi).is_subordinate r

theorem box_integral.tagged_prepartition.is_subordinate.inf_prepartition {ι : Type u_1} {I : box_integral.box ι} {π : box_integral.tagged_prepartition I} {r : (ι → ℝ) → ↥(set.Ioi 0)} [fintype ι] (h : π.is_subordinate r) (π' : box_integral.prepartition I) :

(π.inf_prepartition π').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 I → r₁ 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) :

metric.diam (⇑box_integral.box.Icc J) ≤ 2 * ↑(r (π.tag J))

@[simp]

theorem box_integral.tagged_prepartition.single_to_prepartition {ι : Type u_1} (I J : box_integral.box ι) (hJ : J ≤ I) (x : ι → ℝ) (h : x ∈ ⇑box_integral.box.Icc I) :

(box_integral.tagged_prepartition.single I J hJ x h).to_prepartition = box_integral.prepartition.single I J hJ

def box_integral.tagged_prepartition.single {ι : Type u_1} (I J : box_integral.box ι) (hJ : J ≤ I) (x : ι → ℝ) (h : x ∈ ⇑box_integral.box.Icc I) :

box_integral.tagged_prepartition I

Tagged prepartition with single box and prescribed tag.

Equations

box_integral.tagged_prepartition.single I J hJ x h = {to_prepartition := box_integral.prepartition.single I J hJ, tag := λ (J : box_integral.box ι), x, tag_mem_Icc := _}

@[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) :

(box_integral.tagged_prepartition.single I J hJ x h).tag = λ (J : box_integral.box ι), x

@[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) :

J' ∈ box_integral.tagged_prepartition.single I J hJ x h ↔ J' = J

@[protected, instance]

def box_integral.tagged_prepartition.inhabited {ι : Type u_1} (I : box_integral.box ι) :

inhabited (box_integral.tagged_prepartition I)

Equations

box_integral.tagged_prepartition.inhabited I = {default := box_integral.tagged_prepartition.single I I _ I.upper _}

theorem box_integral.tagged_prepartition.is_partition_single_iff {ι : Type u_1} {I J : box_integral.box ι} {x : ι → ℝ} (hJ : J ≤ I) (h : x ∈ ⇑box_integral.box.Icc I) :

(box_integral.tagged_prepartition.single I J hJ x h).is_partition ↔ J = I

theorem box_integral.tagged_prepartition.is_partition_single {ι : Type u_1} {I : box_integral.box ι} {x : ι → ℝ} (h : x ∈ ⇑box_integral.box.Icc I) :

(box_integral.tagged_prepartition.single I I le_rfl x h).is_partition

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 h → p ((box_integral.tagged_prepartition.single I J hJ x h).tag J') J') ↔ p x J

@[simp]

theorem box_integral.tagged_prepartition.is_Henstock_single_iff {ι : Type u_1} {I J : box_integral.box ι} {x : ι → ℝ} (hJ : J ≤ I) (h : x ∈ ⇑box_integral.box.Icc I) :

(box_integral.tagged_prepartition.single I J hJ x h).is_Henstock ↔ x ∈ ⇑box_integral.box.Icc J

@[simp]

theorem box_integral.tagged_prepartition.is_Henstock_single {ι : Type u_1} {I : box_integral.box ι} {x : ι → ℝ} (h : x ∈ ⇑box_integral.box.Icc I) :

(box_integral.tagged_prepartition.single I I le_rfl x h).is_Henstock

@[simp]

theorem box_integral.tagged_prepartition.is_subordinate_single {ι : Type u_1} {I J : box_integral.box ι} {x : ι → ℝ} {r : (ι → ℝ) → ↥(set.Ioi 0)} [fintype ι] (hJ : J ≤ I) (h : x ∈ ⇑box_integral.box.Icc I) :

(box_integral.tagged_prepartition.single I J hJ x h).is_subordinate r ↔ ⇑box_integral.box.Icc J ⊆ metric.closed_ball x ↑(r x)

@[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) :

(box_integral.tagged_prepartition.single I J hJ x h).Union = ↑J

noncomputable def box_integral.tagged_prepartition.disj_union {ι : Type u_1} {I : box_integral.box ι} (π₁ π₂ : box_integral.tagged_prepartition I) (h : disjoint π₁.Union π₂.Union) :

box_integral.tagged_prepartition I

Union of two tagged prepartitions with disjoint unions of boxes.

Equations

π₁.disj_union π₂ h = {to_prepartition := π₁.to_prepartition.disj_union π₂.to_prepartition h, tag := π₁.to_prepartition.boxes.piecewise π₁.tag π₂.tag (λ (j : box_integral.box ι), finset.decidable_mem j π₁.to_prepartition.boxes), tag_mem_Icc := _}

@[simp]

theorem box_integral.tagged_prepartition.disj_union_boxes {ι : Type u_1} {I : box_integral.box ι} {π₁ π₂ : box_integral.tagged_prepartition I} (h : disjoint π₁.Union π₂.Union) :

(π₁.disj_union π₂ h).to_prepartition.boxes = π₁.to_prepartition.boxes ∪ π₂.to_prepartition.boxes

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

def box_integral.tagged_prepartition.embed_box {ι : Type u_1} (I J : box_integral.box ι) (h : I ≤ J) :

box_integral.tagged_prepartition I ↪ box_integral.tagged_prepartition J

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

Equations

box_integral.tagged_prepartition.embed_box I J h = {to_fun := λ (π : box_integral.tagged_prepartition I), {to_prepartition := {boxes := π.to_prepartition.boxes, le_of_mem' := _, pairwise_disjoint := _}, tag := π.tag, tag_mem_Icc := _}, inj' := _}

noncomputable def box_integral.tagged_prepartition.distortion {ι : Type u_1} {I : box_integral.box ι} (π : box_integral.tagged_prepartition I) [fintype ι] :

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

Equations

π.distortion = π.to_prepartition.distortion

theorem box_integral.tagged_prepartition.distortion_le_of_mem {ι : Type u_1} {I J : box_integral.box ι} (π : box_integral.tagged_prepartition I) [fintype ι] (h : J ∈ π) :

J.distortion ≤ π.distortion

theorem box_integral.tagged_prepartition.distortion_le_iff {ι : Type u_1} {I : box_integral.box ι} (π : box_integral.tagged_prepartition I) [fintype ι] {c : nnreal} :

π.distortion ≤ c ↔ ∀ (J : box_integral.box ι), J ∈ π → J.distortion ≤ c

@[simp]

theorem box_integral.prepartition.distortion_bUnion_tagged {ι : Type u_1} {I : box_integral.box ι} [fintype ι] (π : box_integral.prepartition I) (πi : Π (J : box_integral.box ι), box_integral.tagged_prepartition J) :

(π.bUnion_tagged πi).distortion = π.boxes.sup (λ (J : box_integral.box ι), (πi J).distortion)

@[simp]

theorem box_integral.tagged_prepartition.distortion_bUnion_prepartition {ι : Type u_1} {I : box_integral.box ι} [fintype ι] (π : box_integral.tagged_prepartition I) (πi : Π (J : box_integral.box ι), box_integral.prepartition J) :

(π.bUnion_prepartition πi).distortion = π.to_prepartition.boxes.sup (λ (J : box_integral.box ι), (πi J).distortion)

@[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 = linear_order.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 : nnreal} (h₁ : π.to_prepartition.boxes.nonempty) (h₂ : ∀ (J : box_integral.box ι), J ∈ π → J.distortion = c) :

π.distortion = c

@[simp]

theorem box_integral.tagged_prepartition.distortion_single {ι : Type u_1} {I J : box_integral.box ι} {x : ι → ℝ} [fintype ι] (hJ : J ≤ I) (h : x ∈ ⇑box_integral.box.Icc I) :

(box_integral.tagged_prepartition.single I J hJ x h).distortion = J.distortion

theorem box_integral.tagged_prepartition.distortion_filter_le {ι : Type u_1} {I : box_integral.box ι} (π : box_integral.tagged_prepartition I) [fintype ι] (p : box_integral.box ι → Prop) :

(π.filter p).distortion ≤ π.distortion