BoxIntegral.Box.subbox_induction_on'
theorem BoxIntegral.Box.subbox_induction_on' :
∀ {ι : Type u_1} {p : BoxIntegral.Box ι → Prop} (I : BoxIntegral.Box ι),
(∀ J ≤ I, (∀ (s : Set ι), p (J.splitCenterBox s)) → p J) →
(∀ z ∈ BoxIntegral.Box.Icc I,
∃ U ∈ nhdsWithin z (BoxIntegral.Box.Icc I),
∀ J ≤ I,
∀ (m : ℕ),
z ∈ BoxIntegral.Box.Icc J →
BoxIntegral.Box.Icc J ⊆ U →
(∀ (i : ι), J.upper i - J.lower i = (I.upper i - I.lower i) / 2 ^ m) → p J) →
p I
The theorem `BoxIntegral.Box.subbox_induction_on'` can be described as follows:
Consider a predicate `p` on `Box ι` and a box `I`. Assume the following two properties:
- Property `H_ind`: For any smaller box `J` that is a subdivision of `I`, the hyperplanes passing through `J`'s center split it into `2^n` boxes. If the predicate `p` holds true for each of these smaller boxes, then it holds true for `J`.
- Property `H_nhds`: For each point `z` in the closed box defined by the interval from `I`'s lower bound to its upper bound (denoted `I.Icc`), there exists a neighborhood `U` of `z` within `I.Icc`, such that for every box `J` that is a subdivision of `I` and for which `z` lies within the closed box defined by `J`'s bounds (denoted `J.Icc`) and `J.Icc` is a subset of `U`, if `J` is homothetic to `I` with a rescaling factor of `1 / 2^m` for some `m`, then `p` holds true on `J`.
Then, under these assumptions, the predicate `p` is true on `I`.
The theorem also mentions that the proof would still work if `H_ind` was only assumed for sub-boxes `J` that are homothetic to `I` with a rescaling factor of the form `2^-m`, but this generalization is not yet needed.
More concisely: Given a predicate `p` on `Box ι` and a box `I` with the properties that `p` holds true for all sub-boxes of `I` that are obtained by splitting with hyperplanes passing through their centers (`H_ind`), and for any point `z` in `I.Icc`, there exists a neighborhood `U` of `z` such that `p` holds true for all sub-boxes of `I` containing `z` and homothetic to `I` with a rescaling factor of `2^-m` (`H_nhds`), then `p` holds true on `I`.
|
BoxIntegral.Box.mem_splitCenterBox
theorem BoxIntegral.Box.mem_splitCenterBox :
∀ {ι : Type u_1} {I : BoxIntegral.Box ι} {s : Set ι} {y : ι → ℝ},
y ∈ I.splitCenterBox s ↔ y ∈ I ∧ ∀ (i : ι), (I.lower i + I.upper i) / 2 < y i ↔ i ∈ s
The theorem `BoxIntegral.Box.mem_splitCenterBox` states that for any type `ι`, any box `I` of type `BoxIntegral.Box ι`, any set `s` of type `Set ι`, and any function `y : ι → ℝ`, `y` belongs to the box resulting from splitting `I` at the center by the hyperplanes defined by `s` if and only if `y` belongs to `I` and for each `i` in `ι`, the average of the lower and upper limit of `i` in `I` is less than `y i` if and only if `i` belongs to `s`. This theorem connects the concept of membership in a split box with conditions on coordinates of a box and membership in a defining set.
More concisely: A function belongs to the split box obtained by dividing another box using hyperplanes defined by a set if and only if the function belongs to the original box and the average of the lower and upper limits of the function on each element in the set is strictly less than the function value at that element.
|