feat(analysis/calculus/specific_functions): define normed bump functi…

…ons (#13463)

* Normed bump functions have integral 1 w.r.t. the specified measure.
* Also add a few more properties of bump functions, including its smoothness in all arguments (including midpoint and the two radii).
* From the sphere eversion project
* Required for convolutions

src/analysis/calculus/specific_functions.lean

@@ -1,10 +1,12 @@
 /-
 Copyright (c) 2020 Sébastien Gouëzel. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Sébastien Gouëzel
+Authors: Sébastien Gouëzel, Floris van Doorn
 -/
 import analysis.calculus.iterated_deriv
 import analysis.inner_product_space.euclidean_dist
+import measure_theory.function.locally_integrable
+import measure_theory.integral.set_integral
 
 /-!
 # Infinitely smooth bump function
@@ -29,6 +31,9 @@ function cannot have:
   function: real numbers `r`, `R`, and proofs of `0 < r < R`. The function itself is available
   through `coe_fn`.
 
+* If `f : cont_diff_bump_of_inner c` and `μ` is a measure on the domain of `f`, then `f.normed μ`
+  is a smooth bump function with integral `1` w.r.t. `μ`.
+
 * `f : cont_diff_bump c`, where `c` is a point in a finite dimensional real vector space, is a
   bundled smooth function such that
 
@@ -264,7 +269,7 @@ end smooth_transition
 
 end real
 
-variable {E : Type*}
+variables {E X : Type*}
 
 /-- `f : cont_diff_bump_of_inner c`, where `c` is a point in an inner product space, is a
 bundled smooth function such that
@@ -287,7 +292,8 @@ lemma R_pos {c : E} (f : cont_diff_bump_of_inner c) : 0 < f.R := f.r_pos.trans f
 
 instance (c : E) : inhabited (cont_diff_bump_of_inner c) := ⟨⟨1, 2, zero_lt_one, one_lt_two⟩⟩
 
-variables [inner_product_space ℝ E] {c : E} (f : cont_diff_bump_of_inner c) {x : E}
+variables [inner_product_space ℝ E] [normed_group X] [normed_space ℝ X]
+variables {c : E} (f : cont_diff_bump_of_inner c) {x : E} {n : with_top ℕ}
 
 /-- The function defined by `f : cont_diff_bump_of_inner c`. Use automatic coercion to
 function instead. -/
@@ -296,6 +302,15 @@ def to_fun (f : cont_diff_bump_of_inner c) : E → ℝ :=
 
 instance : has_coe_to_fun (cont_diff_bump_of_inner c) (λ _, E → ℝ) := ⟨to_fun⟩
 
+protected lemma «def» (x : E) : f x = real.smooth_transition ((f.R - dist x c) / (f.R - f.r)) :=
+rfl
+
+protected lemma sub (x : E) : f (c - x) = f (c + x) :=
+by simp_rw [f.def, dist_self_sub_left, dist_self_add_left]
+
+protected lemma neg (f : cont_diff_bump_of_inner (0 : E)) (x : E) : f (- x) = f x :=
+by simp_rw [← zero_sub, f.sub, zero_add]
+
 open real (smooth_transition) real.smooth_transition metric
 
 lemma one_of_mem_closed_ball (hx : x ∈ closed_ball c f.r) :
@@ -304,6 +319,10 @@ one_of_one_le $ (one_le_div (sub_pos.2 f.r_lt_R)).2 $ sub_le_sub_left hx _
 
 lemma nonneg : 0 ≤ f x := nonneg _
 
+/-- A version of `cont_diff_bump_of_inner.nonneg` with `x` explicit -/
+lemma nonneg' (x : E) : 0 ≤ f x :=
+f.nonneg
+
 lemma le_one : f x ≤ 1 := le_one _
 
 lemma pos_of_mem_ball (hx : x ∈ ball c f.R) : 0 < f x :=
@@ -324,6 +343,12 @@ begin
   { simp [hx.not_lt, f.zero_of_le_dist hx] }
 end
 
+lemma tsupport_eq : tsupport f = closed_ball c f.R :=
+by simp_rw [tsupport, f.support_eq, closure_ball _ f.R_pos.ne']
+
+protected lemma has_compact_support [finite_dimensional ℝ E] : has_compact_support f :=
+by simp_rw [has_compact_support, f.tsupport_eq, is_compact_closed_ball]
+
 lemma eventually_eq_one_of_mem_ball (h : x ∈ ball c f.r) :
   f =ᶠ[𝓝 x] 1 :=
 ((is_open_lt (continuous_id.dist continuous_const) continuous_const).eventually_mem h).mono $
@@ -332,26 +357,105 @@ lemma eventually_eq_one_of_mem_ball (h : x ∈ ball c f.r) :
 lemma eventually_eq_one : f =ᶠ[𝓝 c] 1 :=
 f.eventually_eq_one_of_mem_ball (mem_ball_self f.r_pos)
 
-protected lemma cont_diff_at {n} :
-  cont_diff_at ℝ n f x :=
+/-- `cont_diff_bump` is `𝒞ⁿ` in all its arguments. -/
+protected lemma _root_.cont_diff_at.cont_diff_bump {c g : X → E}
+  {f : ∀ x, cont_diff_bump_of_inner (c x)} {x : X}
+  (hc : cont_diff_at ℝ n c x) (hr : cont_diff_at ℝ n (λ x, (f x).r) x)
+  (hR : cont_diff_at ℝ n (λ x, (f x).R) x)
+  (hg : cont_diff_at ℝ n g x) : cont_diff_at ℝ n (λ x, f x (g x)) x :=
 begin
-  rcases em (x = c) with rfl|hx,
-  { refine cont_diff_at.congr_of_eventually_eq _ f.eventually_eq_one,
-    rw pi.one_def,
-    exact cont_diff_at_const },
-  { exact real.smooth_transition.cont_diff_at.comp x
-      (cont_diff_at.div_const $ cont_diff_at_const.sub $
-        cont_diff_at_id.dist cont_diff_at_const hx) }
+  rcases eq_or_ne (g x) (c x) with hx|hx,
+  { have : (λ x, f x (g x)) =ᶠ[𝓝 x] (λ x, 1),
+    { have : dist (g x) (c x) < (f x).r, { simp_rw [hx, dist_self, (f x).r_pos] },
+      have := continuous_at.eventually_lt (hg.continuous_at.dist hc.continuous_at) hr.continuous_at
+        this,
+      exact eventually_of_mem this
+        (λ x hx, (f x).one_of_mem_closed_ball (mem_set_of_eq.mp hx).le) },
+    exact cont_diff_at_const.congr_of_eventually_eq this },
+  { refine real.smooth_transition.cont_diff_at.comp x _,
+    refine ((hR.sub $ hg.dist hc hx).div (hR.sub hr) (sub_pos.mpr (f x).r_lt_R).ne') }
 end
 
-protected lemma cont_diff {n} :
-  cont_diff ℝ n f :=
-cont_diff_iff_cont_diff_at.2 $ λ y, f.cont_diff_at
+lemma _root_.cont_diff.cont_diff_bump {c g : X → E} {f : ∀ x, cont_diff_bump_of_inner (c x)}
+  (hc : cont_diff ℝ n c) (hr : cont_diff ℝ n (λ x, (f x).r)) (hR : cont_diff ℝ n (λ x, (f x).R))
+  (hg : cont_diff ℝ n g) : cont_diff ℝ n (λ x, f x (g x)) :=
+by { rw [cont_diff_iff_cont_diff_at] at *, exact λ x, (hc x).cont_diff_bump (hr x) (hR x) (hg x) }
 
-protected lemma cont_diff_within_at {s n} :
-  cont_diff_within_at ℝ n f s x :=
+protected lemma cont_diff : cont_diff ℝ n f :=
+cont_diff_const.cont_diff_bump cont_diff_const cont_diff_const cont_diff_id
+
+protected lemma cont_diff_at : cont_diff_at ℝ n f x :=
+f.cont_diff.cont_diff_at
+
+protected lemma cont_diff_within_at {s : set E} : cont_diff_within_at ℝ n f s x :=
 f.cont_diff_at.cont_diff_within_at
 
+protected lemma continuous : continuous f :=
+cont_diff_zero.mp f.cont_diff
+
+open measure_theory
+variables [measurable_space E] {μ : measure E}
+
+/-- A bump function normed so that `∫ x, f.normed μ x ∂μ = 1`. -/
+protected def normed (μ : measure E) : E → ℝ :=
+λ x, f x / ∫ x, f x ∂μ
+
+lemma normed_def {μ : measure E} (x : E) : f.normed μ x = f x / ∫ x, f x ∂μ :=
+rfl
+
+lemma nonneg_normed (x : E) : 0 ≤ f.normed μ x :=
+div_nonneg f.nonneg $ integral_nonneg f.nonneg'
+
+lemma cont_diff_normed {n : with_top ℕ} : cont_diff ℝ n (f.normed μ) :=
+f.cont_diff.div_const
+
+lemma continuous_normed : continuous (f.normed μ) :=
+f.continuous.div_const
+
+lemma normed_sub (x : E) : f.normed μ (c - x) = f.normed μ (c + x) :=
+by simp_rw [f.normed_def, f.sub]
+
+lemma normed_neg (f : cont_diff_bump_of_inner (0 : E)) (x : E) : f.normed μ (- x) = f.normed μ x :=
+by simp_rw [f.normed_def, f.neg]
+
+variables [borel_space E] [finite_dimensional ℝ E] [is_locally_finite_measure μ]
+
+protected lemma integrable : integrable f μ :=
+f.continuous.integrable_of_has_compact_support f.has_compact_support
+
+protected lemma integrable_normed : integrable (f.normed μ) μ :=
+f.integrable.div_const _
+
+variables [μ .is_open_pos_measure]
+
+lemma integral_pos : 0 < ∫ x, f x ∂μ :=
+begin
+  refine (integral_pos_iff_support_of_nonneg f.nonneg' f.integrable).mpr _,
+  rw [f.support_eq],
+  refine is_open_ball.measure_pos _ (nonempty_ball.mpr f.R_pos)
+end
+
+lemma integral_normed : ∫ x, f.normed μ x ∂μ = 1 :=
+begin
+  simp_rw [cont_diff_bump_of_inner.normed, div_eq_mul_inv, mul_comm (f _), ← smul_eq_mul,
+    integral_smul],
+  exact inv_mul_cancel (f.integral_pos.ne')
+end
+
+lemma support_normed_eq : support (f.normed μ) = metric.ball c f.R :=
+by simp_rw [cont_diff_bump_of_inner.normed, support_div, f.support_eq,
+  support_const f.integral_pos.ne', inter_univ]
+
+lemma tsupport_normed_eq : tsupport (f.normed μ) = metric.closed_ball c f.R :=
+by simp_rw [tsupport, f.support_normed_eq, closure_ball _ f.R_pos.ne']
+
+lemma has_compact_support_normed : has_compact_support (f.normed μ) :=
+by simp_rw [has_compact_support, f.tsupport_normed_eq, is_compact_closed_ball]
+
+variable (μ)
+lemma integral_normed_smul (z : X) [complete_space X] : ∫ x, f.normed μ x • z ∂μ = z :=
+by simp_rw [integral_smul_const, f.integral_normed, one_smul]
+
 end cont_diff_bump_of_inner
 
 /-- `f : cont_diff_bump c`, where `c` is a point in a finite dimensional real vector space, is

src/analysis/normed/group/basic.lean

@@ -158,6 +158,12 @@ by rw [← dist_zero_left, ← dist_add_left g 0 h, add_zero]
 @[simp] theorem dist_self_add_left (g h : E) : dist (g + h) g = ∥h∥ :=
 by rw [dist_comm, dist_self_add_right]
 
+@[simp] theorem dist_self_sub_right (g h : E) : dist g (g - h) = ∥h∥ :=
+by rw [sub_eq_add_neg, dist_self_add_right, norm_neg]
+
+@[simp] theorem dist_self_sub_left (g h : E) : dist (g - h) g = ∥h∥ :=
+by rw [dist_comm, dist_self_sub_right]
+
 /-- **Triangle inequality** for the norm. -/
 lemma norm_add_le (g h : E) : ∥g + h∥ ≤ ∥g∥ + ∥h∥ :=
 by simpa [dist_eq_norm] using dist_triangle g 0 (-h)

src/measure_theory/function/l1_space.lean

@@ -833,6 +833,10 @@ lemma integrable.mul_const {f : α → ℝ} (h : integrable f μ) (c : ℝ) :
   integrable (λ x, f x * c) μ :=
 by simp_rw [mul_comm, h.const_mul _]
 
+lemma integrable.div_const {f : α → ℝ} (h : integrable f μ) (c : ℝ) :
+  integrable (λ x, f x / c) μ :=
+by simp_rw [div_eq_mul_inv, h.mul_const]
+
 end normed_space
 
 section normed_space_over_complete_field

src/order/cover.lean

@@ -224,6 +224,18 @@ h.wcovby.Icc_eq
 
 end partial_order
 
+section linear_order
+
+variables [linear_order α] {a b : α}
+
+lemma covby.Ioi_eq (h : a ⋖ b) : Ioi a = Ici b :=
+by rw [← Ioo_union_Ici_eq_Ioi h.lt, h.Ioo_eq, empty_union]
+
+lemma covby.Iio_eq (h : a ⋖ b) : Iio b = Iic a :=
+by rw [← Iic_union_Ioo_eq_Iio h.lt, h.Ioo_eq, union_empty]
+
+end linear_order
+
 namespace set
 
 lemma wcovby_insert (x : α) (s : set α) : s ⩿ insert x s :=

src/topology/algebra/order/basic.lean

@@ -559,6 +559,22 @@ lemma continuous.if_le [topological_space γ] [Π x, decidable (f x ≤ g x)] {f
   continuous (λ x, if f x ≤ g x then f' x else g' x) :=
 continuous_if_le hf hg hf'.continuous_on hg'.continuous_on hfg
 
+lemma tendsto.eventually_lt {l : filter γ} {f g : γ → α} {y z : α}
+  (hf : tendsto f l (𝓝 y)) (hg : tendsto g l (𝓝 z)) (hyz : y < z) : ∀ᶠ x in l, f x < g x :=
+begin
+  by_cases h : y ⋖ z,
+  { filter_upwards [hf (Iio_mem_nhds hyz), hg (Ioi_mem_nhds hyz)],
+    rw [h.Iio_eq],
+    exact λ x hfx hgx, lt_of_le_of_lt hfx hgx },
+  { obtain ⟨w, hyw, hwz⟩ := (not_covby_iff hyz).mp h,
+    filter_upwards [hf (Iio_mem_nhds hyw), hg (Ioi_mem_nhds hwz)],
+    exact λ x, lt_trans },
+end
+
+lemma continuous_at.eventually_lt {x₀ : β} (hf : continuous_at f x₀)
+  (hg : continuous_at g x₀) (hfg : f x₀ < g x₀) : ∀ᶠ x in 𝓝 x₀, f x < g x :=
+tendsto.eventually_lt hf hg hfg
+
 @[continuity] lemma continuous.min (hf : continuous f) (hg : continuous g) :
   continuous (λb, min (f b) (g b)) :=
 by { simp only [min_def], exact hf.if_le hg hf hg (λ x, id) }