Exact source: Mathlib/Analysis/Calculus/Rademacher.lean
Pinned GitHub source · Raw UTF-8 source
Back to Signed transfer from the absolute Jacobian formula · Back to Weak Piola identity for a compactly supported test field · Back to The absolute Jacobian integral of a radial sphere extension
1/-2Copyright (c) 2023 Sébastien Gouëzel. All rights reserved.3Released under Apache 2.0 license as described in the file LICENSE.4Authors: Sébastien Gouëzel5-/6module78public import Mathlib.Analysis.Calculus.LineDeriv.Measurable9public import Mathlib.Analysis.Normed.Module.FiniteDimension10public import Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar11public import Mathlib.Analysis.BoundedVariation12public import Mathlib.MeasureTheory.Group.Integral13public import Mathlib.Analysis.Distribution.AEEqOfIntegralContDiff14public import Mathlib.MeasureTheory.Measure.Haar.Disintegration1516/-!17# Rademacher's theorem: a Lipschitz function is differentiable almost everywhere1819This file proves Rademacher's theorem: a Lipschitz function between finite-dimensional real vector20spaces is differentiable almost everywhere with respect to the Lebesgue measure. This is the content21of `LipschitzWith.ae_differentiableAt`. Versions for functions which are Lipschitz on sets are also22given (see `LipschitzOnWith.ae_differentiableWithinAt`).2324## Implementation2526There are many proofs of Rademacher's theorem. We follow the one by Morrey, which is not the most27elementary but maybe the most elegant once necessary prerequisites are set up.28* Step 0: without loss of generality, one may assume that `f` is real-valued.29* Step 1: Since a one-dimensional Lipschitz function has bounded variation, it is differentiable30 almost everywhere. With a Fubini argument, it follows that given any vector `v` then `f` is ae31 differentiable in the direction of `v`. See `LipschitzWith.ae_lineDifferentiableAt`.32* Step 2: the line derivative `LineDeriv ℝ f x v` is ae linear in `v`. Morrey proves this by a33 duality argument, integrating against a smooth compactly supported function `g`, passing the34 derivative to `g` by integration by parts, and using the linearity of the derivative of `g`.35 See `LipschitzWith.ae_lineDeriv_sum_eq`.36* Step 3: consider a countable dense set `s` of directions. Almost everywhere, the function `f`37 is line-differentiable in all these directions and the line derivative is linear. Approximating38 any direction by a direction in `s` and using the fact that `f` is Lipschitz to control the error,39 it follows that `f` is Fréchet-differentiable at these points.40 See `LipschitzWith.hasFDerivAt_of_hasLineDerivAt_of_closure`.4142## References4344* [Pertti Mattila, Geometry of sets and measures in Euclidean spaces, Theorem 7.3][Federer1996]45-/4647public section4849open Filter MeasureTheory Measure Module Metric Set Asymptotics5051open scoped NNReal ENNReal Topology5253variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]54 [MeasurableSpace E] [BorelSpace E]55 {F : Type*} [NormedAddCommGroup F] [NormedSpace ℝ F] {C D : ℝ≥0} {f g : E → ℝ} {s : Set E}56 {μ : Measure E}5758namespace LipschitzWith5960/-!61### Step 1: A Lipschitz function is ae differentiable in any given direction6263This follows from the one-dimensional result that a Lipschitz function on `ℝ` has bounded64variation, and is therefore ae differentiable, together with a Fubini argument.65-/666768theorem memLp_lineDeriv (hf : LipschitzWith C f) (v : E) :69 MemLp (fun x ↦ lineDeriv ℝ f x v) ∞ μ :=70 memLp_top_of_bound (aestronglyMeasurable_lineDeriv hf.continuous μ)71 (C * ‖v‖) (.of_forall fun _x ↦ norm_lineDeriv_le_of_lipschitz ℝ hf)7273variable [FiniteDimensional ℝ E] [IsAddHaarMeasure μ]7475theorem ae_lineDifferentiableAt76 (hf : LipschitzWith C f) (v : E) :77 ∀ᵐ p ∂μ, LineDifferentiableAt ℝ f p v := by78 let L : ℝ →L[ℝ] E := ContinuousLinearMap.smulRight (1 : ℝ →L[ℝ] ℝ) v79 suffices A : ∀ p, ∀ᵐ (t : ℝ) ∂volume, LineDifferentiableAt ℝ f (p + t • v) v from80 ae_mem_of_ae_add_linearMap_mem L.toLinearMap volume μ81 (measurableSet_lineDifferentiableAt hf.continuous) A82 intro p83 have : ∀ᵐ (s : ℝ), DifferentiableAt ℝ (fun t ↦ f (p + t • v)) s :=84 (hf.comp ((LipschitzWith.const p).add L.lipschitz)).ae_differentiableAt_real85 filter_upwards [this] with s hs86 have h's : DifferentiableAt ℝ (fun t ↦ f (p + t • v)) (s + 0) := by simpa using hs87 have : DifferentiableAt ℝ (fun t ↦ s + t) 0 := differentiableAt_id.const_add _88 simp only [LineDifferentiableAt]89 convert! h's.comp 0 this with _ t90 simp only [add_assoc, Function.comp_apply, add_smul]9192theorem locallyIntegrable_lineDeriv (hf : LipschitzWith C f) (v : E) :93 LocallyIntegrable (fun x ↦ lineDeriv ℝ f x v) μ :=94 (hf.memLp_lineDeriv v).locallyIntegrable le_top9596/-!97### Step 2: the ae line derivative is linear9899Surprisingly, this is the hardest step. We prove it using an elegant but slightly sophisticated100argument by Morrey, with a distributional flavor: we integrate against a smooth function, and push101the derivative to the smooth function by integration by parts. As the derivative of a smooth102function is linear, this gives the result.103-/104105theorem integral_inv_smul_sub_mul_tendsto_integral_lineDeriv_mul106 (hf : LipschitzWith C f) (hg : Integrable g μ) (v : E) :107 Tendsto (fun (t : ℝ) ↦ ∫ x, (t⁻¹ • (f (x + t • v) - f x)) * g x ∂μ) (𝓝[>] 0)108 (𝓝 (∫ x, lineDeriv ℝ f x v * g x ∂μ)) := by109 apply tendsto_integral_filter_of_dominated_convergence (fun x ↦ (C * ‖v‖) * ‖g x‖)110 · filter_upwards with t111 apply AEStronglyMeasurable.mul ?_ hg.aestronglyMeasurable112 apply aestronglyMeasurable_const.smul113 apply AEStronglyMeasurable.sub _ hf.continuous.measurable.aestronglyMeasurable114 apply AEMeasurable.aestronglyMeasurable115 exact hf.continuous.measurable.comp_aemeasurable' (aemeasurable_id'.add_const _)116 · filter_upwards [self_mem_nhdsWithin] with t (ht : 0 < t)117 filter_upwards with x118 calc ‖t⁻¹ • (f (x + t • v) - f x) * g x‖119 = (t⁻¹ * ‖f (x + t • v) - f x‖) * ‖g x‖ := by simp [norm_mul, ht.le]120 _ ≤ (t⁻¹ * (C * ‖(x + t • v) - x‖)) * ‖g x‖ := by121 gcongr; exact LipschitzWith.norm_sub_le hf (x + t • v) x122 _ = (C * ‖v‖) * ‖g x‖ := by simp [field, norm_smul, abs_of_nonneg ht.le]123 · exact hg.norm.const_mul _124 · filter_upwards [hf.ae_lineDifferentiableAt v] with x hx125 exact hx.hasLineDerivAt.tendsto_slope_zero_right.mul tendsto_const_nhds126127theorem integral_inv_smul_sub_mul_tendsto_integral_lineDeriv_mul'128 (hf : LipschitzWith C f) (h'f : HasCompactSupport f) (hg : Continuous g) (v : E) :129 Tendsto (fun (t : ℝ) ↦ ∫ x, (t⁻¹ • (f (x + t • v) - f x)) * g x ∂μ) (𝓝[>] 0)130 (𝓝 (∫ x, lineDeriv ℝ f x v * g x ∂μ)) := by131 let K := cthickening (‖v‖) (tsupport f)132 have K_compact : IsCompact K := IsCompact.cthickening h'f133 apply tendsto_integral_filter_of_dominated_convergence134 (K.indicator (fun x ↦ (C * ‖v‖) * ‖g x‖))135 · filter_upwards with t136 apply AEStronglyMeasurable.mul ?_ hg.aestronglyMeasurable137 apply aestronglyMeasurable_const.smul138 apply AEStronglyMeasurable.sub _ hf.continuous.measurable.aestronglyMeasurable139 apply AEMeasurable.aestronglyMeasurable140 exact hf.continuous.measurable.comp_aemeasurable' (aemeasurable_id'.add_const _)141 · filter_upwards [Ioc_mem_nhdsGT zero_lt_one] with t ht142 have t_pos : 0 < t := ht.1143 filter_upwards with x144 by_cases hx : x ∈ K145 · calc ‖t⁻¹ • (f (x + t • v) - f x) * g x‖146 = (t⁻¹ * ‖f (x + t • v) - f x‖) * ‖g x‖ := by simp [norm_mul, t_pos.le]147 _ ≤ (t⁻¹ * (C * ‖(x + t • v) - x‖)) * ‖g x‖ := by148 gcongr; exact LipschitzWith.norm_sub_le hf (x + t • v) x149 _ = (C * ‖v‖) * ‖g x‖ := by simp [field, norm_smul, abs_of_nonneg t_pos.le]150 _ = K.indicator (fun x ↦ (C * ‖v‖) * ‖g x‖) x := by rw [indicator_of_mem hx]151 · have A : f x = 0 := by152 rw [← Function.notMem_support]153 contrapose hx154 exact self_subset_cthickening _ (subset_tsupport _ hx)155 have B : f (x + t • v) = 0 := by156 rw [← Function.notMem_support]157 contrapose hx158 apply mem_cthickening_of_dist_le _ _ (‖v‖) (tsupport f) (subset_tsupport _ hx)159 simp only [dist_eq_norm, sub_add_cancel_left, norm_neg, norm_smul, Real.norm_eq_abs,160 abs_of_nonneg t_pos.le]161 exact mul_le_of_le_one_left (norm_nonneg v) ht.2162 simp only [B, A, _root_.sub_self, smul_eq_mul, mul_zero, zero_mul, norm_zero]163 exact indicator_nonneg (fun y _hy ↦ by positivity) _164 · rw [integrable_indicator_iff K_compact.measurableSet]165 exact ContinuousOn.integrableOn_compact K_compact (by fun_prop)166 · filter_upwards [hf.ae_lineDifferentiableAt v] with x hx167 exact hx.hasLineDerivAt.tendsto_slope_zero_right.mul tendsto_const_nhds168169/-- Integration by parts formula for the line derivative of Lipschitz functions, assuming one of170them is compactly supported. -/171theorem integral_lineDeriv_mul_eq172 (hf : LipschitzWith C f) (hg : LipschitzWith D g) (h'g : HasCompactSupport g) (v : E) :173 ∫ x, lineDeriv ℝ f x v * g x ∂μ = ∫ x, lineDeriv ℝ g x (-v) * f x ∂μ := by174 /- Write down the line derivative as the limit of `(f (x + t v) - f x) / t` and175 `(g (x - t v) - g x) / t`, and therefore the integrals as limits of the corresponding integrals176 thanks to the dominated convergence theorem. At fixed positive `t`, the integrals coincide177 (with the change of variables `y = x + t v`), so the limits also coincide. -/178 have A : Tendsto (fun (t : ℝ) ↦ ∫ x, (t⁻¹ • (f (x + t • v) - f x)) * g x ∂μ) (𝓝[>] 0)179 (𝓝 (∫ x, lineDeriv ℝ f x v * g x ∂μ)) :=180 integral_inv_smul_sub_mul_tendsto_integral_lineDeriv_mul181 hf (hg.continuous.integrable_of_hasCompactSupport h'g) v182 have B : Tendsto (fun (t : ℝ) ↦ ∫ x, (t⁻¹ • (g (x + t • (-v)) - g x)) * f x ∂μ) (𝓝[>] 0)183 (𝓝 (∫ x, lineDeriv ℝ g x (-v) * f x ∂μ)) :=184 integral_inv_smul_sub_mul_tendsto_integral_lineDeriv_mul' hg h'g hf.continuous (-v)185 suffices S1 : ∀ (t : ℝ), ∫ x, (t⁻¹ • (f (x + t • v) - f x)) * g x ∂μ =186 ∫ x, (t⁻¹ • (g (x + t • (-v)) - g x)) * f x ∂μ by187 simp only [S1] at A; exact tendsto_nhds_unique A B188 intro t189 suffices S2 : ∫ x, (f (x + t • v) - f x) * g x ∂μ = ∫ x, f x * (g (x + t • (-v)) - g x) ∂μ by190 simp only [smul_eq_mul, mul_assoc, integral_const_mul, S2, mul_comm (f _)]191 have S3 : ∫ x, f (x + t • v) * g x ∂μ = ∫ x, f x * g (x + t • (-v)) ∂μ := by192 rw [← integral_add_right_eq_self _ (t • (-v))]; simp193 simp_rw [_root_.sub_mul, _root_.mul_sub]194 rw [integral_sub, integral_sub, S3]195 · apply Continuous.integrable_of_hasCompactSupport196 · exact hf.continuous.mul (hg.continuous.comp (continuous_add_const _))197 · exact (h'g.comp_homeomorph (Homeomorph.addRight (t • (-v)))).mul_left198 · exact (hf.continuous.mul hg.continuous).integrable_of_hasCompactSupport h'g.mul_left199 · apply Continuous.integrable_of_hasCompactSupport200 · exact (hf.continuous.comp (continuous_add_const _)).mul hg.continuous201 · exact h'g.mul_left202 · exact (hf.continuous.mul hg.continuous).integrable_of_hasCompactSupport h'g.mul_left203204/-- The line derivative of a Lipschitz function is almost everywhere linear with respect to fixed205coefficients. -/206theorem ae_lineDeriv_sum_eq207 (hf : LipschitzWith C f) {ι : Type*} (s : Finset ι) (a : ι → ℝ) (v : ι → E) :208 ∀ᵐ x ∂μ, lineDeriv ℝ f x (∑ i ∈ s, a i • v i) = ∑ i ∈ s, a i • lineDeriv ℝ f x (v i) := by209 /- Clever argument by Morrey: integrate against a smooth compactly supported function `g`, switch210 the derivative to `g` by integration by parts, and use the linearity of the derivative of `g` to211 conclude that the initial integrals coincide. -/212 apply ae_eq_of_integral_contDiff_smul_eq (hf.locallyIntegrable_lineDeriv _)213 (locallyIntegrable_finsetSum _ (fun i hi ↦ (hf.locallyIntegrable_lineDeriv (v i)).smul (a i)))214 (fun g g_smooth g_comp ↦ ?_)215 simp_rw [Finset.smul_sum]216 have A : ∀ i ∈ s, Integrable (fun x ↦ g x • (a i • fun x ↦ lineDeriv ℝ f x (v i)) x) μ :=217 fun i hi ↦ (g_smooth.continuous.integrable_of_hasCompactSupport g_comp).smul_of_top_left218 ((hf.memLp_lineDeriv (v i)).const_smul (a i))219 rw [integral_finsetSum _ A]220 suffices S1 : ∫ x, lineDeriv ℝ f x (∑ i ∈ s, a i • v i) * g x ∂μ221 = ∑ i ∈ s, a i * ∫ x, lineDeriv ℝ f x (v i) * g x ∂μ by222 dsimp only [smul_eq_mul, Pi.smul_apply]223 simp_rw [← mul_assoc, mul_comm _ (a _), mul_assoc, integral_const_mul, mul_comm (g _), S1]224 suffices S2 : ∫ x, (∑ i ∈ s, a i * fderiv ℝ g x (v i)) * f x ∂μ =225 ∑ i ∈ s, a i * ∫ x, fderiv ℝ g x (v i) * f x ∂μ by226 obtain ⟨D, g_lip⟩ : ∃ D, LipschitzWith D g :=227 ContDiff.lipschitzWith_of_hasCompactSupport g_comp g_smooth (by simp)228 simp_rw [integral_lineDeriv_mul_eq hf g_lip g_comp]229 simp_rw [(g_smooth.differentiable (by simp)).differentiableAt.lineDeriv_eq_fderiv]230 simp only [map_neg, _root_.map_sum, map_smul, smul_eq_mul, neg_mul]231 simp only [integral_neg, mul_neg, Finset.sum_neg_distrib, neg_inj]232 exact S2233 suffices B : ∀ i ∈ s, Integrable (fun x ↦ a i * (fderiv ℝ g x (v i) * f x)) μ by234 simp_rw [Finset.sum_mul, mul_assoc, integral_finsetSum s B, integral_const_mul]235 intro i _hi236 let L : StrongDual ℝ E → ℝ := fun f ↦ f (v i)237 change Integrable (fun x ↦ a i * ((L ∘ (fderiv ℝ g)) x * f x)) μ238 refine (Continuous.integrable_of_hasCompactSupport ?_ ?_).const_mul _239 · exact ((g_smooth.continuous_fderiv (by simp)).clm_apply continuous_const).mul240 hf.continuous241 · exact ((g_comp.fderiv ℝ).comp_left rfl).mul_right242243/-!244### Step 3: construct the derivative using the line derivatives along a basis245-/246247theorem ae_exists_fderiv_of_countable248 (hf : LipschitzWith C f) {s : Set E} (hs : s.Countable) :249 ∀ᵐ x ∂μ, ∃ (L : StrongDual ℝ E), ∀ v ∈ s, HasLineDerivAt ℝ f (L v) x v := by250 have B := Basis.ofVectorSpace ℝ E251 have I1 : ∀ᵐ (x : E) ∂μ, ∀ v ∈ s, lineDeriv ℝ f x (∑ i, (B.repr v i) • B i) =252 ∑ i, B.repr v i • lineDeriv ℝ f x (B i) :=253 (ae_ball_iff hs).2 (fun v _ ↦ hf.ae_lineDeriv_sum_eq _ _ _)254 have I2 : ∀ᵐ (x : E) ∂μ, ∀ v ∈ s, LineDifferentiableAt ℝ f x v :=255 (ae_ball_iff hs).2 (fun v _ ↦ hf.ae_lineDifferentiableAt v)256 filter_upwards [I1, I2] with x hx h'x257 let L : StrongDual ℝ E :=258 LinearMap.toContinuousLinearMap (B.constr ℝ (fun i ↦ lineDeriv ℝ f x (B i)))259 refine ⟨L, fun v hv ↦ ?_⟩260 have J : L v = lineDeriv ℝ f x v := by convert! (hx v hv).symm <;> simp [L, B.sum_repr v]261 simpa [J] using (h'x v hv).hasLineDerivAt262263omit [MeasurableSpace E] in264/-- If a Lipschitz functions has line derivatives in a dense set of directions, all of them given by265a single continuous linear map `L`, then it admits `L` as Fréchet derivative. -/266theorem hasFDerivAt_of_hasLineDerivAt_of_closure267 {f : E → F} (hf : LipschitzWith C f) {s : Set E} (hs : sphere 0 1 ⊆ closure s)268 {L : E →L[ℝ] F} {x : E} (hL : ∀ v ∈ s, HasLineDerivAt ℝ f (L v) x v) :269 HasFDerivAt f L x := by270 rw [hasFDerivAt_iff_isLittleO_nhds_zero, isLittleO_iff]271 intro ε εpos272 obtain ⟨δ, δpos, hδ⟩ : ∃ δ, 0 < δ ∧ (C + ‖L‖ + 1) * δ = ε :=273 ⟨ε / (C + ‖L‖ + 1), by positivity, mul_div_cancel₀ ε (by positivity)⟩274 obtain ⟨q, hqs, q_fin, hq⟩ : ∃ q, q ⊆ s ∧ q.Finite ∧ sphere 0 1 ⊆ ⋃ y ∈ q, ball y δ := by275 have : sphere 0 1 ⊆ ⋃ y ∈ s, ball y δ := by276 apply hs.trans (fun z hz ↦ ?_)277 obtain ⟨y, ys, hy⟩ : ∃ y ∈ s, dist z y < δ := Metric.mem_closure_iff.1 hz δ δpos278 exact mem_biUnion ys hy279 exact (isCompact_sphere 0 1).elim_finite_subcover_image (fun y _hy ↦ isOpen_ball) this280 have I : ∀ᶠ t in 𝓝 (0 : ℝ), ∀ v ∈ q, ‖f (x + t • v) - f x - t • L v‖ ≤ δ * ‖t‖ := by281 apply (Finite.eventually_all q_fin).2 (fun v hv ↦ ?_)282 apply Asymptotics.IsLittleO.def ?_ δpos283 exact hasLineDerivAt_iff_isLittleO_nhds_zero.1 (hL v (hqs hv))284 obtain ⟨r, r_pos, hr⟩ : ∃ (r : ℝ), 0 < r ∧ ∀ (t : ℝ), ‖t‖ < r →285 ∀ v ∈ q, ‖f (x + t • v) - f x - t • L v‖ ≤ δ * ‖t‖ := by286 rcases Metric.mem_nhds_iff.1 I with ⟨r, r_pos, hr⟩287 exact ⟨r, r_pos, fun t ht v hv ↦ hr (mem_ball_zero_iff.2 ht) v hv⟩288 apply Metric.mem_nhds_iff.2 ⟨r, r_pos, fun v hv ↦ ?_⟩289 rcases eq_or_ne v 0 with rfl | v_ne290 · simp291 obtain ⟨w, ρ, w_mem, hvw, hρ⟩ : ∃ w ρ, w ∈ sphere 0 1 ∧ v = ρ • w ∧ ρ = ‖v‖ := by292 refine ⟨‖v‖⁻¹ • v, ‖v‖, by simp [norm_smul, inv_mul_cancel₀ (norm_ne_zero_iff.2 v_ne)], ?_, rfl⟩293 simp [smul_smul, mul_inv_cancel₀ (norm_ne_zero_iff.2 v_ne)]294 have norm_rho : ‖ρ‖ = ρ := by rw [hρ, norm_norm]295 have rho_pos : 0 ≤ ρ := by simp [hρ]296 obtain ⟨y, yq, hy⟩ : ∃ y ∈ q, ‖w - y‖ < δ := by simpa [← dist_eq_norm] using hq w_mem297 have : ‖y - w‖ < δ := by rwa [norm_sub_rev]298 calc ‖f (x + v) - f x - L v‖299 = ‖f (x + ρ • w) - f x - ρ • L w‖ := by simp [hvw]300 _ = ‖(f (x + ρ • w) - f (x + ρ • y)) + (ρ • L y - ρ • L w)301 + (f (x + ρ • y) - f x - ρ • L y)‖ := by congr; abel302 _ ≤ ‖f (x + ρ • w) - f (x + ρ • y)‖ + ‖ρ • L y - ρ • L w‖303 + ‖f (x + ρ • y) - f x - ρ • L y‖ := norm_add₃_le304 _ ≤ C * ‖(x + ρ • w) - (x + ρ • y)‖ + ρ * (‖L‖ * ‖y - w‖) + δ * ρ := by305 gcongr306 · exact hf.norm_sub_le _ _307 · rw [← smul_sub, norm_smul, norm_rho]308 gcongr309 exact L.lipschitz.norm_sub_le _ _310 · conv_rhs => rw [← norm_rho]311 apply hr _ _ _ yq312 simpa [norm_rho, hρ] using hv313 _ ≤ C * (ρ * δ) + ρ * (‖L‖ * δ) + δ * ρ := by314 simp only [add_sub_add_left_eq_sub, ← smul_sub, norm_smul, norm_rho]; gcongr315 _ = ((C + ‖L‖ + 1) * δ) * ρ := by ring316 _ = ε * ‖v‖ := by rw [hδ, hρ]317318/-- A real-valued function on a finite-dimensional space which is Lipschitz is319differentiable almost everywhere. Superseded by320`LipschitzWith.ae_differentiableAt` which works for functions taking value in any321finite-dimensional space. -/322theorem ae_differentiableAt_of_real (hf : LipschitzWith C f) :323 ∀ᵐ x ∂μ, DifferentiableAt ℝ f x := by324 obtain ⟨s, s_count, s_dense⟩ : ∃ (s : Set E), s.Countable ∧ Dense s :=325 TopologicalSpace.exists_countable_dense E326 have hs : sphere 0 1 ⊆ closure s := by rw [s_dense.closure_eq]; exact subset_univ _327 filter_upwards [hf.ae_exists_fderiv_of_countable s_count]328 rintro x ⟨L, hL⟩329 exact (hf.hasFDerivAt_of_hasLineDerivAt_of_closure hs hL).differentiableAt330331end LipschitzWith332333variable [FiniteDimensional ℝ E] [FiniteDimensional ℝ F] [IsAddHaarMeasure μ]334335namespace LipschitzOnWith336337/-- A real-valued function on a finite-dimensional space which is Lipschitz on a set is338differentiable almost everywhere in this set. Superseded by339`LipschitzOnWith.ae_differentiableWithinAt_of_mem` which works for functions taking value in any340finite-dimensional space. -/341theorem ae_differentiableWithinAt_of_mem_of_real (hf : LipschitzOnWith C f s) :342 ∀ᵐ x ∂μ, x ∈ s → DifferentiableWithinAt ℝ f s x := by343 obtain ⟨g, g_lip, hg⟩ : ∃ (g : E → ℝ), LipschitzWith C g ∧ EqOn f g s := hf.extend_real344 filter_upwards [g_lip.ae_differentiableAt_of_real] with x hx xs345 exact hx.differentiableWithinAt.congr hg (hg xs)346347/-- A function on a finite-dimensional space which is Lipschitz on a set and taking values in a348product space is differentiable almost everywhere in this set. Superseded by349`LipschitzOnWith.ae_differentiableWithinAt_of_mem` which works for functions taking value in any350finite-dimensional space. -/351theorem ae_differentiableWithinAt_of_mem_pi352 {ι : Type*} [Fintype ι] {f : E → ι → ℝ} {s : Set E}353 (hf : LipschitzOnWith C f s) : ∀ᵐ x ∂μ, x ∈ s → DifferentiableWithinAt ℝ f s x := by354 have A : ∀ i : ι, LipschitzWith 1 (fun x : ι → ℝ ↦ x i) := fun i => LipschitzWith.eval i355 have : ∀ i : ι, ∀ᵐ x ∂μ, x ∈ s → DifferentiableWithinAt ℝ (fun x : E ↦ f x i) s x := fun i ↦ by356 apply ae_differentiableWithinAt_of_mem_of_real357 exact LipschitzWith.comp_lipschitzOnWith (A i) hf358 filter_upwards [ae_all_iff.2 this] with x hx xs359 exact differentiableWithinAt_pi.2 (fun i ↦ hx i xs)360361/-- *Rademacher's theorem*: a function between finite-dimensional real vector spaces which is362Lipschitz on a set is differentiable almost everywhere in this set. -/363theorem ae_differentiableWithinAt_of_mem {f : E → F} (hf : LipschitzOnWith C f s) :364 ∀ᵐ x ∂μ, x ∈ s → DifferentiableWithinAt ℝ f s x := by365 have A := (Basis.ofVectorSpace ℝ F).equivFun.toContinuousLinearEquiv366 suffices H : ∀ᵐ x ∂μ, x ∈ s → DifferentiableWithinAt ℝ (A ∘ f) s x by367 filter_upwards [H] with x hx xs368 have : f = (A.symm ∘ A) ∘ f := by369 simp only [ContinuousLinearEquiv.symm_comp_self, Function.id_comp]370 rw [this]371 exact A.symm.differentiableAt.comp_differentiableWithinAt x (hx xs)372 apply ae_differentiableWithinAt_of_mem_pi373 exact A.lipschitz.comp_lipschitzOnWith hf374375/-- *Rademacher's theorem*: a function between finite-dimensional real vector spaces which is376Lipschitz on a set is differentiable almost everywhere in this set. -/377theorem ae_differentiableWithinAt {f : E → F} (hf : LipschitzOnWith C f s)378 (hs : MeasurableSet s) :379 ∀ᵐ x ∂(μ.restrict s), DifferentiableWithinAt ℝ f s x := by380 rw [ae_restrict_iff' hs]381 exact hf.ae_differentiableWithinAt_of_mem382383end LipschitzOnWith384385/-- *Rademacher's theorem*: a Lipschitz function between finite-dimensional real vector spaces is386differentiable almost everywhere. -/387theorem LipschitzWith.ae_differentiableAt {f : E → F} (h : LipschitzWith C f) :388 ∀ᵐ x ∂μ, DifferentiableAt ℝ f x := by389 rw [← lipschitzOnWith_univ] at h390 simpa [differentiableWithinAt_univ] using h.ae_differentiableWithinAt_of_mem391392/-- In a real finite-dimensional normed vector space,393 the norm is almost everywhere differentiable. -/394theorem ae_differentiableAt_norm :395 ∀ᵐ x ∂μ, DifferentiableAt ℝ (‖·‖) x := lipschitzWith_one_norm.ae_differentiableAt396397omit [MeasurableSpace E] in398/-- In a real finite-dimensional normed vector space,399 the set of points where the norm is differentiable at is dense. -/400theorem dense_differentiableAt_norm :401 Dense {x : E | DifferentiableAt ℝ (‖·‖) x} :=402 let _ : MeasurableSpace E := borel E403 have _ : BorelSpace E := ⟨rfl⟩404 let w := Basis.ofVectorSpace ℝ E405 MeasureTheory.Measure.dense_of_ae (ae_differentiableAt_norm (μ := w.addHaar))