mathlib documentation

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.

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 I.split_center_box s y I (i : ι), (I.lower i + I.upper i) / 2 < y i i s
@[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
@[simp]
@[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 : box_integral.box ι Prop} (I : box_integral.box ι) (H_ind : (J : box_integral.box ι), J I ( (s : set ι), p (J.split_center_box s)) p J) (H_nhds : (z : ι ), z box_integral.box.Icc I ( (U : set )) (H : U nhds_within z (box_integral.box.Icc I)), (J : box_integral.box ι), J I (m : ), z box_integral.box.Icc J box_integral.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 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.