English
If f is differentiable and injective on a measurable set, then the restriction yields a measurable embedding.
Русский
Если f дифференцируема и инъективна на измеримом множестве, ограничение даёт измеримое вложение.
LaTeX
$$$$ \text{MeasurableEmbedding}(s\restriction f) $$$$
Lean4
theorem lintegral_abs_det_fderiv_le_addHaar_image (hs : MeasurableSet s) (hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x)
(hf : InjOn f s) : (∫⁻ x in s, ENNReal.ofReal |(f' x).det| ∂μ) ≤ μ (f '' s) := 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
(∫⁻ x in s, ENNReal.ofReal |(f' x).det| ∂μ) = ∑' n, ∫⁻ x in s ∩ u n, ENNReal.ofReal |(f' x).det| ∂μ :=
by
conv_lhs => rw [A]
rw [lintegral_iUnion]
· intro n; exact hs.inter (u_meas n)
· exact pairwise_disjoint_mono (disjoint_disjointed _) fun n => inter_subset_right
_ ≤ ∑' n, μ (f '' (s ∩ u n)) := by
apply ENNReal.tsum_le_tsum fun n => ?_
apply
lintegral_abs_det_fderiv_le_addHaar_image_aux2 μ (hs.inter (u_meas n)) _
(fun x hx => (hf' x hx.1).mono inter_subset_left) (hf.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)
_ = μ (f '' s) := by
conv_rhs => rw [A, image_iUnion]
rw [measure_iUnion]
· intro i j hij
apply Disjoint.image _ hf inter_subset_left inter_subset_left
exact Disjoint.mono inter_subset_right inter_subset_right (disjoint_disjointed _ hij)
· intro i
exact
measurable_image_of_fderivWithin (hs.inter (u_meas i)) (fun x hx => (hf' x hx.1).mono inter_subset_left)
(hf.mono inter_subset_left)
