BoxIntegral.Box.lower_le_upper
theorem BoxIntegral.Box.lower_le_upper : ∀ {ι : Type u_1} (I : BoxIntegral.Box ι), I.lower ≤ I.upper
This theorem states that, for any given box `I` of an arbitrary type `ι` in the context of integral calculus, the lower bound of the box is always less than or equal to the upper bound of the box. The theorem follows the fundamental principle that the lower limits are always smaller or equal to the upper limits in mathematical intervals or boxes.
More concisely: For any box I of type ι in integral calculus, the lower bound of I is less than or equal to the upper bound.
|
BoxIntegral.Box.coe_mk'
theorem BoxIntegral.Box.coe_mk' :
∀ {ι : Type u_1} (l u : ι → ℝ), ↑(BoxIntegral.Box.mk' l u) = Set.univ.pi fun i => Set.Ioc (l i) (u i)
This theorem states that for any type `ι` and two functions `l` and `u` from `ι` to the real numbers ℝ, the box defined by `l` and `u` (which may be the empty set if `l i` is not less than `u i` for all `i`) corresponds to the set of all functions from `ι` to ℝ that for each index `i` map to a value in the left-open right-closed interval from `l i` to `u i`. This means that all values that such a function can take are within the defined box.
More concisely: For any type `ι` and functions `l` and `u` from `ι` to the real numbers, the set of functions from `ι` to the real numbers mapping each index `i` to a value in the left-open right-closed interval `[l i, u i]` is equal to the set of functions whose image under `l` and `u` define a box containing their entire image.
|
BoxIntegral.Box.withBotCoe_subset_iff
theorem BoxIntegral.Box.withBotCoe_subset_iff : ∀ {ι : Type u_1} {I J : WithBot (BoxIntegral.Box ι)}, ↑I ⊆ ↑J ↔ I ≤ J
This theorem states that for any type `ι` and any two instances `I` and `J` of the type `WithBot (BoxIntegral.Box ι)`, the subset relation `↑I ⊆ ↑J` holds if and only if the relation `I ≤ J` holds. In other words, the subset relationship between the underlying sets of two possible-bottom boxes is equivalent to the order relationship between the possible-bottom boxes. This theorem allows us to make decisions about the subset relationship by checking the less-than-or-equal-to relationship, and vice versa.
More concisely: For any type `ι` and instances `I` and `J` of `WithBot (BoxIntegral.Box ι)`, `↑I ⊆ ↑J` if and only if `I ≤ J`.
|
BoxIntegral.Box.coe_inf
theorem BoxIntegral.Box.coe_inf : ∀ {ι : Type u_1} (I J : WithBot (BoxIntegral.Box ι)), ↑(I ⊓ J) = ↑I ∩ ↑J
This theorem is about the intersection of two possibly bounded boxes in an arbitrary dimension. More specifically, for any type `ι` and any two possibly bounded boxes `I` and `J` (where a possibly bounded box is represented by the `WithBot` type constructor applied to `BoxIntegral.Box ι`), the box resulting from the infimum (greatest lower bound) of `I` and `J` is equivalent to the intersection of the boxes `I` and `J`. Here, the `coe` function is used to remove the `WithBot` wrapping, and `⊓` denotes the infimum operation.
More concisely: For any type `ι` and boxes `I` and `J` of type `WithBot (Box ι)`, the infimum `I ⊓ J` is equivalent to the intersection of `I` and `J`, i.e., `{x : ι | x ∈ I ∧ x ∈ J}`.
|
BoxIntegral.Box.monotone_upper
theorem BoxIntegral.Box.monotone_upper : ∀ {ι : Type u_1}, Monotone fun I => I.upper
The theorem `BoxIntegral.Box.monotone_upper` states that for any type `ι`, the function that maps a box `I` to its upper bound is monotone. In other words, if we have two boxes `A` and `B` such that `A ≤ B`, then the upper bound of `A` is less than or equal to the upper bound of `B`. This is a property of the upper bound function in the context of box integrals.
More concisely: For any type ι, the function that maps a box I to its upper bound is monotone, i.e., if A ≤ B are boxes, then the upper bound of A is less than or equal to the upper bound of B.
|
BoxIntegral.Box.coe_eq_pi
theorem BoxIntegral.Box.coe_eq_pi :
∀ {ι : Type u_1} (I : BoxIntegral.Box ι), ↑I = Set.univ.pi fun i => Set.Ioc (I.lower i) (I.upper i)
This theorem states that for any given box `I` in the space indexed by the type `ι`, the set corresponding to the box `I` equals the set of all dependent functions (indexed by `ι`) that map each index to a left-open right-closed interval. Specifically, the interval is from the lower limit of the box `I` at that index to the upper limit of the box `I` at that index. The theorem applies to all elements in the universal set, i.e., all elements of the type `ι`.
More concisely: For any box `I` in the indexed space `ι`, the set of functions from `ι` to the real numbers with each function mapping an index `i` to the left-open right-closed interval `[I.lower i, I.upper i)` is equal to the set corresponding to the box `I`.
|
BoxIntegral.Box.le_TFAE
theorem BoxIntegral.Box.le_TFAE :
∀ {ι : Type u_1} (I J : BoxIntegral.Box ι),
[I ≤ J, ↑I ⊆ ↑J, Set.Icc I.lower I.upper ⊆ Set.Icc J.lower J.upper, J.lower ≤ I.lower ∧ I.upper ≤ J.upper].TFAE
This theorem states that for any two boxes `I` and `J` of any type `ι`, the following propositions are equivalent: (1) `I` is less than or equal to `J`, (2) the set denoted by `I` is a subset of the set denoted by `J`, (3) the closed interval from the lower value of `I` to the upper value of `I` is a subset of the closed interval from the lower value of `J` to the upper value of `J`, and (4) the lower value of `J` is less than or equal to the lower value of `I` and the upper value of `I` is less than or equal to the upper value of `J`. In other words, all these conditions are equivalent ways of expressing that `I` is less than or equal to `J`.
More concisely: For any boxes I and J of type ι, I ≤ J if and only if (i) I is a subset of J, (ii) the interval [lower I, upper I] is a subset of the interval [lower J, upper J], and (iii) lower I ≤ lower J and upper I ≤ upper J.
|
BoxIntegral.Box.le_iff_bounds
theorem BoxIntegral.Box.le_iff_bounds :
∀ {ι : Type u_1} {I J : BoxIntegral.Box ι}, I ≤ J ↔ J.lower ≤ I.lower ∧ I.upper ≤ J.upper
This theorem states that, for any two boxes `I` and `J` in a given type `ι`, `I` is less than or equal to `J` if and only if the lower bound of `J` is less than or equal to the lower bound of `I` and the upper bound of `I` is less than or equal to the upper bound of `J`. In other words, one box is considered "smaller" than another if its bounds are contained within the bounds of the other.
More concisely: For boxes I and J in a type ι, I ≤ J if and only if inf I ≤ inf J and sup I ≤ sup J.
|
BoxIntegral.Box.upper_mem
theorem BoxIntegral.Box.upper_mem : ∀ {ι : Type u_1} (I : BoxIntegral.Box ι), I.upper ∈ I
This theorem states that for any box `I` of any type `ι`, the upper bound of the box `I` is an element of the box `I`. In mathematical terms, if `I` is an interval in a Euclidean space (or more generally, a product of intervals), its "upper" bound (one of its endpoints) is considered a point in `I`.
More concisely: For any interval `I` in a Euclidean space, the upper bound of `I` is an element of `I`.
|
BoxIntegral.Box.antitone_lower
theorem BoxIntegral.Box.antitone_lower : ∀ {ι : Type u_1}, Antitone fun I => I.lower
This theorem states that for any type `ι`, the function that maps a box `I` to its lower bound is antitone. In other words, if we have two boxes `a` and `b` such that `a` is less than or equal to `b`, then the lower bound of `b` is less than or equal to the lower bound of `a`. This is a property of order-reversing functions in the context of box integrals.
More concisely: For any type `ι`, the function that maps a box `I` to its lower bound is order-reversing with respect to box inclusion.
|
BoxIntegral.Box.nonempty_coe
theorem BoxIntegral.Box.nonempty_coe : ∀ {ι : Type u_1} (I : BoxIntegral.Box ι), (↑I).Nonempty
This theorem states that for any given box `I` of type `BoxIntegral.Box ι`, where `ι` is any type, the set corresponding to `I` (denoted by `↑I`) is not empty. In other words, the theorem asserts that there always exists some element in the set corresponding to the box `I`.
More concisely: For any `BoxIntegral.Box ι I`, the set `↑I` is non-empty.
|
BoxIntegral.Box.disjoint_coe
theorem BoxIntegral.Box.disjoint_coe : ∀ {ι : Type u_1} {I J : BoxIntegral.Box ι}, Disjoint ↑I ↑J ↔ Disjoint ↑I ↑J := by
sorry
The theorem `BoxIntegral.Box.disjoint_coe` states that for any type `ι` and any two box integrals `I` and `J` of this type, the proposition `Disjoint ↑I ↑J` is equivalent to itself. In other words, if two elements of a lattice (the box integrals `I` and `J`) are disjoint, meaning their infimum is the bottom element, then that fact remains true if we restate it; the disjointness of the two elements is invariant under restatement. This theorem might be a tautology used for some specific purpose in the context of the `BoxIntegral.Box` namespace.
More concisely: The theorem `BoxIntegral.Box.disjoint_coe` asserts that the disjointness of two box integrals is a reflexive property.
|
BoxIntegral.Box.mem_coe
theorem BoxIntegral.Box.mem_coe : ∀ {ι : Type u_1} (I : BoxIntegral.Box ι) {x : ι → ℝ}, x ∈ ↑I ↔ x ∈ I
This theorem states that for any BoxIntegral (denoted by `I`), and for any function `x` from `ι` to the set of real numbers (ℝ), `x` is an element of the coerced BoxIntegral (i.e., `↑I`) if and only if `x` is an element of `I`. In other words, a point is in the BoxIntegral whether you consider it as a box or as a coerced box.
More concisely: For any BoxIntegral `I` and any function `x` from an index set `ι` to the real numbers, `x` is in the coerced BoxIntegral `↑I` if and only if `x` is in `I`.
|
BoxIntegral.Box.le_iff_Icc
theorem BoxIntegral.Box.le_iff_Icc :
∀ {ι : Type u_1} {I J : BoxIntegral.Box ι}, I ≤ J ↔ BoxIntegral.Box.Icc I ⊆ BoxIntegral.Box.Icc J
This theorem establishes a relationship between two boxes in the context of box integrals in Lean 4. In particular, for any types `ι` and any two Boxes `I` and `J`, the box `I` is less than or equal to the box `J` if and only if the closed box corresponding to `I` is a subset of the closed box corresponding to `J`. Here, a "box" refers to a multi-dimensional interval in real number space, and the "closed box" is the set of all points between the lower and upper bounds of each interval in the box.
More concisely: For any types ι and boxes I and J in Lean 4, I ≤ J if and only if the closed interval I.min ≤ I.max and I.min ≤ J.min, and I.max ≤ J.max hold.
|