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 : BoxIntegral.Box ι) extends BoxIntegral.Prepartition : Type u_1

• boxes : Finset (BoxIntegral.Box ι)
• le_of_mem' : ∀ (J : BoxIntegral.Box ι), J ∈ s.boxes → J ≤ I
• pairwiseDisjoint : Set.Pairwise (↑s.boxes) (Disjoint on BoxIntegral.Box.toSet)
• tag : BoxIntegral.Box ι → ι → ℝ
• tag_mem_Icc : ∀ (J : BoxIntegral.Box ι), BoxIntegral.TaggedPrepartition.tag s 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.

instance BoxIntegral.TaggedPrepartition.instMembershipBoxTaggedPrepartition {ι : Type u_1} {I : BoxIntegral.Box ι} : Membership (BoxIntegral.Box ι) (BoxIntegral.TaggedPrepartition I)

Equations

• BoxIntegral.TaggedPrepartition.instMembershipBoxTaggedPrepartition = { mem := fun J π => J ∈ π.boxes }

@[simp]

theorem BoxIntegral.TaggedPrepartition.mem_toPrepartition {ι : Type u_1} {I : BoxIntegral.Box ι} {J : BoxIntegral.Box ι} {π : BoxIntegral.TaggedPrepartition I} : J ∈ π.toPrepartition ↔ J ∈ π

@[simp]

theorem BoxIntegral.TaggedPrepartition.mem_mk {ι : Type u_1} {I : BoxIntegral.Box ι} {J : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I) (f : BoxIntegral.Box ι → ι → ℝ) (h : ∀ (J : BoxIntegral.Box ι), f J ∈ ↑BoxIntegral.Box.Icc I) : J ∈ { toPrepartition := π, tag := f, tag_mem_Icc := h } ↔ J ∈ π

def BoxIntegral.TaggedPrepartition.iUnion {ι : Type u_1} {I : BoxIntegral.Box ι} (π : BoxIntegral.TaggedPrepartition I) : Set (ι → ℝ)

Union of all boxes of a tagged prepartition.

Equations

• BoxIntegral.TaggedPrepartition.iUnion π = BoxIntegral.Prepartition.iUnion π.toPrepartition

theorem BoxIntegral.TaggedPrepartition.iUnion_def {ι : Type u_1} {I : BoxIntegral.Box ι} (π : BoxIntegral.TaggedPrepartition I) : BoxIntegral.TaggedPrepartition.iUnion π = ⋃ (J : BoxIntegral.Box ι) (_ : J ∈ π), ↑J

@[simp]

theorem BoxIntegral.TaggedPrepartition.iUnion_mk {ι : Type u_1} {I : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I) (f : BoxIntegral.Box ι → ι → ℝ) (h : ∀ (J : BoxIntegral.Box ι), f J ∈ ↑BoxIntegral.Box.Icc I) : BoxIntegral.TaggedPrepartition.iUnion { toPrepartition := π, tag := f, tag_mem_Icc := h } = BoxIntegral.Prepartition.iUnion π

@[simp]

theorem BoxIntegral.TaggedPrepartition.iUnion_toPrepartition {ι : Type u_1} {I : BoxIntegral.Box ι} (π : BoxIntegral.TaggedPrepartition I) : BoxIntegral.Prepartition.iUnion π.toPrepartition = BoxIntegral.TaggedPrepartition.iUnion π

@[simp]

theorem BoxIntegral.TaggedPrepartition.mem_iUnion {ι : Type u_1} {I : BoxIntegral.Box ι} (π : BoxIntegral.TaggedPrepartition I) {x : ι → ℝ} : x ∈ BoxIntegral.TaggedPrepartition.iUnion π ↔ ∃ J, J ∈ π ∧ x ∈ J

theorem BoxIntegral.TaggedPrepartition.subset_iUnion {ι : Type u_1} {I : BoxIntegral.Box ι} {J : BoxIntegral.Box ι} (π : BoxIntegral.TaggedPrepartition I) (h : J ∈ π) : ↑J ⊆ BoxIntegral.TaggedPrepartition.iUnion π

theorem BoxIntegral.TaggedPrepartition.iUnion_subset {ι : Type u_1} {I : BoxIntegral.Box ι} (π : BoxIntegral.TaggedPrepartition I) : BoxIntegral.TaggedPrepartition.iUnion π ⊆ ↑I

def BoxIntegral.TaggedPrepartition.IsPartition {ι : Type u_1} {I : BoxIntegral.Box ι} (π : BoxIntegral.TaggedPrepartition I) : Prop

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

Equations

• BoxIntegral.TaggedPrepartition.IsPartition π = BoxIntegral.Prepartition.IsPartition π.toPrepartition

theorem BoxIntegral.TaggedPrepartition.isPartition_iff_iUnion_eq {ι : Type u_1} {I : BoxIntegral.Box ι} (π : BoxIntegral.TaggedPrepartition I) : BoxIntegral.TaggedPrepartition.IsPartition π ↔ BoxIntegral.TaggedPrepartition.iUnion π = ↑I

@[simp]

theorem BoxIntegral.TaggedPrepartition.filter_boxes_val {ι : Type u_1} {I : BoxIntegral.Box ι} (π : BoxIntegral.TaggedPrepartition I) (p : BoxIntegral.Box ι → Prop) : (BoxIntegral.TaggedPrepartition.filter π p).toPrepartition.boxes.val = Multiset.filter p π.boxes.val

@[simp]

theorem BoxIntegral.TaggedPrepartition.filter_tag {ι : Type u_1} {I : BoxIntegral.Box ι} (π : BoxIntegral.TaggedPrepartition I) (p : BoxIntegral.Box ι → Prop) : (BoxIntegral.TaggedPrepartition.filter π p).tag = π.tag

def BoxIntegral.TaggedPrepartition.filter {ι : Type u_1} {I : BoxIntegral.Box ι} (π : BoxIntegral.TaggedPrepartition I) (p : BoxIntegral.Box ι → Prop) : BoxIntegral.TaggedPrepartition I

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

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem BoxIntegral.TaggedPrepartition.mem_filter {ι : Type u_1} {I : BoxIntegral.Box ι} {J : BoxIntegral.Box ι} (π : BoxIntegral.TaggedPrepartition I) {p : BoxIntegral.Box ι → Prop} : J ∈ BoxIntegral.TaggedPrepartition.filter π p ↔ J ∈ π ∧ p J

@[simp]

theorem BoxIntegral.TaggedPrepartition.iUnion_filter_not {ι : Type u_1} {I : BoxIntegral.Box ι} (π : BoxIntegral.TaggedPrepartition I) (p : BoxIntegral.Box ι → Prop) : BoxIntegral.TaggedPrepartition.iUnion (BoxIntegral.TaggedPrepartition.filter π fun J => ¬p J) = BoxIntegral.TaggedPrepartition.iUnion π \ BoxIntegral.TaggedPrepartition.iUnion (BoxIntegral.TaggedPrepartition.filter π p)

def BoxIntegral.Prepartition.biUnionTagged {ι : Type u_1} {I : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I) (πi : (J : BoxIntegral.Box ι) → BoxIntegral.TaggedPrepartition J) : BoxIntegral.TaggedPrepartition 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.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem BoxIntegral.Prepartition.mem_biUnionTagged {ι : Type u_1} {I : BoxIntegral.Box ι} {J : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I) {πi : (J : BoxIntegral.Box ι) → BoxIntegral.TaggedPrepartition J} : J ∈ BoxIntegral.Prepartition.biUnionTagged π πi ↔ ∃ J', J' ∈ π ∧ J ∈ πi J'

theorem BoxIntegral.Prepartition.tag_biUnionTagged {ι : Type u_1} {I : BoxIntegral.Box ι} {J : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I) {πi : (J : BoxIntegral.Box ι) → BoxIntegral.TaggedPrepartition J} (hJ : J ∈ π) {J' : BoxIntegral.Box ι} (hJ' : J' ∈ πi J) : BoxIntegral.TaggedPrepartition.tag (BoxIntegral.Prepartition.biUnionTagged π πi) J' = BoxIntegral.TaggedPrepartition.tag (πi J) J'

@[simp]

theorem BoxIntegral.Prepartition.iUnion_biUnionTagged {ι : Type u_1} {I : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I) (πi : (J : BoxIntegral.Box ι) → BoxIntegral.TaggedPrepartition J) : BoxIntegral.TaggedPrepartition.iUnion (BoxIntegral.Prepartition.biUnionTagged π πi) = ⋃ (J : BoxIntegral.Box ι) (_ : J ∈ π), BoxIntegral.TaggedPrepartition.iUnion (πi J)

theorem BoxIntegral.Prepartition.forall_biUnionTagged {ι : Type u_1} {I : BoxIntegral.Box ι} (p : (ι → ℝ) → BoxIntegral.Box ι → Prop) (π : BoxIntegral.Prepartition I) (πi : (J : BoxIntegral.Box ι) → BoxIntegral.TaggedPrepartition J) : ((J : BoxIntegral.Box ι) → J ∈ BoxIntegral.Prepartition.biUnionTagged π πi → p (BoxIntegral.TaggedPrepartition.tag (BoxIntegral.Prepartition.biUnionTagged π πi) J) J) ↔ (J : BoxIntegral.Box ι) → J ∈ π → (J' : BoxIntegral.Box ι) → J' ∈ πi J → p (BoxIntegral.TaggedPrepartition.tag (πi J) J') J'

theorem BoxIntegral.Prepartition.IsPartition.biUnionTagged {ι : Type u_1} {I : BoxIntegral.Box ι} {π : BoxIntegral.Prepartition I} (h : BoxIntegral.Prepartition.IsPartition π) {πi : (J : BoxIntegral.Box ι) → BoxIntegral.TaggedPrepartition J} (hi : ∀ (J : BoxIntegral.Box ι), J ∈ π → BoxIntegral.TaggedPrepartition.IsPartition (πi J)) : BoxIntegral.TaggedPrepartition.IsPartition (BoxIntegral.Prepartition.biUnionTagged π πi)

@[simp]

theorem BoxIntegral.TaggedPrepartition.biUnionPrepartition_tag {ι : Type u_1} {I : BoxIntegral.Box ι} (π : BoxIntegral.TaggedPrepartition I) (πi : (J : BoxIntegral.Box ι) → BoxIntegral.Prepartition J) : (BoxIntegral.TaggedPrepartition.biUnionPrepartition π πi).tag = fun J => BoxIntegral.TaggedPrepartition.tag π (BoxIntegral.Prepartition.biUnionIndex π.toPrepartition πi J)

def BoxIntegral.TaggedPrepartition.biUnionPrepartition {ι : Type u_1} {I : BoxIntegral.Box ι} (π : BoxIntegral.TaggedPrepartition I) (πi : (J : BoxIntegral.Box ι) → BoxIntegral.Prepartition J) : BoxIntegral.TaggedPrepartition 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

• One or more equations did not get rendered due to their size.

theorem BoxIntegral.TaggedPrepartition.IsPartition.biUnionPrepartition {ι : Type u_1} {I : BoxIntegral.Box ι} {π : BoxIntegral.TaggedPrepartition I} (h : BoxIntegral.TaggedPrepartition.IsPartition π) {πi : (J : BoxIntegral.Box ι) → BoxIntegral.Prepartition J} (hi : ∀ (J : BoxIntegral.Box ι), J ∈ π → BoxIntegral.Prepartition.IsPartition (πi J)) : BoxIntegral.TaggedPrepartition.IsPartition (BoxIntegral.TaggedPrepartition.biUnionPrepartition π πi)

def BoxIntegral.TaggedPrepartition.infPrepartition {ι : Type u_1} {I : BoxIntegral.Box ι} (π : BoxIntegral.TaggedPrepartition I) (π' : BoxIntegral.Prepartition I) : BoxIntegral.TaggedPrepartition 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.

Equations

• BoxIntegral.TaggedPrepartition.infPrepartition π π' = BoxIntegral.TaggedPrepartition.biUnionPrepartition π fun J => BoxIntegral.Prepartition.restrict π' J

@[simp]

theorem BoxIntegral.TaggedPrepartition.infPrepartition_toPrepartition {ι : Type u_1} {I : BoxIntegral.Box ι} (π : BoxIntegral.TaggedPrepartition I) (π' : BoxIntegral.Prepartition I) : (BoxIntegral.TaggedPrepartition.infPrepartition π π').toPrepartition = π.toPrepartition ⊓ π'

theorem BoxIntegral.TaggedPrepartition.mem_infPrepartition_comm {ι : Type u_1} {I : BoxIntegral.Box ι} {J : BoxIntegral.Box ι} {π₁ : BoxIntegral.TaggedPrepartition I} {π₂ : BoxIntegral.TaggedPrepartition I} : J ∈ BoxIntegral.TaggedPrepartition.infPrepartition π₁ π₂.toPrepartition ↔ J ∈ BoxIntegral.TaggedPrepartition.infPrepartition π₂ π₁.toPrepartition

theorem BoxIntegral.TaggedPrepartition.IsPartition.infPrepartition {ι : Type u_1} {I : BoxIntegral.Box ι} {π₁ : BoxIntegral.TaggedPrepartition I} (h₁ : BoxIntegral.TaggedPrepartition.IsPartition π₁) {π₂ : BoxIntegral.Prepartition I} (h₂ : BoxIntegral.Prepartition.IsPartition π₂) : BoxIntegral.TaggedPrepartition.IsPartition (BoxIntegral.TaggedPrepartition.infPrepartition π₁ π₂)

def BoxIntegral.TaggedPrepartition.IsHenstock {ι : Type u_1} {I : BoxIntegral.Box ι} (π : BoxIntegral.TaggedPrepartition 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

• BoxIntegral.TaggedPrepartition.IsHenstock π = ∀ (J : BoxIntegral.Box ι), J ∈ π → BoxIntegral.TaggedPrepartition.tag π J ∈ ↑BoxIntegral.Box.Icc J

@[simp]

theorem BoxIntegral.TaggedPrepartition.isHenstock_biUnionTagged {ι : Type u_1} {I : BoxIntegral.Box ι} {π : BoxIntegral.Prepartition I} {πi : (J : BoxIntegral.Box ι) → BoxIntegral.TaggedPrepartition J} : BoxIntegral.TaggedPrepartition.IsHenstock (BoxIntegral.Prepartition.biUnionTagged π πi) ↔ ∀ (J : BoxIntegral.Box ι), J ∈ π → BoxIntegral.TaggedPrepartition.IsHenstock (πi J)

theorem BoxIntegral.TaggedPrepartition.IsHenstock.card_filter_tag_eq_le {ι : Type u_1} {I : BoxIntegral.Box ι} {π : BoxIntegral.TaggedPrepartition I} [Fintype ι] (h : BoxIntegral.TaggedPrepartition.IsHenstock π) (x : ι → ℝ) : Finset.card (Finset.filter (fun J => BoxIntegral.TaggedPrepartition.tag π J = x) π.boxes) ≤ 2 ^ Fintype.card ι

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

def BoxIntegral.TaggedPrepartition.IsSubordinate {ι : Type u_1} {I : BoxIntegral.Box ι} [Fintype ι] (π : BoxIntegral.TaggedPrepartition 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

• One or more equations did not get rendered due to their size.

@[simp]

theorem BoxIntegral.TaggedPrepartition.isSubordinate_biUnionTagged {ι : Type u_1} {I : BoxIntegral.Box ι} {r : (ι → ℝ) → ↑(Set.Ioi 0)} [Fintype ι] {π : BoxIntegral.Prepartition I} {πi : (J : BoxIntegral.Box ι) → BoxIntegral.TaggedPrepartition J} : BoxIntegral.TaggedPrepartition.IsSubordinate (BoxIntegral.Prepartition.biUnionTagged π πi) r ↔ ∀ (J : BoxIntegral.Box ι), J ∈ π → BoxIntegral.TaggedPrepartition.IsSubordinate (πi J) r

theorem BoxIntegral.TaggedPrepartition.IsSubordinate.biUnionPrepartition {ι : Type u_1} {I : BoxIntegral.Box ι} {π : BoxIntegral.TaggedPrepartition I} {r : (ι → ℝ) → ↑(Set.Ioi 0)} [Fintype ι] (h : BoxIntegral.TaggedPrepartition.IsSubordinate π r) (πi : (J : BoxIntegral.Box ι) → BoxIntegral.Prepartition J) : BoxIntegral.TaggedPrepartition.IsSubordinate (BoxIntegral.TaggedPrepartition.biUnionPrepartition π πi) r

theorem BoxIntegral.TaggedPrepartition.IsSubordinate.infPrepartition {ι : Type u_1} {I : BoxIntegral.Box ι} {π : BoxIntegral.TaggedPrepartition I} {r : (ι → ℝ) → ↑(Set.Ioi 0)} [Fintype ι] (h : BoxIntegral.TaggedPrepartition.IsSubordinate π r) (π' : BoxIntegral.Prepartition I) : BoxIntegral.TaggedPrepartition.IsSubordinate (BoxIntegral.TaggedPrepartition.infPrepartition π π') r

theorem BoxIntegral.TaggedPrepartition.IsSubordinate.mono' {ι : Type u_1} {I : BoxIntegral.Box ι} {r₁ : (ι → ℝ) → ↑(Set.Ioi 0)} {r₂ : (ι → ℝ) → ↑(Set.Ioi 0)} [Fintype ι] {π : BoxIntegral.TaggedPrepartition I} (hr₁ : BoxIntegral.TaggedPrepartition.IsSubordinate π r₁) (h : ∀ (J : BoxIntegral.Box ι), J ∈ π → r₁ (BoxIntegral.TaggedPrepartition.tag π J) ≤ r₂ (BoxIntegral.TaggedPrepartition.tag π J)) : BoxIntegral.TaggedPrepartition.IsSubordinate π r₂

theorem BoxIntegral.TaggedPrepartition.IsSubordinate.mono {ι : Type u_1} {I : BoxIntegral.Box ι} {r₁ : (ι → ℝ) → ↑(Set.Ioi 0)} {r₂ : (ι → ℝ) → ↑(Set.Ioi 0)} [Fintype ι] {π : BoxIntegral.TaggedPrepartition I} (hr₁ : BoxIntegral.TaggedPrepartition.IsSubordinate π r₁) (h : ∀ (x : ι → ℝ), x ∈ ↑BoxIntegral.Box.Icc I → r₁ x ≤ r₂ x) : BoxIntegral.TaggedPrepartition.IsSubordinate π r₂

theorem BoxIntegral.TaggedPrepartition.IsSubordinate.diam_le {ι : Type u_1} {I : BoxIntegral.Box ι} {J : BoxIntegral.Box ι} {r : (ι → ℝ) → ↑(Set.Ioi 0)} [Fintype ι] {π : BoxIntegral.TaggedPrepartition I} (h : BoxIntegral.TaggedPrepartition.IsSubordinate π r) (hJ : J ∈ π.boxes) : Metric.diam (↑BoxIntegral.Box.Icc J) ≤ 2 * ↑(r (BoxIntegral.TaggedPrepartition.tag π J))

@[simp]

theorem BoxIntegral.TaggedPrepartition.single_tag {ι : Type u_1} (I : BoxIntegral.Box ι) (J : BoxIntegral.Box ι) (hJ : J ≤ I) (x : ι → ℝ) (h : x ∈ ↑BoxIntegral.Box.Icc I) : (BoxIntegral.TaggedPrepartition.single I J hJ x h).tag = fun x => x

@[simp]

theorem BoxIntegral.TaggedPrepartition.single_boxes_val {ι : Type u_1} (I : BoxIntegral.Box ι) (J : BoxIntegral.Box ι) (hJ : J ≤ I) (x : ι → ℝ) (h : x ∈ ↑BoxIntegral.Box.Icc I) : (BoxIntegral.TaggedPrepartition.single I J hJ x h).toPrepartition.boxes.val = {J}

def BoxIntegral.TaggedPrepartition.single {ι : Type u_1} (I : BoxIntegral.Box ι) (J : BoxIntegral.Box ι) (hJ : J ≤ I) (x : ι → ℝ) (h : x ∈ ↑BoxIntegral.Box.Icc I) : BoxIntegral.TaggedPrepartition I

Tagged prepartition with single box and prescribed tag.

Equations

• BoxIntegral.TaggedPrepartition.single I J hJ x h = { toPrepartition := BoxIntegral.Prepartition.single I J hJ, tag := fun x => x, tag_mem_Icc := fun x => h }

@[simp]

theorem BoxIntegral.TaggedPrepartition.mem_single {ι : Type u_1} {I : BoxIntegral.Box ι} {J : BoxIntegral.Box ι} {x : ι → ℝ} {J' : BoxIntegral.Box ι} (hJ : J ≤ I) (h : x ∈ ↑BoxIntegral.Box.Icc I) : J' ∈ BoxIntegral.TaggedPrepartition.single I J hJ x h ↔ J' = J

instance BoxIntegral.TaggedPrepartition.instInhabitedTaggedPrepartition {ι : Type u_1} (I : BoxIntegral.Box ι) : Inhabited (BoxIntegral.TaggedPrepartition I)

Equations

• BoxIntegral.TaggedPrepartition.instInhabitedTaggedPrepartition I = { default := BoxIntegral.TaggedPrepartition.single I I (_ : I ≤ I) I.upper (_ : I.upper ∈ ↑BoxIntegral.Box.Icc I) }

theorem BoxIntegral.TaggedPrepartition.isPartition_single_iff {ι : Type u_1} {I : BoxIntegral.Box ι} {J : BoxIntegral.Box ι} {x : ι → ℝ} (hJ : J ≤ I) (h : x ∈ ↑BoxIntegral.Box.Icc I) : BoxIntegral.TaggedPrepartition.IsPartition (BoxIntegral.TaggedPrepartition.single I J hJ x h) ↔ J = I

theorem BoxIntegral.TaggedPrepartition.isPartition_single {ι : Type u_1} {I : BoxIntegral.Box ι} {x : ι → ℝ} (h : x ∈ ↑BoxIntegral.Box.Icc I) : BoxIntegral.TaggedPrepartition.IsPartition (BoxIntegral.TaggedPrepartition.single I I (_ : I ≤ I) x h)

theorem BoxIntegral.TaggedPrepartition.forall_mem_single {ι : Type u_1} {I : BoxIntegral.Box ι} {J : BoxIntegral.Box ι} {x : ι → ℝ} (p : (ι → ℝ) → BoxIntegral.Box ι → Prop) (hJ : J ≤ I) (h : x ∈ ↑BoxIntegral.Box.Icc I) : ((J' : BoxIntegral.Box ι) → J' ∈ BoxIntegral.TaggedPrepartition.single I J hJ x h → p (BoxIntegral.TaggedPrepartition.tag (BoxIntegral.TaggedPrepartition.single I J hJ x h) J') J') ↔ p x J

@[simp]

theorem BoxIntegral.TaggedPrepartition.isHenstock_single_iff {ι : Type u_1} {I : BoxIntegral.Box ι} {J : BoxIntegral.Box ι} {x : ι → ℝ} (hJ : J ≤ I) (h : x ∈ ↑BoxIntegral.Box.Icc I) : BoxIntegral.TaggedPrepartition.IsHenstock (BoxIntegral.TaggedPrepartition.single I J hJ x h) ↔ x ∈ ↑BoxIntegral.Box.Icc J

theorem BoxIntegral.TaggedPrepartition.isHenstock_single {ι : Type u_1} {I : BoxIntegral.Box ι} {x : ι → ℝ} (h : x ∈ ↑BoxIntegral.Box.Icc I) : BoxIntegral.TaggedPrepartition.IsHenstock (BoxIntegral.TaggedPrepartition.single I I (_ : I ≤ I) x h)

@[simp]

theorem BoxIntegral.TaggedPrepartition.isSubordinate_single {ι : Type u_1} {I : BoxIntegral.Box ι} {J : BoxIntegral.Box ι} {x : ι → ℝ} {r : (ι → ℝ) → ↑(Set.Ioi 0)} [Fintype ι] (hJ : J ≤ I) (h : x ∈ ↑BoxIntegral.Box.Icc I) : BoxIntegral.TaggedPrepartition.IsSubordinate (BoxIntegral.TaggedPrepartition.single I J hJ x h) r ↔ ↑BoxIntegral.Box.Icc J ⊆ Metric.closedBall x ↑(r x)

@[simp]

theorem BoxIntegral.TaggedPrepartition.iUnion_single {ι : Type u_1} {I : BoxIntegral.Box ι} {J : BoxIntegral.Box ι} {x : ι → ℝ} (hJ : J ≤ I) (h : x ∈ ↑BoxIntegral.Box.Icc I) : BoxIntegral.TaggedPrepartition.iUnion (BoxIntegral.TaggedPrepartition.single I J hJ x h) = ↑J

def BoxIntegral.TaggedPrepartition.disjUnion {ι : Type u_1} {I : BoxIntegral.Box ι} (π₁ : BoxIntegral.TaggedPrepartition I) (π₂ : BoxIntegral.TaggedPrepartition I) (h : Disjoint (BoxIntegral.TaggedPrepartition.iUnion π₁) (BoxIntegral.TaggedPrepartition.iUnion π₂)) : BoxIntegral.TaggedPrepartition I

Union of two tagged prepartitions with disjoint unions of boxes.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem BoxIntegral.TaggedPrepartition.disjUnion_boxes {ι : Type u_1} {I : BoxIntegral.Box ι} {π₁ : BoxIntegral.TaggedPrepartition I} {π₂ : BoxIntegral.TaggedPrepartition I} (h : Disjoint (BoxIntegral.TaggedPrepartition.iUnion π₁) (BoxIntegral.TaggedPrepartition.iUnion π₂)) : (BoxIntegral.TaggedPrepartition.disjUnion π₁ π₂ h).toPrepartition.boxes = π₁.boxes ∪ π₂.boxes

@[simp]

theorem BoxIntegral.TaggedPrepartition.mem_disjUnion {ι : Type u_1} {I : BoxIntegral.Box ι} {J : BoxIntegral.Box ι} {π₁ : BoxIntegral.TaggedPrepartition I} {π₂ : BoxIntegral.TaggedPrepartition I} (h : Disjoint (BoxIntegral.TaggedPrepartition.iUnion π₁) (BoxIntegral.TaggedPrepartition.iUnion π₂)) : J ∈ BoxIntegral.TaggedPrepartition.disjUnion π₁ π₂ h ↔ J ∈ π₁ ∨ J ∈ π₂

@[simp]

theorem BoxIntegral.TaggedPrepartition.iUnion_disjUnion {ι : Type u_1} {I : BoxIntegral.Box ι} {π₁ : BoxIntegral.TaggedPrepartition I} {π₂ : BoxIntegral.TaggedPrepartition I} (h : Disjoint (BoxIntegral.TaggedPrepartition.iUnion π₁) (BoxIntegral.TaggedPrepartition.iUnion π₂)) : BoxIntegral.TaggedPrepartition.iUnion (BoxIntegral.TaggedPrepartition.disjUnion π₁ π₂ h) = BoxIntegral.TaggedPrepartition.iUnion π₁ ∪ BoxIntegral.TaggedPrepartition.iUnion π₂

theorem BoxIntegral.TaggedPrepartition.disjUnion_tag_of_mem_left {ι : Type u_1} {I : BoxIntegral.Box ι} {J : BoxIntegral.Box ι} {π₁ : BoxIntegral.TaggedPrepartition I} {π₂ : BoxIntegral.TaggedPrepartition I} (h : Disjoint (BoxIntegral.TaggedPrepartition.iUnion π₁) (BoxIntegral.TaggedPrepartition.iUnion π₂)) (hJ : J ∈ π₁) : BoxIntegral.TaggedPrepartition.tag (BoxIntegral.TaggedPrepartition.disjUnion π₁ π₂ h) J = BoxIntegral.TaggedPrepartition.tag π₁ J

theorem BoxIntegral.TaggedPrepartition.disjUnion_tag_of_mem_right {ι : Type u_1} {I : BoxIntegral.Box ι} {J : BoxIntegral.Box ι} {π₁ : BoxIntegral.TaggedPrepartition I} {π₂ : BoxIntegral.TaggedPrepartition I} (h : Disjoint (BoxIntegral.TaggedPrepartition.iUnion π₁) (BoxIntegral.TaggedPrepartition.iUnion π₂)) (hJ : J ∈ π₂) : BoxIntegral.TaggedPrepartition.tag (BoxIntegral.TaggedPrepartition.disjUnion π₁ π₂ h) J = BoxIntegral.TaggedPrepartition.tag π₂ J

theorem BoxIntegral.TaggedPrepartition.IsSubordinate.disjUnion {ι : Type u_1} {I : BoxIntegral.Box ι} {π₁ : BoxIntegral.TaggedPrepartition I} {π₂ : BoxIntegral.TaggedPrepartition I} {r : (ι → ℝ) → ↑(Set.Ioi 0)} [Fintype ι] (h₁ : BoxIntegral.TaggedPrepartition.IsSubordinate π₁ r) (h₂ : BoxIntegral.TaggedPrepartition.IsSubordinate π₂ r) (h : Disjoint (BoxIntegral.TaggedPrepartition.iUnion π₁) (BoxIntegral.TaggedPrepartition.iUnion π₂)) : BoxIntegral.TaggedPrepartition.IsSubordinate (BoxIntegral.TaggedPrepartition.disjUnion π₁ π₂ h) r

theorem BoxIntegral.TaggedPrepartition.IsHenstock.disjUnion {ι : Type u_1} {I : BoxIntegral.Box ι} {π₁ : BoxIntegral.TaggedPrepartition I} {π₂ : BoxIntegral.TaggedPrepartition I} (h₁ : BoxIntegral.TaggedPrepartition.IsHenstock π₁) (h₂ : BoxIntegral.TaggedPrepartition.IsHenstock π₂) (h : Disjoint (BoxIntegral.TaggedPrepartition.iUnion π₁) (BoxIntegral.TaggedPrepartition.iUnion π₂)) : BoxIntegral.TaggedPrepartition.IsHenstock (BoxIntegral.TaggedPrepartition.disjUnion π₁ π₂ h)

def BoxIntegral.TaggedPrepartition.embedBox {ι : Type u_1} (I : BoxIntegral.Box ι) (J : BoxIntegral.Box ι) (h : I ≤ J) : BoxIntegral.TaggedPrepartition I ↪ BoxIntegral.TaggedPrepartition J

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

Equations

• One or more equations did not get rendered due to their size.

def BoxIntegral.TaggedPrepartition.distortion {ι : Type u_1} {I : BoxIntegral.Box ι} (π : BoxIntegral.TaggedPrepartition I) [Fintype ι] : NNReal

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

Equations

• BoxIntegral.TaggedPrepartition.distortion π = BoxIntegral.Prepartition.distortion π.toPrepartition

theorem BoxIntegral.TaggedPrepartition.distortion_le_of_mem {ι : Type u_1} {I : BoxIntegral.Box ι} {J : BoxIntegral.Box ι} (π : BoxIntegral.TaggedPrepartition I) [Fintype ι] (h : J ∈ π) : BoxIntegral.Box.distortion J ≤ BoxIntegral.TaggedPrepartition.distortion π

theorem BoxIntegral.TaggedPrepartition.distortion_le_iff {ι : Type u_1} {I : BoxIntegral.Box ι} (π : BoxIntegral.TaggedPrepartition I) [Fintype ι] {c : NNReal} : BoxIntegral.TaggedPrepartition.distortion π ≤ c ↔ ∀ (J : BoxIntegral.Box ι), J ∈ π → BoxIntegral.Box.distortion J ≤ c

@[simp]

theorem BoxIntegral.Prepartition.distortion_biUnionTagged {ι : Type u_1} {I : BoxIntegral.Box ι} [Fintype ι] (π : BoxIntegral.Prepartition I) (πi : (J : BoxIntegral.Box ι) → BoxIntegral.TaggedPrepartition J) : BoxIntegral.TaggedPrepartition.distortion (BoxIntegral.Prepartition.biUnionTagged π πi) = Finset.sup π.boxes fun J => BoxIntegral.TaggedPrepartition.distortion (πi J)

@[simp]

theorem BoxIntegral.TaggedPrepartition.distortion_biUnionPrepartition {ι : Type u_1} {I : BoxIntegral.Box ι} [Fintype ι] (π : BoxIntegral.TaggedPrepartition I) (πi : (J : BoxIntegral.Box ι) → BoxIntegral.Prepartition J) : BoxIntegral.TaggedPrepartition.distortion (BoxIntegral.TaggedPrepartition.biUnionPrepartition π πi) = Finset.sup π.boxes fun J => BoxIntegral.Prepartition.distortion (πi J)

@[simp]

theorem BoxIntegral.TaggedPrepartition.distortion_disjUnion {ι : Type u_1} {I : BoxIntegral.Box ι} {π₁ : BoxIntegral.TaggedPrepartition I} {π₂ : BoxIntegral.TaggedPrepartition I} [Fintype ι] (h : Disjoint (BoxIntegral.TaggedPrepartition.iUnion π₁) (BoxIntegral.TaggedPrepartition.iUnion π₂)) : BoxIntegral.TaggedPrepartition.distortion (BoxIntegral.TaggedPrepartition.disjUnion π₁ π₂ h) = max (BoxIntegral.TaggedPrepartition.distortion π₁) (BoxIntegral.TaggedPrepartition.distortion π₂)

theorem BoxIntegral.TaggedPrepartition.distortion_of_const {ι : Type u_1} {I : BoxIntegral.Box ι} (π : BoxIntegral.TaggedPrepartition I) [Fintype ι] {c : NNReal} (h₁ : Finset.Nonempty π.boxes) (h₂ : ∀ (J : BoxIntegral.Box ι), J ∈ π → BoxIntegral.Box.distortion J = c) : BoxIntegral.TaggedPrepartition.distortion π = c

@[simp]

theorem BoxIntegral.TaggedPrepartition.distortion_single {ι : Type u_1} {I : BoxIntegral.Box ι} {J : BoxIntegral.Box ι} {x : ι → ℝ} [Fintype ι] (hJ : J ≤ I) (h : x ∈ ↑BoxIntegral.Box.Icc I) : BoxIntegral.TaggedPrepartition.distortion (BoxIntegral.TaggedPrepartition.single I J hJ x h) = BoxIntegral.Box.distortion J

theorem BoxIntegral.TaggedPrepartition.distortion_filter_le {ι : Type u_1} {I : BoxIntegral.Box ι} (π : BoxIntegral.TaggedPrepartition I) [Fintype ι] (p : BoxIntegral.Box ι → Prop) : BoxIntegral.TaggedPrepartition.distortion (BoxIntegral.TaggedPrepartition.filter π p) ≤ BoxIntegral.TaggedPrepartition.distortion π