# Induction on subboxes #

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

def BoxIntegral.Box.splitCenterBox {ι : Type u_1} (I : ) (s : Set ι) :

For a box I, the hyperplanes passing through its center split I into 2 ^ card ι boxes. BoxIntegral.Box.splitCenterBox I s is one of these boxes. See also BoxIntegral.Partition.splitCenter for the corresponding BoxIntegral.Partition.

Equations
• I.splitCenterBox s = { lower := s.piecewise (fun (i : ι) => (I.lower i + I.upper i) / 2) I.lower, upper := s.piecewise I.upper fun (i : ι) => (I.lower i + I.upper i) / 2, lower_lt_upper := }
Instances For
theorem BoxIntegral.Box.mem_splitCenterBox {ι : Type u_1} {I : } {s : Set ι} {y : ι} :
y I.splitCenterBox s y I ∀ (i : ι), (I.lower i + I.upper i) / 2 < y i i s
theorem BoxIntegral.Box.splitCenterBox_le {ι : Type u_1} (I : ) (s : Set ι) :
I.splitCenterBox s I
theorem BoxIntegral.Box.disjoint_splitCenterBox {ι : Type u_1} (I : ) {s : Set ι} {t : Set ι} (h : s t) :
Disjoint (I.splitCenterBox s) (I.splitCenterBox t)
theorem BoxIntegral.Box.injective_splitCenterBox {ι : Type u_1} (I : ) :
Function.Injective I.splitCenterBox
@[simp]
theorem BoxIntegral.Box.exists_mem_splitCenterBox {ι : Type u_1} {I : } {x : ι} :
(∃ (s : Set ι), x I.splitCenterBox s) x I
@[simp]
theorem BoxIntegral.Box.splitCenterBoxEmb_apply {ι : Type u_1} (I : ) (s : Set ι) :
I.splitCenterBoxEmb s = I.splitCenterBox s
def BoxIntegral.Box.splitCenterBoxEmb {ι : Type u_1} (I : ) :

BoxIntegral.Box.splitCenterBox bundled as a Function.Embedding.

Equations
• I.splitCenterBoxEmb = { toFun := I.splitCenterBox, inj' := }
Instances For
@[simp]
theorem BoxIntegral.Box.iUnion_coe_splitCenterBox {ι : Type u_1} (I : ) :
⋃ (s : Set ι), (I.splitCenterBox s) = I
@[simp]
theorem BoxIntegral.Box.upper_sub_lower_splitCenterBox {ι : Type u_1} (I : ) (s : Set ι) (i : ι) :
(I.splitCenterBox s).upper i - (I.splitCenterBox s).lower i = (I.upper i - I.lower i) / 2
theorem BoxIntegral.Box.subbox_induction_on' {ι : Type u_1} {p : } (I : ) (H_ind : JI, (∀ (s : Set ι), p (J.splitCenterBox s))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.

• 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 BoxIntegral.Box.subbox_induction_on for a version using BoxIntegral.Prepartition.splitCenter instead of BoxIntegral.Box.splitCenterBox.

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.