feat: a function which is zero as a distribution vanishes almost ever…

…ywhere (#6532)

We first prove this on real manifolds and then deduce it for vector spaces to avoid duplication.

Mathlib.lean

@@ -657,6 +657,7 @@ import Mathlib.Analysis.Convex.StrictConvexSpace
 import Mathlib.Analysis.Convex.Topology
 import Mathlib.Analysis.Convex.Uniform
 import Mathlib.Analysis.Convolution
+import Mathlib.Analysis.Distribution.AEEqOfIntegralContDiff
 import Mathlib.Analysis.Distribution.SchwartzSpace
 import Mathlib.Analysis.Fourier.AddCircle
 import Mathlib.Analysis.Fourier.FourierTransform

Mathlib/Analysis/Distribution/AEEqOfIntegralContDiff.lean

@@ -0,0 +1,154 @@
+/-
+Copyright (c) 2023 Sébastien Gouëzel. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Sébastien Gouëzel
+-/
+import Mathlib.Geometry.Manifold.PartitionOfUnity
+import Mathlib.Geometry.Manifold.Metrizable
+
+/-!
+# Functions which vanish as distributions vanish as functions
+
+In a finite dimensional normed real vector space endowed with a Borel measure, consider a locally
+integrable function whose integral against all compactly supported smooth functions vanishes. Then
+the function is almost everywhere zero.
+This is proved in `ae_eq_zero_of_integral_contDiff_smul_eq_zero`.
+
+A version for two functions having the same integral when multiplied by smooth compactly supported
+functions is also given in `ae_eq_of_integral_contDiff_smul_eq`.
+
+These are deduced from the same results on finite-dimensional real manifolds, given respectively
+as `ae_eq_zero_of_integral_smooth_smul_eq_zero` and `ae_eq_of_integral_smooth_smul_eq`.
+-/
+
+open MeasureTheory Filter Metric Function Set TopologicalSpace
+
+open scoped Topology Manifold
+
+variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E]
+  {F : Type*} [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F]
+
+section Manifold
+
+variable {H : Type*} [TopologicalSpace H] (I : ModelWithCorners ℝ E H)
+  {M : Type*} [TopologicalSpace M] [ChartedSpace H M] [SmoothManifoldWithCorners I M]
+  [MeasurableSpace M] [BorelSpace M] [SigmaCompactSpace M] [T2Space M]
+  {f f' : M → F} {μ : Measure M}
+
+/-- If a locally integrable function `f` on a finite-dimensional real manifold has zero integral
+when multiplied by any smooth compactly supported function, then `f` vanishes almost everywhere. -/
+theorem ae_eq_zero_of_integral_smooth_smul_eq_zero (hf : LocallyIntegrable f μ)
+    (h : ∀ (g : M → ℝ), Smooth I 𝓘(ℝ) g → HasCompactSupport g → ∫ x, g x • f x ∂μ = 0) :
+    ∀ᵐ x ∂μ, f x = 0 := by
+  -- record topological properties of `M`
+  have := I.locally_compact
+  have := ChartedSpace.locallyCompact H M
+  have := I.secondCountableTopology
+  have := ChartedSpace.secondCountable_of_sigma_compact H M
+  have := ManifoldWithCorners.metrizableSpace I M
+  let _ : MetricSpace M := TopologicalSpace.metrizableSpaceMetric M
+  -- it suffices to show that the integral of the function vanishes on any compact set `s`
+  apply ae_eq_zero_of_forall_set_integral_isCompact_eq_zero' hf (fun s hs ↦ Eq.symm ?_)
+  obtain ⟨δ, δpos, hδ⟩ : ∃ δ, 0 < δ ∧ IsCompact (cthickening δ s) := hs.exists_isCompact_cthickening
+  -- choose a sequence of smooth functions `gₙ` equal to `1` on `s` and vanishing outside of the
+  -- `uₙ`-neighborhood of `s`, where `uₙ` tends to zero. Then each integral `∫ gₙ f` vanishes,
+  -- and by dominated convergence these integrals converge to `∫ x in s, f`.
+  obtain ⟨u, -, u_pos, u_lim⟩ : ∃ u, StrictAnti u ∧ (∀ (n : ℕ), u n ∈ Ioo 0 δ)
+    ∧ Tendsto u atTop (𝓝 0) := exists_seq_strictAnti_tendsto' δpos
+  let v : ℕ → Set M := fun n ↦ thickening (u n) s
+  obtain ⟨K, K_compact, vK⟩ : ∃ K, IsCompact K ∧ ∀ n, v n ⊆ K :=
+    ⟨_, hδ, fun n ↦ thickening_subset_cthickening_of_le (u_pos n).2.le _⟩
+  have : ∀ n, ∃ (g : M → ℝ), support g = v n ∧ Smooth I 𝓘(ℝ) g ∧ Set.range g ⊆ Set.Icc 0 1
+          ∧ ∀ x ∈ s, g x = 1 := by
+    intro n
+    rcases exists_msmooth_support_eq_eq_one_iff I isOpen_thickening hs.isClosed
+      (self_subset_thickening (u_pos n).1 s) with ⟨g, g_smooth, g_range, g_supp, hg⟩
+    exact ⟨g, g_supp, g_smooth, g_range, fun x hx ↦ (hg x).1 hx⟩
+  choose g g_supp g_diff g_range hg using this
+  -- main fact: the integral of `∫ gₙ f` tends to `∫ x in s, f`.
+  have L : Tendsto (fun n ↦ ∫ x, g n x • f x ∂μ) atTop (𝓝 (∫ x in s, f x ∂μ)) := by
+    rw [← integral_indicator hs.measurableSet]
+    let bound : M → ℝ := K.indicator (fun x ↦ ‖f x‖)
+    have A : ∀ n, AEStronglyMeasurable (fun x ↦ g n x • f x) μ :=
+      fun n ↦ (g_diff n).continuous.aestronglyMeasurable.smul hf.aestronglyMeasurable
+    have B : Integrable bound μ := by
+      rw [integrable_indicator_iff K_compact.measurableSet]
+      exact (hf.integrableOn_isCompact K_compact).norm
+    have C : ∀ n, ∀ᵐ x ∂μ, ‖g n x • f x‖ ≤ bound x := by
+      intro n
+      apply eventually_of_forall (fun x ↦ ?_)
+      rw [norm_smul]
+      refine le_indicator_apply (fun _ ↦ ?_) (fun hxK ↦ ?_)
+      · have : ‖g n x‖ ≤ 1 := by
+          have := g_range n (mem_range_self (f := g n) x)
+          rw [Real.norm_of_nonneg this.1]
+          exact this.2
+        exact mul_le_of_le_one_left (norm_nonneg _) this
+      · have : g n x = 0 := by rw [← nmem_support, g_supp]; contrapose! hxK; exact vK n hxK
+        simp [this]
+    have D : ∀ᵐ x ∂μ, Tendsto (fun n => g n x • f x) atTop (𝓝 (s.indicator f x)) := by
+      apply eventually_of_forall (fun x ↦ ?_)
+      by_cases hxs : x ∈ s
+      · have : ∀ n, g n x = 1 := fun n ↦ hg n x hxs
+        simp [this, indicator_of_mem hxs f]
+      · simp_rw [indicator_of_not_mem hxs f]
+        apply tendsto_const_nhds.congr'
+        suffices H : ∀ᶠ n in atTop, g n x = 0
+        · filter_upwards [H] with n hn using by simp [hn]
+        obtain ⟨ε, εpos, hε⟩ : ∃ ε, 0 < ε ∧ x ∉ thickening ε s := by
+          rw [← hs.isClosed.closure_eq, closure_eq_iInter_thickening s] at hxs
+          simpa using hxs
+        filter_upwards [(tendsto_order.1 u_lim).2 _ εpos] with n hn
+        rw [← nmem_support, g_supp]
+        contrapose! hε
+        exact thickening_mono hn.le s hε
+    exact tendsto_integral_of_dominated_convergence bound A B C D
+  -- deduce that `∫ x in s, f = 0` as each integral `∫ gₙ f` vanishes by assumption
+  have : ∀ n, ∫ x, g n x • f x ∂μ = 0 := by
+    refine' fun n ↦ h _ (g_diff n) _
+    apply HasCompactSupport.of_support_subset_isCompact K_compact
+    simpa [g_supp] using vK n
+  simpa [this] using L
+
+/-- If two locally integrable functions on a finite-dimensional real manifold have the same integral
+when multiplied by any smooth compactly supported function, then they coincide almost everywhere. -/
+theorem ae_eq_of_integral_smooth_smul_eq
+    (hf : LocallyIntegrable f μ) (hf' : LocallyIntegrable f' μ) (h : ∀ (g : M → ℝ),
+      Smooth I 𝓘(ℝ) g → HasCompactSupport g → ∫ x, g x • f x ∂μ = ∫ x, g x • f' x ∂μ) :
+    ∀ᵐ x ∂μ, f x = f' x := by
+  have : ∀ᵐ x ∂μ, (f - f') x = 0 := by
+    apply ae_eq_zero_of_integral_smooth_smul_eq_zero I (hf.sub hf')
+    intro g g_diff g_supp
+    simp only [Pi.sub_apply, smul_sub]
+    rw [integral_sub, sub_eq_zero]
+    · exact h g g_diff g_supp
+    · exact hf.integrable_smul_left_of_hasCompactSupport g_diff.continuous g_supp
+    · exact hf'.integrable_smul_left_of_hasCompactSupport g_diff.continuous g_supp
+  filter_upwards [this] with x hx
+  simpa [sub_eq_zero] using hx
+
+end Manifold
+
+section VectorSpace
+
+variable [MeasurableSpace E] [BorelSpace E] {f f' : E → F} {μ : Measure E}
+
+/-- If a locally integrable function `f` on a finite-dimensional real vector space has zero integral
+when multiplied by any smooth compactly supported function, then `f` vanishes almost everywhere. -/
+theorem ae_eq_zero_of_integral_contDiff_smul_eq_zero (hf : LocallyIntegrable f μ)
+    (h : ∀ (g : E → ℝ), ContDiff ℝ ⊤ g → HasCompactSupport g → ∫ x, g x • f x ∂μ = 0) :
+    ∀ᵐ x ∂μ, f x = 0 :=
+  ae_eq_zero_of_integral_smooth_smul_eq_zero 𝓘(ℝ, E) hf
+    (fun g g_diff g_supp ↦ h g g_diff.contDiff g_supp)
+
+/-- If two locally integrable functions on a finite-dimensional real vector space have the same
+integral when multiplied by any smooth compactly supported function, then they coincide almost
+everywhere. -/
+theorem ae_eq_of_integral_contDiff_smul_eq
+    (hf : LocallyIntegrable f μ) (hf' : LocallyIntegrable f' μ) (h : ∀ (g : E → ℝ),
+      ContDiff ℝ ⊤ g → HasCompactSupport g → ∫ x, g x • f x ∂μ = ∫ x, g x • f' x ∂μ) :
+    ∀ᵐ x ∂μ, f x = f' x :=
+  ae_eq_of_integral_smooth_smul_eq 𝓘(ℝ, E) hf hf'
+    (fun g g_diff g_supp ↦ h g g_diff.contDiff g_supp)
+
+end VectorSpace

Mathlib/Topology/MetricSpace/HausdorffDistance.lean

@@ -1291,6 +1291,13 @@ theorem _root_.IsCompact.exists_cthickening_subset_open (hs : IsCompact s) (ht :
     ⟨h.1, disjoint_compl_right_iff_subset.1 <| h.2.mono_right <| self_subset_cthickening _⟩
 #align is_compact.exists_cthickening_subset_open IsCompact.exists_cthickening_subset_open
 
+theorem _root_.IsCompact.exists_isCompact_cthickening [LocallyCompactSpace α] (hs : IsCompact s) :
+    ∃ δ, 0 < δ ∧ IsCompact (cthickening δ s) := by
+  rcases exists_compact_superset hs with ⟨K, K_compact, hK⟩
+  rcases hs.exists_cthickening_subset_open isOpen_interior hK with ⟨δ, δpos, hδ⟩
+  refine ⟨δ, δpos, ?_⟩
+  exact isCompact_of_isClosed_subset K_compact isClosed_cthickening (hδ.trans interior_subset)
+
 theorem _root_.IsCompact.exists_thickening_subset_open (hs : IsCompact s) (ht : IsOpen t)
     (hst : s ⊆ t) : ∃ δ, 0 < δ ∧ thickening δ s ⊆ t :=
   let ⟨δ, h₀, hδ⟩ := hs.exists_cthickening_subset_open ht hst