English
Under appropriate hypotheses, the lintegral of |det f'| over s equals the image measure μ(f''s).
Русский
При определённых гипотезах линеграл модуля детерминанта совпадает с мерой образа.
LaTeX
$$$$ \int_{s} |\det f'(x)| \, d\mu = \mu(f''s). $$$$
Lean4
theorem addHaar_image_le_lintegral_abs_det_fderiv_aux2 (hs : MeasurableSet s) (h's : μ s ≠ ∞)
(hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x) : μ (f '' s) ≤ ∫⁻ x in s, ENNReal.ofReal |(f' x).det| ∂μ := by
-- We just need to let the error tend to `0` in the previous lemma.
have :
Tendsto (fun ε : ℝ≥0 => (∫⁻ x in s, ENNReal.ofReal |(f' x).det| ∂μ) + 2 * ε * μ s) (𝓝[>] 0)
(𝓝 ((∫⁻ x in s, ENNReal.ofReal |(f' x).det| ∂μ) + 2 * (0 : ℝ≥0) * μ s)) :=
by
apply Tendsto.mono_left _ nhdsWithin_le_nhds
refine tendsto_const_nhds.add ?_
refine ENNReal.Tendsto.mul_const ?_ (Or.inr h's)
exact ENNReal.Tendsto.const_mul (ENNReal.tendsto_coe.2 tendsto_id) (Or.inr ENNReal.coe_ne_top)
simp only [add_zero, zero_mul, mul_zero, ENNReal.coe_zero] at this
apply ge_of_tendsto this
filter_upwards [self_mem_nhdsWithin]
intro ε εpos
rw [mem_Ioi] at εpos
exact addHaar_image_le_lintegral_abs_det_fderiv_aux1 μ hs hf' εpos
