OrthonormalBasis.volume_parallelepiped
theorem OrthonormalBasis.volume_parallelepiped :
∀ {ι : Type u_1} {F : Type u_3} [inst : Fintype ι] [inst_1 : NormedAddCommGroup F] [inst_2 : InnerProductSpace ℝ F]
[inst_3 : FiniteDimensional ℝ F] [inst_4 : MeasurableSpace F] [inst_5 : BorelSpace F]
(b : OrthonormalBasis ι ℝ F), ↑↑MeasureTheory.volume (parallelepiped ⇑b) = 1
This theorem, "OrthonormalBasis.volume_parallelepiped", states that in a finite-dimensional inner product space, the volume measure assigns a measure of `1` to the parallelepiped that is spanned by any orthonormal basis.
In other words, if we take any finite-dimensional inner product space over the real numbers and consider the parallelepiped defined by an orthonormal basis of this space, the volume of this parallelepiped (measured using the standard measure theory volume) will always be `1`. This holds true for all orthonormal bases and all finite-dimensional inner product spaces over the real numbers.
More concisely: In a finite-dimensional real inner product space, the volume of the parallelepiped spanned by an orthonormal basis is 1.
|
OrthonormalBasis.measurePreserving_measurableEquiv
theorem OrthonormalBasis.measurePreserving_measurableEquiv :
∀ {ι : Type u_1} {F : Type u_3} [inst : Fintype ι] [inst_1 : NormedAddCommGroup F] [inst_2 : InnerProductSpace ℝ F]
[inst_3 : FiniteDimensional ℝ F] [inst_4 : MeasurableSpace F] [inst_5 : BorelSpace F]
(b : OrthonormalBasis ι ℝ F),
MeasureTheory.MeasurePreserving (⇑b.measurableEquiv) MeasureTheory.volume MeasureTheory.volume
This theorem states that for any orthonormal basis of a real, finite-dimensional normed additive commutative group that is also an inner product space with a Borel measurable space structure, the measurable equivalence defined by the basis preserves volume. In other words, given such an orthonormal basis, the measure of a set under the volume measure before and after applying the measurable equivalence is the same.
More concisely: For any Borel measurable orthonormal basis of a finite-dimensional real inner product space, the volume measure is preserved under the measurable equivalence induced by the basis.
|
Orientation.measure_orthonormalBasis
theorem Orientation.measure_orthonormalBasis :
∀ {ι : Type u_1} {F : Type u_3} [inst : Fintype ι] [inst_1 : NormedAddCommGroup F] [inst_2 : InnerProductSpace ℝ F]
[inst_3 : FiniteDimensional ℝ F] [inst_4 : MeasurableSpace F] [inst_5 : BorelSpace F] {n : ℕ}
[_i : Fact (FiniteDimensional.finrank ℝ F = n)] (o : Orientation ℝ F (Fin n)) (b : OrthonormalBasis ι ℝ F),
↑↑o.volumeForm.measure (parallelepiped ⇑b) = 1
This theorem states that for a given finite-dimensional inner product space over the real numbers, if we have an orientation and an orthonormal basis in this space, the volume form associated with the orientation assigns the measure `1` to the parallelepiped defined by the orthonormal basis. This is essentially a reformulation of the statement that the absolute value of the volume form applied to any orthonormal basis is `1`, but expressed in terms of measures.
More concisely: For a finite-dimensional real inner product space with an orientation and an orthonormal basis, the orientation's volume form assigns a measure of 1 to the parallelepiped spanned by the basis.
|
Orientation.measure_eq_volume
theorem Orientation.measure_eq_volume :
∀ {F : Type u_3} [inst : NormedAddCommGroup F] [inst_1 : InnerProductSpace ℝ F] [inst_2 : FiniteDimensional ℝ F]
[inst_3 : MeasurableSpace F] [inst_4 : BorelSpace F] {n : ℕ} [_i : Fact (FiniteDimensional.finrank ℝ F = n)]
(o : Orientation ℝ F (Fin n)), o.volumeForm.measure = MeasureTheory.volume
This theorem, named "Orientation.measure_eq_volume", states that in any oriented inner product space (a space with both an inner product and a chosen orientation), the measure derived from the canonical volume form associated with an orientation is equal to the volume of the space. More formally, for any such space F (which has the properties of being a normed add-commutative group, an inner product space over the real numbers ℝ, and a finite-dimensional space), the measure associated to any orientation is equal to the volume as defined by measure theory. This is true for any orientation of F that respects a given finite dimension n of the space.
More concisely: In any finite-dimensional oriented inner product space, the measure derived from the canonical volume form associated with an orientation equals the space's volume.
|
PiLp.volume_preserving_equiv
theorem PiLp.volume_preserving_equiv :
∀ (ι : Type u_4) [inst : Fintype ι],
MeasureTheory.MeasurePreserving (⇑(WithLp.equiv 2 (ι → ℝ))) MeasureTheory.volume MeasureTheory.volume
This theorem, `PiLp.volume_preserving_equiv`, states that for any type `ι` that has finite number of elements (or is "finitely typed"), the canonical equivalence between `WithLp 2 (ι → ℝ)` and `(ι → ℝ)` (given by `WithLp.equiv 2 (ι → ℝ)`) is volume preserving with respect to the Lebesgue measure (`MeasureTheory.volume`). In the context of measure theory, an operation or transformation is said to be 'volume preserving' if the measure (volume) of any set remains the same after the operation or transformation is applied.
More concisely: For any finitely typed `ι`, the canonical equivalence between `WithLp 2 (ι → ℝ)` and `(ι → ℝ)` preserves Lebesgue measure.
|
EuclideanSpace.volume_preserving_measurableEquiv
theorem EuclideanSpace.volume_preserving_measurableEquiv :
∀ (ι : Type u_4) [inst : Fintype ι],
MeasureTheory.MeasurePreserving (⇑(EuclideanSpace.measurableEquiv ι)) MeasureTheory.volume MeasureTheory.volume
The theorem `EuclideanSpace.volume_preserving_measurableEquiv` establishes that for any finite type `ι`, the measure equivalence between the Euclidean space of real numbers parameterized by `ι` and the function space from `ι` to real numbers, as defined by `EuclideanSpace.measurableEquiv ι`, preserves volume. In other words, this measure equivalence doesn't change the measure (in this case the "volume") of sets under the transformation.
More concisely: The measure equivalence between Euclidean spaces parameterized by a finite type `ι` and real-valued functions on `ι`, as defined by `EuclideanSpace.measurableEquiv ι`, preserves volumes of sets.
|
PiLp.volume_preserving_equiv_symm
theorem PiLp.volume_preserving_equiv_symm :
∀ (ι : Type u_4) [inst : Fintype ι],
MeasureTheory.MeasurePreserving (⇑(WithLp.equiv 2 (ι → ℝ)).symm) MeasureTheory.volume MeasureTheory.volume
This theorem, `PiLp.volume_preserving_equiv_symm`, states that for any type `ι` which has a finite number of elements (indicated by `Fintype ι`), the function given by the inverse (`symm`) of the equivalence (`equiv`) between `WithLp` over the reals (`ℝ`) and the type `ι → ℝ` (i.e., functions from `ι` to the reals), where `WithLp` is instantiated with `p` equals to `2`, is measure preserving. That is, it preserves the volume, as given by the Lebesgue measure (`MeasureTheory.volume`), under measure transformations. This theorem provides the reverse direction of `PiLp.volume_preserving_measurableEquiv`, and is needed because `MeasurePreserving.symm` only works for `MeasurableEquiv`s.
More concisely: The theorem asserts that the inverse of a finite equivalence between `WithLp` (instantiated with `p=2`) over the reals and functions from a finite type to the reals is measure preserving with respect to Lebesgue measure.
|
OrthonormalBasis.addHaar_eq_volume
theorem OrthonormalBasis.addHaar_eq_volume :
∀ {ι : Type u_4} {F : Type u_5} [inst : Fintype ι] [inst_1 : NormedAddCommGroup F] [inst_2 : InnerProductSpace ℝ F]
[inst_3 : FiniteDimensional ℝ F] [inst_4 : MeasurableSpace F] [inst_5 : BorelSpace F]
(b : OrthonormalBasis ι ℝ F), b.toBasis.addHaar = MeasureTheory.volume
This theorem states that for any finite-dimensional inner product space over the real numbers, the Haar measure defined by any orthonormal basis of this space is equal to its volume measure. The inner product space is denoted by `F` and the type of the basis elements is `ι`. The necessary conditions include: `F` being a group under addition with a norm (`NormedAddCommGroup`), having an inner product (`InnerProductSpace`), being finite-dimensional (`FiniteDimensional`), and being measurable with a Borel sigma-algebra (`MeasurableSpace` and `BorelSpace`). The orthonormal basis of the space is represented by `b`. The conclusion of the theorem is expressed in Lean as `b.toBasis.addHaar = MeasureTheory.volume`, meaning the Haar measure assigned to the basis `b` is equal to the volume measure of the space.
More concisely: For any finite-dimensional inner product space over the real numbers endowed with a Borel sigma-algebra and equipped with an orthonormal basis, the Haar measure induced by this basis equals the volume measure.
|