English
If a differentiable injective function has a zero determinant everywhere on a set, the image of the set is null-measurable.
Русский
Если дифференцируемая инъективная функция имеет нулевой детерминант на множестве, образ множества нулим.
LaTeX
$$$$ \mu(f''s) = 0 \quad \text{when } \forall x \in s, \det f'(x) = 0 \text{ and } f \text{ is injective on } s.$$$$
Lean4
/-- A version of **Sard's lemma** in fixed dimension: given a differentiable function from `E`
to `E` and a set where the differential is not invertible, then the image of this set has
zero measure. Here, we give an auxiliary statement towards this result. -/
theorem addHaar_image_eq_zero_of_det_fderivWithin_eq_zero_aux (hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x) (R : ℝ)
(hs : s ⊆ closedBall 0 R) (ε : ℝ≥0) (εpos : 0 < ε) (h'f' : ∀ x ∈ s, (f' x).det = 0) :
μ (f '' s) ≤ ε * μ (closedBall 0 R) :=
by
rcases eq_empty_or_nonempty s with (rfl | h's); · simp only [measure_empty, zero_le, image_empty]
have :
∀ A : E →L[ℝ] E,
∃ δ : ℝ≥0,
0 < δ ∧ ∀ (t : Set E), ApproximatesLinearOn f A t δ → μ (f '' t) ≤ (Real.toNNReal |A.det| + ε : ℝ≥0) * μ t :=
by
intro A
let m : ℝ≥0 := Real.toNNReal |A.det| + ε
have I : ENNReal.ofReal |A.det| < m := by
simp only [m, ENNReal.ofReal, lt_add_iff_pos_right, εpos, 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_disj, t_meas, t_cover, ht, Af'⟩ :
∃ (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 = f' y) :=
exists_partition_approximatesLinearOn_of_hasFDerivWithinAt f s f' hf' δ fun A => (hδ A).1.ne'
calc
μ (f '' s) ≤ μ (⋃ n, f '' (s ∩ t n)) := by
rw [← image_iUnion, ← inter_iUnion]
gcongr
exact subset_inter Subset.rfl t_cover
_ ≤ ∑' n, μ (f '' (s ∩ t n)) := (measure_iUnion_le _)
_ ≤ ∑' n, (Real.toNNReal |(A n).det| + ε : ℝ≥0) * μ (s ∩ t n) :=
by
gcongr
exact (hδ (A _)).2 _ (ht _)
_ = ∑' n, ε * μ (s ∩ t n) := by
congr with n
rcases Af' h's n with ⟨y, ys, hy⟩
simp only [hy, h'f' y ys, Real.toNNReal_zero, abs_zero, zero_add]
_ ≤ ε * ∑' n, μ (closedBall 0 R ∩ t n) := by
rw [ENNReal.tsum_mul_left]
gcongr
_ = ε * μ (⋃ n, closedBall 0 R ∩ t n) := by
rw [measure_iUnion]
· exact pairwise_disjoint_mono t_disj fun n => inter_subset_right
· intro n
exact measurableSet_closedBall.inter (t_meas n)
_ ≤ ε * μ (closedBall 0 R) := by
rw [← inter_iUnion]
exact mul_le_mul_left' (measure_mono inter_subset_left) _
