English
The integral under a real-linear change of variable matches the standard scaling relation with finrank, for real-valued functions.
Русский
Интеграл при линейном преобразовании соответствует стандартному масштабному соотношению по finrank.
LaTeX
$$$\int_E f(R x) dx = |R|^{\mathrm{finrank}} \int_E f(x) dx$$$
Lean4
theorem integrable_comp_smul_iff {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E]
[FiniteDimensional ℝ E] (μ : Measure E) [IsAddHaarMeasure μ] (f : E → F) {R : ℝ} (hR : R ≠ 0) :
Integrable (fun x => f (R • x)) μ ↔ Integrable f μ := by
-- reduce to one-way implication
suffices ∀ {g : E → F} (_ : Integrable g μ) {S : ℝ} (_ : S ≠ 0), Integrable (fun x => g (S • x)) μ
by
refine ⟨fun hf => ?_, fun hf => this hf hR⟩
convert this hf (inv_ne_zero hR)
rw [← mul_smul, mul_inv_cancel₀ hR, one_smul]
-- now prove
intro g hg S hS
let t := ((Homeomorph.smul (isUnit_iff_ne_zero.2 hS).unit).toMeasurableEquiv : E ≃ᵐ E)
refine (integrable_map_equiv t g).mp (?_ : Integrable g (map (S • ·) μ))
rwa [map_addHaar_smul μ hS, integrable_smul_measure _ ENNReal.ofReal_ne_top]
simpa only [Ne, ENNReal.ofReal_eq_zero, not_le, abs_pos] using inv_ne_zero (pow_ne_zero _ hS)
