Induction on subboxes

In this file we prove (see BoxIntegral.Box.exists_taggedPartition_isHenstock_isSubordinate_homothetic) that for every box I in ℝⁿ and a function r : ℝⁿ → ℝ positive on I there exists a tagged partition π of I such that

• π is a Henstock partition;
• π is subordinate to r;
• each box in π is homothetic to I with coefficient of the form 1 / 2 ^ n.

Later we will use this lemma to prove that the Henstock filter is nontrivial, hence the Henstock integral is well-defined.

Tags

partition, tagged partition, Henstock integral

def BoxIntegral.Prepartition.splitCenter {ι : Type u_1} [Fintype ι] (I : BoxIntegral.Box ι) : BoxIntegral.Prepartition I

Split a box in ℝⁿ into 2 ^ n boxes by hyperplanes passing through its center.

Equations

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

@[simp]

theorem BoxIntegral.Prepartition.mem_splitCenter {ι : Type u_1} [Fintype ι] {I : BoxIntegral.Box ι} {J : BoxIntegral.Box ι} : J ∈ BoxIntegral.Prepartition.splitCenter I ↔ ∃ s, BoxIntegral.Box.splitCenterBox I s = J

theorem BoxIntegral.Prepartition.isPartition_splitCenter {ι : Type u_1} [Fintype ι] (I : BoxIntegral.Box ι) : BoxIntegral.Prepartition.IsPartition (BoxIntegral.Prepartition.splitCenter I)

theorem BoxIntegral.Prepartition.upper_sub_lower_of_mem_splitCenter {ι : Type u_1} [Fintype ι] {I : BoxIntegral.Box ι} {J : BoxIntegral.Box ι} (h : J ∈ BoxIntegral.Prepartition.splitCenter I) (i : ι) : BoxIntegral.Box.upper J i - BoxIntegral.Box.lower J i = (BoxIntegral.Box.upper I i - BoxIntegral.Box.lower I i) / 2

theorem BoxIntegral.Box.subbox_induction_on {ι : Type u_1} [Fintype ι] {p : BoxIntegral.Box ι → Prop} (I : BoxIntegral.Box ι) (H_ind : (J : BoxIntegral.Box ι) → J ≤ I → ((J' : BoxIntegral.Box ι) → J' ∈ BoxIntegral.Prepartition.splitCenter J → p J') → p J) (H_nhds : ∀ (z : ι → ℝ), z ∈ ↑BoxIntegral.Box.Icc I → ∃ U, U ∈ nhdsWithin z (↑BoxIntegral.Box.Icc I) ∧ ((J : BoxIntegral.Box ι) → J ≤ I → (m : ℕ) → z ∈ ↑BoxIntegral.Box.Icc J → ↑BoxIntegral.Box.Icc J ⊆ U → (∀ (i : ι), BoxIntegral.Box.upper J i - BoxIntegral.Box.lower J i = (BoxIntegral.Box.upper I i - BoxIntegral.Box.lower I i) / 2 ^ m) → p J)) : p I

Let p be a predicate on Box ι, let I be a box. Suppose that the following two properties hold true.

• Consider a smaller box J ≤ I. The hyperplanes passing through the center of J split it into 2 ^ n boxes. If p holds true on each of these boxes, then it true on J.
• For each z in the closed box I.Icc there exists a neighborhood U of z within I.Icc such that for every box J ≤ I such that z ∈ J.Icc ⊆ U, if J is homothetic to I with a coefficient of the form 1 / 2 ^ m, then p is true on J.

Then p I is true. See also BoxIntegral.Box.subbox_induction_on' for a version using BoxIntegral.Box.splitCenterBox instead of BoxIntegral.Prepartition.splitCenter.

theorem BoxIntegral.Box.exists_taggedPartition_isHenstock_isSubordinate_homothetic {ι : Type u_1} [Fintype ι] (I : BoxIntegral.Box ι) (r : (ι → ℝ) → ↑(Set.Ioi 0)) : ∃ π, BoxIntegral.TaggedPrepartition.IsPartition π ∧ BoxIntegral.TaggedPrepartition.IsHenstock π ∧ BoxIntegral.TaggedPrepartition.IsSubordinate π r ∧ (∀ (J : BoxIntegral.Box ι), J ∈ π → ∃ m, ∀ (i : ι), BoxIntegral.Box.upper J i - BoxIntegral.Box.lower J i = (BoxIntegral.Box.upper I i - BoxIntegral.Box.lower I i) / 2 ^ m) ∧ BoxIntegral.TaggedPrepartition.distortion π = BoxIntegral.Box.distortion I

Given a box I in ℝⁿ and a function r : ℝⁿ → (0, ∞), there exists a tagged partition π of I such that

• π is a Henstock partition;
• π is subordinate to r;
• each box in π is homothetic to I with coefficient of the form 1 / 2 ^ m.

This lemma implies that the Henstock filter is nontrivial, hence the Henstock integral is well-defined.

theorem BoxIntegral.Prepartition.exists_tagged_le_isHenstock_isSubordinate_iUnion_eq {ι : Type u_1} [Fintype ι] {I : BoxIntegral.Box ι} (r : (ι → ℝ) → ↑(Set.Ioi 0)) (π : BoxIntegral.Prepartition I) : ∃ π', π'.toPrepartition ≤ π ∧ BoxIntegral.TaggedPrepartition.IsHenstock π' ∧ BoxIntegral.TaggedPrepartition.IsSubordinate π' r ∧ BoxIntegral.TaggedPrepartition.distortion π' = BoxIntegral.Prepartition.distortion π ∧ BoxIntegral.TaggedPrepartition.iUnion π' = BoxIntegral.Prepartition.iUnion π

Given a box I in ℝⁿ, a function r : ℝⁿ → (0, ∞), and a prepartition π of I, there exists a tagged prepartition π' of I such that

• each box of π' is included in some box of π;
• π' is a Henstock partition;
• π' is subordinate to r;
• π' covers exactly the same part of I as π;
• the distortion of π' is equal to the distortion of π.

def BoxIntegral.Prepartition.toSubordinate {ι : Type u_1} [Fintype ι] {I : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I) (r : (ι → ℝ) → ↑(Set.Ioi 0)) : BoxIntegral.TaggedPrepartition I

Given a prepartition π of a box I and a function r : ℝⁿ → (0, ∞), π.toSubordinate r is a tagged partition π' such that

• each box of π' is included in some box of π;
• π' is a Henstock partition;
• π' is subordinate to r;
• π' covers exactly the same part of I as π;
• the distortion of π' is equal to the distortion of π.

Equations

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

theorem BoxIntegral.Prepartition.toSubordinate_toPrepartition_le {ι : Type u_1} [Fintype ι] {I : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I) (r : (ι → ℝ) → ↑(Set.Ioi 0)) : (BoxIntegral.Prepartition.toSubordinate π r).toPrepartition ≤ π

theorem BoxIntegral.Prepartition.isHenstock_toSubordinate {ι : Type u_1} [Fintype ι] {I : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I) (r : (ι → ℝ) → ↑(Set.Ioi 0)) : BoxIntegral.TaggedPrepartition.IsHenstock (BoxIntegral.Prepartition.toSubordinate π r)

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

@[simp]

theorem BoxIntegral.Prepartition.distortion_toSubordinate {ι : Type u_1} [Fintype ι] {I : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I) (r : (ι → ℝ) → ↑(Set.Ioi 0)) : BoxIntegral.TaggedPrepartition.distortion (BoxIntegral.Prepartition.toSubordinate π r) = BoxIntegral.Prepartition.distortion π

@[simp]

theorem BoxIntegral.Prepartition.iUnion_toSubordinate {ι : Type u_1} [Fintype ι] {I : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I) (r : (ι → ℝ) → ↑(Set.Ioi 0)) : BoxIntegral.TaggedPrepartition.iUnion (BoxIntegral.Prepartition.toSubordinate π r) = BoxIntegral.Prepartition.iUnion π

def BoxIntegral.TaggedPrepartition.unionComplToSubordinate {ι : Type u_1} [Fintype ι] {I : BoxIntegral.Box ι} (π₁ : BoxIntegral.TaggedPrepartition I) (π₂ : BoxIntegral.Prepartition I) (hU : BoxIntegral.Prepartition.iUnion π₂ = ↑I \ BoxIntegral.TaggedPrepartition.iUnion π₁) (r : (ι → ℝ) → ↑(Set.Ioi 0)) : BoxIntegral.TaggedPrepartition I

Given a tagged prepartition π₁, a prepartition π₂ that covers exactly I \ π₁.iUnion, and a function r : ℝⁿ → (0, ∞), returns the union of π₁ and π₂.toSubordinate r. This partition π has the following properties:

• π is a partition, i.e. it covers the whole I;
• π₁.boxes ⊆ π.boxes;
• π.tag J = π₁.tag J whenever J ∈ π₁;
• π is Henstock outside of π₁: π.tag J ∈ J.Icc whenever J ∈ π, J ∉ π₁;
• π is subordinate to r outside of π₁;
• the distortion of π is equal to the maximum of the distortions of π₁ and π₂.

Equations

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

theorem BoxIntegral.TaggedPrepartition.isPartition_unionComplToSubordinate {ι : Type u_1} [Fintype ι] {I : BoxIntegral.Box ι} (π₁ : BoxIntegral.TaggedPrepartition I) (π₂ : BoxIntegral.Prepartition I) (hU : BoxIntegral.Prepartition.iUnion π₂ = ↑I \ BoxIntegral.TaggedPrepartition.iUnion π₁) (r : (ι → ℝ) → ↑(Set.Ioi 0)) : BoxIntegral.TaggedPrepartition.IsPartition (BoxIntegral.TaggedPrepartition.unionComplToSubordinate π₁ π₂ hU r)

@[simp]

theorem BoxIntegral.TaggedPrepartition.unionComplToSubordinate_boxes {ι : Type u_1} [Fintype ι] {I : BoxIntegral.Box ι} (π₁ : BoxIntegral.TaggedPrepartition I) (π₂ : BoxIntegral.Prepartition I) (hU : BoxIntegral.Prepartition.iUnion π₂ = ↑I \ BoxIntegral.TaggedPrepartition.iUnion π₁) (r : (ι → ℝ) → ↑(Set.Ioi 0)) : (BoxIntegral.TaggedPrepartition.unionComplToSubordinate π₁ π₂ hU r).toPrepartition.boxes = π₁.boxes ∪ (BoxIntegral.Prepartition.toSubordinate π₂ r).toPrepartition.boxes

@[simp]

theorem BoxIntegral.TaggedPrepartition.iUnion_unionComplToSubordinate_boxes {ι : Type u_1} [Fintype ι] {I : BoxIntegral.Box ι} (π₁ : BoxIntegral.TaggedPrepartition I) (π₂ : BoxIntegral.Prepartition I) (hU : BoxIntegral.Prepartition.iUnion π₂ = ↑I \ BoxIntegral.TaggedPrepartition.iUnion π₁) (r : (ι → ℝ) → ↑(Set.Ioi 0)) : BoxIntegral.TaggedPrepartition.iUnion (BoxIntegral.TaggedPrepartition.unionComplToSubordinate π₁ π₂ hU r) = ↑I

@[simp]

theorem BoxIntegral.TaggedPrepartition.distortion_unionComplToSubordinate {ι : Type u_1} [Fintype ι] {I : BoxIntegral.Box ι} (π₁ : BoxIntegral.TaggedPrepartition I) (π₂ : BoxIntegral.Prepartition I) (hU : BoxIntegral.Prepartition.iUnion π₂ = ↑I \ BoxIntegral.TaggedPrepartition.iUnion π₁) (r : (ι → ℝ) → ↑(Set.Ioi 0)) : BoxIntegral.TaggedPrepartition.distortion (BoxIntegral.TaggedPrepartition.unionComplToSubordinate π₁ π₂ hU r) = max (BoxIntegral.TaggedPrepartition.distortion π₁) (BoxIntegral.Prepartition.distortion π₂)