# mathlibdocumentation

analysis.box_integral.box.subbox_induction

# Induction on subboxes #

In this file we prove the following induction principle for box_integral.box, see box_integral.box.subbox_induction_on. Let p be a predicate on box_integral.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 is 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.

## Tags #

rectangular box, induction

noncomputable def box_integral.box.split_center_box {ι : Type u_1} (I : box_integral.box ι) (s : set ι) :

For a box I, the hyperplanes passing through its center split I into 2 ^ card ι boxes. box_integral.box.split_center_box I s is one of these boxes. See also box_integral.partition.split_center for the corresponding box_integral.partition.

Equations
theorem box_integral.box.mem_split_center_box {ι : Type u_1} {I : box_integral.box ι} {s : set ι} {y : ι → } :
y y I ∀ (i : ι), (I.lower i + I.upper i) / 2 < y i i s
theorem box_integral.box.split_center_box_le {ι : Type u_1} (I : box_integral.box ι) (s : set ι) :
I
theorem box_integral.box.disjoint_split_center_box {ι : Type u_1} (I : box_integral.box ι) {s t : set ι} (h : s t) :
@[simp]
theorem box_integral.box.exists_mem_split_center_box {ι : Type u_1} {I : box_integral.box ι} {x : ι → } :
(∃ (s : set ι), x I.split_center_box s) x I
noncomputable def box_integral.box.split_center_box_emb {ι : Type u_1} (I : box_integral.box ι) :

box_integral.box.split_center_box bundled as a function.embedding.

Equations
@[simp]
@[simp]
theorem box_integral.box.Union_coe_split_center_box {ι : Type u_1} (I : box_integral.box ι) :
(⋃ (s : set ι), (I.split_center_box s)) = I
@[simp]
theorem box_integral.box.upper_sub_lower_split_center_box {ι : Type u_1} (I : box_integral.box ι) (s : set ι) (i : ι) :
theorem box_integral.box.subbox_induction_on' {ι : Type u_1} {p : → Prop} (I : box_integral.box ι) (H_ind : ∀ (J : , J I(∀ (s : set ι), p (J.split_center_box s))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.

• H_ind : 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.

• H_nhds : 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.prepartition.split_center instead of box_integral.box.split_center_box.

The proof still works if we assume H_ind only for subboxes J ≤ I that are homothetic to I with a coefficient of the form 2⁻ᵐ but we do not need this generalization yet.