feat(analysis/calculus/bump_function_findim): construct good bump functions on finite-dimensional spaces (#18095)

On any finite-dimensional real vector space, we construct a smooth family of smooth functions indexed by `R > 1` which are equal to `1` on the ball `B 0 1`, and with support exactly `B 0 R`. This is the main ingredient to construct nice bump functions.

Author: sgouezel

src/analysis/calculus/bump_function_findim.lean

@@ -7,6 +7,7 @@ import analysis.calculus.specific_functions
 import analysis.calculus.series
 import analysis.convolution
 import data.set.pointwise.support
+import measure_theory.measure.haar_lebesgue
 
 /-!
 # Bump functions in finite-dimensional vector spaces
@@ -194,3 +195,376 @@ begin
 end
 
 end
+
+section
+
+namespace exists_cont_diff_bump_base
+
+/-- An auxiliary function to construct partitions of unity on finite-dimensional real vector spaces.
+It is the characteristic function of the closed unit ball. -/
+def φ : E → ℝ := (closed_ball (0 : E) 1).indicator (λ y, (1 : ℝ))
+
+variables [normed_space ℝ E]  [finite_dimensional ℝ E]
+
+section helper_definitions
+
+variable (E)
+lemma u_exists : ∃ u : E → ℝ, cont_diff ℝ ⊤ u ∧
+  (∀ x, u x ∈ Icc (0 : ℝ) 1) ∧ (support u = ball 0 1) ∧ (∀ x, u (-x) = u x) :=
+begin
+  have A : is_open (ball (0 : E) 1), from is_open_ball,
+  obtain ⟨f, f_support, f_smooth, f_range⟩ :
+    ∃ (f : E → ℝ), f.support = ball (0 : E) 1 ∧ cont_diff ℝ ⊤ f ∧ set.range f ⊆ set.Icc 0 1,
+    from A.exists_smooth_support_eq,
+  have B : ∀ x, f x ∈ Icc (0 : ℝ) 1 := λ x, f_range (mem_range_self x),
+  refine ⟨λ x, (f x + f (-x)) / 2, _, _, _, _⟩,
+  { exact (f_smooth.add (f_smooth.comp cont_diff_neg)).div_const },
+  { assume x,
+    split,
+    { linarith [(B x).1, (B (-x)).1] },
+    { linarith [(B x).2, (B (-x)).2] } },
+  { refine support_eq_iff.2 ⟨λ x hx, _, λ x hx, _⟩,
+    { apply ne_of_gt,
+      have : 0 < f x,
+      { apply lt_of_le_of_ne (B x).1 (ne.symm _),
+        rwa ← f_support at hx },
+      linarith [(B (-x)).1] },
+    { have I1 : x ∉ support f, by rwa f_support,
+      have I2 : -x ∉ support f,
+      { rw f_support,
+        simp only at hx,
+        simpa using hx },
+      simp only [mem_support, not_not] at I1 I2,
+      simp only [I1, I2, add_zero, zero_div] } },
+  { assume x, simp only [add_comm, neg_neg] }
+end
+
+variable {E}
+
+/-- An auxiliary function to construct partitions of unity on finite-dimensional real vector spaces,
+which is smooth, symmetric, and with support equal to the unit ball. -/
+def u (x : E) : ℝ := classical.some (u_exists E) x
+
+variable (E)
+lemma u_smooth : cont_diff ℝ ⊤ (u : E → ℝ) := (classical.some_spec (u_exists E)).1
+
+lemma u_continuous : continuous (u : E → ℝ) := (u_smooth E).continuous
+
+lemma u_support : support (u : E → ℝ) = ball 0 1 := (classical.some_spec (u_exists E)).2.2.1
+
+lemma u_compact_support : has_compact_support (u : E → ℝ) :=
+begin
+  rw [has_compact_support_def, u_support, closure_ball (0 : E) one_ne_zero],
+  exact is_compact_closed_ball _ _,
+end
+variable {E}
+
+lemma u_nonneg (x : E) : 0 ≤ u x := ((classical.some_spec (u_exists E)).2.1 x).1
+
+lemma u_le_one (x : E) : u x ≤ 1 := ((classical.some_spec (u_exists E)).2.1 x).2
+
+lemma u_neg (x : E) : u (-x) = u x := (classical.some_spec (u_exists E)).2.2.2 x
+
+variables [measurable_space E] [borel_space E]
+
+local notation `μ` := measure_theory.measure.add_haar
+
+variable (E)
+lemma u_int_pos : 0 < ∫ (x : E), u x ∂μ :=
+begin
+  refine (integral_pos_iff_support_of_nonneg u_nonneg _).mpr _,
+  { exact (u_continuous E).integrable_of_has_compact_support (u_compact_support E) },
+  { rw u_support, exact measure_ball_pos _ _ zero_lt_one }
+end
+variable {E}
+
+/-- An auxiliary function to construct partitions of unity on finite-dimensional real vector spaces,
+which is smooth, symmetric, with support equal to the ball of radius `D` and integral `1`. -/
+def W (D : ℝ) (x : E) : ℝ := ((∫ (x : E), u x ∂μ) * |D|^(finrank ℝ E))⁻¹ • u (D⁻¹ • x)
+
+lemma W_def (D : ℝ) :
+  (W D : E → ℝ) = λ x, ((∫ (x : E), u x ∂μ) * |D|^(finrank ℝ E))⁻¹ • u (D⁻¹ • x) :=
+by { ext1 x, refl }
+
+lemma W_nonneg (D : ℝ) (x : E) : 0 ≤ W D x :=
+begin
+  apply mul_nonneg _ (u_nonneg _),
+  apply inv_nonneg.2,
+  apply mul_nonneg (u_int_pos E).le,
+  apply pow_nonneg (abs_nonneg D)
+end
+
+lemma W_mul_φ_nonneg (D : ℝ) (x y : E) : 0 ≤ W D y * φ (x - y) :=
+mul_nonneg (W_nonneg D y) (indicator_nonneg (by simp only [zero_le_one, implies_true_iff]) _)
+
+variable (E)
+
+lemma W_integral {D : ℝ} (Dpos : 0 < D) : ∫ (x : E), W D x ∂μ = 1 :=
+begin
+  simp_rw [W, integral_smul],
+  rw [integral_comp_inv_smul_of_nonneg μ (u : E → ℝ) Dpos.le,
+    abs_of_nonneg Dpos.le, mul_comm],
+  field_simp [Dpos.ne', (u_int_pos E).ne'],
+end
+
+lemma W_support {D : ℝ} (Dpos : 0 < D) : support (W D : E → ℝ) = ball 0 D :=
+begin
+  have B : D • ball (0 : E) 1 = ball 0 D,
+    by rw [smul_unit_ball Dpos.ne', real.norm_of_nonneg Dpos.le],
+  have C : D ^ finrank ℝ E ≠ 0, from pow_ne_zero _ Dpos.ne',
+  simp only [W_def, algebra.id.smul_eq_mul, support_mul, support_inv, univ_inter,
+    support_comp_inv_smul₀ Dpos.ne', u_support, B, support_const (u_int_pos E).ne',
+    support_const C, abs_of_nonneg Dpos.le],
+end
+
+lemma W_compact_support {D : ℝ} (Dpos : 0 < D) : has_compact_support (W D : E → ℝ) :=
+begin
+  rw [has_compact_support_def, W_support E Dpos, closure_ball (0 : E) Dpos.ne'],
+  exact is_compact_closed_ball _ _,
+end
+variable {E}
+
+/-- An auxiliary function to construct partitions of unity on finite-dimensional real vector spaces.
+It is the convolution between a smooth function of integral `1` supported in the ball of radius `D`,
+with the indicator function of the closed unit ball. Therefore, it is smooth, equal to `1` on the
+ball of radius `1 - D`, with support equal to the ball of radius `1 + D`. -/
+def Y (D : ℝ) : E → ℝ := W D ⋆[lsmul ℝ ℝ, μ] φ
+
+lemma Y_neg (D : ℝ) (x : E) : Y D (-x) = Y D x :=
+begin
+  apply convolution_neg_of_neg_eq,
+  { apply eventually_of_forall (λ x, _),
+    simp only [W_def, u_neg, smul_neg, algebra.id.smul_eq_mul, mul_eq_mul_left_iff,
+      eq_self_iff_true, true_or], },
+  { apply eventually_of_forall (λ x, _),
+    simp only [φ, indicator, mem_closed_ball_zero_iff, norm_neg] },
+end
+
+lemma Y_eq_one_of_mem_closed_ball {D : ℝ} {x : E} (Dpos : 0 < D)
+  (hx : x ∈ closed_ball (0 : E) (1 - D)) : Y D x = 1 :=
+begin
+  change (W D ⋆[lsmul ℝ ℝ, μ] φ) x = 1,
+  have B : ∀ (y : E), y ∈ ball x D → φ y = 1,
+  { have C : ball x D ⊆ ball 0 1,
+    { apply ball_subset_ball',
+      simp only [mem_closed_ball] at hx,
+      linarith only [hx] },
+    assume y hy,
+    simp only [φ, indicator, mem_closed_ball, ite_eq_left_iff, not_le, zero_ne_one],
+    assume h'y,
+    linarith only [mem_ball.1 (C hy), h'y] },
+  have Bx : φ x = 1, from B _ (mem_ball_self Dpos),
+  have B' : ∀ y, y ∈ ball x D → φ y = φ x, by { rw Bx, exact B },
+  rw convolution_eq_right' _ (le_of_eq (W_support E Dpos)) B',
+  simp only [lsmul_apply, algebra.id.smul_eq_mul, integral_mul_right, W_integral E Dpos, Bx,
+    one_mul],
+end
+
+lemma Y_eq_zero_of_not_mem_ball {D : ℝ} {x : E} (Dpos : 0 < D)
+  (hx : x ∉ ball (0 : E) (1 + D)) : Y D x = 0 :=
+begin
+  change (W D ⋆[lsmul ℝ ℝ, μ] φ) x = 0,
+  have B : ∀ y, y ∈ ball x D →  φ y = 0,
+  { assume y hy,
+    simp only [φ, indicator, mem_closed_ball_zero_iff, ite_eq_right_iff, one_ne_zero],
+    assume h'y,
+    have C : ball y D ⊆ ball 0 (1+D),
+    { apply ball_subset_ball',
+      rw ← dist_zero_right at h'y,
+      linarith only [h'y] },
+    exact hx (C (mem_ball_comm.1 hy)) },
+  have Bx : φ x = 0, from B _ (mem_ball_self Dpos),
+  have B' : ∀ y, y ∈ ball x D → φ y = φ x, by { rw Bx, exact B },
+  rw convolution_eq_right' _ (le_of_eq (W_support E Dpos)) B',
+  simp only [lsmul_apply, algebra.id.smul_eq_mul, Bx, mul_zero, integral_const]
+end
+
+lemma Y_nonneg (D : ℝ) (x : E) : 0 ≤ Y D x :=
+integral_nonneg (W_mul_φ_nonneg D x)
+
+lemma Y_le_one {D : ℝ} (x : E) (Dpos : 0 < D) : Y D x ≤ 1 :=
+begin
+  have A : (W D ⋆[lsmul ℝ ℝ, μ] φ) x ≤ (W D ⋆[lsmul ℝ ℝ, μ] 1) x,
+  { apply convolution_mono_right_of_nonneg _ (W_nonneg D)
+      (indicator_le_self' (λ x hx, zero_le_one)) (λ x, zero_le_one),
+    refine (has_compact_support.convolution_exists_left _ (W_compact_support E Dpos) _
+      (locally_integrable_const (1 : ℝ)) x).integrable,
+    exact continuous_const.mul ((u_continuous E).comp (continuous_id.const_smul _)) },
+  have B : (W D ⋆[lsmul ℝ ℝ, μ] (λ y, (1 : ℝ))) x = 1,
+    by simp only [convolution, continuous_linear_map.map_smul, mul_inv_rev, coe_smul', mul_one,
+      lsmul_apply, algebra.id.smul_eq_mul, integral_mul_left, W_integral E Dpos, pi.smul_apply],
+  exact A.trans (le_of_eq B)
+end
+
+lemma Y_pos_of_mem_ball {D : ℝ} {x : E} (Dpos : 0 < D) (D_lt_one : D < 1)
+  (hx : x ∈ ball (0 : E) (1 + D)) : 0 < Y D x :=
+begin
+  simp only [mem_ball_zero_iff] at hx,
+  refine (integral_pos_iff_support_of_nonneg (W_mul_φ_nonneg D x) _).2 _,
+  { have F_comp : has_compact_support (W D),
+      from W_compact_support E Dpos,
+    have B : locally_integrable (φ : E → ℝ) μ,
+      from (locally_integrable_const _).indicator measurable_set_closed_ball,
+    have C : continuous (W D : E → ℝ),
+      from continuous_const.mul ((u_continuous E).comp (continuous_id.const_smul _)),
+    exact (has_compact_support.convolution_exists_left (lsmul ℝ ℝ : ℝ →L[ℝ] ℝ →L[ℝ] ℝ)
+      F_comp C B x).integrable },
+  { set z := (D / (1 + D)) • x with hz,
+    have B : 0 < 1 + D, by linarith,
+    have C : ball z (D * (1 + D- ‖x‖) / (1 + D)) ⊆ support (λ (y : E), W D y * φ (x - y)),
+    { assume y hy,
+      simp only [support_mul, W_support E Dpos],
+      simp only [φ, mem_inter_iff, mem_support, ne.def, indicator_apply_eq_zero,
+        mem_closed_ball_zero_iff, one_ne_zero, not_forall, not_false_iff, exists_prop, and_true],
+      split,
+      { apply ball_subset_ball' _ hy,
+        simp only [z, norm_smul, abs_of_nonneg Dpos.le, abs_of_nonneg B.le, dist_zero_right,
+          real.norm_eq_abs, abs_div],
+        simp only [div_le_iff B] with field_simps,
+        ring_nf },
+      { have ID : ‖D / (1 + D) - 1‖ = 1 / (1 + D),
+        { rw real.norm_of_nonpos,
+          { simp only [B.ne', ne.def, not_false_iff, mul_one, neg_sub, add_tsub_cancel_right]
+              with field_simps},
+          { simp only [B.ne', ne.def, not_false_iff, mul_one] with field_simps,
+            apply div_nonpos_of_nonpos_of_nonneg _ B.le,
+            linarith only, } },
+        rw ← mem_closed_ball_iff_norm',
+        apply closed_ball_subset_closed_ball' _ (ball_subset_closed_ball hy),
+        rw [← one_smul ℝ x, dist_eq_norm, hz, ← sub_smul, one_smul, norm_smul, ID],
+        simp only [-one_div, -mul_eq_zero, B.ne', div_le_iff B] with field_simps,
+        simp only [mem_ball_zero_iff] at hx,
+        nlinarith only [hx, D_lt_one] } },
+    apply lt_of_lt_of_le _ (measure_mono C),
+    apply measure_ball_pos,
+    exact div_pos (mul_pos Dpos (by linarith only [hx])) B }
+end
+
+variable (E)
+
+lemma Y_smooth : cont_diff_on ℝ ⊤ (uncurry Y) ((Ioo (0 : ℝ) 1) ×ˢ (univ : set E)) :=
+begin
+  have hs : is_open (Ioo (0 : ℝ) (1 : ℝ)), from is_open_Ioo,
+  have hk : is_compact (closed_ball (0 : E) 1), from proper_space.is_compact_closed_ball _ _,
+  refine cont_diff_on_convolution_left_with_param (lsmul ℝ ℝ) hs hk _ _ _,
+  { rintros p x hp hx,
+    simp only [W, mul_inv_rev, algebra.id.smul_eq_mul, mul_eq_zero, inv_eq_zero],
+    right,
+    contrapose! hx,
+    have : p⁻¹ • x ∈ support u, from mem_support.2 hx,
+    simp only [u_support, norm_smul, mem_ball_zero_iff, real.norm_eq_abs, abs_inv,
+      abs_of_nonneg hp.1.le, ← div_eq_inv_mul, div_lt_one hp.1] at this,
+    rw mem_closed_ball_zero_iff,
+    exact this.le.trans hp.2.le },
+  { exact (locally_integrable_const _).indicator measurable_set_closed_ball },
+  { apply cont_diff_on.mul,
+    { refine (cont_diff_on_const.mul _).inv
+        (λ x hx, ne_of_gt (mul_pos (u_int_pos E) (pow_pos (abs_pos_of_pos hx.1.1) _))),
+      apply cont_diff_on.pow,
+      simp_rw [← real.norm_eq_abs],
+      apply @cont_diff_on.norm ℝ,
+      { exact cont_diff_on_fst },
+      { assume x hx, exact ne_of_gt hx.1.1 } },
+    { apply (u_smooth E).comp_cont_diff_on,
+      exact cont_diff_on.smul (cont_diff_on_fst.inv (λ x hx, ne_of_gt hx.1.1)) cont_diff_on_snd } },
+end
+
+lemma Y_support {D : ℝ} (Dpos : 0 < D) (D_lt_one : D < 1) :
+  support (Y D : E → ℝ) = ball (0 : E) (1 + D) :=
+support_eq_iff.2 ⟨λ x hx, (Y_pos_of_mem_ball Dpos D_lt_one hx).ne',
+  λ x hx, Y_eq_zero_of_not_mem_ball Dpos hx⟩
+
+variable {E}
+
+end helper_definitions
+
+/-- The base function from which one will construct a family of bump functions. One could
+add more properties if they are useful and satisfied in the examples of inner product spaces
+and finite dimensional vector spaces, notably derivative norm control in terms of `R - 1`.
+TODO: move to the right file and use this to refactor bump functions in general. -/
+@[nolint has_nonempty_instance]
+structure _root_.cont_diff_bump_base (E : Type*) [normed_add_comm_group E] [normed_space ℝ E] :=
+(to_fun : ℝ → E → ℝ)
+(mem_Icc   : ∀ (R : ℝ) (x : E), to_fun R x ∈ Icc (0 : ℝ) 1)
+(symmetric : ∀ (R : ℝ) (x : E), to_fun R (-x) = to_fun R x)
+(smooth    : cont_diff_on ℝ ⊤ (uncurry to_fun) ((Ioi (1 : ℝ)) ×ˢ (univ : set E)))
+(eq_one    : ∀ (R : ℝ) (hR : 1 < R) (x : E) (hx : ‖x‖ ≤ 1), to_fun R x = 1)
+(support   : ∀ (R : ℝ) (hR : 1 < R), support (to_fun R) = metric.ball (0 : E) R)
+
+/-- A class registering that a real vector space admits bump functions. This will be instantiated
+first for inner product spaces, and then for finite-dimensional normed spaces.
+We use a specific class instead of `nonempty (cont_diff_bump_base E)` for performance reasons. -/
+class _root_.has_cont_diff_bump (E : Type*) [normed_add_comm_group E] [normed_space ℝ E] : Prop :=
+(out : nonempty (cont_diff_bump_base E))
+
+@[priority 100]
+instance {E : Type*} [normed_add_comm_group E] [normed_space ℝ E] [finite_dimensional ℝ E] :
+  has_cont_diff_bump E :=
+begin
+  refine ⟨⟨_⟩⟩,
+  borelize E,
+  have IR : ∀ (R : ℝ), 1 < R → 0 < (R - 1) / (R + 1),
+  { assume R hR, apply div_pos; linarith },
+  exact
+  { to_fun := λ R x, if 1 < R then Y ((R - 1) / (R + 1)) (((R + 1) / 2)⁻¹ • x) else 0,
+    mem_Icc := λ R x, begin
+      split_ifs,
+      { refine ⟨Y_nonneg _ _, Y_le_one _ (IR R h)⟩ },
+      { simp only [pi.zero_apply, left_mem_Icc, zero_le_one] }
+    end,
+    symmetric := λ R x, begin
+      split_ifs,
+      { simp only [Y_neg, smul_neg] },
+      { refl },
+    end,
+    smooth := begin
+      suffices : cont_diff_on ℝ ⊤
+        ((uncurry Y) ∘ (λ (p : ℝ × E), ((p.1 - 1) / (p.1 + 1), ((p.1 + 1)/2)⁻¹ • p.2)))
+        (Ioi 1 ×ˢ univ),
+      { apply this.congr,
+        rintros ⟨R, x⟩ ⟨(hR : 1 < R), hx⟩,
+        simp only [hR, uncurry_apply_pair, if_true, comp_app], },
+      apply (Y_smooth E).comp,
+      { apply cont_diff_on.prod,
+        { refine (cont_diff_on_fst.sub cont_diff_on_const).div
+            (cont_diff_on_fst.add cont_diff_on_const) _,
+          rintros ⟨R, x⟩ ⟨(hR : 1 < R), hx⟩,
+          apply ne_of_gt,
+          dsimp only,
+          linarith, },
+        { apply cont_diff_on.smul _ cont_diff_on_snd,
+          refine (cont_diff_on_fst.add cont_diff_on_const).div_const.inv _,
+          rintros ⟨R, x⟩ ⟨(hR : 1 < R), hx⟩,
+          apply ne_of_gt,
+          dsimp only,
+          linarith } },
+      { rintros ⟨R, x⟩ ⟨(hR : 1 < R), hx⟩,
+        have A : 0 < (R - 1) / (R + 1), by { apply div_pos; linarith },
+        have B :  (R - 1) / (R + 1) < 1, by { apply (div_lt_one _ ).2; linarith },
+        simp only [mem_preimage, prod_mk_mem_set_prod_eq, mem_Ioo, mem_univ, and_true, A, B] }
+    end,
+    eq_one := λ R hR x hx, begin
+      have A : 0 < R + 1, by linarith,
+      simp only [hR, if_true],
+      apply Y_eq_one_of_mem_closed_ball (IR R hR),
+      simp only [norm_smul, inv_div, mem_closed_ball_zero_iff, real.norm_eq_abs, abs_div,
+                 abs_two, abs_of_nonneg A.le],
+      calc 2 / (R + 1) * ‖x‖ ≤ 2 / (R + 1) * 1 :
+        mul_le_mul_of_nonneg_left hx (div_nonneg zero_le_two A.le)
+      ... = 1 - (R - 1) / (R + 1) : by { field_simp [A.ne'], ring }
+    end,
+    support := λ R hR, begin
+      have A : 0 < (R + 1) / 2, by linarith,
+      have A' : 0 < R + 1, by linarith,
+      have C :  (R - 1) / (R + 1) < 1, by { apply (div_lt_one _ ).2; linarith },
+      simp only [hR, if_true, support_comp_inv_smul₀ A.ne', Y_support _ (IR R hR) C,
+        smul_ball A.ne', real.norm_of_nonneg A.le, smul_zero],
+      congr' 1,
+      field_simp [A'.ne'],
+      ring,
+    end },
+end
+
+end exists_cont_diff_bump_base
+
+end