English
The norm on a finite-dimensional real vector space is differentiable almost everywhere; in fact, the set of nondifferentiable points is meager and the norm is a.a. differentiable.
Русский
Норма в конечномерном вещественном векторном пространстве дифференцируема почти всюду; множество точек несходимости тоще, чемли ({не дифференцируемо}) является малым.
LaTeX
$$$\text{ae}\; D\|x\|=\text{differentiable a.e.}$$$
Lean4
/-- If a Lipschitz functions has line derivatives in a dense set of directions, all of them given by
a single continuous linear map `L`, then it admits `L` as Fréchet derivative. -/
theorem hasFDerivAt_of_hasLineDerivAt_of_closure {f : E → F} (hf : LipschitzWith C f) {s : Set E}
(hs : sphere 0 1 ⊆ closure s) {L : E →L[ℝ] F} {x : E} (hL : ∀ v ∈ s, HasLineDerivAt ℝ f (L v) x v) :
HasFDerivAt f L x := by
rw [hasFDerivAt_iff_isLittleO_nhds_zero, isLittleO_iff]
intro ε εpos
obtain ⟨δ, δpos, hδ⟩ : ∃ δ, 0 < δ ∧ (C + ‖L‖ + 1) * δ = ε :=
⟨ε / (C + ‖L‖ + 1), by positivity, mul_div_cancel₀ ε (by positivity)⟩
obtain ⟨q, hqs, q_fin, hq⟩ : ∃ q, q ⊆ s ∧ q.Finite ∧ sphere 0 1 ⊆ ⋃ y ∈ q, ball y δ :=
by
have : sphere 0 1 ⊆ ⋃ y ∈ s, ball y δ := by
apply hs.trans (fun z hz ↦ ?_)
obtain ⟨y, ys, hy⟩ : ∃ y ∈ s, dist z y < δ := Metric.mem_closure_iff.1 hz δ δpos
exact mem_biUnion ys hy
exact (isCompact_sphere 0 1).elim_finite_subcover_image (fun y _hy ↦ isOpen_ball) this
have I : ∀ᶠ t in 𝓝 (0 : ℝ), ∀ v ∈ q, ‖f (x + t • v) - f x - t • L v‖ ≤ δ * ‖t‖ :=
by
apply (Finite.eventually_all q_fin).2 (fun v hv ↦ ?_)
apply Asymptotics.IsLittleO.def ?_ δpos
exact hasLineDerivAt_iff_isLittleO_nhds_zero.1 (hL v (hqs hv))
obtain ⟨r, r_pos, hr⟩ : ∃ (r : ℝ), 0 < r ∧ ∀ (t : ℝ), ‖t‖ < r → ∀ v ∈ q, ‖f (x + t • v) - f x - t • L v‖ ≤ δ * ‖t‖ :=
by
rcases Metric.mem_nhds_iff.1 I with ⟨r, r_pos, hr⟩
exact ⟨r, r_pos, fun t ht v hv ↦ hr (mem_ball_zero_iff.2 ht) v hv⟩
apply Metric.mem_nhds_iff.2 ⟨r, r_pos, fun v hv ↦ ?_⟩
rcases eq_or_ne v 0 with rfl | v_ne
· simp
obtain ⟨w, ρ, w_mem, hvw, hρ⟩ : ∃ w ρ, w ∈ sphere 0 1 ∧ v = ρ • w ∧ ρ = ‖v‖ :=
by
refine ⟨‖v‖⁻¹ • v, ‖v‖, by simp [norm_smul, inv_mul_cancel₀ (norm_ne_zero_iff.2 v_ne)], ?_, rfl⟩
simp [smul_smul, mul_inv_cancel₀ (norm_ne_zero_iff.2 v_ne)]
have norm_rho : ‖ρ‖ = ρ := by rw [hρ, norm_norm]
have rho_pos : 0 ≤ ρ := by simp [hρ]
obtain ⟨y, yq, hy⟩ : ∃ y ∈ q, ‖w - y‖ < δ := by simpa [← dist_eq_norm] using hq w_mem
have : ‖y - w‖ < δ := by rwa [norm_sub_rev]
calc
‖f (x + v) - f x - L v‖ = ‖f (x + ρ • w) - f x - ρ • L w‖ := by simp [hvw]
_ = ‖(f (x + ρ • w) - f (x + ρ • y)) + (ρ • L y - ρ • L w) + (f (x + ρ • y) - f x - ρ • L y)‖ := by congr; abel
_ ≤ ‖f (x + ρ • w) - f (x + ρ • y)‖ + ‖ρ • L y - ρ • L w‖ + ‖f (x + ρ • y) - f x - ρ • L y‖ := norm_add₃_le
_ ≤ C * ‖(x + ρ • w) - (x + ρ • y)‖ + ρ * (‖L‖ * ‖y - w‖) + δ * ρ :=
by
gcongr
· exact hf.norm_sub_le _ _
· rw [← smul_sub, norm_smul, norm_rho]
gcongr
exact L.lipschitz.norm_sub_le _ _
· conv_rhs => rw [← norm_rho]
apply hr _ _ _ yq
simpa [norm_rho, hρ] using hv
_ ≤ C * (ρ * δ) + ρ * (‖L‖ * δ) + δ * ρ := by simp only [add_sub_add_left_eq_sub, ← smul_sub, norm_smul, norm_rho];
gcongr
_ = ((C + ‖L‖ + 1) * δ) * ρ := by ring
_ = ε * ‖v‖ := by rw [hδ, hρ]
