MeasureTheory.Measure.integral_comp_inv_smul_of_nonneg
theorem MeasureTheory.Measure.integral_comp_inv_smul_of_nonneg :
∀ {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 : Type u_2} [inst_6 : NormedAddCommGroup F] [inst_7 : NormedSpace ℝ F]
(f : E → F) {R : ℝ}, 0 ≤ R → ∫ (x : E), f (R⁻¹ • x) ∂μ = R ^ FiniteDimensional.finrank ℝ E • ∫ (x : E), f x ∂μ
This theorem states that for any normed additive commutative group `E`, which is also a real normed space, measurable space, Borel space, and finite-dimensional over the reals, and given a measure `μ` that is an additive Haar measure, and a function `f` from `E` to another normed additive commutative group `F` that is also a real normed space, then for any nonnegative real number `R`, the integral of `f (R⁻¹ • x)` with respect to `μ` is equal to `R` raised to the power of the rank of `E` over the reals, scaled by the integral of `f` with respect to `μ`. This holds even if `f` is not integrable or `R = 0`, since by convention a non-integrable function has integral zero.
More concisely: For any normed additive commutative group `E` over the reals, finite-dimensional with Haar measure `μ`, and any real-valued function `f` on `E`, the integral of `f(R⁻¹ • x)` with respect to `μ` equals `R^n` times the integral of `f` if `E` has dimension `n` and `R` is non-negative.
|
MeasureTheory.Measure.integral_comp_smul
theorem MeasureTheory.Measure.integral_comp_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] {F : Type u_2} [inst_6 : NormedAddCommGroup F] [inst_7 : NormedSpace ℝ F]
(f : E → F) (R : ℝ), ∫ (x : E), f (R • x) ∂μ = |(R ^ FiniteDimensional.finrank ℝ E)⁻¹| • ∫ (x : E), f x ∂μ
This theorem states that for any normed add-commutative group `E`, equipped with a normed space structure over the real numbers ℝ, a measurable space structure, a Borel space structure, and a finite-dimensional real vector space structure, and given an additive Haar measure `μ` on `E`, if we take any normed add-commutative group `F`, equipped with a normed space structure over ℝ, and a function `f` from `E` to `F`, then the integral of the function `f` after scalar multiplication by a real number `R` (written as `f (R • x)`) with respect to the measure `μ` is equal to a scaled version of the integral of `f` with respect to `μ`. The scaling factor is the absolute value of the reciprocal of the real number `R` raised to the power of the rank of the vector space `E` (using `FiniteDimensional.finrank`). This theorem holds even when `f` is not integrable or when `R` equals zero due to the convention that a non-integrable function has an integral of zero.
More concisely: For any normed add-commutative groups `E` and `F` with finite-dimensional normed space structures over the real numbers, and additive Haar measure `μ` on `E`, the integral of `f: E → F` with respect to `μ` after scalar multiplication by `R ∈ ℝ` is equal to the scaled version of the integral of `f` with a factor of `|R|^{-rank(E)}`, where `rank(E)` is the rank of `E`.
|
MeasureTheory.Measure.integral_comp_smul_of_nonneg
theorem MeasureTheory.Measure.integral_comp_smul_of_nonneg :
∀ {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 : Type u_2} [inst_6 : NormedAddCommGroup F] [inst_7 : NormedSpace ℝ F]
(f : E → F) (R : ℝ) {hR : 0 ≤ R},
∫ (x : E), f (R • x) ∂μ = (R ^ FiniteDimensional.finrank ℝ E)⁻¹ • ∫ (x : E), f x ∂μ
The theorem `MeasureTheory.Measure.integral_comp_smul_of_nonneg` establishes the relationship between the integral of a function `f` and the integral of the function `f` composed with scaling by a non-negative real number `R`. Specifically, for any normed additively commutative group `E` that forms a normed real vector space, with a measure `μ` that is an additive Haar measure, and for any normed additively commutative group `F` that also forms a normed real vector space, and a function `f` from `E` to `F`, the integral with respect to `μ` of `f` composed with scaling by `R` equals the scaling by the reciprocal of `R` raised to the power of the dimension of `E` of the integral with respect to `μ` of `f`. This holds true even when `f` is not integrable or `R` equals zero due to the convention that the integral of a non-integrable function is zero.
More concisely: For any non-negative real number $R$ and a function $f$ from a normed additive commutative group $E$ to another such group $F$, with respect to an additive Haar measure $\mu$ on $E$, the integral of $f$ composed with scaling by $R$ equals $R^{-\dim(E)}$ times the integral of $f$ with respect to $\mu$.
|
MeasureTheory.Measure.integral_comp_inv_smul
theorem MeasureTheory.Measure.integral_comp_inv_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] {F : Type u_2} [inst_6 : NormedAddCommGroup F] [inst_7 : NormedSpace ℝ F]
(f : E → F) (R : ℝ), ∫ (x : E), f (R⁻¹ • x) ∂μ = |R ^ FiniteDimensional.finrank ℝ E| • ∫ (x : E), f x ∂μ
The theorem `MeasureTheory.Measure.integral_comp_inv_smul` provides a result in measure theory, specifically concerning integration over a vector space. For any normed and measurable vector space `E` over the real numbers with additive Haar measure `μ`, and any normed vector space `F` also over the real numbers, given a function `f` from `E` to `F` and a real number `R`, the integral of the function `f` applied to `R` inverse scaled `x` with respect to the measure `μ` is equal to the absolute value of `R` raised to the power of the rank of the vector space `E`, scaled by the integral of `f` over `x` with respect to the measure `μ`. This result holds even when `f` is not integrable or `R` equals zero, as by convention, a non-integrable function has an integral of zero.
More concisely: For any normed and measurable vector space `E` over the real numbers with additive Haar measure `μ`, and any function `f` from `E` to a normed vector space `F` over the real numbers, the integral of `f(Rx)` with respect to `μ` is equal to the absolute value of `R` raised to the power of the rank of `E` times the integral of `f` with respect to `μ`.
|