parallelepiped_single
theorem parallelepiped_single :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (a : ι → ℝ),
(parallelepiped fun i => Pi.single i (a i)) = Set.uIcc 0 a
This theorem states that the axis-aligned parallelepiped over a function from an index set `ι` to the real numbers `ℝ` is a cuboid. Specifically, given any function `a : ι → ℝ` where `ι` is a finite type and has a decidable equality, the parallelepiped spanned by the vectors generated through `Pi.single` function (which assigns each index `i` the coordinate `a i` and zero otherwise) equals the set of elements lying between `0` and `a` (inclusive), which forms a multidimensional interval or a cuboid. This essentially means that the parallelepiped formed by the vectors where each vector has only one non-zero component (the value given by function `a` at that index) forms a cuboid.
More concisely: Given a finite type `ι` with decidable equality and a function `a : ι → ℝ`, the parallelepiped spanned by the vectors `Pi.single i a i ∣ i ∈ ι` is a cuboid.
|
parallelepiped_eq_convexHull
theorem parallelepiped_eq_convexHull :
∀ {ι : Type u_1} {E : Type u_3} [inst : Fintype ι] [inst_1 : AddCommGroup E] [inst_2 : Module ℝ E] (v : ι → E),
parallelepiped v = (convexHull ℝ) (Finset.univ.sum fun i => {0, v i})
This theorem states that for any finite set `ι` and any additive commutative group `E` with a module structure over the real numbers `ℝ`, if we take any vector function `v` mapping `ι` to `E`, then the parallelepiped spanned by this vector function `v` is equal to the convex hull of the set of points that are the sum of all vectors `v i` for each `i` in `ι`, where each `v i` is scaled by either 0 or 1. The convex hull here is defined as the smallest convex set that contains these points, and the summation is taken over all elements in the universal finite set of `ι`, which is implied by the type `Finset ι`.
More concisely: For any finite set `ι`, and any additive commutative group `E` with a real number module structure, the parallelepiped spanned by a vector function mapping `ι` to `E` is equal to the convex hull of the set of points obtained by summing and scaling each vector in the function with 0 or 1.
|
Basis.addHaar_def
theorem Basis.addHaar_def :
∀ {ι : Type u_5} {E : Type u_6} [inst : Fintype ι] [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace ℝ E]
[inst_3 : MeasurableSpace E] [inst_4 : BorelSpace E] (b : Basis ι ℝ E),
b.addHaar = MeasureTheory.Measure.addHaarMeasure b.parallelepiped
This theorem states that for any basis `b` of a real normed vector space `E` of finite type `ι`, the Lebesgue measure associated to this basis (`Basis.addHaar b`), which gives measure `1` to the parallelepiped spanned by the basis, is equal to the Haar measure of the parallelepiped spanned by the basis (`MeasureTheory.Measure.addHaarMeasure (Basis.parallelepiped b)`).
More concisely: For any finite basis `b` of a real normed vector space `E`, the Lebesgue measure and Haar measure of the parallelepiped spanned by `b` are equal.
|
Basis.addHaar_eq_iff
theorem Basis.addHaar_eq_iff :
∀ {ι : Type u_1} {E : Type u_3} [inst : Fintype ι] [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace ℝ E]
[inst_3 : MeasurableSpace E] [inst_4 : BorelSpace E] [inst_5 : SecondCountableTopology E] (b : Basis ι ℝ E)
(μ : MeasureTheory.Measure E) [inst_6 : MeasureTheory.SigmaFinite μ] [inst_7 : μ.IsAddLeftInvariant],
b.addHaar = μ ↔ ↑↑μ ↑b.parallelepiped = 1
This theorem states that for a given sigma-finite left-invariant measure `μ` on a vector space `E`, `μ` is equal to the Haar measure defined by a basis `b` if and only if the parallelepiped defined by `b` has measure `1` with respect to `μ`. Here, `E` is a finite-dimensional, real normed vector space equipped with a suitable topology and a Borel measurable space structure. The Haar measure and the parallelepiped are both defined in the context of the vector space structure of `E`. The Haar measure `b.addHaar` of `b` is a particular measure associated with the basis `b`, and the parallelepiped `b.parallelepiped` is the set spanned by the vectors in `b`.
More concisely: A sigma-finite left-invariant measure `μ` on a finite-dimensional real normed vector space `E` equals the Haar measure defined by a basis `b` if and only if the parallelepiped defined by `b` has measure `1` with respect to `μ`.
|
parallelepiped_comp_equiv
theorem parallelepiped_comp_equiv :
∀ {ι : Type u_1} {ι' : Type u_2} {E : Type u_3} [inst : Fintype ι] [inst_1 : Fintype ι'] [inst_2 : AddCommGroup E]
[inst_3 : Module ℝ E] (v : ι → E) (e : ι' ≃ ι), parallelepiped (v ∘ ⇑e) = parallelepiped v
This theorem states that reindexing a family of vectors does not alter the parallelepiped they form. Specifically, if you have a family of vectors `v : ι → E` indexed by type `ι`, and an equivalence `e : ι' ≃ ι` between `ι'` and `ι`, then the parallelepiped formed by the vectors reindexed by `e` (i.e., `(v ∘ ⇑e)`) is the same as the original parallelepiped of `v`. This is to say, changing the labels or the indexing of the vectors doesn't affect the geometric parallelepiped shape they span in the vector space `E`.
More concisely: Given a family of vectors `v : ι → E` and an equivalence `e : ι' ≃ ι`, the parallelepipeds spanned by `v` and `(v ∘ ⇑e)` are equal in `E`.
|