English
Let p be a predicate on Box ι. If for every J ≤ I, whenever p holds for all J' in splitCenter J, then p holds for J; and a second external condition about neighborhoods (nhds) holds, then p I holds.
Русский
Пусть p — предикат на Box ι. Если для каждого J ≤ I, верно, что если p верно на всех J' из splitCenter(J), то p верно на J, и добавляется дополнительное условие локальности, то p I верно.
LaTeX
$$$ p(I) \\leftarrow \\big( \\forall J \\le I,\\ \\big( \\forall J' \\in \\mathrm{splitCenter}(J), p(J') \\big) \\rightarrow p(J) \\big) \\land \\text{nhds-condition} \\Rightarrow p(I) $$$
Lean4
/-- Let `p` be a predicate on `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 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. See also `BoxIntegral.Box.subbox_induction_on'` for a version using
`BoxIntegral.Box.splitCenterBox` instead of `BoxIntegral.Prepartition.splitCenter`. -/
@[elab_as_elim]
theorem subbox_induction_on {p : Box ι → Prop} (I : Box ι) (H_ind : ∀ J ≤ I, (∀ J' ∈ splitCenter J, p J') → p J)
(H_nhds :
∀ z ∈ Box.Icc I,
∃ U ∈ 𝓝[Box.Icc I] z,
∀ J ≤ I,
∀ (m : ℕ),
z ∈ Box.Icc J → Box.Icc J ⊆ U → (∀ i, J.upper i - J.lower i = (I.upper i - I.lower i) / 2 ^ m) → p J) :
p I := by
refine subbox_induction_on' I (fun J hle hs => H_ind J hle fun J' h' => ?_) H_nhds
rcases mem_splitCenter.1 h' with ⟨s, rfl⟩
exact hs s
