English
Let E be a finite-dimensional real vector space with a Haar measure μ. If f: E → F is integrable with respect to μ and R ≠ 0, then the function x ↦ f(Rx) is integrable with respect to μ.
Русский
Пусть E — конечномерное вещественное векторное пространство с мерой Хаара μ. Если f: E → F интегрируема по μ и R ≠ 0, то функция x ↦ f(Rx) интегрируема по μ.
LaTeX
$$$\\int_E \\|f(x)\\| \\, d\\mu(x) < \\infty \\quad\\Rightarrow\\quad \\int_E \\|f(Rx)\\| \\, d\\mu(x) < \\infty$, при $R \\neq 0$.$$
Lean4
theorem comp_smul {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E]
[FiniteDimensional ℝ E] {μ : Measure E} [IsAddHaarMeasure μ] {f : E → F} (hf : Integrable f μ) {R : ℝ}
(hR : R ≠ 0) : Integrable (fun x => f (R • x)) μ :=
(integrable_comp_smul_iff μ f hR).2 hf
