Exact source: MathlibAnnex/Analysis/Calculus/Mollification.lean
Pinned GitHub source · Raw UTF-8 source
Back to Strong local convergence of mollified derivatives · Back to Maximal-minor integral differences for Lipschitz perturbations
1import Mathlib.Analysis.Calculus.BumpFunction.Convolution2import Mathlib.Analysis.Calculus.Rademacher3import Mathlib.Analysis.Calculus.ParametricIntegral4import Mathlib.MeasureTheory.Function.LpSpace.Basic5import Mathlib.MeasureTheory.SpecificCodomains.Pi6import Mathlib.Tactic78/-!9# Strong local convergence of mollified derivatives1011Derivatives of a globally Lipschitz map converge in the original dimension12exponent on compact sets. The conclusion records both seminorm convergence13and eventual membership in the corresponding Lp space.14-/1516noncomputable section17open Set MeasureTheory Filter18open scoped Convolution Topology ENNReal NNReal Pointwise19namespace MathlibAnnex20namespace Mollification2122noncomputable def standardMollifier {n : ℕ} (ε : ℝ) : (Fin n → ℝ) → ℝ :=23 let φ : ContDiffBump (0 : (Fin n → ℝ)) :=24 if hε : 0 < ε then25 { rIn := ε / 226 rOut := ε27 rIn_pos := by positivity28 rIn_lt_rOut := by nlinarith }29 else30 { rIn := (1 : ℝ) / 231 rOut := 132 rIn_pos := by norm_num33 rIn_lt_rOut := by norm_num }34 φ.normed volume3536noncomputable def mollify {n N : ℕ} (ε : ℝ)37 (f : (Fin n → ℝ) → (Fin N → ℝ)) : (Fin n → ℝ) → (Fin N → ℝ) :=38 standardMollifier ε ⋆[ContinuousLinearMap.lsmul ℝ ℝ, volume] f39open scoped Pointwise4041theorem hasCompactSupport_standardMollifier {n : ℕ} (ε : ℝ) :42 HasCompactSupport (standardMollifier (n := n) ε) := by43 unfold standardMollifier44 split_ifs <;> exact ContDiffBump.hasCompactSupport_normed _4546theorem continuous_standardMollifier {n : ℕ} (ε : ℝ) :47 Continuous (standardMollifier (n := n) ε) := by48 unfold standardMollifier49 split_ifs <;>50 exact (ContDiffBump.contDiff_normed (n := (⊤ : ℕ∞)) _).continuous5152theorem mollify_add {n N : ℕ} (ε : ℝ)53 (f g : (Fin n → ℝ) → (Fin N → ℝ))54 (hf : LocallyIntegrable f volume) (hg : LocallyIntegrable g volume) :55 mollify ε (fun x => f x + g x) =56 fun x => mollify ε f x + mollify ε g x := by5758 funext x59 have hcf := hasCompactSupport_standardMollifier (n := n) ε60 have hcont := continuous_standardMollifier (n := n) ε61 have hif := hcf.convolutionExists_left62 (ContinuousLinearMap.lsmul ℝ ℝ) hcont hf63 have hig := hcf.convolutionExists_left64 (ContinuousLinearMap.lsmul ℝ ℝ) hcont hg65 simp only [mollify, MeasureTheory.convolution_def, ContinuousLinearMap.lsmul_apply,66 smul_add]67 exact MeasureTheory.integral_add (hif x).integrable (hig x).integrable6869theorem contDiff_mollify {n N : ℕ} {ε : ℝ} (hε : 0 < ε)70 {f : (Fin n → ℝ) → (Fin N → ℝ)} (hf : LocallyIntegrable f volume) :71 ContDiff ℝ (↑(⊤ : ℕ∞)) (mollify ε f) := by7273 let φ : ContDiffBump (0 : (Fin n → ℝ)) :=74 { rIn := ε / 275 rOut := ε76 rIn_pos := by positivity77 rIn_lt_rOut := by nlinarith }78 have hstd : standardMollifier (n := n) ε = φ.normed volume := by79 simp [standardMollifier, φ, hε]80 rw [mollify, hstd]81 exact (φ.hasCompactSupport_normed (μ := volume)).contDiff_convolution_left82 (ContinuousLinearMap.lsmul ℝ ℝ)83 (φ.contDiff_normed (n := (⊤ : ℕ∞))) hf8485theorem eventually_tsupport_mollify_subset_compact86 {n N : ℕ} {u : (Fin n → ℝ) → (Fin N → ℝ)} (hu : HasCompactSupport u) :87 ∃ K : Set ((Fin n → ℝ)), IsCompact K ∧ tsupport u ⊆ K ∧88 ∀ᶠ ε in 𝓝[>] (0 : ℝ), tsupport (mollify ε u) ⊆ K := by8990 rcases (Metric.isBounded_iff_subset_closedBall (0 : (Fin n → ℝ))).mp91 hu.isCompact.isBounded with ⟨R, hR⟩92 let K : Set ((Fin n → ℝ)) := Metric.closedBall 0 (R + 1)93 refine ⟨K, ProperSpace.isCompact_closedBall _ _, ?_, ?_⟩94 · intro x hx95 exact Metric.mem_closedBall'.296 (le_trans (Metric.mem_closedBall'.1 (hR hx)) (by linarith))97 · have hone : ∀ᶠ ε : ℝ in 𝓝[>] (0 : ℝ), ε < 1 :=98 Filter.Eventually.filter_mono inf_le_left99 (isOpen_Iio.mem_nhds (by norm_num))100 filter_upwards [self_mem_nhdsWithin, hone] with ε hε hε1101 have hεpos : 0 < ε := hε102 let φ : ContDiffBump (0 : (Fin n → ℝ)) :=103 { rIn := ε / 2104 rOut := ε105 rIn_pos := by positivity106 rIn_lt_rOut := by nlinarith }107 have hstd : standardMollifier (n := n) ε = φ.normed volume := by108 simp [standardMollifier, φ, hεpos]109 unfold tsupport110 apply closure_minimal111 · intro x hx112 rcases (MeasureTheory.support_convolution_subset113 (ContinuousLinearMap.lsmul ℝ ℝ) hx) with ⟨a, ha, b, hb, rfl⟩114 rw [hstd, φ.support_normed_eq] at ha115 have ha' : ‖a‖ < ε := by116 simpa only [Metric.mem_ball, dist_zero_right] using ha117 have hb' : ‖b‖ ≤ R := by118 simpa only [Metric.mem_closedBall, dist_zero_right] using119 hR (subset_closure hb)120 change a + b ∈ Metric.closedBall (0 : (Fin n → ℝ)) (R + 1)121 rw [Metric.mem_closedBall, dist_zero_right]122 exact le_trans (norm_add_le a b) (by linarith)123 · exact Metric.isClosed_closedBall124125theorem eventually_mollify_fderiv_memLpOn_compact126 {m N : ℕ} {f : (Fin (m + 1) → ℝ) → (Fin N → ℝ)} {C : ℝ≥0} (hf : LipschitzWith C f)127 {K : Set ((Fin (m + 1) → ℝ))} (hK : IsCompact K) :128 ∀ᶠ ε in 𝓝[>] (0 : ℝ),129 MemLp (fun x => fderiv ℝ (mollify ε f) x)130 (m + 1) (volume.restrict K) := by131132 filter_upwards [self_mem_nhdsWithin] with ε hε133 have hεpos : 0 < ε := hε134 have hLip := hf135 have hsmooth := contDiff_mollify hεpos hLip.continuous.locallyIntegrable136 have hDcont : Continuous (fun x => fderiv ℝ (mollify ε f) x) :=137 hsmooth.continuous_fderiv (by simp)138 have hnormcont : Continuous (fun x => ‖fderiv ℝ (mollify ε f) x‖) :=139 continuous_norm.comp hDcont140 have hbdd : BddAbove ((fun x => ‖fderiv ℝ (mollify ε f) x‖) '' K) :=141 (hK.image hnormcont).isBounded.bddAbove142 rcases hbdd with ⟨B, hB⟩143 letI : IsFiniteMeasure (volume.restrict K) :=144 ⟨by simpa using hK.measure_lt_top⟩145 apply MemLp.of_bound hDcont.stronglyMeasurable.aestronglyMeasurable B146 filter_upwards [ae_restrict_mem hK.measurableSet] with x hx147 exact hB ⟨x, hx, rfl⟩148149theorem tendsto_eLpNorm_fderiv_mollify_sub150 {m N : ℕ} {f : (Fin (m + 1) → ℝ) → (Fin N → ℝ)} {C : ℝ≥0} (hf : LipschitzWith C f)151 {K : Set ((Fin (m + 1) → ℝ))} (hK : IsCompact K) :152 (Tendsto (fun ε => eLpNorm153 (fun x => fderiv ℝ (mollify ε f) x - fderiv ℝ f x)154 ((m + 1 : ℕ) : ℝ≥0∞) (volume.restrict K)) (𝓝[>] (0 : ℝ)) (𝓝 0)) ∧155 ∀ᶠ ε in 𝓝[>] (0 : ℝ), MemLp156 (fun x => fderiv ℝ (mollify ε f) x) ((m + 1 : ℕ) : ℝ≥0∞) (volume.restrict K) := by157 constructor158 · classical159 have hLip := hf160 have hdiff : ∀ᵐ z ∂volume, DifferentiableAt ℝ f z :=161 hLip.ae_differentiableAt162 have hderiv (ε : ℝ) (hε : 0 < ε) (x₀ : (Fin (m + 1) → ℝ)) :163 fderiv ℝ (mollify ε f) x₀ =164 ∫ y : (Fin (m + 1) → ℝ),165 standardMollifier ε y • fderiv ℝ f (x₀ - y) := by166 let φ : ContDiffBump (0 : (Fin (m + 1) → ℝ)) :=167 { rIn := ε / 2168 rOut := ε169 rIn_pos := by positivity170 rIn_lt_rOut := by nlinarith }171 have hstd : standardMollifier (n := m + 1) ε = φ.normed volume := by172 simp [standardMollifier, φ, hε]173 have hk : Integrable (standardMollifier (n := m + 1) ε) volume := by174 rw [hstd]175 exact φ.integrable_normed176 have hkc : HasCompactSupport177 (standardMollifier (n := m + 1) ε) := by178 rw [hstd]179 exact φ.hasCompactSupport_normed180 have hkcont : Continuous181 (standardMollifier (n := m + 1) ε) := by182 rw [hstd]183 exact (φ.contDiff_normed (μ := volume) (n := (1 : ℕ∞))).continuous184 have hconv : ∀ x : (Fin (m + 1) → ℝ), Integrable185 (fun y : (Fin (m + 1) → ℝ) =>186 standardMollifier ε y • f (x - y)) volume := by187 intro x188 exact (hkc.convolutionExists_left189 (ContinuousLinearMap.lsmul ℝ ℝ) hkcont190 hLip.continuous.locallyIntegrable) x191 have hdiffx : ∀ᵐ y ∂volume, DifferentiableAt ℝ f (x₀ - y) :=192 (MeasureTheory.Measure.measurePreserving_sub_left volume x₀).quasiMeasurePreserving.ae193 hdiff194 have hparam := hasFDerivAt_integral_of_dominated_loc_of_lip'195 (μ := volume)196 (F := fun x y : (Fin (m + 1) → ℝ) =>197 standardMollifier ε y • f (x - y))198 (F' := fun y : (Fin (m + 1) → ℝ) =>199 standardMollifier ε y • fderiv ℝ f (x₀ - y))200 (bound := fun y : (Fin (m + 1) → ℝ) =>201 ‖standardMollifier ε y‖ * (C : ℝ))202 (s := Set.univ) (x₀ := x₀)203 (show Set.univ ∈ nhds x₀ from univ_mem)204 (by intro x hx; exact (hconv x).aestronglyMeasurable)205 (hconv x₀)206 (by207 have hmfd : AEStronglyMeasurable208 (fun y : (Fin (m + 1) → ℝ) => fderiv ℝ f (x₀ - y)) volume := by209 exact (((measurable_fderiv ℝ f).comp210 (measurable_const.sub measurable_id)).stronglyMeasurable).aestronglyMeasurable211 exact hk.aestronglyMeasurable.smul hmfd)212 (by213 filter_upwards with y214 intro x hx215 rw [← smul_sub, norm_smul]216 have hb : ‖f (x - y) - f (x₀ - y)‖ ≤217 (C : ℝ) * ‖(x - y) - (x₀ - y)‖ := by218 simpa only [dist_eq_norm] using219 hLip.dist_le_mul (x - y) (x₀ - y)220 calc221 ‖standardMollifier ε y‖ * ‖f (x - y) - f (x₀ - y)‖ ≤222 ‖standardMollifier ε y‖ *223 ((C : ℝ) * ‖x - x₀‖) := by224 gcongr225 simpa only [show (x - y) - (x₀ - y) = x - x₀ by module] using hb226 _ = (‖standardMollifier ε y‖ * (C : ℝ)) *227 ‖x - x₀‖ := by ring)228 (hk.norm.mul_const (C : ℝ))229 (by230 filter_upwards [hdiffx] with y hy231 have hsub : HasFDerivAt (fun x : (Fin (m + 1) → ℝ) => x - y)232 (ContinuousLinearMap.id ℝ ((Fin (m + 1) → ℝ))) x₀ := by233 exact (hasFDerivAt_id (𝕜 := ℝ) x₀).sub_const y234 have hc := hy.hasFDerivAt.comp x₀ hsub235 have hc' : HasFDerivAt (fun x : (Fin (m + 1) → ℝ) => f (x - y))236 (fderiv ℝ f (x₀ - y)) x₀ := by237 change HasFDerivAt (f ∘ fun x : (Fin (m + 1) → ℝ) => x - y)238 (fderiv ℝ f (x₀ - y)) x₀239 simpa only [ContinuousLinearMap.comp_id] using hc240 exact hc'.const_smul (standardMollifier ε y))241 have hd := hparam.2.fderiv242 change fderiv ℝ (fun x : (Fin (m + 1) → ℝ) =>243 ∫ y : (Fin (m + 1) → ℝ), standardMollifier ε y • f (x - y)) x₀ = _244 exact hd245 obtain ⟨R, hKR⟩ := hK.isBounded.subset_closedBall246 (0 : (Fin (m + 1) → ℝ))247 let S : Set ((Fin (m + 1) → ℝ)) :=248 Metric.closedBall 0 (max R 0 + 1)249 have hKS : K ⊆ S := by250 intro x hx251 have hxR : ‖x‖ ≤ R := by252 simpa only [Metric.mem_closedBall, dist_zero_right] using hKR hx253 have hxS : ‖x‖ ≤ max R 0 + 1 :=254 hxR.trans (le_trans (le_max_left _ _) (le_add_of_nonneg_right zero_le_one))255 simpa only [S, Metric.mem_closedBall, dist_zero_right] using hxS256 have hScompact : IsCompact S := by257 exact isCompact_closedBall (0 : (Fin (m + 1) → ℝ)) (max R 0 + 1)258 have hSmeas : MeasurableSet S := hScompact.measurableSet259 have hSfin : volume S < ∞ := hScompact.measure_lt_top260 let entry (i : Fin (m + 1)) (j : Fin N) :261 ((Fin (m + 1) → ℝ) →L[ℝ] (Fin N → ℝ)) →L[ℝ] ℝ :=262 (ContinuousLinearMap.proj j).comp263 (ContinuousLinearMap.apply ℝ ((Fin N → ℝ)) (Pi.single i 1))264 let q (i : Fin (m + 1)) (j : Fin N) : (Fin (m + 1) → ℝ) → ℝ :=265 S.indicator (fun x => entry i j (fderiv ℝ f x))266 have hentry_meas (i : Fin (m + 1)) (j : Fin N) :267 StronglyMeasurable (fun x : (Fin (m + 1) → ℝ) =>268 entry i j (fderiv ℝ f x)) := by269 exact ((entry i j).continuous.measurable.comp270 (measurable_fderiv ℝ f)).stronglyMeasurable271 have hq (i : Fin (m + 1)) (j : Fin N) :272 MemLp (q i j) ((m + 1 : ℕ) : ℝ≥0∞) volume := by273 letI : IsFiniteMeasure (volume.restrict S) :=274 ⟨by simpa using hSfin⟩275 have hlocal : MemLp (fun x : (Fin (m + 1) → ℝ) =>276 entry i j (fderiv ℝ f x)) ((m + 1 : ℕ) : ℝ≥0∞)277 (volume.restrict S) := by278 apply MemLp.of_bound (hentry_meas i j).aestronglyMeasurable279 (‖entry i j‖ * (C : ℝ))280 filter_upwards with x281 calc282 ‖entry i j (fderiv ℝ f x)‖ ≤283 ‖entry i j‖ * ‖fderiv ℝ f x‖ :=284 (entry i j).le_opNorm _285 _ ≤ ‖entry i j‖ * (C : ℝ) := by286 exact mul_le_mul_of_nonneg_left287 (norm_fderiv_le_of_lipschitz ℝ hLip) (norm_nonneg (entry i j))288 constructor289 · exact ((hentry_meas i j).indicator hSmeas).aestronglyMeasurable290 · change eLpNorm291 (S.indicator (fun x => entry i j (fderiv ℝ f x)))292 ((m + 1 : ℕ) : ℝ≥0∞) volume < ∞293 rw [MeasureTheory.eLpNorm_indicator_eq_eLpNorm_restrict hSmeas]294 exact hlocal.eLpNorm_lt_top295 letI : Fact (1 ≤ ((m + 1 : ℕ) : ℝ≥0∞)) :=296 ⟨by exact_mod_cast Nat.succ_le_succ (Nat.zero_le m)⟩297 letI : Fact (((m + 1 : ℕ) : ℝ≥0∞) ≠ ∞) := ⟨by simp⟩298 have hcoord_full (i : Fin (m + 1)) (j : Fin N) :299 Tendsto300 (fun ε => eLpNorm301 (fun x =>302 ((standardMollifier ε) ⋆[303 ContinuousLinearMap.lsmul ℝ ℝ, volume] (q i j)) x - q i j x)304 ((m + 1 : ℕ) : ℝ≥0∞) volume)305 (nhdsWithin (0 : ℝ) (Set.Ioi 0)) (nhds 0) := by306 let p : ℝ≥0∞ := ((m + 1 : ℕ) : ℝ≥0∞)307 let B : ℝ := ‖entry i j‖ * (C : ℝ)308 have hB : 0 ≤ B :=309 mul_nonneg (norm_nonneg (entry i j)) C.coe_nonneg310 have hq_bound (x : (Fin (m + 1) → ℝ)) : ‖q i j x‖ ≤ B := by311 by_cases hx : x ∈ S312 · simp only [q, Set.indicator_of_mem hx]313 calc314 ‖entry i j (fderiv ℝ f x)‖ ≤315 ‖entry i j‖ * ‖fderiv ℝ f x‖ := (entry i j).le_opNorm _316 _ ≤ B := by317 exact mul_le_mul_of_nonneg_left318 (norm_fderiv_le_of_lipschitz ℝ hLip)319 (norm_nonneg (entry i j))320 · simp only [q]321 simp [hx]322 exact hB323 have hqsupp : Function.support (q i j) ⊆ S := by324 intro x hx325 by_contra hxS326 simp [q, hxS] at hx327 let T : Set ((Fin (m + 1) → ℝ)) := Metric.closedBall 0 (max R 0 + 2)328 have hTcompact : IsCompact T :=329 ProperSpace.isCompact_closedBall _ _330 have hTmeas : MeasurableSet T := hTcompact.measurableSet331 have hTfin : volume T < ∞ := hTcompact.measure_lt_top332 let φ (ε : ℝ) : ContDiffBump (0 : (Fin (m + 1) → ℝ)) :=333 if hε : 0 < ε then334 { rIn := ε / 2335 rOut := ε336 rIn_pos := by positivity337 rIn_lt_rOut := by nlinarith }338 else339 { rIn := (1 : ℝ) / 2340 rOut := 1341 rIn_pos := by norm_num342 rIn_lt_rOut := by norm_num }343 have hstd (ε : ℝ) (hε : 0 < ε) :344 standardMollifier (n := m + 1) ε = (φ ε).normed volume := by345 simp [standardMollifier, φ, hε]346 have hrout : Tendsto (fun ε => (φ ε).rOut)347 (nhdsWithin (0 : ℝ) (Set.Ioi 0)) (nhds 0) := by348 have heq : (fun ε => (φ ε).rOut) =ᶠ[349 nhdsWithin (0 : ℝ) (Set.Ioi 0)] (fun ε => ε) := by350 filter_upwards [self_mem_nhdsWithin] with ε hε351 have hε' : 0 < ε := hε352 simp [φ, hε']353 exact (tendsto_id.mono_left inf_le_left).congr' heq.symm354 have hratio : ∀ᶠ ε in nhdsWithin (0 : ℝ) (Set.Ioi 0),355 (φ ε).rOut ≤ 2 * (φ ε).rIn := by356 filter_upwards [self_mem_nhdsWithin] with ε hε357 have hε' : 0 < ε := hε358 simp [φ, hε']359 linarith360 have hqLI : LocallyIntegrable (q i j) volume :=361 (hq i j).locallyIntegrable Fact.out362 have haeφ : ∀ᵐ x ∂volume,363 Tendsto364 (fun ε => ((φ ε).normed volume) ⋆[365 ContinuousLinearMap.lsmul ℝ ℝ, volume] (q i j) $ x)366 (nhdsWithin (0 : ℝ) (Set.Ioi 0)) (nhds (q i j x)) :=367 ContDiffBump.ae_convolution_tendsto_right_of_locallyIntegrable368 hrout hratio hqLI369 have hae : ∀ᵐ x ∂volume,370 Tendsto371 (fun ε => ((standardMollifier ε) ⋆[372 ContinuousLinearMap.lsmul ℝ ℝ, volume] (q i j)) x)373 (nhdsWithin (0 : ℝ) (Set.Ioi 0)) (nhds (q i j x)) := by374 filter_upwards [haeφ] with x hx375 apply hx.congr'376 filter_upwards [self_mem_nhdsWithin] with ε hε377 rw [hstd ε hε]378 have hST : S ⊆ T := by379 intro x hx380 have hx' : ‖x‖ ≤ max R 0 + 1 := by381 simpa only [S, Metric.mem_closedBall, dist_zero_right] using hx382 simpa only [T, Metric.mem_closedBall, dist_zero_right] using383 (hx'.trans (by linarith))384 have hconv_cont (ε : ℝ) (hε : 0 < ε) : Continuous385 (((standardMollifier ε) ⋆[386 ContinuousLinearMap.lsmul ℝ ℝ, volume] (q i j))) := by387 rw [hstd ε hε]388 exact ((φ ε).hasCompactSupport_normed (μ := volume)).contDiff_convolution_left389 (ContinuousLinearMap.lsmul ℝ ℝ)390 ((φ ε).contDiff_normed (n := (⊤ : ℕ∞))) hqLI |>.continuous391 have hdist (ε : ℝ) (hε : 0 < ε) (x : (Fin (m + 1) → ℝ)) :392 ‖((standardMollifier ε) ⋆[393 ContinuousLinearMap.lsmul ℝ ℝ, volume] (q i j)) x - q i j x‖ ≤394 2 * B := by395 rw [hstd ε hε, ← dist_eq_norm]396 apply ContDiffBump.dist_normed_convolution_le (hq i j).1397 intro y hy398 rw [Real.dist_eq]399 calc400 |q i j y - q i j x| ≤ ‖q i j y‖ + ‖q i j x‖ :=401 abs_sub _ _402 _ ≤ B + B := add_le_add (hq_bound y) (hq_bound x)403 _ = 2 * B := by ring404 have hconv_supp (ε : ℝ) (hε : 0 < ε) (hε1 : ε < 1) :405 Function.support (((standardMollifier ε) ⋆[406 ContinuousLinearMap.lsmul ℝ ℝ, volume] (q i j))) ⊆ T := by407 intro x hx408 rcases (MeasureTheory.support_convolution_subset409 (ContinuousLinearMap.lsmul ℝ ℝ) hx) with ⟨a, ha, b, hb, rfl⟩410 rw [hstd ε hε, (φ ε).support_normed_eq] at ha411 have ha' : ‖a‖ < ε := by412 have hr : (φ ε).rOut = ε := by simp [φ, hε]413 simpa only [Metric.mem_ball, dist_zero_right, hr] using ha414 have hbS := hqsupp hb415 have hb' : ‖b‖ ≤ max R 0 + 1 := by416 simpa only [S, Metric.mem_closedBall, dist_zero_right] using hbS417 change a + b ∈ T418 simp only [T, Metric.mem_closedBall, dist_zero_right]419 exact le_trans (norm_add_le a b) (by linarith)420 have hzero_out (ε : ℝ) (hε : 0 < ε) (hε1 : ε < 1)421 {x : (Fin (m + 1) → ℝ)} (hx : x ∉ T) :422 ((standardMollifier ε) ⋆[423 ContinuousLinearMap.lsmul ℝ ℝ, volume] (q i j)) x - q i j x = 0 := by424 have hc : ((standardMollifier ε) ⋆[425 ContinuousLinearMap.lsmul ℝ ℝ, volume] (q i j)) x = 0 := by426 by_contra hc427 exact hx (hconv_supp ε hε hε1 hc)428 have hqx : q i j x = 0 := by429 by_contra hqx430 exact hx (hST (hqsupp hqx))431 rw [hc, hqx, sub_zero]432 have hconv_mem (ε : ℝ) (hε : 0 < ε) (hε1 : ε < 1) :433 MemLp (((standardMollifier ε) ⋆[434 ContinuousLinearMap.lsmul ℝ ℝ, volume] (q i j))) p volume := by435 letI : IsFiniteMeasure (volume.restrict T) :=436 ⟨by simpa using hTfin⟩437 have hlocal : MemLp (((standardMollifier ε) ⋆[438 ContinuousLinearMap.lsmul ℝ ℝ, volume] (q i j))) p439 (volume.restrict T) := by440 apply MemLp.of_bound (hconv_cont ε hε).stronglyMeasurable.aestronglyMeasurable441 (3 * B)442 filter_upwards with x443 have hd := hdist ε hε x444 have htri :445 ‖((standardMollifier ε) ⋆[446 ContinuousLinearMap.lsmul ℝ ℝ, volume] (q i j)) x‖ ≤447 ‖((standardMollifier ε) ⋆[448 ContinuousLinearMap.lsmul ℝ ℝ, volume] (q i j)) x - q i j x‖ +449 ‖q i j x‖ := by450 simpa only [sub_add_cancel] using451 norm_add_le452 (((standardMollifier ε) ⋆[453 ContinuousLinearMap.lsmul ℝ ℝ, volume] (q i j)) x - q i j x)454 (q i j x)455 exact htri.trans (by linarith [hq_bound x])456 have hind : T.indicator (((standardMollifier ε) ⋆[457 ContinuousLinearMap.lsmul ℝ ℝ, volume] (q i j))) =458 (((standardMollifier ε) ⋆[459 ContinuousLinearMap.lsmul ℝ ℝ, volume] (q i j))) := by460 funext x461 by_cases hx : x ∈ T462 · simp [hx]463 · simp only [Set.indicator]464 simp [hx]465 by_contra hc466 exact hx (hconv_supp ε hε hε1 (Ne.symm hc))467 rw [← hind]468 exact (MeasureTheory.memLp_indicator_iff_restrict hTmeas).2 hlocal469 have hdiff_mem (ε : ℝ) (hε : 0 < ε) (hε1 : ε < 1) :470 MemLp (fun x =>471 ((standardMollifier ε) ⋆[472 ContinuousLinearMap.lsmul ℝ ℝ, volume] (q i j)) x - q i j x)473 p volume :=474 (hconv_mem ε hε hε1).sub (hq i j)475 let F (ε : ℝ) (x : (Fin (m + 1) → ℝ)) : ℝ :=476 ‖((standardMollifier ε) ⋆[477 ContinuousLinearMap.lsmul ℝ ℝ, volume] (q i j)) x - q i j x‖ ^ (m + 1)478 let bound (x : (Fin (m + 1) → ℝ)) : ℝ :=479 T.indicator (fun _ => (2 * B) ^ (m + 1)) x480 have hbound_int : Integrable bound volume := by481 apply (MeasureTheory.integrable_indicator_iff hTmeas).2482 exact ContinuousOn.integrableOn_compact hTcompact483 (continuousOn_const : ContinuousOn484 (fun _ : (Fin (m + 1) → ℝ) => (2 * B) ^ (m + 1)) T)485 have hsmall : ∀ᶠ ε in nhdsWithin (0 : ℝ) (Set.Ioi 0),486 0 < ε ∧ ε < 1 := by487 have hone : ∀ᶠ ε : ℝ in nhdsWithin (0 : ℝ) (Set.Ioi 0), ε < 1 :=488 Filter.Eventually.filter_mono inf_le_left489 (isOpen_Iio.mem_nhds (by norm_num))490 filter_upwards [self_mem_nhdsWithin, hone] with ε hε hε1491 exact ⟨hε, hε1⟩492 have hFmeas : ∀ᶠ ε in nhdsWithin (0 : ℝ) (Set.Ioi 0),493 AEStronglyMeasurable (F ε) volume := by494 filter_upwards [hsmall] with ε hε495 exact (hdiff_mem ε hε.1 hε.2).1.norm.pow (m + 1)496 have hFbound : ∀ᶠ ε in nhdsWithin (0 : ℝ) (Set.Ioi 0),497 ∀ᵐ x ∂volume, ‖F ε x‖ ≤ bound x := by498 filter_upwards [hsmall] with ε hε499 filter_upwards with x500 by_cases hx : x ∈ T501 · simp only [bound, Set.indicator_of_mem hx, F, norm_pow, norm_norm]502 exact pow_le_pow_left₀ (norm_nonneg _) (hdist ε hε.1 x) _503 · simp only [F]504 rw [hzero_out ε hε.1 hε.2 hx]505 simp [bound, hx]506 have hFlim : ∀ᵐ x ∂volume,507 Tendsto (fun ε => F ε x)508 (nhdsWithin (0 : ℝ) (Set.Ioi 0)) (nhds 0) := by509 filter_upwards [hae] with x hx510 have hconst : Tendsto (fun _ : ℝ => q i j x)511 (nhdsWithin (0 : ℝ) (Set.Ioi 0)) (nhds (q i j x)) :=512 tendsto_const_nhds513 simpa only [F, sub_self, norm_zero, zero_pow (Nat.succ_ne_zero m)] using514 (hx.sub hconst).norm.pow (m + 1)515 have hInt : Tendsto (fun ε => ∫ x, F ε x)516 (nhdsWithin (0 : ℝ) (Set.Ioi 0)) (nhds 0) := by517 simpa only [integral_zero] using518 tendsto_integral_filter_of_dominated_convergence bound hFmeas hFbound519 hbound_int hFlim520 have hpReal : p.toReal = (m + 1 : ℝ) := by521 dsimp only [p]522 rw [ENNReal.toReal_natCast]523 norm_num524 have hnorm_eq : ∀ᶠ ε in nhdsWithin (0 : ℝ) (Set.Ioi 0),525 eLpNorm526 (fun x =>527 ((standardMollifier ε) ⋆[528 ContinuousLinearMap.lsmul ℝ ℝ, volume] (q i j)) x - q i j x)529 p volume =530 ENNReal.ofReal ((∫ x, F ε x) ^ p.toReal⁻¹) := by531 filter_upwards [hsmall] with ε hε532 rw [(hdiff_mem ε hε.1 hε.2).eLpNorm_eq_integral_rpow_norm]533 · congr 2534 apply integral_congr_ae535 filter_upwards with x536 rw [hpReal]537 rw [show (m : ℝ) + 1 = ((m + 1 : ℕ) : ℝ) by norm_num]538 exact Real.rpow_natCast _ (m + 1)539 · simp [p]540 · simp [p]541 have ha : 0 < p.toReal⁻¹ := by rw [hpReal]; positivity542 have hpow : Tendsto (fun z : ℝ => z ^ p.toReal⁻¹)543 (nhds 0) (nhds 0) := by544 simpa [Real.zero_rpow ha.ne'] using545 (Real.continuous_rpow_const ha.le).tendsto (0 : ℝ)546 have hof : Tendsto (fun z : ℝ => ENNReal.ofReal z)547 (nhds 0) (nhds 0) := by548 simpa using ENNReal.continuous_ofReal.tendsto (0 : ℝ)549 have hnormEq :550 (fun ε => eLpNorm551 (fun x =>552 ((standardMollifier ε) ⋆[553 ContinuousLinearMap.lsmul ℝ ℝ, volume] (q i j)) x - q i j x)554 p volume) =ᶠ[nhdsWithin (0 : ℝ) (Set.Ioi 0)]555 (fun ε => ENNReal.ofReal ((∫ x, F ε x) ^ p.toReal⁻¹)) := hnorm_eq556 exact (hof.comp (hpow.comp hInt)).congr' hnormEq.symm557 have hsmall : ∀ᶠ ε in nhdsWithin (0 : ℝ) (Set.Ioi 0),558 0 < ε ∧ ε < 1 := by559 have hone : ∀ᶠ ε : ℝ in nhdsWithin (0 : ℝ) (Set.Ioi 0), ε < 1 :=560 Filter.Eventually.filter_mono inf_le_left561 (isOpen_Iio.mem_nhds (by norm_num))562 filter_upwards [self_mem_nhdsWithin, hone] with ε hε hε1563 exact ⟨hε, hε1⟩564 have hscalar (ε : ℝ) (hε : 0 < ε) (hε1 : ε < 1)565 (i : Fin (m + 1)) (j : Fin N) (x : (Fin (m + 1) → ℝ)) (hx : x ∈ K) :566 entry i j (fderiv ℝ (mollify ε f) x - fderiv ℝ f x) =567 ((standardMollifier ε) ⋆[568 ContinuousLinearMap.lsmul ℝ ℝ, volume] (q i j)) x - q i j x := by569 let φ : ContDiffBump (0 : (Fin (m + 1) → ℝ)) :=570 { rIn := ε / 2571 rOut := ε572 rIn_pos := by positivity573 rIn_lt_rOut := by nlinarith }574 have hstd : standardMollifier (n := m + 1) ε = φ.normed volume := by575 simp [standardMollifier, φ, hε]576 have hk : Integrable (standardMollifier (n := m + 1) ε) volume := by577 rw [hstd]578 exact φ.integrable_normed579 have hInt : Integrable (fun y : (Fin (m + 1) → ℝ) =>580 standardMollifier ε y • fderiv ℝ f (x - y)) volume := by581 have hm : AEStronglyMeasurable (fun y : (Fin (m + 1) → ℝ) =>582 standardMollifier ε y • fderiv ℝ f (x - y)) volume := by583 have hmfd : AEStronglyMeasurable584 (fun y : (Fin (m + 1) → ℝ) => fderiv ℝ f (x - y)) volume := by585 exact (((measurable_fderiv ℝ f).comp586 (measurable_const.sub measurable_id)).stronglyMeasurable).aestronglyMeasurable587 exact hk.aestronglyMeasurable.smul hmfd588 apply (hk.norm.mul_const (C : ℝ)).mono' hm589 filter_upwards with y590 rw [norm_smul]591 exact mul_le_mul_of_nonneg_left592 (norm_fderiv_le_of_lipschitz ℝ hLip) (norm_nonneg _)593 have hmove : entry i j (∫ y : (Fin (m + 1) → ℝ),594 standardMollifier ε y • fderiv ℝ f (x - y)) =595 ∫ y : (Fin (m + 1) → ℝ),596 entry i j (standardMollifier ε y • fderiv ℝ f (x - y)) :=597 ((entry i j).integral_comp_comm hInt).symm598 have hmem (y : (Fin (m + 1) → ℝ))599 (hy : standardMollifier ε y ≠ 0) : x - y ∈ S := by600 have hysupp : y ∈ Function.support (standardMollifier ε) := hy601 rw [hstd, φ.support_normed_eq] at hysupp602 have hyε : ‖y‖ < ε := by603 simpa only [Metric.mem_ball, dist_zero_right] using hysupp604 have hxR : ‖x‖ ≤ R := by605 simpa only [Metric.mem_closedBall, dist_zero_right] using hKR hx606 have hxy : ‖x - y‖ ≤ max R 0 + 1 := by607 calc608 ‖x - y‖ ≤ ‖x‖ + ‖y‖ := norm_sub_le x y609 _ ≤ R + 1 := add_le_add hxR (le_of_lt (hyε.trans hε1))610 _ ≤ max R 0 + 1 := by gcongr; exact le_max_left R 0611 simpa only [S, Metric.mem_closedBall, dist_zero_right] using hxy612 have hconv : (∫ y : (Fin (m + 1) → ℝ),613 standardMollifier ε y * entry i j (fderiv ℝ f (x - y))) =614 ∫ y : (Fin (m + 1) → ℝ), standardMollifier ε y * q i j (x - y) := by615 apply integral_congr_ae616 filter_upwards with y617 by_cases hy : standardMollifier ε y = 0618 · simp only [hy, zero_mul]619 · simp only [q, Set.indicator_of_mem (hmem y hy)]620 have hqx : q i j x = entry i j (fderiv ℝ f x) := by621 simp only [q, Set.indicator_of_mem (hKS hx)]622 rw [map_sub, hderiv ε hε x, hmove]623 change (∫ y : (Fin (m + 1) → ℝ),624 standardMollifier ε y * entry i j (fderiv ℝ f (x - y))) -625 entry i j (fderiv ℝ f x) =626 (∫ y : (Fin (m + 1) → ℝ), standardMollifier ε y * q i j (x - y)) -627 q i j x628 rw [hconv, hqx]629 have hcoord_restrict (i : Fin (m + 1)) (j : Fin N) :630 Tendsto631 (fun ε => eLpNorm632 (fun x =>633 ((standardMollifier ε) ⋆[634 ContinuousLinearMap.lsmul ℝ ℝ, volume] (q i j)) x - q i j x)635 ((m + 1 : ℕ) : ℝ≥0∞) (volume.restrict K))636 (nhdsWithin (0 : ℝ) (Set.Ioi 0)) (nhds 0) := by637 have ht := hcoord_full i j638 rw [tendsto_order] at ht ⊢639 constructor640 · intro a ha641 exact (not_lt_of_ge bot_le ha).elim642 · intro b hb643 filter_upwards [ht.2 b hb] with ε hε644 exact lt_of_le_of_lt645 (MeasureTheory.eLpNorm_restrict_le646 (fun x =>647 ((standardMollifier ε) ⋆[648 ContinuousLinearMap.lsmul ℝ ℝ, volume] (q i j)) x - q i j x)649 ((m + 1 : ℕ) : ℝ≥0∞) volume K) hε650 have hcoord (i : Fin (m + 1)) (j : Fin N) :651 Tendsto652 (fun ε => eLpNorm653 (fun x => entry i j654 (fderiv ℝ (mollify ε f) x - fderiv ℝ f x))655 ((m + 1 : ℕ) : ℝ≥0∞) (volume.restrict K))656 (nhdsWithin (0 : ℝ) (Set.Ioi 0)) (nhds 0) := by657 have heq : (fun ε => eLpNorm658 (fun x => entry i j659 (fderiv ℝ (mollify ε f) x - fderiv ℝ f x))660 ((m + 1 : ℕ) : ℝ≥0∞) (volume.restrict K)) =ᶠ[661 nhdsWithin (0 : ℝ) (Set.Ioi 0)]662 (fun ε => eLpNorm663 (fun x =>664 ((standardMollifier ε) ⋆[665 ContinuousLinearMap.lsmul ℝ ℝ, volume] (q i j)) x - q i j x)666 ((m + 1 : ℕ) : ℝ≥0∞) (volume.restrict K)) := by667 filter_upwards [hsmall] with ε hε668 apply eLpNorm_congr_ae669 filter_upwards [ae_restrict_mem hK.measurableSet] with x hx670 exact hscalar ε hε.1 hε.2 i j x hx671 exact (hcoord_restrict i j).congr' heq.symm672 have hpi {d : ℕ} (v : Fin d → ℝ) :673 ‖v‖ ≤ ∑ j, ‖v j‖ := by674 rw [Pi.norm_def]675 have hs := Finset.apply_sup_le_sum676 (f := fun r : ℝ≥0 => (r : ℝ))677 (by simp)678 (by679 intro a b680 change max (a : ℝ) (b : ℝ) ≤ (a : ℝ) + (b : ℝ)681 exact max_le_add_of_nonneg (NNReal.coe_nonneg a) (NNReal.coe_nonneg b))682 (s := fun j : Fin d => ‖v j‖₊)683 (Finset.univ : Finset (Fin d))684 simpa only [NNReal.coe_sum, coe_nnnorm] using hs685 have hcoord_le {d : ℕ} (v : Fin d → ℝ) (i : Fin d) :686 ‖v i‖ ≤ ‖v‖ := by687 rw [Pi.norm_def]688 exact_mod_cast Finset.le_sup (s := Finset.univ)689 (f := fun k : Fin d => ‖v k‖₊) (Finset.mem_univ i)690 have hOp (A : (Fin (m + 1) → ℝ) →L[ℝ] (Fin N → ℝ)) :691 ‖A‖ ≤ ∑ i, ∑ j, ‖entry i j A‖ := by692 apply A.opNorm_le_bound693 (Finset.sum_nonneg fun i _ => Finset.sum_nonneg fun j _ => norm_nonneg _)694 intro v695 have hvsum : (∑ i : Fin (m + 1), v i • (Pi.single i 1)) = v := by696 ext k697 simp [Pi.single_apply]698 calc699 ‖A v‖ = ‖A (∑ i : Fin (m + 1), v i • Pi.single i 1)‖ := by700 rw [hvsum]701 _ = ‖∑ i : Fin (m + 1), A (v i • Pi.single i 1)‖ := by702 rw [map_sum]703 _ ≤704 ∑ i : Fin (m + 1), ‖A (v i • Pi.single i 1)‖ :=705 norm_sum_le _ _706 _ ≤ ∑ i : Fin (m + 1),707 ‖v‖ * (∑ j : Fin N, ‖entry i j A‖) := by708 apply Finset.sum_le_sum709 intro i hi710 rw [map_smul, norm_smul]711 apply mul_le_mul (hcoord_le v i)712 · have hout := hpi (A (Pi.single i 1))713 change ‖A (Pi.single i 1)‖ ≤714 ∑ j : Fin N, ‖entry i j A‖715 exact hout716 · exact norm_nonneg _717 · exact norm_nonneg _718 _ = (∑ i : Fin (m + 1), ∑ j : Fin N, ‖entry i j A‖) * ‖v‖ := by719 rw [← Finset.mul_sum]720 exact mul_comm _ _721 have hmain_le (ε : ℝ) (hε : 0 < ε) :722 eLpNorm723 (fun x => fderiv ℝ (mollify ε f) x - fderiv ℝ f x)724 ((m + 1 : ℕ) : ℝ≥0∞) (volume.restrict K) ≤725 ∑ i : Fin (m + 1), ∑ j : Fin N,726 eLpNorm727 (fun x => entry i j728 (fderiv ℝ (mollify ε f) x - fderiv ℝ f x))729 ((m + 1 : ℕ) : ℝ≥0∞) (volume.restrict K) := by730 have hsmooth := contDiff_mollify hε hLip.continuous.locallyIntegrable731 have hDmeas : StronglyMeasurable732 (fun x => fderiv ℝ (mollify ε f) x - fderiv ℝ f x) :=733 ((hsmooth.continuous_fderiv (by simp)).measurable.sub734 (measurable_fderiv ℝ f)).stronglyMeasurable735 have hRmeas (z : Fin (m + 1) × Fin N) :736 AEStronglyMeasurable737 (fun x => ‖entry z.1 z.2738 (fderiv ℝ (mollify ε f) x - fderiv ℝ f x)‖)739 (volume.restrict K) := by740 exact ((((entry z.1 z.2).continuous.measurable.comp741 hDmeas.measurable).norm).stronglyMeasurable).aestronglyMeasurable742 calc743 eLpNorm744 (fun x => fderiv ℝ (mollify ε f) x - fderiv ℝ f x)745 ((m + 1 : ℕ) : ℝ≥0∞) (volume.restrict K) ≤746 eLpNorm747 (fun x => ∑ i : Fin (m + 1), ∑ j : Fin N,748 ‖entry i j749 (fderiv ℝ (mollify ε f) x - fderiv ℝ f x)‖)750 ((m + 1 : ℕ) : ℝ≥0∞) (volume.restrict K) := by751 apply MeasureTheory.eLpNorm_mono_real752 intro x753 exact hOp _754 _ = eLpNorm755 (∑ z : Fin (m + 1) × Fin N, fun x =>756 ‖entry z.1 z.2757 (fderiv ℝ (mollify ε f) x - fderiv ℝ f x)‖)758 ((m + 1 : ℕ) : ℝ≥0∞) (volume.restrict K) := by759 congr 1760 funext x761 simp only [Finset.sum_apply]762 rw [Fintype.sum_prod_type]763 _ ≤ ∑ z : Fin (m + 1) × Fin N,764 eLpNorm765 (fun x => ‖entry z.1 z.2766 (fderiv ℝ (mollify ε f) x - fderiv ℝ f x)‖)767 ((m + 1 : ℕ) : ℝ≥0∞) (volume.restrict K) := by768 apply MeasureTheory.eLpNorm_sum_le769 · intro z hz770 exact hRmeas z771 · exact Fact.out772 _ = ∑ i : Fin (m + 1), ∑ j : Fin N,773 eLpNorm774 (fun x => entry i j775 (fderiv ℝ (mollify ε f) x - fderiv ℝ f x))776 ((m + 1 : ℕ) : ℝ≥0∞) (volume.restrict K) := by777 rw [Fintype.sum_prod_type]778 simp only [eLpNorm_norm]779 have hsum_tendsto : Tendsto780 (fun ε => ∑ i : Fin (m + 1), ∑ j : Fin N,781 eLpNorm782 (fun x => entry i j783 (fderiv ℝ (mollify ε f) x - fderiv ℝ f x))784 ((m + 1 : ℕ) : ℝ≥0∞) (volume.restrict K))785 (nhdsWithin (0 : ℝ) (Set.Ioi 0)) (nhds 0) := by786 have hj (i : Fin (m + 1)) : Tendsto787 (fun ε => ∑ j : Fin N,788 eLpNorm789 (fun x => entry i j790 (fderiv ℝ (mollify ε f) x - fderiv ℝ f x))791 ((m + 1 : ℕ) : ℝ≥0∞) (volume.restrict K))792 (nhdsWithin (0 : ℝ) (Set.Ioi 0)) (nhds 0) := by793 simpa using tendsto_finsetSum Finset.univ794 (fun j hj => hcoord i j)795 simpa using tendsto_finsetSum Finset.univ (fun i hi => hj i)796 have ht := hsum_tendsto797 rw [tendsto_order] at ht ⊢798 constructor799 · intro a ha800 exact (not_lt_of_ge bot_le ha).elim801 · intro b hb802 filter_upwards [ht.2 b hb, hsmall] with ε hsum hε803 exact lt_of_le_of_lt (hmain_le ε hε.1) hsum804 · simpa only [Nat.cast_add, Nat.cast_one] using805 eventually_mollify_fderiv_memLpOn_compact hf hK806807theorem lipschitz_fderiv_memLpOn_compact808 {m N : ℕ} {f : (Fin (m + 1) → ℝ) → (Fin N → ℝ)} {C : ℝ≥0} (hf : LipschitzWith C f)809 {K : Set ((Fin (m + 1) → ℝ))} (hK : IsCompact K) :810 MemLp (fun x => fderiv ℝ f x) (m + 1) (volume.restrict K) := by811 have hC := hf812 have hd : ∀ᵐ x ∂volume, DifferentiableAt ℝ f x :=813 hC.ae_differentiableAt814 have hdr : ∀ᵐ x ∂volume.restrict K, DifferentiableAt ℝ f x :=815 ae_restrict_of_ae hd816 letI : IsFiniteMeasure (volume.restrict K) :=817 ⟨by simpa using hK.measure_lt_top⟩818 apply MemLp.of_bound819 (measurable_fderiv ℝ f).stronglyMeasurable.aestronglyMeasurable C820 filter_upwards [hdr] with x hx821 exact norm_fderiv_le_of_lipschitz ℝ hC (x₀ := x)822823end Mollification824end MathlibAnnex