# 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} [] (I : ) :

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

Equations
• = { boxes := Finset.map I.splitCenterBoxEmb Finset.univ, le_of_mem' := , pairwiseDisjoint := }
Instances For
@[simp]
theorem BoxIntegral.Prepartition.mem_splitCenter {ι : Type u_1} [] {I : } {J : } :
∃ (s : Set ι), I.splitCenterBox s = J
theorem BoxIntegral.Prepartition.isPartition_splitCenter {ι : Type u_1} [] (I : ) :
.IsPartition
theorem BoxIntegral.Prepartition.upper_sub_lower_of_mem_splitCenter {ι : Type u_1} [] {I : } {J : } (h : ) (i : ι) :
J.upper i - J.lower i = (I.upper i - I.lower i) / 2
theorem BoxIntegral.Box.subbox_induction_on {ι : Type u_1} [] {p : } (I : ) (H_ind : JI, (J', p J')p J) (H_nhds : zBoxIntegral.Box.Icc I, UnhdsWithin z (BoxIntegral.Box.Icc I), JI, ∀ (m : ), z BoxIntegral.Box.Icc JBoxIntegral.Box.Icc J U(∀ (i : ι), J.upper i - J.lower i = (I.upper i - I.lower 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} [] (I : ) (r : (ι)()) :
∃ (π : ), π.IsPartition π.IsHenstock π.IsSubordinate r (Jπ, ∃ (m : ), ∀ (i : ι), J.upper i - J.lower i = (I.upper i - I.lower i) / 2 ^ m) π.distortion = I.distortion

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} [] {I : } (r : (ι)()) (π : ) :
∃ (π' : ), π'.toPrepartition π π'.IsHenstock π'.IsSubordinate r π'.distortion = π.distortion π'.iUnion = π.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} [] {I : } (π : ) (r : (ι)()) :

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
• π.toSubordinate r = .choose
Instances For
theorem BoxIntegral.Prepartition.toSubordinate_toPrepartition_le {ι : Type u_1} [] {I : } (π : ) (r : (ι)()) :
(π.toSubordinate r).toPrepartition π
theorem BoxIntegral.Prepartition.isHenstock_toSubordinate {ι : Type u_1} [] {I : } (π : ) (r : (ι)()) :
(π.toSubordinate r).IsHenstock
theorem BoxIntegral.Prepartition.isSubordinate_toSubordinate {ι : Type u_1} [] {I : } (π : ) (r : (ι)()) :
(π.toSubordinate r).IsSubordinate r
@[simp]
theorem BoxIntegral.Prepartition.distortion_toSubordinate {ι : Type u_1} [] {I : } (π : ) (r : (ι)()) :
(π.toSubordinate r).distortion = π.distortion
@[simp]
theorem BoxIntegral.Prepartition.iUnion_toSubordinate {ι : Type u_1} [] {I : } (π : ) (r : (ι)()) :
(π.toSubordinate r).iUnion = π.iUnion
def BoxIntegral.TaggedPrepartition.unionComplToSubordinate {ι : Type u_1} [] {I : } (π₁ : ) (π₂ : ) (hU : π₂.iUnion = I \ π₁.iUnion) (r : (ι)()) :

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
• π₁.unionComplToSubordinate π₂ hU r = π₁.disjUnion (π₂.toSubordinate r)
Instances For
theorem BoxIntegral.TaggedPrepartition.isPartition_unionComplToSubordinate {ι : Type u_1} [] {I : } (π₁ : ) (π₂ : ) (hU : π₂.iUnion = I \ π₁.iUnion) (r : (ι)()) :
(π₁.unionComplToSubordinate π₂ hU r).IsPartition
@[simp]
theorem BoxIntegral.TaggedPrepartition.unionComplToSubordinate_boxes {ι : Type u_1} [] {I : } (π₁ : ) (π₂ : ) (hU : π₂.iUnion = I \ π₁.iUnion) (r : (ι)()) :
(π₁.unionComplToSubordinate π₂ hU r).boxes = π₁.boxes (π₂.toSubordinate r).boxes
@[simp]
theorem BoxIntegral.TaggedPrepartition.iUnion_unionComplToSubordinate_boxes {ι : Type u_1} [] {I : } (π₁ : ) (π₂ : ) (hU : π₂.iUnion = I \ π₁.iUnion) (r : (ι)()) :
(π₁.unionComplToSubordinate π₂ hU r).iUnion = I
@[simp]
theorem BoxIntegral.TaggedPrepartition.distortion_unionComplToSubordinate {ι : Type u_1} [] {I : } (π₁ : ) (π₂ : ) (hU : π₂.iUnion = I \ π₁.iUnion) (r : (ι)()) :
(π₁.unionComplToSubordinate π₂ hU r).distortion = max π₁.distortion π₂.distortion