MeasureTheory.Measure.addHaar_image_continuousLinearMap
theorem MeasureTheory.Measure.addHaar_image_continuousLinearMap :
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : MeasurableSpace E]
[inst_3 : BorelSpace E] [inst_4 : FiniteDimensional ℝ E] (μ : MeasureTheory.Measure E)
[inst_5 : μ.IsAddHaarMeasure] (f : E →L[ℝ] E) (s : Set E),
↑↑μ (⇑f '' s) = ENNReal.ofReal |LinearMap.det ↑f| * ↑↑μ s
This theorem states that for a given set `s` in a finite-dimensional real normed add-commutative group `E`, the measure of the image of this set under a continuous linear map `f` is equal to the measure of the original set `s` multiplied by the absolute value of the determinant of `f`. This measure is with respect to a measure `μ` which is an additive Haar measure. The measure of the image set and the measure of the original set are both extended non-negative real numbers (`ENNReal`). The determinant of the linear map `f` is interpreted as a real number, and its absolute value is taken. If this real number is non-negative, it is considered as an extended non-negative real number; otherwise, it is considered as zero.
More concisely: The measure of the image of a finite-dimensional real set under a continuous linear map, with respect to an additive Haar measure, is equal to the measure of the original set multiplied by the absolute value of the determinant of the linear map.
|
MeasureTheory.Measure.addHaar_preimage_continuousLinearEquiv
theorem MeasureTheory.Measure.addHaar_preimage_continuousLinearEquiv :
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : MeasurableSpace E]
[inst_3 : BorelSpace E] [inst_4 : FiniteDimensional ℝ E] (μ : MeasureTheory.Measure E)
[inst_5 : μ.IsAddHaarMeasure] (f : E ≃L[ℝ] E) (s : Set E),
↑↑μ (⇑f ⁻¹' s) = ENNReal.ofReal |LinearMap.det ↑↑f.symm| * ↑↑μ s
This theorem states that for a set `s` when mapped using a continuous linear equivalence `f`, the measure of the preimage of the set `s` is equal to the measure of `s` times the absolute value of the inverse of the determinant of `f`. This is applicable in the context of a normed add commutative group `E` that is a normed space over the real numbers, is measurable, has Borel space structure, and is finite-dimensional. The measure `μ` is assumed to be an additive Haar measure. Here, the determinant of an endomorphism is defined independently of basis, and the measure is an extended nonnegative real number.
More concisely: For a finite-dimensional, measurable, normed space over the real numbers `E` with additive Haar measure `μ`, the measure of the preimage of a set `s` under a continuous linear equivalence `f` is equal to the measure of `s` times the absolute value of the determinant of `f`.
|
MeasureTheory.Measure.addHaar_closedBall'
theorem MeasureTheory.Measure.addHaar_closedBall' :
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : MeasurableSpace E]
[inst_3 : BorelSpace E] [inst_4 : FiniteDimensional ℝ E] (μ : MeasureTheory.Measure E)
[inst_5 : μ.IsAddHaarMeasure] (x : E) {r : ℝ},
0 ≤ r →
↑↑μ (Metric.closedBall x r) =
ENNReal.ofReal (r ^ FiniteDimensional.finrank ℝ E) * ↑↑μ (Metric.closedBall 0 1)
This theorem states that in a finite-dimensional real vector space, which is also a normed additively commutative group and has a Borel measurable space structure, the measure of a closed ball can be expressed in terms of the measure of the closed unit ball. More specifically, given an Add Haar measure on this space, the measure of the closed ball centered at any point "x" with a nonnegative radius "r" is equal to the measure of the unit closed ball multiplied by the real value of "r" raised to the power of the rank of the vector space. The rank is defined as the cardinality of a basis set, or 0 if the space has infinite dimension. The `ENNReal.ofReal` function is used to convert the real number to an extended non-negative real number.
More concisely: In a finite-dimensional real normed vector space with a Borel measurable space structure and Add Haar measure, the measure of a closed ball is equal to the measure of the unit ball multiplied by the radius raised to the power of the vector space's dimension.
|
MeasureTheory.Measure.tendsto_addHaar_inter_smul_one_of_density_one
theorem MeasureTheory.Measure.tendsto_addHaar_inter_smul_one_of_density_one :
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : MeasurableSpace E]
[inst_3 : BorelSpace E] [inst_4 : FiniteDimensional ℝ E] (μ : MeasureTheory.Measure E)
[inst_5 : μ.IsAddHaarMeasure] (s : Set E) (x : E),
Filter.Tendsto (fun r => ↑↑μ (s ∩ Metric.closedBall x r) / ↑↑μ (Metric.closedBall x r)) (nhdsWithin 0 (Set.Ioi 0))
(nhds 1) →
∀ (t : Set E),
MeasurableSet t →
↑↑μ t ≠ 0 →
↑↑μ t ≠ ⊤ →
Filter.Tendsto (fun r => ↑↑μ (s ∩ ({x} + r • t)) / ↑↑μ ({x} + r • t)) (nhdsWithin 0 (Set.Ioi 0))
(nhds 1)
This theorem states the following: consider a set `s` in a finite-dimensional real vector space `E`, equipped with a measure `μ` that is an additive Haar measure. Assume that at a certain point `x` in `E`, `s` has density one with respect to closed balls under the measure `μ`. This means that, as we take smaller and smaller closed balls centered at `x`, the proportion of each such ball that is occupied by `s` approaches one. Then, the theorem asserts, this property also holds for any measurable set `t` with non-zero and non-infinite measure: if we rescale `t` by a factor `r` and shift it so that `x` is in the rescaled set, then as `r` tends to zero, the proportion of the rescaled and shifted `t` that is occupied by `s` also approaches one. In other words, `s` has density one at `x` not just with respect to closed balls, but also with respect to any measurable set.
More concisely: If a set `s` in a finite-dimensional real vector space `E` has density one with respect to closed balls at a point `x` under an additive Haar measure `μ`, then `s` has density one at `x` with respect to any measurable set `t` with non-zero and non-infinite measure.
|
MeasureTheory.Measure.addHaar_submodule
theorem MeasureTheory.Measure.addHaar_submodule :
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : MeasurableSpace E]
[inst_3 : BorelSpace E] [inst_4 : FiniteDimensional ℝ E] (μ : MeasureTheory.Measure E)
[inst_5 : μ.IsAddHaarMeasure] (s : Submodule ℝ E), s ≠ ⊤ → ↑↑μ ↑s = 0
This theorem states that for a given strict vector subspace, its measure is zero. More specifically, consider a normed additive commutative group `E` over the real numbers, which is also a measurable space and a Borel space, and is finite dimensional. Let `μ` be a measure on `E` that is an additive Haar measure. For any submodule `s` of `E` that is not the entire space, the measure of `s` according to `μ` is zero.
More concisely: In a finite-dimensional, normed additive commutative group `E` over the real numbers equipped with an additive Haar measure `μ`, any submodule `s` that is proper to the entire space has measure zero according to `μ`.
|
MeasureTheory.Measure.tendsto_addHaar_inter_smul_zero_of_density_zero
theorem MeasureTheory.Measure.tendsto_addHaar_inter_smul_zero_of_density_zero :
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : MeasurableSpace E]
[inst_3 : BorelSpace E] [inst_4 : FiniteDimensional ℝ E] (μ : MeasureTheory.Measure E)
[inst_5 : μ.IsAddHaarMeasure] (s : Set E) (x : E),
Filter.Tendsto (fun r => ↑↑μ (s ∩ Metric.closedBall x r) / ↑↑μ (Metric.closedBall x r)) (nhdsWithin 0 (Set.Ioi 0))
(nhds 0) →
∀ (t : Set E),
MeasurableSet t →
↑↑μ t ≠ ⊤ →
Filter.Tendsto (fun r => ↑↑μ (s ∩ ({x} + r • t)) / ↑↑μ ({x} + r • t)) (nhdsWithin 0 (Set.Ioi 0))
(nhds 0)
This theorem relates to the concept of density of a set `s` at a point `x` in the context of measure theory. If the set `s` has density zero at point `x` with respect to closed balls, that is, the measure of the intersection of `s` and a closed ball centered at `x` with radius `r`, divided by the measure of the closed ball, tends to zero as `r` tends to zero, then the same holds true for any measurable set `t`. That is, the proportion of points in `s` belonging to a rescaled copy of `t` (denoted by `{x} + r • t` where `r` is a scaling factor) tends to zero as `r` tends to zero. This is true for any finitely-dimensional vector space `E` over the real numbers that is equipped with a measure `μ` that is an add-Haar measure (a type of measure preserving the volume under addition and scalar multiplication operations).
More concisely: If a set `s` has density zero at a point `x` with respect to closed balls in a finitely-dimensional real vector space `E` equipped with an add-Haar measure `μ`, then the proportion of points in any measurable set `t` belonging to rescaled copies of `t` around `x` tends to zero as the scaling factor `r` approaches zero.
|
MeasureTheory.Measure.addHaar_eq_zero_of_disjoint_translates_aux
theorem MeasureTheory.Measure.addHaar_eq_zero_of_disjoint_translates_aux :
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : MeasurableSpace E]
[inst_3 : BorelSpace E] [inst_4 : FiniteDimensional ℝ E] (μ : MeasureTheory.Measure E)
[inst_5 : μ.IsAddHaarMeasure] {s : Set E} (u : ℕ → E),
Bornology.IsBounded s →
Bornology.IsBounded (Set.range u) → Pairwise (Disjoint on fun n => {u n} + s) → MeasurableSet s → ↑↑μ s = 0
This theorem states that given a set `s` in a finite dimensional real normed add-commutative group `E` (with a Borel measurable structure and a normed space over the reals), and a sequence `u` of elements in `E`, if `s` and the range of `u` are both bounded, `s` is a measurable set, and for every two distinct elements `n` and `m` from the naturals, the translates `{u n} + s` and `{u m} + s` are disjoint, then the measure (in the sense of AddHaar measure) of the set `s` is zero.
In simpler words, if we translate a bounded and measurable set by infinitely many distinct bounded vectors such that no two translates overlap, then the original set must have measure zero.
More concisely: If a bounded, measurable set in a finite-dimensional real normed add-commutative group with disjoint translates by infinitely many distinct bounded vectors has zero measure sum.
Or, using Lean 4 notation:
`(∀ n m : ℕ, n ≠ m → s.bounded → {u : E} → bounded u → {u n + s} ∩ {u m + s} = ∅) → ∫ x in s, ∣∣x∣∣² dμ = 0`
where `E` is a finite-dimensional real normed add-commutative group, `s` is a measurable set, and `dμ` is the AddHaar measure.
|
MeasureTheory.Measure.addHaar_eq_zero_of_disjoint_translates
theorem MeasureTheory.Measure.addHaar_eq_zero_of_disjoint_translates :
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : MeasurableSpace E]
[inst_3 : BorelSpace E] [inst_4 : FiniteDimensional ℝ E] (μ : MeasureTheory.Measure E)
[inst_5 : μ.IsAddHaarMeasure] {s : Set E} (u : ℕ → E),
Bornology.IsBounded (Set.range u) → Pairwise (Disjoint on fun n => {u n} + s) → MeasurableSet s → ↑↑μ s = 0
This theorem states that if we have a set, in the context of a finite dimensional normed vector space over the real numbers with a specified measure that is an additive Haar measure, and this set is disjoint from its translations by infinitely many bounded vectors, then the measure of the set is zero. The theorem requires the set to be measurable and the vectors to be bounded and pairwise disjoint when added to the set. The translations of the set are indicated by the notation `{u n} + s`, which represents adding each vector `u n` to all elements of the set `s`. The condition `Pairwise (Disjoint on fun n => {u n} + s)` means that for all pairs of distinct natural numbers, the translations of the set by the corresponding vectors are disjoint.
More concisely: In a finite-dimensional real normed vector space endowed with an additive Haar measure, if a measurable set is disjoint from its translations by infinitely many bounded, pairwise disjoint vectors, then the set has measure zero.
|
MeasureTheory.Measure.addHaar_preimage_linearMap
theorem MeasureTheory.Measure.addHaar_preimage_linearMap :
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : MeasurableSpace E]
[inst_3 : BorelSpace E] [inst_4 : FiniteDimensional ℝ E] (μ : MeasureTheory.Measure E)
[inst_5 : μ.IsAddHaarMeasure] {f : E →ₗ[ℝ] E},
LinearMap.det f ≠ 0 → ∀ (s : Set E), ↑↑μ (⇑f ⁻¹' s) = ENNReal.ofReal |(LinearMap.det f)⁻¹| * ↑↑μ s
This theorem states that for a given normed additively commutative group `E` over the real numbers, which also has a finite dimension and a Borel measurable structure, if we have a measure `μ` that is an additive Haar measure, and a linear map `f` from `E` to `E` with a nonzero determinant, then for any set `s` of `E`, the measure of the preimage of `s` under `f` is equal to the measure of `s` times the absolute value of the inverse of the determinant of `f`. In simpler terms, it describes how the measure of a set changes when the set is transformed by a linear map with a nonzero determinant.
More concisely: For a finite-dimensional normed additively commutative group `E` over the real numbers with a Borel measurable structure and an additive Haar measure `μ`, if `f : E → E` is a linear map with a nonzero determinant, then `μ(f⁻¹(s)) = |det(f)| * μ(s)` for any measurable set `s ∈ E`.
|
MeasureTheory.Measure.addHaar_smul
theorem MeasureTheory.Measure.addHaar_smul :
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : MeasurableSpace E]
[inst_3 : BorelSpace E] [inst_4 : FiniteDimensional ℝ E] (μ : MeasureTheory.Measure E)
[inst_5 : μ.IsAddHaarMeasure] (r : ℝ) (s : Set E),
↑↑μ (r • s) = ENNReal.ofReal |r ^ FiniteDimensional.finrank ℝ E| * ↑↑μ s
This theorem states that for a given normed additive commutative group `E` that also has a structure of a real normed space, measurable space, and Borel space, and is of finite dimension over the real numbers, with `μ` as an add-Haar measure on `E`, the measure of the set obtained by scaling a set `s` by a factor `r` is equal to the absolute value of `r` raised to the power of the rank of the finite dimensional space `E` times the measure of the original set `s`. In mathematical terms, if `μ` is a measure and `s` is a set in `E`, then the measure of the scaled set `r•s` is `|r|^dim(E) * μ(s)`, where `dim(E)` is the dimension of the vector space `E`.
More concisely: For a finite-dimensional, real normed space `E` with Haar measure `μ`, the measure of a set `s` is equal to the absolute value of the scaling factor `r` raised to the power of the space's dimension, multiplied by the measure of the scaled set `r•s`.
|
MeasureTheory.addHaarMeasure_eq_volume
theorem MeasureTheory.addHaarMeasure_eq_volume :
MeasureTheory.Measure.addHaarMeasure TopologicalSpace.PositiveCompacts.Icc01 = MeasureTheory.volume
This theorem states that the Haar measure, when applied to the compact set with non-empty interior that represents the interval `[0,1]` in the real numbers, is equivalent to the Lebesgue measure on the real numbers. The Haar measure and the Lebesgue measure are both concepts in measure theory, a branch of Mathematics related to determining the size or volume of mathematical objects.
More concisely: The Haar measure and Lebesgue measure agree on the Borel sets of the real numbers when restricted to the interval [0,1].
|
MeasureTheory.Measure.addHaar_preimage_linearEquiv
theorem MeasureTheory.Measure.addHaar_preimage_linearEquiv :
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : MeasurableSpace E]
[inst_3 : BorelSpace E] [inst_4 : FiniteDimensional ℝ E] (μ : MeasureTheory.Measure E)
[inst_5 : μ.IsAddHaarMeasure] (f : E ≃ₗ[ℝ] E) (s : Set E),
↑↑μ (⇑f ⁻¹' s) = ENNReal.ofReal |LinearMap.det ↑f.symm| * ↑↑μ s
This theorem states that for any normed additive commutative group `E` which is also a normed space over the real numbers and has finite dimension, and for any measure `μ` that is an additive Haar measure on `E`, the measure of the preimage of a set `s` under a linear equivalence `f` is equal to the measure of `s` times the absolute value of the inverse of the determinant of `f`. In simpler terms, it describes a property of measures under linear transformations, particularly stating that the measure of a transformed set is proportional to the measure of the original set and the determinant of the transformation.
More concisely: For any finite-dimensional normed additive commutative group `E` over the real numbers, endowed with an additive Haar measure `μ`, and any linear equivalence `f : E → E`, the measure of `μ(f⁻¹(s))` equals `|det(f)| * μ(s)` for any set `s ⊆ E`.
|
MeasureTheory.addHaarMeasure_eq_volume_pi
theorem MeasureTheory.addHaarMeasure_eq_volume_pi :
∀ (ι : Type u_1) [inst : Fintype ι],
MeasureTheory.Measure.addHaarMeasure (TopologicalSpace.PositiveCompacts.piIcc01 ι) = MeasureTheory.volume
This theorem states that for any finite type `ι`, the Haar measure on the compact set with non-empty interior `[0,1]^ι` is equal to the Lebesgue measure in `ℝ^ι`. In other words, the Haar measure and the Lebesgue measure give the same result when applied to the unit interval [0, 1] in the `ι`-dimensional real space, where `ι` is a finite type.
More concisely: For any finite type `ι`, the Haar measure on the compact unit cube `[0,1]^ι` in `ℝ^ι` equals the Lebesgue measure.
|
MeasureTheory.Measure.addHaar_closedBall_center
theorem MeasureTheory.Measure.addHaar_closedBall_center :
∀ {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : MeasurableSpace E] [inst_2 : BorelSpace E]
(μ : MeasureTheory.Measure E) [inst_3 : μ.IsAddHaarMeasure] (x : E) (r : ℝ),
↑↑μ (Metric.closedBall x r) = ↑↑μ (Metric.closedBall 0 r)
This theorem states that for any normed additive commutative group `E` with a measurable space structure, a Borel space structure, and an associated Add Haar measure `μ`, the measure of the closed ball of radius `r` centered at any point `x` in `E` is equal to the measure of the closed ball of the same radius `r` centered at the origin. In other words, Add Haar measures are translation invariant in the sense that shifting the center of a closed ball doesn't change its measure.
More concisely: For any normed additive commutative group `E` with a measurable space structure, Borel space structure, and an Add Haar measure `μ`, the measure of a closed ball in `E` is translation invariant, i.e., the measure of the closed ball centered at `x` with radius `r` is equal to the measure of the closed ball centered at the origin with radius `r`.
|
AlternatingMap.measure_def
theorem AlternatingMap.measure_def :
∀ {G : Type u_5} [inst : NormedAddCommGroup G] [inst_1 : NormedSpace ℝ G] [inst_2 : MeasurableSpace G]
[inst_3 : BorelSpace G] [inst_4 : FiniteDimensional ℝ G] {n : ℕ} [_i : Fact (FiniteDimensional.finrank ℝ G = n)]
(ω : G [⋀^Fin n]→ₗ[ℝ] ℝ),
ω.measure =
‖ω ⇑(FiniteDimensional.finBasisOfFinrankEq ℝ G ⋯)‖₊ • (FiniteDimensional.finBasisOfFinrankEq ℝ G ⋯).addHaar
This theorem, `AlternatingMap.measure_def`, is about the measure associated with an alternating multilinear map `ω` on a finite-dimensional real vector space `G`. If `G` is an `n`-dimensional real vector space (i.e., `FiniteDimensional.finrank ℝ G = n`), then the measure of `ω` is defined as the product of the operator norm of `ω` applied to a basis of `G` (obtained using `FiniteDimensional.finBasisOfFinrankEq`) and the Lebesgue measure associated with that basis (`Basis.addHaar`). This Lebesgue measure is defined such that the volume of the parallelepiped spanned by the basis vectors is `1`.
More concisely: The measure of an alternating multilinear map on a finite-dimensional real vector space is equal to the product of its operator norm with respect to a basis and the Lebesgue measure associated with that basis, where the Lebesgue measure is such that the volume of the basis's parallelepiped is 1.
|
MeasureTheory.Measure.addHaar_image_linearMap
theorem MeasureTheory.Measure.addHaar_image_linearMap :
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : MeasurableSpace E]
[inst_3 : BorelSpace E] [inst_4 : FiniteDimensional ℝ E] (μ : MeasureTheory.Measure E)
[inst_5 : μ.IsAddHaarMeasure] (f : E →ₗ[ℝ] E) (s : Set E),
↑↑μ (⇑f '' s) = ENNReal.ofReal |LinearMap.det f| * ↑↑μ s
The theorem `MeasureTheory.Measure.addHaar_image_linearMap` states that for any normed additively commutative group `E` that has a normed real vector space structure, measurable space structure, Borel space structure, and which is also a finite-dimensional real vector space, given a measure `μ` that is an additive Haar measure, a linear map `f` from `E` to `E`, and a set `s` of `E`, the measure of the image of the set `s` under the linear map `f` is equal to the measure of `s` times the absolute value of the determinant of `f`. In mathematical notation, if `μ` is a measure, `f: E → E` a linear map, and `s ⊆ E` a set, then `μ(f(s)) = |det(f)| * μ(s)`, where `f(s)` is the image of `s` under `f` and `det(f)` is the determinant of `f`.
More concisely: For any finite-dimensional, normed, additively commutative group `E` with Haar measure `μ`, a linear map `f: E → E`, and measurable set `s ⊆ E`, the image `f(s)` has measure `|det(f)| * μ(s)`.
|
MeasureTheory.Measure.addHaar_image_continuousLinearEquiv
theorem MeasureTheory.Measure.addHaar_image_continuousLinearEquiv :
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : MeasurableSpace E]
[inst_3 : BorelSpace E] [inst_4 : FiniteDimensional ℝ E] (μ : MeasureTheory.Measure E)
[inst_5 : μ.IsAddHaarMeasure] (f : E ≃L[ℝ] E) (s : Set E),
↑↑μ (⇑f '' s) = ENNReal.ofReal |LinearMap.det ↑↑f| * ↑↑μ s
This theorem states that, given a normed additive commutative group `E` that is a normed space over the real numbers and has a finite dimension, along with a measure `μ` on `E` that is an additive Haar measure, a continuous linear equivalence `f` from `E` to `E`, and a set `s` in `E`, the measure of the image of the set `s` under `f` is equal to the measure of `s` times the absolute value of the determinant of `f`. In mathematical terms, this translates to $\mu(f(s)) = |\det(f)| \cdot \mu(s)$.
More concisely: Given a finite-dimensional normed space `E` over the real numbers with an additive Haar measure `μ`, a continuous linear equivalence `f` from `E` to `E`, and a set `s` in `E`, the measure of `s` under `μ` is equal to the measure of `f(s)` multiplied by the absolute value of the determinant of `f`. In symbols: $\mu(s) = |\det(f)| \cdot \mu(f(s))$.
|
MeasureTheory.Measure.addHaar_closedBall_eq_addHaar_ball
theorem MeasureTheory.Measure.addHaar_closedBall_eq_addHaar_ball :
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : MeasurableSpace E]
[inst_3 : BorelSpace E] [inst_4 : FiniteDimensional ℝ E] (μ : MeasureTheory.Measure E)
[inst_5 : μ.IsAddHaarMeasure] [inst_6 : Nontrivial E] (x : E) (r : ℝ),
↑↑μ (Metric.closedBall x r) = ↑↑μ (Metric.ball x r)
This theorem, named `MeasureTheory.Measure.addHaar_closedBall_eq_addHaar_ball`, states that for any normed additively commutative group `E` that is also a real normed space with a measurable and Borel space structure, and finite-dimensionality over the real numbers, given an additive Haar measure `μ` on this space `E` and a nontrivial element `x` of `E` along with a real number `r`, the measure of the closed ball centered at `x` with radius `r` under `μ` is equal to the measure of the open ball centered at `x` with radius `r` under `μ`. The closed ball is the set of all points whose distance from `x` is less than or equal to `r`, and the open ball is the set of all points whose distance from `x` is strictly less than `r`.
More concisely: For any finite-dimensional, real normed space `E` with a measurable and Borel structure, and additive Haar measure `μ`, the measure of a closed ball equals the measure of the corresponding open ball.
|
MeasureTheory.Measure.addHaar_affineSubspace
theorem MeasureTheory.Measure.addHaar_affineSubspace :
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : MeasurableSpace E]
[inst_3 : BorelSpace E] [inst_4 : FiniteDimensional ℝ E] (μ : MeasureTheory.Measure E)
[inst_5 : μ.IsAddHaarMeasure] (s : AffineSubspace ℝ E), s ≠ ⊤ → ↑↑μ ↑s = 0
This theorem states that for any strict affine subspace `s` of a real finite-dimensional normed additive commutative group `E` that is also a normed space and a measurable space with a Borel sigma-algebra, the measure of `s` with respect to any additively Haar measure `μ` on `E` is zero. In simpler terms, it says that any strict affine subspace of a real finite-dimensional vector space carries zero measure under any translation-invariant measure on the whole space.
More concisely: Any strict affine subspace of a real finite-dimensional normed additive commutative group, considered as a normed space and measurable space with a Borel sigma-algebra, has measure zero with respect to any additively Haar measure.
|
MeasureTheory.Measure.eventually_nonempty_inter_smul_of_density_one
theorem MeasureTheory.Measure.eventually_nonempty_inter_smul_of_density_one :
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : MeasurableSpace E]
[inst_3 : BorelSpace E] [inst_4 : FiniteDimensional ℝ E] (μ : MeasureTheory.Measure E)
[inst_5 : μ.IsAddHaarMeasure] (s : Set E) (x : E),
Filter.Tendsto (fun r => ↑↑μ (s ∩ Metric.closedBall x r) / ↑↑μ (Metric.closedBall x r)) (nhdsWithin 0 (Set.Ioi 0))
(nhds 1) →
∀ (t : Set E),
MeasurableSet t → ↑↑μ t ≠ 0 → ∀ᶠ (r : ℝ) in nhdsWithin 0 (Set.Ioi 0), (s ∩ ({x} + r • t)).Nonempty
Given a point `x` in a normed additive commutative group `E` (which is also a normed space over the real numbers, a measurable space, a Borel space, and a finite-dimensional vector space), and a measure `μ` on `E` that is an additive Haar measure, consider a set `s` such that the density of `s` at the point `x` with respect to closed balls is 1 - this is to say, as we take increasingly small closed balls centered at `x`, the ratio of the measure of the intersection of `s` with the closed ball to the measure of the closed ball itself tends to 1.
The theorem asserts that under these conditions, for any measurable set `t` with non-zero measure, if we take sufficiently small real numbers `r` and consider the set obtained by scaling `t` by `r` and translating by `x`, then the intersection of this set with `s` is non-empty. In other words, `s` intersects the rescaled and translated copies of `t` for any small enough `r`. This holds true whenever `r` is drawn from a neighborhood of 0 that excludes non-positive numbers.
More concisely: Given a point `x` in a finite-dimensional normed additive commutative group `E` with an additive Haar measure `μ`, if `s` is a measurable set with density 1 at `x` and `t` is a measurable set with non-zero measure, then for any small enough positive real number `r`, the intersection of `s` with the translated and scaled copy of `t` by `r` and `x` is non-empty.
|
Basis.parallelepiped_eq_map
theorem Basis.parallelepiped_eq_map :
∀ {ι : Type u_1} {E : Type u_2} [inst : Fintype ι] [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace ℝ E]
(b : Basis ι ℝ E),
b.parallelepiped =
TopologicalSpace.PositiveCompacts.map ⇑b.equivFun.symm ⋯ ⋯ (TopologicalSpace.PositiveCompacts.piIcc01 ι)
The theorem `Basis.parallelepiped_eq_map` states that for any finite type `ι` and any normed additive commutative group `E` with a normed space structure over the real numbers `ℝ`, given a basis `b` of `E`, the parallelepiped spanned by this basis can be expressed as the image of the compact set `[0,1]^ι` under a continuous open map, where the continuous open map is the inverse function `b.equivFun.symm` of the coordinate function of the basis. In other words, the parallelepiped is the result of applying the inverse coordinate function to each point in the compact set `[0,1]^ι`.
More concisely: The parallelepiped spanned by a basis of a normed additive commutative group is the image of the unit cube under the inverse coordinate function of the basis.
|
MeasureTheory.Measure.addHaar_preimage_continuousLinearMap
theorem MeasureTheory.Measure.addHaar_preimage_continuousLinearMap :
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : MeasurableSpace E]
[inst_3 : BorelSpace E] [inst_4 : FiniteDimensional ℝ E] (μ : MeasureTheory.Measure E)
[inst_5 : μ.IsAddHaarMeasure] {f : E →L[ℝ] E},
LinearMap.det ↑f ≠ 0 → ∀ (s : Set E), ↑↑μ (⇑f ⁻¹' s) = ENNReal.ofReal |(LinearMap.det ↑f)⁻¹| * ↑↑μ s
This theorem states that for any normed additive commutative group `E` that forms a normed space over the real numbers, and which is a measurable space with a Borel sigma-algebra and is finite dimensional as a real vector space, given a measure `μ` which is a Haar measure and a continuous linear map `f` from `E` to `E` with a nonzero determinant, the measure of the preimage of a set `s` under the map `f` is equal to the measure of `s` times the absolute value of the inverse of the determinant of `f`. In other words, in this context, the measure of the preimage of a set under a continuous linear map with nonzero determinant is scaled by the absolute value of the inverse of the determinant of the map.
More concisely: Given a finite-dimensional, real normed space `E` with Haar measure `μ` and a continuous linear map `f` with nonzero determinant, the measure of `f⁻¹(s)` equals `|det(f)|⁻¹ * μ(s)`, where `s` is a set in `E`.
|
Basis.parallelepiped_basisFun
theorem Basis.parallelepiped_basisFun :
∀ (ι : Type u_1) [inst : Fintype ι],
(Pi.basisFun ℝ ι).parallelepiped = TopologicalSpace.PositiveCompacts.piIcc01 ι
The theorem `Basis.parallelepiped_basisFun` states that for any finite type `ι`, the parallelepiped formed from the standard basis for `ι → ℝ` (defined by `Pi.basisFun ℝ ι`) is the set `[0,1]^ι` (represented by `TopologicalSpace.PositiveCompacts.piIcc01 ι`). In other words, the parallelepiped spanned by the standard basis vectors in the function space `ι → ℝ` is equivalent to the interval `[0,1]` taken over all elements in `ι`.
More concisely: The parallelepiped formed from the standard basis of `ι → ℝ` is equal to `[0,1]^ι`.
|