# Documentation

Mathlib.Analysis.BoxIntegral.Partition.SubboxInduction

# 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.

Instances For
@[simp]
theorem BoxIntegral.Prepartition.mem_splitCenter {ι : Type u_1} [] {I : } {J : } :
theorem BoxIntegral.Prepartition.upper_sub_lower_of_mem_splitCenter {ι : Type u_1} [] {I : } {J : } (h : ) (i : ι) :
= () / 2
theorem BoxIntegral.Box.subbox_induction_on {ι : Type u_1} [] {p : } (I : ) (H_ind : (J : ) → J I((J' : ) → p J') → p J) (H_nhds : ∀ (z : ι), z BoxIntegral.Box.Icc IU, U nhdsWithin z (BoxIntegral.Box.Icc I) ((J : ) → J I(m : ) → z BoxIntegral.Box.Icc JBoxIntegral.Box.Icc J U(∀ (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 : (ι) → ↑()) :
π, (∀ (J : ), J πm, ∀ (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.

theorem BoxIntegral.Prepartition.exists_tagged_le_isHenstock_isSubordinate_iUnion_eq {ι : Type u_1} [] {I : } (r : (ι) → ↑()) (π : ) :
π', π'.toPrepartition π

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 π.
Instances For
theorem BoxIntegral.Prepartition.toSubordinate_toPrepartition_le {ι : Type u_1} [] {I : } (π : ) (r : (ι) → ↑()) :
().toPrepartition π
theorem BoxIntegral.Prepartition.isHenstock_toSubordinate {ι : Type u_1} [] {I : } (π : ) (r : (ι) → ↑()) :
theorem BoxIntegral.Prepartition.isSubordinate_toSubordinate {ι : Type u_1} [] {I : } (π : ) (r : (ι) → ↑()) :
@[simp]
theorem BoxIntegral.Prepartition.distortion_toSubordinate {ι : Type u_1} [] {I : } (π : ) (r : (ι) → ↑()) :
@[simp]
theorem BoxIntegral.Prepartition.iUnion_toSubordinate {ι : Type u_1} [] {I : } (π : ) (r : (ι) → ↑()) :
def BoxIntegral.TaggedPrepartition.unionComplToSubordinate {ι : Type u_1} [] {I : } (π₁ : ) (π₂ : ) (hU : ) (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 π₂.
Instances For
theorem BoxIntegral.TaggedPrepartition.isPartition_unionComplToSubordinate {ι : Type u_1} [] {I : } (π₁ : ) (π₂ : ) (hU : ) (r : (ι) → ↑()) :
@[simp]
theorem BoxIntegral.TaggedPrepartition.unionComplToSubordinate_boxes {ι : Type u_1} [] {I : } (π₁ : ) (π₂ : ) (hU : ) (r : (ι) → ↑()) :
().toPrepartition.boxes = π₁.boxes ().toPrepartition.boxes
@[simp]
theorem BoxIntegral.TaggedPrepartition.iUnion_unionComplToSubordinate_boxes {ι : Type u_1} [] {I : } (π₁ : ) (π₂ : ) (hU : ) (r : (ι) → ↑()) :
@[simp]
theorem BoxIntegral.TaggedPrepartition.distortion_unionComplToSubordinate {ι : Type u_1} [] {I : } (π₁ : ) (π₂ : ) (hU : ) (r : (ι) → ↑()) :