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 : BoxIntegral.Box ι) (s : Set ι) : BoxIntegral.Box ι

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

• One or more equations did not get rendered due to their size.

theorem BoxIntegral.Box.mem_splitCenterBox {ι : Type u_1} {I : BoxIntegral.Box ι} {s : Set ι} {y : ι → ℝ} : y ∈ BoxIntegral.Box.splitCenterBox I s ↔ y ∈ I ∧ ∀ (i : ι), (BoxIntegral.Box.lower I i + BoxIntegral.Box.upper I i) / 2 < y i ↔ i ∈ s

theorem BoxIntegral.Box.splitCenterBox_le {ι : Type u_1} (I : BoxIntegral.Box ι) (s : Set ι) : BoxIntegral.Box.splitCenterBox I s ≤ I

theorem BoxIntegral.Box.disjoint_splitCenterBox {ι : Type u_1} (I : BoxIntegral.Box ι) {s : Set ι} {t : Set ι} (h : s ≠ t) : Disjoint ↑(BoxIntegral.Box.splitCenterBox I s) ↑(BoxIntegral.Box.splitCenterBox I t)

theorem BoxIntegral.Box.injective_splitCenterBox {ι : Type u_1} (I : BoxIntegral.Box ι) : Function.Injective (BoxIntegral.Box.splitCenterBox I)

@[simp]

theorem BoxIntegral.Box.exists_mem_splitCenterBox {ι : Type u_1} {I : BoxIntegral.Box ι} {x : ι → ℝ} : (∃ s, x ∈ BoxIntegral.Box.splitCenterBox I s) ↔ x ∈ I

@[simp]

theorem BoxIntegral.Box.splitCenterBoxEmb_apply {ι : Type u_1} (I : BoxIntegral.Box ι) (s : Set ι) : ↑(BoxIntegral.Box.splitCenterBoxEmb I) s = BoxIntegral.Box.splitCenterBox I s

def BoxIntegral.Box.splitCenterBoxEmb {ι : Type u_1} (I : BoxIntegral.Box ι) : Set ι ↪ BoxIntegral.Box ι

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

Equations

• BoxIntegral.Box.splitCenterBoxEmb I = { toFun := BoxIntegral.Box.splitCenterBox I, inj' := (_ : Function.Injective (BoxIntegral.Box.splitCenterBox I)) }

@[simp]

theorem BoxIntegral.Box.iUnion_coe_splitCenterBox {ι : Type u_1} (I : BoxIntegral.Box ι) : ⋃ (s : Set ι), ↑(BoxIntegral.Box.splitCenterBox I s) = ↑I

@[simp]

theorem BoxIntegral.Box.upper_sub_lower_splitCenterBox {ι : Type u_1} (I : BoxIntegral.Box ι) (s : Set ι) (i : ι) : BoxIntegral.Box.upper (BoxIntegral.Box.splitCenterBox I s) i - BoxIntegral.Box.lower (BoxIntegral.Box.splitCenterBox I s) i = (BoxIntegral.Box.upper I i - BoxIntegral.Box.lower I i) / 2

theorem BoxIntegral.Box.subbox_induction_on' {ι : Type u_1} {p : BoxIntegral.Box ι → Prop} (I : BoxIntegral.Box ι) (H_ind : (J : BoxIntegral.Box ι) → J ≤ I → ((s : Set ι) → p (BoxIntegral.Box.splitCenterBox J s)) → p J) (H_nhds : ∀ (z : ι → ℝ), z ∈ ↑BoxIntegral.Box.Icc I → ∃ U, U ∈ nhdsWithin z (↑BoxIntegral.Box.Icc I) ∧ ((J : BoxIntegral.Box ι) → J ≤ I → (m : ℕ) → z ∈ ↑BoxIntegral.Box.Icc J → ↑BoxIntegral.Box.Icc J ⊆ U → (∀ (i : ι), BoxIntegral.Box.upper J i - BoxIntegral.Box.lower J i = (BoxIntegral.Box.upper I i - BoxIntegral.Box.lower I 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.