English
If a differentiable injective map is considered on a set, the image is null-measurable.
Русский
Если отображение дифференцируемо и инъективно на множестве, образ нулем измеримости.
LaTeX
$$$$ \exists \text{nullMeasurable image } f''s.$$$$
Lean4
/-- A version of Sard 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. -/
theorem addHaar_image_eq_zero_of_det_fderivWithin_eq_zero (hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x)
(h'f' : ∀ x ∈ s, (f' x).det = 0) : μ (f '' s) = 0 :=
by
suffices H : ∀ R, μ (f '' (s ∩ closedBall 0 R)) = 0
by
apply le_antisymm _ (zero_le _)
rw [← iUnion_inter_closedBall_nat s 0]
calc
μ (f '' ⋃ n : ℕ, s ∩ closedBall 0 n) ≤ ∑' n : ℕ, μ (f '' (s ∩ closedBall 0 n)) := by rw [image_iUnion];
exact measure_iUnion_le _
_ ≤ 0 := by simp only [H, tsum_zero, nonpos_iff_eq_zero]
intro R
have A : ∀ (ε : ℝ≥0), 0 < ε → μ (f '' (s ∩ closedBall 0 R)) ≤ ε * μ (closedBall 0 R) := fun ε εpos =>
addHaar_image_eq_zero_of_det_fderivWithin_eq_zero_aux μ (fun x hx => (hf' x hx.1).mono inter_subset_left) R
inter_subset_right ε εpos fun x hx => h'f' x hx.1
have B : Tendsto (fun ε : ℝ≥0 => (ε : ℝ≥0∞) * μ (closedBall 0 R)) (𝓝[>] 0) (𝓝 0) :=
by
have :
Tendsto (fun ε : ℝ≥0 => (ε : ℝ≥0∞) * μ (closedBall 0 R)) (𝓝 0) (𝓝 (((0 : ℝ≥0) : ℝ≥0∞) * μ (closedBall 0 R))) :=
ENNReal.Tendsto.mul_const (ENNReal.tendsto_coe.2 tendsto_id) (Or.inr measure_closedBall_lt_top.ne)
simp only [zero_mul, ENNReal.coe_zero] at this
exact Tendsto.mono_left this nhdsWithin_le_nhds
apply le_antisymm _ (zero_le _)
apply ge_of_tendsto B
filter_upwards [self_mem_nhdsWithin]
exact A
