English
If a function is differentiable on a set with a null-measure, the image of that set is null-measurable.
Русский
Если функция дифференцируема на множестве нулевой меры, образ этого множества нулево измерим.
LaTeX
$$$$ \text{NullMeasurable}(f''s)$$$$
Lean4
/-- If a function is differentiable and injective on a null measurable set,
then the image is null measurable. -/
theorem nullMeasurable_image_of_fderivWithin (hs : NullMeasurableSet s μ)
(hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x) (hf : InjOn f s) : NullMeasurableSet (f '' s) μ :=
by
rcases hs.exists_measurable_subset_ae_eq with ⟨t, ts, ht, t_eq_s⟩
have A : f '' s =ᵐ[μ] f '' t :=
by
have : s = t ∪ (s \ t) := by simp [union_eq_self_of_subset_left ts]
rw [this, image_union]
refine union_ae_eq_left_of_ae_eq_empty (ae_eq_empty.mpr ?_)
apply addHaar_image_eq_zero_of_differentiableOn_of_addHaar_eq_zero _ (fun x hx ↦ ?_) (ae_eq_set.1 t_eq_s).2
exact (hf' x hx.1).differentiableWithinAt.mono diff_subset
apply NullMeasurableSet.congr _ A.symm
apply MeasurableSet.nullMeasurableSet
apply measurable_image_of_fderivWithin ht _ (hf.mono ts) (f' := f')
intro x hx
exact (hf' x (ts hx)).mono ts
