English
In a Haar-measure space, the image measure is bounded by the integral of |det f'| over the domain, under injectivity and differentiability assumptions.
Русский
В Haar-мерном пространстве образ меры ограничен интегралом по области от |det f'| при предположениях инъективности и дифференцируемости.
LaTeX
$$$$ \mu(f''s) \le \int_s |\det f'(x)| \, d\mu. $$$$
Lean4
theorem addHaar_image_le_lintegral_abs_det_fderiv (hs : MeasurableSet s)
(hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x) : μ (f '' s) ≤ ∫⁻ x in s, ENNReal.ofReal |(f' x).det| ∂μ := by
/- We already know the result for finite-measure sets. We cover `s` by finite-measure sets using
`spanningSets μ`, and apply the previous result to each of these parts. -/
let u n := disjointed (spanningSets μ) n
have u_meas : ∀ n, MeasurableSet (u n) := by
intro n
apply MeasurableSet.disjointed fun i => ?_
exact measurableSet_spanningSets μ i
have A : s = ⋃ n, s ∩ u n := by rw [← inter_iUnion, iUnion_disjointed, iUnion_spanningSets, inter_univ]
calc
μ (f '' s) ≤ ∑' n, μ (f '' (s ∩ u n)) := by
conv_lhs => rw [A, image_iUnion]
exact measure_iUnion_le _
_ ≤ ∑' n, ∫⁻ x in s ∩ u n, ENNReal.ofReal |(f' x).det| ∂μ :=
by
apply ENNReal.tsum_le_tsum fun n => ?_
apply
addHaar_image_le_lintegral_abs_det_fderiv_aux2 μ (hs.inter (u_meas n)) _ fun x hx =>
(hf' x hx.1).mono inter_subset_left
have : μ (u n) < ∞ := lt_of_le_of_lt (measure_mono (disjointed_subset _ _)) (measure_spanningSets_lt_top μ n)
exact ne_of_lt (lt_of_le_of_lt (measure_mono inter_subset_right) this)
_ = ∫⁻ x in s, ENNReal.ofReal |(f' x).det| ∂μ :=
by
conv_rhs => rw [A]
rw [lintegral_iUnion]
· intro n; exact hs.inter (u_meas n)
· exact pairwise_disjoint_mono (disjoint_disjointed _) fun n => inter_subset_right
