English
For any nonzero a ∈ ℝ, ENNReal.ofReal |a| • map (a ·) volume = volume.
Русский
Для любого a ≠ 0 в ℝ, ENNReal.ofReal |a| умножает отображение по объему слева и сохраняет меру: ENNReal.ofReal |a| · map (a ·) volume = volume.
LaTeX
$$$$ \\mathrm{ENNReal.ofReal}(|a|) \\cdot \\mathrm{Measure.map}(a \\cdot, \\mathrm{volume}) = \\mathrm{volume}. $$$$
Lean4
theorem smul_map_volume_mul_left {a : ℝ} (h : a ≠ 0) : ENNReal.ofReal |a| • Measure.map (a * ·) volume = volume :=
by
refine (Real.measure_ext_Ioo_rat fun p q => ?_).symm
rcases lt_or_gt_of_ne h with h | h
·
simp only [Real.volume_Ioo, Measure.smul_apply, ← ENNReal.ofReal_mul (le_of_lt <| neg_pos.2 h),
Measure.map_apply (measurable_const_mul a) measurableSet_Ioo, neg_sub_neg, neg_mul,
preimage_const_mul_Ioo_of_neg _ _ h, abs_of_neg h, mul_sub, smul_eq_mul, mul_div_cancel₀ _ (ne_of_lt h)]
·
simp only [Real.volume_Ioo, Measure.smul_apply, ← ENNReal.ofReal_mul (le_of_lt h),
Measure.map_apply (measurable_const_mul a) measurableSet_Ioo, preimage_const_mul_Ioo _ _ h, abs_of_pos h, mul_sub,
mul_div_cancel₀ _ (ne_of_gt h), smul_eq_mul]
