integral_comp_inv_mul_left — Mathlib

English

Equivalence of integral under inverse multiplication: ∫ g(a x) equals ∫ g under a⁻¹-scaling.

Русский

Эквивалентность интеграла при обратном умножении: ∫ g(a x) равен ∫ g на масштабе a⁻¹.

LaTeX

$$$\int g(a x) dμ = |a^{-1}| \int g(x) dμ$$$

Lean4

theorem integral_comp_inv_mul_left (g : ℝ → F) (a : ℝ) : (∫ x : ℝ, g (a⁻¹ * x)) = |a| • ∫ y : ℝ, g y := by
  simp_rw [← smul_eq_mul, Measure.integral_comp_inv_smul, Module.finrank_self, pow_one]

Похожие утверждения