English
Let p be a predicate on Box ι. If for every J ≤ I, p holds for all center-splits splitCenterBox J s, and a certain local-homothetic condition holds near every point of I.Icc, then p I holds. This is a box-analytic induction principle.
Русский
Пусть p — предикат на Box ι. Если для любой J ≤ I выполняются условия: p для всех разбиений centerBox J s и при определённых локальных условиях в I.Icc, то p I истинно. Это принцип индукции по подBox.
LaTeX
$$$$\text{Let } p: Box ι \to \text{Prop}. \\text{If } (\forall J \le I)(\forall s, p( splitCenterBox(J,s) )) \Rightarrow p(J) \ \text{and}\ \\text{a nhds-condition } H_{nhds}, \text{then } p(I).$$$$
Lean4
/-- 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`. -/
def splitCenterBox (I : Box ι) (s : Set ι) : Box ι
where
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
i := by
dsimp only [Set.piecewise]
split_ifs <;> simp only [left_lt_add_div_two, add_div_two_lt_right, I.lower_lt_upper]
