BoxIntegral.Prepartition.isPartitionSplit
theorem BoxIntegral.Prepartition.isPartitionSplit :
∀ {ι : Type u_1} (I : BoxIntegral.Box ι) (i : ι) (x : ℝ), (BoxIntegral.Prepartition.split I i x).IsPartition := by
sorry
The theorem `BoxIntegral.Prepartition.isPartitionSplit` states that for any type `ι`, any box `I` of type `BoxIntegral.Box ι`, any element `i` from `ι`, and any real number `x`, the result of splitting `I` at `x` along the dimension `i` using the function `BoxIntegral.Prepartition.split`, yields a partition of `I`. In other words, the boxes obtained from the split cover the whole box `I`.
More concisely: For any box `I` of type `BoxIntegral.Box ι`, any element `i` from `ι`, and any real number `x`, the partition obtained by splitting `I` at `x` along dimension `i` using `BoxIntegral.Prepartition.split` is a valid partition of `I`.
|
BoxIntegral.Prepartition.split_of_not_mem_Ioo
theorem BoxIntegral.Prepartition.split_of_not_mem_Ioo :
∀ {ι : Type u_1} {I : BoxIntegral.Box ι} {i : ι} {x : ℝ},
x ∉ Set.Ioo (I.lower i) (I.upper i) → BoxIntegral.Prepartition.split I i x = ⊤
In natural language, this theorem states that for any type `ι`, box `I` of type `BoxIntegral.Box ι`, index `i` from `ι`, and real number `x`, if `x` does not belong to the interval `(I.lower i, I.upper i)` (i.e., `x` is not strictly between the lower and upper bounds of `I` along the `i`th dimension), then the hyperplane defined by `{y | y i = x}` cannot split `I`. In other words, the partition of `I` into boxes at `x` along the `i`th dimension results in the trivial partition `⊤`.
More concisely: For any type `ι`, box `I` of type `BoxIntegral.Box ι`, index `i` from `ι`, and real number `x` not in the interval `(I.lower i, I.upper i)`, the hyperplane `{y | y i = x}` does not split box `I`.
|
BoxIntegral.Box.coe_splitLower
theorem BoxIntegral.Box.coe_splitLower :
∀ {ι : Type u_1} {I : BoxIntegral.Box ι} {i : ι} {x : ℝ}, ↑(I.splitLower i x) = ↑I ∩ {y | y i ≤ x}
The theorem `BoxIntegral.Box.coe_splitLower` states that for any type `ι`, any box `I` of type `BoxIntegral.Box ι`, any `i` of type `ι`, and any real number `x`, the co-domain of the function `BoxIntegral.Box.splitLower I i x` is equal to the intersection of the co-domain of `I` and the set of all `y` such that `y i` is less than or equal to `x`. In other words, it demonstrates that splitting the box `I` at a hyperplane defined by `y i = x` results in a new box that contains all points of `I` where `y i` is less than or equal to `x`.
More concisely: The theorem `BoxIntegral.Box.coe_splitLower` asserts that the co-domain of `BoxIntegral.Box.splitLower I i x` is equal to the intersection of the co-domain of box `I` and the set of `y` for which `y i ≤ x`.
|
BoxIntegral.Prepartition.compl_congr
theorem BoxIntegral.Prepartition.compl_congr :
∀ {ι : Type u_1} {I : BoxIntegral.Box ι} [inst : Finite ι] {π₁ π₂ : BoxIntegral.Prepartition I},
π₁.iUnion = π₂.iUnion → π₁.compl = π₂.compl
This theorem states that, for any type `ι`, any box `I` of type `ι`, and any two prepartitions `π₁` and `π₂` of the box `I`, if the union of all boxes in `π₁` is equal to the union of all boxes in `π₂`, then the complement of `π₁` is equal to the complement of `π₂`. This theorem is relying on the fact that the definition of the complement of a prepartition (`BoxIntegral.Prepartition.compl`) uses `Exists.choose`, which means the result only depends on the union of all boxes in the prepartition (`π.iUnion`).
More concisely: Given any type `ι`, box `I` of type `ι`, and partitions `π₁` and `π₂` of `I`, if `ιUnion π₁ = ιUnion π₂`, then `BoxIntegral.Prepartition.compl π₁ = BoxIntegral.Prepartition.compl π₂`.
|
BoxIntegral.Prepartition.IsPartition.exists_splitMany_le
theorem BoxIntegral.Prepartition.IsPartition.exists_splitMany_le :
∀ {ι : Type u_1} [inst : Finite ι] {I : BoxIntegral.Box ι} {π : BoxIntegral.Prepartition I},
π.IsPartition → ∃ s, BoxIntegral.Prepartition.splitMany I s ≤ π
The theorem `BoxIntegral.Prepartition.IsPartition.exists_splitMany_le` states that for any partition `π` of a box `I`, there exists a finite set `s` of hyperplanes such that the box `I` split along these hyperplanes (according to the `splitMany` operation) forms a prepartition which is coarser than or equal to `π`. Here, `ι` is a finite type representing the dimensions, and `I` is a box in the `ι`-dimensional space. The `splitMany` operation takes a box and a finite set of hyperplanes (represented as a set of pairs `(i, x)` where `i` is the dimension and `x` is the coordinate of the hyperplane along that dimension), and splits the box along these hyperplanes. The relation `≤` between prepartitions is the refinement order: a prepartition `π1` is finer than or equal to a prepartition `π2` (denoted `π2 ≤ π1`) if each box in `π1` is contained in some box of `π2`. In this context, the theorem guarantees the existence of some set of hyperplanes such that the resulting prepartition from splitting the box along these hyperplanes is no finer than the given partition `π`.
More concisely: Given a box `I` and a partition `π` in an `ι`-dimensional space, there exists a finite set `s` of hyperplanes such that the prepartition obtained by splitting `I` along these hyperplanes is coarser than or equal to `π`.
|
BoxIntegral.Prepartition.eventually_splitMany_inf_eq_filter
theorem BoxIntegral.Prepartition.eventually_splitMany_inf_eq_filter :
∀ {ι : Type u_1} {I : BoxIntegral.Box ι} [inst : Finite ι] (π : BoxIntegral.Prepartition I),
∀ᶠ (t : Finset (ι × ℝ)) in Filter.atTop,
π ⊓ BoxIntegral.Prepartition.splitMany I t =
(BoxIntegral.Prepartition.splitMany I t).filter fun J => ↑J ⊆ π.iUnion
This theorem states that for any type `ι`, any box `I` of type `BoxIntegral.Box ι` and any prepartition `π` of `I`, eventually for every `t` in the filter `atTop` (which represents a limit towards infinity), the intersection of `π` and the prepartition resulting from splitting `I` along many hyperplanes defined by `t`, is equal to filtering the prepartition from splitting `I` along `t`, such that each resultant box `J` is a subset of the union of boxes in `π`.
In other words, if we keep splitting a box `I` along more and more hyperplanes, eventually the part that overlaps with a given prepartition `π` is exactly the part where every box from the splitting is covered by `π`.
More concisely: For any type `ι`, box `I` of type `BoxIntegral.Box ι`, prepartition `π` of `I`, and filter `atTop`, as `t` approaches `atTop`, the intersection of `π` and the partition obtained by splitting `I` along hyperplanes defined by `t` is equal to filtering `π` to only keep the parts that are subsets of the union of boxes in the resulting partition.
|
BoxIntegral.Prepartition.iUnion_compl
theorem BoxIntegral.Prepartition.iUnion_compl :
∀ {ι : Type u_1} {I : BoxIntegral.Box ι} [inst : Finite ι] (π : BoxIntegral.Prepartition I),
π.compl.iUnion = ↑I \ π.iUnion
This theorem states that for any given prepartition `π` of a box `I` in a finite-dimensional space `ι`, the union of the boxes in the complement prepartition `π.compl` equals the set difference of the box `I` and the union of the boxes in the original prepartition `π`. In other words, the part of the box `I` not covered by the prepartition `π` is exactly what is covered by the complement prepartition `π.compl`.
More concisely: For any prepartition π of a box I in a finite-dimensional space, the complement π.compl covers the complement of the union of the boxes in π, that is, I \ ∪ π = ∪ (box j : π.compl) box j.
|
BoxIntegral.Prepartition.exists_iUnion_eq_diff
theorem BoxIntegral.Prepartition.exists_iUnion_eq_diff :
∀ {ι : Type u_1} {I : BoxIntegral.Box ι} [inst : Finite ι] (π : BoxIntegral.Prepartition I),
∃ π', π'.iUnion = ↑I \ π.iUnion
This theorem states that for any given prepartition `π` of a box `I` (in any finite-dimensional space), there exists another prepartition `π'` such that the union of the boxes in `π'` is exactly the set difference between the original box `I` and the union of the boxes in `π`. In other words, `π'` covers exactly the parts of `I` not covered by `π`.
More concisely: For any prepartition `π` of a box `I` in a finite-dimensional space, there exists a prepartition `π'` such that `I = π ∖ ⋃π'`.
|
BoxIntegral.Prepartition.inf_split
theorem BoxIntegral.Prepartition.inf_split :
∀ {ι : Type u_1} {I : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I) (i : ι) (x : ℝ),
π ⊓ BoxIntegral.Prepartition.split I i x = π.biUnion fun J => BoxIntegral.Prepartition.split J i x
This theorem states that for any type `ι`, any integral box `I` of this type, a partition `π` of `I`, a member `i` of `ι`, and a real number `x`, the intersection of the partition `π` and the split of `I` at `x` along the `i`-th axis is equal to a bi-union over `π`. Specifically, the bi-union is between `π` and the split of each box `J` in `π` at `x` along the `i`-th axis. In other words, it splits every box in the prepartition `π` at the same point `x`, and this split operation commutes with intersections.
More concisely: For any type `ι`, integral box `I` of type `ι`, partition `π` of `I`, element `i` of `ι`, and real number `x`, the intersection of `π` with the split of `I` at `x` along the `i`-th axis equals the bi-union of `π` and the split of each box in `π` at `x` along the `i`-th axis.
|
BoxIntegral.Box.coe_splitUpper
theorem BoxIntegral.Box.coe_splitUpper :
∀ {ι : Type u_1} {I : BoxIntegral.Box ι} {i : ι} {x : ℝ}, ↑(I.splitUpper i x) = ↑I ∩ {y | x < y i}
This theorem states that for any given box `I`, index `i`, and real number `x`, the box obtained by splitting `I` at the hyperplane `{y : ι → ℝ | y i = x}` and taking the portion where `y i > x` (which is given by the `BoxIntegral.Box.splitUpper` function) is exactly equal to the intersection of the original box `I` with the set `{y | x < y i}`. In other words, `BoxIntegral.Box.splitUpper` function correctly computes the upper half of the box `I` split by the hyperplane determined by `i` and `x`.
More concisely: For any box `I`, index `i`, and real number `x`, `BoxIntegral.Box.splitUpper I i x` equals the intersection of `I` with the set `{y : ι → ℝ | x < y i}` where `ι` is the type of indices of `I`.
|
BoxIntegral.Prepartition.eventually_not_disjoint_imp_le_of_mem_splitMany
theorem BoxIntegral.Prepartition.eventually_not_disjoint_imp_le_of_mem_splitMany :
∀ {ι : Type u_1} [inst : Finite ι] (s : Finset (BoxIntegral.Box ι)),
∀ᶠ (t : Finset (ι × ℝ)) in Filter.atTop,
∀ (I J : BoxIntegral.Box ι), J ∈ s → ∀ J' ∈ BoxIntegral.Prepartition.splitMany I t, ¬Disjoint ↑J ↑J' → J' ≤ J
Let `s` be a finite set of boxes in `ℝⁿ = ι → ℝ`. There exists a finite set `t₀` of hyperplanes, which are the set of all hyperfaces of boxes in `s`, such that for any set `t` which includes `t₀` and any box `I` in `ℝⁿ`, the hyperplanes from `t` split `I` into sub-boxes. Now, if `J'` is one of these sub-boxes and `J` is one of the boxes in `s` and if these boxes have a non-empty intersection, then `J'` is a sub-box of `J`, i.e., `J'` is less than or equal to `J`. This condition is satisfied for large enough `t`.
In other words, this theorem states that given a set of boxes, you can find a set of hyperplanes that can split any other box in such a way that if any generated sub-box intersects with a box from the original set, the sub-box is either the same as or smaller than that original box.
More concisely: Given a finite set of boxes in ℝⁿ, there exists a finite set of hyperplanes such that any box intersecting with a hyperplane from the set splits into sub-boxes where any sub-box intersecting with an original box is a sub-box of it.
|
BoxIntegral.Prepartition.splitMany_insert
theorem BoxIntegral.Prepartition.splitMany_insert :
∀ {ι : Type u_1} (I : BoxIntegral.Box ι) (s : Finset (ι × ℝ)) (p : ι × ℝ),
BoxIntegral.Prepartition.splitMany I (insert p s) =
BoxIntegral.Prepartition.splitMany I s ⊓ BoxIntegral.Prepartition.split I p.1 p.2
The theorem `BoxIntegral.Prepartition.splitMany_insert` states that for any given box `I` of type `ι`, a finite set `s` of pairs of `ι` and real numbers, and a pair `p` of `ι` and a real number, splitting the box `I` along the hyperplanes defined by the union of `s` and `p` is equivalent to splitting the box `I` along the hyperplanes defined by `s` and then further splitting along the hyperplane defined by `p`. This splitting divides the box into sub-boxes. Here, the hyperplanes are defined by the equations `y = x` for each pair `(i, x)` in the set.
More concisely: Given a box I of type ι, a finite set s of pairs (i, x) of type ι × ℝ, and a pair (j, y) of type ι × ℝ, splitting I along the hyperplanes defined by s and then further splitting along the hyperplane defined by (j, y) is equivalent to first splitting I along the hyperplanes defined by s and then splitting each sub-box along the hyperplane defined by (j, y).
|
BoxIntegral.Prepartition.not_disjoint_imp_le_of_subset_of_mem_splitMany
theorem BoxIntegral.Prepartition.not_disjoint_imp_le_of_subset_of_mem_splitMany :
∀ {ι : Type u_1} {I J Js : BoxIntegral.Box ι} {s : Finset (ι × ℝ)},
(∀ (i : ι), {(i, J.lower i), (i, J.upper i)} ⊆ s) →
Js ∈ BoxIntegral.Prepartition.splitMany I s → ¬Disjoint ↑J ↑Js → Js ≤ J
The theorem states that for a given set `s` of hyperplanes in multi-dimensional real coordinate space `ι → ℝ`, encoded as pairs `(i, r)`, let's assume this set includes all faces of a box `J`. These hyperplanes split another box `I` into smaller subboxes. Now, consider one of these subboxes, `Js`. If `J` and `Js` have a nonempty intersection, meaning they are not disjoint, then it can be inferred that `Js` is indeed a subbox of `J`. This is assuming that every dimension `i` of `J` has its lower and upper limits included in the set of hyperplanes `s`.
More concisely: If a box `J` intersects a subbox `Js` formed by the intersection of `J` with a set of hyperplanes `s` that includes all bounds of each dimension of `J`, then `Js` is a subbox of `J`.
|