# mathlibdocumentation

analysis.box_integral.partition.subbox_induction

# Induction on subboxes #

In this file we prove (see box_integral.tagged_partition.exists_is_Henstock_is_subordinate_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

noncomputable def box_integral.prepartition.split_center {ι : Type u_1} [fintype ι] (I : box_integral.box ι) :

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

Equations
@[simp]
theorem box_integral.prepartition.mem_split_center {ι : Type u_1} [fintype ι] {I J : box_integral.box ι} :
∃ (s : set ι), = J
theorem box_integral.prepartition.upper_sub_lower_of_mem_split_center {ι : Type u_1} [fintype ι] {I J : box_integral.box ι} (i : ι) :
J.upper i - J.lower i = (I.upper i - I.lower i) / 2
theorem box_integral.box.subbox_induction_on {ι : Type u_1} [fintype ι] {p : → Prop} (I : box_integral.box ι) (H_ind : ∀ (J : , J I(∀ (J' : , p J')p J) (H_nhds : ∀ (z : ι → ), (∃ (U : set (ι → )) (H : U , ∀ (J : , J I∀ (m : ), (∀ (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 box_integral.box.subbox_induction_on' for a version using box_integral.box.split_center_box instead of box_integral.prepartition.split_center.

theorem box_integral.box.exists_tagged_partition_is_Henstock_is_subordinate_homothetic {ι : Type u_1} [fintype ι] (I : box_integral.box ι) (r : (ι → )(set.Ioi 0)) :
∃ (π : , π.is_partition π.is_Henstock (∀ (J : , J π(∃ (m : ), ∀ (i : ι), J.upper i - J.lower i = (I.upper i - I.lower i) / 2 ^ m))

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.

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 π.
noncomputable def box_integral.prepartition.to_subordinate {ι : Type u_1} [fintype ι] {I : box_integral.box ι} (r : (ι → )(set.Ioi 0)) :

Given a prepartition π of a box I and a function r : ℝⁿ → (0, ∞), π.to_subordinate 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
theorem box_integral.prepartition.to_subordinate_to_prepartition_le {ι : Type u_1} [fintype ι] {I : box_integral.box ι} (r : (ι → )(set.Ioi 0)) :
π
theorem box_integral.prepartition.is_Henstock_to_subordinate {ι : Type u_1} [fintype ι] {I : box_integral.box ι} (r : (ι → )(set.Ioi 0)) :
@[simp]
theorem box_integral.prepartition.distortion_to_subordinate {ι : Type u_1} [fintype ι] {I : box_integral.box ι} (r : (ι → )(set.Ioi 0)) :
@[simp]
theorem box_integral.prepartition.Union_to_subordinate {ι : Type u_1} [fintype ι] {I : box_integral.box ι} (r : (ι → )(set.Ioi 0)) :
noncomputable def box_integral.tagged_prepartition.union_compl_to_subordinate {ι : Type u_1} [fintype ι] {I : box_integral.box ι} (π₂ : box_integral.prepartition I) (hU : π₂.Union = I \ π₁.Union) (r : (ι → )(set.Ioi 0)) :

Given a tagged prepartition π₁, a prepartition π₂ that covers exactly I \ π₁.Union, and a function r : ℝⁿ → (0, ∞), returns the union of π₁ and π₂.to_subordinate 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
theorem box_integral.tagged_prepartition.is_partition_union_compl_to_subordinate {ι : Type u_1} [fintype ι] {I : box_integral.box ι} (π₂ : box_integral.prepartition I) (hU : π₂.Union = I \ π₁.Union) (r : (ι → )(set.Ioi 0)) :
@[simp]
theorem box_integral.tagged_prepartition.union_compl_to_subordinate_boxes {ι : Type u_1} [fintype ι] {I : box_integral.box ι} (π₂ : box_integral.prepartition I) (hU : π₂.Union = I \ π₁.Union) (r : (ι → )(set.Ioi 0)) :
@[simp]
theorem box_integral.tagged_prepartition.Union_union_compl_to_subordinate_boxes {ι : Type u_1} [fintype ι] {I : box_integral.box ι} (π₂ : box_integral.prepartition I) (hU : π₂.Union = I \ π₁.Union) (r : (ι → )(set.Ioi 0)) :
hU r).Union = I
@[simp]
theorem box_integral.tagged_prepartition.distortion_union_compl_to_subordinate {ι : Type u_1} [fintype ι] {I : box_integral.box ι} (π₂ : box_integral.prepartition I) (hU : π₂.Union = I \ π₁.Union) (r : (ι → )(set.Ioi 0)) :
hU r).distortion =