Induction on subboxes #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

source

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

box_integral.box ι

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

I.split_center_box s = {lower := s.piecewise (λ (i : ι), (I.lower i + I.upper i) / 2) I.lower (λ (j : ι), classical.prop_decidable (j ∈ s)), upper := s.piecewise I.upper (λ (i : ι), (I.lower i + I.upper i) / 2) (λ (j : ι), classical.prop_decidable (j ∈ s)), lower_lt_upper := _}

source

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

source

theorem box_integral.box.split_center_box_le {ι : Type u_1} (I : box_integral.box ι) (s : set ι) :

I.split_center_box s ≤ I

source

theorem box_integral.box.disjoint_split_center_box {ι : Type u_1} (I : box_integral.box ι) {s t : set ι} (h : s ≠ t) :

disjoint ↑(I.split_center_box s) ↑(I.split_center_box t)

source

theorem box_integral.box.injective_split_center_box {ι : Type u_1} (I : box_integral.box ι) :

function.injective I.split_center_box

source

@[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

source

noncomputable def box_integral.box.split_center_box_emb {ι : Type u_1} (I : box_integral.box ι) :

set ι ↪ box_integral.box ι

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

Equations

I.split_center_box_emb = {to_fun := I.split_center_box, inj' := _}

source

@[simp]

theorem box_integral.box.split_center_box_emb_apply {ι : Type u_1} (I : box_integral.box ι) (s : set ι) :

⇑(I.split_center_box_emb) s = I.split_center_box s

source

@[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

source

@[simp]

theorem box_integral.box.upper_sub_lower_split_center_box {ι : Type u_1} (I : box_integral.box ι) (s : set ι) (i : ι) :

(I.split_center_box s).upper i - (I.split_center_box s).lower i = (I.upper i - I.lower i) / 2

source

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.