English
The derivative map is almost everywhere measurable on the domain where the derivative exists.
Русский
Карта производной измерима почти повсеместно на области существования производной.
LaTeX
$$$$ \text{A.e. } x \in s, \ f'(x) \text{ is measurable on } s.$$$$
Lean4
/-- A differentiable function maps sets of measure zero to sets of measure zero. -/
theorem addHaar_image_eq_zero_of_differentiableOn_of_addHaar_eq_zero (hf : DifferentiableOn ℝ f s) (hs : μ s = 0) :
μ (f '' s) = 0 := by
refine le_antisymm ?_ (zero_le _)
have :
∀ A : E →L[ℝ] E,
∃ δ : ℝ≥0,
0 < δ ∧ ∀ (t : Set E), ApproximatesLinearOn f A t δ → μ (f '' t) ≤ (Real.toNNReal |A.det| + 1 : ℝ≥0) * μ t :=
by
intro A
let m : ℝ≥0 := Real.toNNReal |A.det| + 1
have I : ENNReal.ofReal |A.det| < m := by
simp only [m, ENNReal.ofReal, lt_add_iff_pos_right, zero_lt_one, ENNReal.coe_lt_coe]
rcases ((addHaar_image_le_mul_of_det_lt μ A I).and self_mem_nhdsWithin).exists with ⟨δ, h, h'⟩
exact ⟨δ, h', fun t ht => h t f ht⟩
choose δ hδ using this
obtain ⟨t, A, _, _, t_cover, ht, -⟩ :
∃ (t : ℕ → Set E) (A : ℕ → E →L[ℝ] E),
Pairwise (Disjoint on t) ∧
(∀ n : ℕ, MeasurableSet (t n)) ∧
(s ⊆ ⋃ n : ℕ, t n) ∧
(∀ n : ℕ, ApproximatesLinearOn f (A n) (s ∩ t n) (δ (A n))) ∧
(s.Nonempty → ∀ n, ∃ y ∈ s, A n = fderivWithin ℝ f s y) :=
exists_partition_approximatesLinearOn_of_hasFDerivWithinAt f s (fderivWithin ℝ f s)
(fun x xs => (hf x xs).hasFDerivWithinAt) δ fun A => (hδ A).1.ne'
calc
μ (f '' s) ≤ μ (⋃ n, f '' (s ∩ t n)) := by
apply measure_mono
rw [← image_iUnion, ← inter_iUnion]
exact Set.image_mono (subset_inter Subset.rfl t_cover)
_ ≤ ∑' n, μ (f '' (s ∩ t n)) := (measure_iUnion_le _)
_ ≤ ∑' n, (Real.toNNReal |(A n).det| + 1 : ℝ≥0) * μ (s ∩ t n) :=
by
apply ENNReal.tsum_le_tsum fun n => ?_
apply (hδ (A n)).2
exact ht n
_ ≤ ∑' n, ((Real.toNNReal |(A n).det| + 1 : ℝ≥0) : ℝ≥0∞) * 0 :=
by
refine ENNReal.tsum_le_tsum fun n => mul_le_mul_left' ?_ _
exact le_trans (measure_mono inter_subset_left) (le_of_eq hs)
_ = 0 := by simp only [tsum_zero, mul_zero]
