feat(Analysis/ContDiff): smooth compactly supported functions are dense in Lp (#31079)

Author: mcdoll

Mathlib.lean

@@ -1920,6 +1920,7 @@ public import Mathlib.Analysis.Normed.Lp.LpEquiv
 public import Mathlib.Analysis.Normed.Lp.MeasurableSpace
 public import Mathlib.Analysis.Normed.Lp.PiLp
 public import Mathlib.Analysis.Normed.Lp.ProdLp
+public import Mathlib.Analysis.Normed.Lp.SmoothApprox
 public import Mathlib.Analysis.Normed.Lp.WithLp
 public import Mathlib.Analysis.Normed.Lp.lpSpace
 public import Mathlib.Analysis.Normed.Module.Alternating.Basic

Mathlib/Analysis/Normed/Lp/SmoothApprox.lean

@@ -0,0 +1,103 @@
+/-
+Copyright (c) 2025 Moritz Doll. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Moritz Doll
+-/
+module
+
+public import Mathlib.Geometry.Manifold.SmoothApprox
+public import Mathlib.MeasureTheory.Function.ContinuousMapDense
+public import Mathlib.Tactic.MoveAdd
+
+/-!
+
+# Density of smooth compactly supported functions in `Lp`
+
+In this file, we prove that `Lp` functions can be approximated by smooth compactly supported
+functions for `p < ∞`.
+
+This result is recorded in `MeasureTheory.MemLp.exist_sub_eLpNorm_le`.
+-/
+
+variable {α β E F : Type*} [MeasurableSpace E] [NormedAddCommGroup F]
+
+open scoped Nat NNReal ContDiff
+open MeasureTheory Pointwise ENNReal
+
+namespace HasCompactSupport
+
+variable [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [BorelSpace E]
+  [NormedSpace ℝ F]
+  (μ : Measure E := by volume_tac) [IsFiniteMeasureOnCompacts μ]
+
+/-- For every continuous compactly supported function `f`there exists a smooth compactly supported
+function `g` such that `f - g` is arbitrary small in the `Lp`-norm for `p < ∞`. -/
+theorem exist_eLpNorm_sub_le_of_continuous {p : ℝ≥0∞} (hp : p ≠ ⊤) {ε : ℝ} (hε : 0 < ε) {f : E → F}
+    (h₁ : HasCompactSupport f) (h₂ : Continuous f) :
+    ∃ (g : E → F), HasCompactSupport g ∧ ContDiff ℝ ∞ g ∧
+    eLpNorm (f - g) p μ ≤ ENNReal.ofReal ε := by
+  by_cases hf : f =ᵐ[μ] 0
+  -- We will need that the support is non-empty, so we treat the trivial case `f = 0` first.
+  · use 0
+    simpa [HasCompactSupport.zero, eLpNorm_congr_ae hf] using contDiff_const
+  have hs₁ : μ (tsupport f) ≠ ⊤ := h₁.measure_lt_top.ne
+  have hs₂ : 0 < (μ <| tsupport f).toReal := by
+    -- Since `f` is not the zero function `tsupport f` has positive measure
+    rw [← Measure.measure_support_eq_zero_iff _] at hf
+    exact toReal_pos (pos_mono (subset_tsupport f) (pos_of_ne_zero hf)).ne' hs₁
+  set ε' := ε * (μ <| tsupport f).toReal ^ (-(1 / p.toReal)) with ε'_def
+  have hε' : 0 < ε' := by positivity
+  have hε₂ : ENNReal.ofReal ε' * μ (tsupport f) ^ (1 / p.toReal) ≤ ENNReal.ofReal ε := by
+    rw [← ofReal_toReal hs₁, ofReal_rpow_of_pos hs₂, ← ofReal_mul hε'.le,
+      ofReal_le_ofReal_iff hε.le, ε'_def, mul_assoc, ← Real.rpow_add hs₂, neg_add_cancel,
+      Real.rpow_zero, mul_one]
+  obtain ⟨g, hg₁, hg₂, hg₃⟩ := h₂.exists_contDiff_approx ⊤ (ε := fun _ ↦ ε') (by fun_prop)
+    (by intro; positivity)
+  refine ⟨g, h₁.mono hg₃, hg₁, (eLpNorm_sub_le_of_dist_bdd μ hp h₁.measurableSet hε'.le ?_
+    (subset_tsupport f) (hg₃.trans (subset_tsupport f))).trans hε₂⟩
+  intro x
+  rw [dist_comm]
+  exact (hg₂ x).le
+
+end HasCompactSupport
+
+namespace MeasureTheory.MemLp
+
+variable [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [BorelSpace E]
+  [NormedSpace ℝ F]
+  {μ : Measure E} [IsFiniteMeasureOnCompacts μ]
+
+/-- Every `Lp` function can be approximated by a smooth compactly supported function provided that
+`p < ∞`. -/
+theorem exist_eLpNorm_sub_le {p : ℝ≥0∞} (hp : p ≠ ⊤) (hp₂ : 1 ≤ p) {f : E → F} (hf : MemLp f p μ)
+    {ε : ℝ} (hε : 0 < ε) :
+    ∃ g, HasCompactSupport g ∧ ContDiff ℝ ∞ g ∧ eLpNorm (f - g) p μ ≤ ENNReal.ofReal ε := by
+  -- We use a standard ε / 2 argument to deduce the result from the approximation for
+  -- continuous compactly supported functions.
+  have hε₂ : 0 < ε / 2 := by positivity
+  have hε₂' : 0 < ENNReal.ofReal (ε / 2) := by positivity
+  obtain ⟨g, hg₁, hg₂, hg₃, hg₄⟩ := hf.exists_hasCompactSupport_eLpNorm_sub_le hp hε₂'.ne'
+  obtain ⟨g', hg'₁, hg'₂, hg'₃⟩ := hg₁.exist_eLpNorm_sub_le_of_continuous μ hp hε₂ hg₃
+  refine ⟨g', hg'₁, hg'₂, ?_⟩
+  have : f - g' = (f - g) - (g' - g) := by simp
+  grw [this, eLpNorm_sub_le (hf.aestronglyMeasurable.sub hg₄.aestronglyMeasurable)
+    (hg'₂.continuous.aestronglyMeasurable.sub hg₄.aestronglyMeasurable) hp₂, hg₂,
+    eLpNorm_sub_comm, hg'₃, ← ENNReal.ofReal_add hε₂.le hε₂.le, add_halves]
+
+theorem _root_.MeasureTheory.Lp.dense_hasCompactSupport_contDiff {p : ℝ≥0∞} (hp : p ≠ ⊤)
+    [hp₂ : Fact (1 ≤ p)] :
+    Dense {f : Lp F p μ | ∃ (g : E → F), f =ᵐ[μ] g ∧ HasCompactSupport g ∧ ContDiff ℝ ∞ g} := by
+  intro f
+  refine (mem_closure_iff_nhds_basis Metric.nhds_basis_closedBall).2 fun ε hε ↦ ?_
+  obtain ⟨g, hg₁, hg₂, hg₃⟩ := exist_eLpNorm_sub_le hp hp₂.out (Lp.memLp f) hε
+  have hg₄ : MemLp g p μ := hg₂.continuous.memLp_of_hasCompactSupport hg₁
+  use hg₄.toLp
+  use ⟨g, hg₄.coeFn_toLp, hg₁, hg₂⟩
+  rw [Metric.mem_closedBall, dist_comm, Lp.dist_def,
+    ← le_ofReal_iff_toReal_le ((Lp.memLp f).sub (Lp.memLp hg₄.toLp)).eLpNorm_ne_top hε.le]
+  convert hg₃ using 1
+  apply eLpNorm_congr_ae
+  gcongr
+  exact hg₄.coeFn_toLp
+
+end MeasureTheory.MemLp

Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean

@@ -754,6 +754,32 @@ protected lemma MemLp.piecewise {f : α → ε} [DecidablePred (· ∈ s)] {g} (
     rw [setLIntegral_congr_fun hs.compl h]
     exact lintegral_rpow_enorm_lt_top_of_eLpNorm_lt_top hp_zero hp_top hg.2
 
+theorem eLpNorm_indicator_sub_le_of_dist_bdd {β : Type*} [NormedAddCommGroup β]
+    (μ : Measure α := by volume_tac) (hp' : p ≠ ∞) (hs : MeasurableSet s)
+    {f g : α → β} {c : ℝ} (hc : 0 ≤ c) (hf : ∀ x ∈ s, dist (f x) (g x) ≤ c) :
+    eLpNorm (s.indicator (f - g)) p μ ≤ ENNReal.ofReal c * μ s ^ (1 / p.toReal) := by
+  by_cases hp : p = 0
+  · simp [hp]
+  have : ∀ x, ‖s.indicator (f - g) x‖ ≤ ‖s.indicator (fun _ => c) x‖ := by
+    intro x
+    by_cases hx : x ∈ s
+    · rw [Set.indicator_of_mem hx, Set.indicator_of_mem hx, Pi.sub_apply, ← dist_eq_norm,
+        Real.norm_eq_abs, abs_of_nonneg hc]
+      exact hf x hx
+    · simp [Set.indicator_of_notMem hx]
+  grw [eLpNorm_mono this, eLpNorm_indicator_const hs hp hp', ← ofReal_norm_eq_enorm,
+    Real.norm_eq_abs, abs_of_nonneg hc]
+
+theorem eLpNorm_sub_le_of_dist_bdd {β : Type*} [NormedAddCommGroup β]
+    (μ : Measure α := by volume_tac) (hp : p ≠ ⊤) (hs : MeasurableSet s) {c : ℝ} (hc : 0 ≤ c)
+    {f g : α → β} (h : ∀ x, dist (f x) (g x) ≤ c) (hs₁ : f.support ⊆ s) (hs₂ : g.support ⊆ s) :
+    eLpNorm (f - g) p μ ≤ ENNReal.ofReal c * μ s ^ (1 / p.toReal) := by
+  have hs₃ : s.indicator (f - g) = f - g := by
+    rw [Set.indicator_eq_self]
+    exact (Function.support_sub _ _).trans (Set.union_subset hs₁ hs₂)
+  rw [← hs₃]
+  exact eLpNorm_indicator_sub_le_of_dist_bdd μ hp hs hc (fun x _ ↦ h x)
+
 end Indicator
 
 section ENormedAddMonoid
@@ -1481,3 +1507,5 @@ theorem MemLp.exists_eLpNorm_indicator_compl_lt {β : Type*} [NormedAddCommGroup
 end UnifTight
 end Lp
 end MeasureTheory
+
+set_option linter.style.longFile 1700

Mathlib/MeasureTheory/Function/UniformIntegrable.lean

@@ -452,22 +452,6 @@ theorem unifIntegrable_finite [Finite ι] (hp_one : 1 ≤ p) (hp_top : p ≠ ∞
 
 end
 
-theorem eLpNorm_sub_le_of_dist_bdd (μ : Measure α)
-    {p : ℝ≥0∞} (hp' : p ≠ ∞) {s : Set α} (hs : MeasurableSet[m] s)
-    {f g : α → β} {c : ℝ} (hc : 0 ≤ c) (hf : ∀ x ∈ s, dist (f x) (g x) ≤ c) :
-    eLpNorm (s.indicator (f - g)) p μ ≤ ENNReal.ofReal c * μ s ^ (1 / p.toReal) := by
-  by_cases hp : p = 0
-  · simp [hp]
-  have : ∀ x, ‖s.indicator (f - g) x‖ ≤ ‖s.indicator (fun _ => c) x‖ := by
-    intro x
-    by_cases hx : x ∈ s
-    · rw [Set.indicator_of_mem hx, Set.indicator_of_mem hx, Pi.sub_apply, ← dist_eq_norm,
-        Real.norm_eq_abs, abs_of_nonneg hc]
-      exact hf x hx
-    · simp [Set.indicator_of_notMem hx]
-  grw [eLpNorm_mono this, eLpNorm_indicator_const hs hp hp', ← ofReal_norm_eq_enorm,
-    Real.norm_eq_abs, abs_of_nonneg hc]
-
 /-- A sequence of uniformly integrable functions which converges μ-a.e. converges in Lp. -/
 theorem tendsto_Lp_finite_of_tendsto_ae_of_meas [IsFiniteMeasure μ] (hp : 1 ≤ p) (hp' : p ≠ ∞)
     {f : ℕ → α → β} {g : α → β} (hf : ∀ n, StronglyMeasurable (f n)) (hg : StronglyMeasurable g)
@@ -509,7 +493,7 @@ theorem tendsto_Lp_finite_of_tendsto_ae_of_meas [IsFiniteMeasure μ] (hp : 1 ≤
   have hlt : eLpNorm (tᶜ.indicator (f n - g)) p μ ≤ ENNReal.ofReal (ε.toReal / 3) := by
     specialize hN n hn
     have : 0 ≤ ε.toReal / (3 * measureUnivNNReal μ ^ (1 / p.toReal)) := by positivity
-    have := eLpNorm_sub_le_of_dist_bdd μ hp' htm.compl this fun x hx =>
+    have := eLpNorm_indicator_sub_le_of_dist_bdd μ hp' htm.compl this fun x hx =>
       (dist_comm (g x) (f n x) ▸ (hN x hx).le :
         dist (f n x) (g x) ≤ ε.toReal / (3 * measureUnivNNReal μ ^ (1 / p.toReal)))
     refine le_trans this ?_

Mathlib/MeasureTheory/Measure/MeasureSpace.lean

@@ -1177,6 +1177,10 @@ lemma nonempty_of_neZero (μ : Measure α) [NeZero μ] : Nonempty α :=
   (isEmpty_or_nonempty α).resolve_left fun h ↦ by
     simpa [eq_empty_of_isEmpty] using NeZero.ne (μ univ)
 
+theorem measure_support_eq_zero_iff {E : Type*} [Zero E] (μ : Measure α := by volume_tac)
+    {f : α → E} : μ f.support = 0 ↔ f =ᵐ[μ] 0 := by
+  rfl
+
 section Sum
 variable {f : ι → Measure α}