feat(analysis/convolution): the predicate convolution_exists (#13541)

* This PR defines the predicate that a convolution exists.
* This is not that interesting by itself, but it is a preparation for #13540
* I'm using the full module doc for the convolution file, even though not everything promised in the module doc is in this PR.
* From the sphere eversion project

src/analysis/convolution.lean

@@ -0,0 +1,352 @@
+/-
+Copyright (c) 2022 Floris van Doorn. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Floris van Doorn
+-/
+import measure_theory.group.integration
+import measure_theory.group.prod
+import measure_theory.function.locally_integrable
+import analysis.calculus.specific_functions
+
+/-!
+# Convolution of functions
+
+This file defines the convolution on two functions, i.e. `x ↦ ∫ f(t)g(x - t) ∂t`.
+In the general case, these functions can be vector-valued, and have an arbitrary (additive)
+group as domain. We use a continuous bilinear operation `L` on these function values as
+"multiplication". The domain must be equipped with a Haar measure `μ`
+(though many individual results have weaker conditions on `μ`).
+
+For many applications we can take `L = lsmul ℝ ℝ` or `L = lmul ℝ ℝ`.
+
+We also define `convolution_exists` and `convolution_exists_at` to state that the convolution is
+well-defined (everywhere or at a single point). These conditions are needed for pointwise
+computations (e.g. `convolution_exists_at.distrib_add`), but are generally not stong enough for any
+local (or global) properties of the convolution. For this we need stronger assumptions on `f`
+and/or `g`, and generally if we impose stronger conditions on one of the functions, we can impose
+weaker conditions on the other.
+We have proven many of the properties of the convolution assuming one of these functions
+has compact support (in which case the other function only needs to be locally integrable).
+We still need to prove the properties for other pairs of conditions (e.g. both functions are
+rapidly decreasing)
+
+# Design Decisions
+
+We use a bilinear map `L` to "multiply" the two functions in the integrand.
+This generality has several advantages
+
+* This allows us to compute the total derivative of the convolution, in case the functions are
+  multivariate. The total derivative is again a convolution, but where the codomains of the
+  functions can be higher-dimensional. See `has_compact_support.has_fderiv_at_convolution_right`.
+* This allows us to use `@[to_additive]` everywhere (which would not be possible if we would use
+  `mul`/`smul` in the integral, since `@[to_additive]` will incorrectly also try to additivize
+  those definitions).
+* We need to support the case where at least one of the functions is vector-valued, but if we use
+  `smul` to multiply the functions, that would be an asymmetric definition.
+
+# Main Definitions
+* `convolution f g L μ x = (f ⋆[L, μ] g) x = ∫ t, L (f t) (g (x - t)) ∂μ` is the convolution of
+  `f` and `g` w.r.t. the continuous bilinear map `L` and measure `μ`.
+* `convolution_exists_at f g x L μ` states that the convolution `(f ⋆[L, μ] g) x` is well-defined
+  (i.e. the integral exists).
+* `convolution_exists f g L μ` states that the convolution `f ⋆[L, μ] g` is well-defined at each
+  point.
+
+# Main Results
+* `has_compact_support.has_fderiv_at_convolution_right` and
+  `has_compact_support.has_fderiv_at_convolution_left`: we can compute the total derivative
+  of the convolution as a convolution with the total derivative of the right (left) function.
+* `has_compact_support.cont_diff_convolution_right` and
+  `has_compact_support.cont_diff_convolution_left`: the convolution is `𝒞ⁿ` if one of the functions
+  is `𝒞ⁿ` with compact support and the other function in locally integrable.
+* `convolution_tendsto_right`: Given a sequence of nonnegative normalized functions whose support
+  tends to a small neighborhood around `0`, the convolution tends to the right argument.
+  This is specialized to bump functions in `cont_diff_bump_of_inner.convolution_tendsto_right`.
+
+# Notation
+The following notations are localized in the locale `convolution`:
+* `f ⋆[L, μ] g` for the convolution. Note: you have to use parentheses to apply the convolution
+  to an argument: `(f ⋆[L, μ] g) x`.
+* `f ⋆[L] g := f ⋆[L, volume] g`
+* `f ⋆ g := f ⋆[lsmul ℝ ℝ] g`
+
+# To do
+* Prove properties about the convolution if both functions are rapidly decreasing.
+* Use `@[to_additive]` everywhere
+-/
+
+open set function filter measure_theory measure_theory.measure topological_space
+open continuous_linear_map metric
+open_locale pointwise topological_space
+
+variables {𝕜 G E E' E'' F : Type*}
+variables [normed_group E] [normed_group E'] [normed_group E''] [normed_group F]
+variables {f f' : G → E} {g g' : G → E'} {x x' : G} {y y' : E}
+
+section nondiscrete_normed_field
+
+variables [nondiscrete_normed_field 𝕜]
+variables [normed_space 𝕜 E] [normed_space 𝕜 E'] [normed_space 𝕜 E''] [normed_space 𝕜 F]
+variables (L : E →L[𝕜] E' →L[𝕜] F)
+
+section no_measurability
+
+variables [add_group G] [topological_space G]
+
+lemma has_compact_support.convolution_integrand_bound_right (hcg : has_compact_support g)
+  (hg : continuous g) {x t : G} {s : set G} (hx : x ∈ s) :
+  ∥L (f t) (g (x - t))∥ ≤ (- tsupport g + s).indicator (λ t, ∥L∥ * ∥f t∥ * (⨆ i, ∥g i∥)) t :=
+begin
+  refine le_indicator (λ t ht, _) (λ t ht, _) t,
+  { refine (L.le_op_norm₂ _ _).trans _,
+    exact mul_le_mul_of_nonneg_left
+        (le_csupr (hg.norm.bdd_above_range_of_has_compact_support hcg.norm) $ x - t)
+        (mul_nonneg (norm_nonneg _) (norm_nonneg _)) },
+  { have : x - t ∉ support g,
+    { refine mt (λ hxt, _) ht, refine ⟨_, _, set.neg_mem_neg.mpr (subset_closure hxt), hx, _⟩,
+      rw [neg_sub, sub_add_cancel] },
+    rw [nmem_support.mp this, (L _).map_zero, norm_zero] }
+end
+
+lemma continuous.convolution_integrand_fst [has_continuous_sub G] (hg : continuous g) (t : G) :
+  continuous (λ x, L (f t) (g (x - t))) :=
+L.continuous₂.comp₂ continuous_const $ hg.comp $ continuous_id.sub continuous_const
+
+lemma has_compact_support.convolution_integrand_bound_left (hcf : has_compact_support f)
+  (hf : continuous f) {x t : G} {s : set G} (hx : x ∈ s) :
+  ∥L (f (x - t)) (g t)∥ ≤ (- tsupport f + s).indicator (λ t, ∥L∥ * (⨆ i, ∥f i∥) * ∥g t∥) t :=
+by { convert hcf.convolution_integrand_bound_right L.flip hf hx,
+  simp_rw [L.op_norm_flip, mul_right_comm] }
+
+end no_measurability
+
+section measurability
+
+variables [measurable_space G] {μ : measure G}
+
+/-- The convolution of `f` and `g` exists at `x` when the function `t ↦ L (f t) (g (x - t))` is
+  integrable. There are various conditions on `f` and `g` to prove this. -/
+def convolution_exists_at [has_sub G] (f : G → E) (g : G → E') (x : G) (L : E →L[𝕜] E' →L[𝕜] F)
+  (μ : measure G . volume_tac) : Prop :=
+integrable (λ t, L (f t) (g (x - t))) μ
+
+/-- The convolution of `f` and `g` exists when the function `t ↦ L (f t) (g (x - t))` is integrable
+  for all `x : G`. There are various conditions on `f` and `g` to prove this. -/
+def convolution_exists [has_sub G] (f : G → E) (g : G → E') (L : E →L[𝕜] E' →L[𝕜] F)
+  (μ : measure G . volume_tac) : Prop :=
+∀ x : G, convolution_exists_at f g x L μ
+
+section convolution_exists
+
+variables {L}
+lemma convolution_exists_at.integrable [has_sub G] {x : G} (h : convolution_exists_at f g x L μ) :
+  integrable (λ t, L (f t) (g (x - t))) μ :=
+h
+
+variables (L)
+
+section group
+
+variables [add_group G]
+variables [has_measurable_add₂ G] [has_measurable_neg G]
+
+lemma measure_theory.ae_strongly_measurable.convolution_integrand' [sigma_finite μ]
+  (hf : ae_strongly_measurable f μ)
+  (hg : ae_strongly_measurable g $ map (λ (p : G × G), p.1 - p.2) (μ.prod μ)) :
+  ae_strongly_measurable (λ p : G × G, L (f p.2) (g (p.1 - p.2))) (μ.prod μ) :=
+L.ae_strongly_measurable_comp₂ hf.snd $ hg.comp_measurable $ measurable_fst.sub measurable_snd
+
+lemma measure_theory.ae_strongly_measurable.convolution_integrand_snd'
+  (hf : ae_strongly_measurable f μ) {x : G}
+  (hg : ae_strongly_measurable g $ map (λ t, x - t) μ) :
+  ae_strongly_measurable (λ t, L (f t) (g (x - t))) μ :=
+L.ae_strongly_measurable_comp₂ hf $ hg.comp_measurable $ measurable_id.const_sub x
+
+lemma measure_theory.ae_strongly_measurable.convolution_integrand_swap_snd'
+  {x : G} (hf : ae_strongly_measurable f $ map (λ t, x - t) μ)
+  (hg : ae_strongly_measurable g μ) : ae_strongly_measurable (λ t, L (f (x - t)) (g t)) μ :=
+L.ae_strongly_measurable_comp₂ (hf.comp_measurable $ measurable_id.const_sub x) hg
+
+/-- A sufficient condition to prove that `f ⋆[L, μ] g` exists.
+We assume that the integrand has compact support and `g` is bounded on this support (note that
+both properties hold if `g` is continuous with compact support). We also require that `f` is
+integrable on the support of the integrand, and that both functions are strongly measurable.
+
+Note: we could weaken the measurability condition to hold only for `μ.restrict s`. -/
+lemma bdd_above.convolution_exists_at' {x₀ : G}
+  {s : set G} (hbg : bdd_above ((λ i, ∥g i∥) '' ((λ t, - t + x₀) ⁻¹' s)))
+  (hs : measurable_set s) (h2s : support (λ t, L (f t) (g (x₀ - t))) ⊆ s)
+  (hf : integrable_on f s μ)
+  (hmf : ae_strongly_measurable f μ)
+  (hmg : ae_strongly_measurable g $ map (λ t, x₀ - t) μ) :
+    convolution_exists_at f g x₀ L μ :=
+begin
+  set s' := (λ t, - t + x₀) ⁻¹' s,
+  have : ∀ᵐ (t : G) ∂μ,
+    ∥L (f t) (g (x₀ - t))∥ ≤ s.indicator (λ t, ∥L∥ * ∥f t∥ * ⨆ i : s', ∥g i∥) t,
+  { refine eventually_of_forall _,
+    refine le_indicator (λ t ht, _) (λ t ht, _),
+    { refine (L.le_op_norm₂ _ _).trans _,
+      refine mul_le_mul_of_nonneg_left
+        (le_csupr_set hbg $ mem_preimage.mpr _)
+        (mul_nonneg (norm_nonneg _) (norm_nonneg _)),
+      rwa [neg_sub, sub_add_cancel] },
+    { have : t ∉ support (λ t, L (f t) (g (x₀ - t))) := mt (λ h, h2s h) ht,
+      rw [nmem_support.mp this, norm_zero] } },
+  refine integrable.mono' _ _ this,
+  { rw [integrable_indicator_iff hs], exact (hf.norm.const_mul _).mul_const _ },
+  { exact hmf.convolution_integrand_snd' L hmg }
+end
+
+section left
+variables [sigma_finite μ] [is_add_left_invariant μ]
+
+lemma measure_theory.ae_strongly_measurable.convolution_integrand_snd
+  (hf : ae_strongly_measurable f μ) (hg : ae_strongly_measurable g μ)
+  (x : G) : ae_strongly_measurable (λ t, L (f t) (g (x - t))) μ :=
+hf.convolution_integrand_snd' L $ hg.mono' $ map_sub_left_absolutely_continuous μ x
+
+lemma measure_theory.ae_strongly_measurable.convolution_integrand_swap_snd
+  (hf : ae_strongly_measurable f μ) (hg : ae_strongly_measurable g μ)
+  (x : G) : ae_strongly_measurable (λ t, L (f (x - t)) (g t)) μ :=
+(hf.mono' (map_sub_left_absolutely_continuous μ x)).convolution_integrand_swap_snd' L hg
+
+end left
+
+section right
+
+variables [sigma_finite μ] [is_add_right_invariant μ]
+
+lemma measure_theory.ae_strongly_measurable.convolution_integrand
+  (hf : ae_strongly_measurable f μ) (hg : ae_strongly_measurable g μ) :
+  ae_strongly_measurable (λ p : G × G, L (f p.2) (g (p.1 - p.2))) (μ.prod μ) :=
+hf.convolution_integrand' L $ hg.mono' (quasi_measure_preserving_sub μ).absolutely_continuous
+
+lemma measure_theory.integrable.convolution_integrand (hf : integrable f μ) (hg : integrable g μ) :
+  integrable (λ p : G × G, L (f p.2) (g (p.1 - p.2))) (μ.prod μ) :=
+begin
+  have h_meas : ae_strongly_measurable (λ (p : G × G), (L (f p.2)) (g (p.1 - p.2))) (μ.prod μ) :=
+    hf.ae_strongly_measurable.convolution_integrand L hg.ae_strongly_measurable,
+  have h2_meas : ae_strongly_measurable (λ (y : G), ∫ (x : G), ∥(L (f y)) (g (x - y))∥ ∂μ) μ :=
+    h_meas.prod_swap.norm.integral_prod_right',
+  simp_rw [integrable_prod_iff' h_meas],
+  refine ⟨eventually_of_forall (λ t, (L (f t)).integrable_comp (hg.comp_sub_right t)), _⟩,
+  refine integrable.mono' _ h2_meas (eventually_of_forall $
+    λ t, (_ : _ ≤ ∥L∥ * ∥f t∥ * ∫ x, ∥g (x - t)∥ ∂μ)),
+  { simp_rw [integral_sub_right_eq_self (λ t, ∥ g t ∥)],
+    exact (hf.norm.const_mul _).mul_const _ },
+  { simp_rw [← integral_mul_left],
+    rw [real.norm_of_nonneg],
+    { exact integral_mono_of_nonneg (eventually_of_forall $ λ t, norm_nonneg _)
+        ((hg.comp_sub_right t).norm.const_mul _) (eventually_of_forall $ λ t, L.le_op_norm₂ _ _) },
+    exact integral_nonneg (λ x, norm_nonneg _) }
+end
+
+lemma measure_theory.integrable.ae_convolution_exists (hf : integrable f μ) (hg : integrable g μ) :
+  ∀ᵐ x ∂μ, convolution_exists_at f g x L μ :=
+((integrable_prod_iff $ hf.ae_strongly_measurable.convolution_integrand L
+  hg.ae_strongly_measurable).mp $ hf.convolution_integrand L hg).1
+
+end right
+
+variables [topological_space G] [topological_add_group G] [borel_space G]
+  [second_countable_topology G] [sigma_compact_space G]
+
+lemma has_compact_support.convolution_exists_at {x₀ : G}
+  (h : has_compact_support (λ t, L (f t) (g (x₀ - t)))) (hf : locally_integrable f μ)
+  (hg : continuous g) : convolution_exists_at f g x₀ L μ :=
+((((homeomorph.neg G).trans $ homeomorph.add_right x₀).compact_preimage.mpr h).bdd_above_image
+  hg.norm.continuous_on).convolution_exists_at' L is_closed_closure.measurable_set subset_closure
+  (hf h) hf.ae_strongly_measurable hg.ae_strongly_measurable
+
+lemma has_compact_support.convolution_exists_right
+  (hcg : has_compact_support g) (hf : locally_integrable f μ) (hg : continuous g) :
+  convolution_exists f g L μ :=
+begin
+  intro x₀,
+  refine has_compact_support.convolution_exists_at L _ hf hg,
+  refine (hcg.comp_homeomorph (homeomorph.sub_left x₀)).mono _,
+  refine λ t, mt (λ ht : g (x₀ - t) = 0, _),
+  simp_rw [ht, (L _).map_zero]
+end
+
+lemma has_compact_support.convolution_exists_left_of_continuous_right
+  (hcf : has_compact_support f) (hf : locally_integrable f μ) (hg : continuous g) :
+  convolution_exists f g L μ :=
+begin
+  intro x₀,
+  refine has_compact_support.convolution_exists_at L _ hf hg,
+  refine hcf.mono _,
+  refine λ t, mt (λ ht : f t = 0, _),
+  simp_rw [ht, L.map_zero₂]
+end
+
+end group
+
+section comm_group
+
+variables [add_comm_group G]
+
+section measurable_group
+
+variables [has_measurable_add₂ G] [has_measurable_neg G] [is_add_left_invariant μ]
+
+/-- A sufficient condition to prove that `f ⋆[L, μ] g` exists.
+We assume that the integrand has compact support and `g` is bounded on this support (note that
+both properties hold if `g` is continuous with compact support). We also require that `f` is
+integrable on the support of the integrand, and that both functions are strongly measurable.
+
+This is a variant of `bdd_above.convolution_exists_at'` in an abelian group with a left-invariant
+measure. This allows us to state the boundedness and measurability of `g` in a more natural way. -/
+lemma bdd_above.convolution_exists_at [sigma_finite μ] {x₀ : G}
+  {s : set G} (hbg : bdd_above ((λ i, ∥g i∥) '' ((λ t, x₀ - t) ⁻¹' s)))
+  (hs : measurable_set s) (h2s : support (λ t, L (f t) (g (x₀ - t))) ⊆ s)
+  (hf : integrable_on f s μ)
+  (hmf : ae_strongly_measurable f μ)
+  (hmg : ae_strongly_measurable g μ) :
+    convolution_exists_at f g x₀ L μ :=
+begin
+  refine bdd_above.convolution_exists_at' L _ hs h2s hf hmf _,
+  { simp_rw [← sub_eq_neg_add, hbg] },
+  { exact hmg.mono' (map_sub_left_absolutely_continuous μ x₀) }
+end
+
+variables {L} [is_neg_invariant μ]
+
+lemma convolution_exists_at_flip :
+  convolution_exists_at g f x L.flip μ ↔ convolution_exists_at f g x L μ :=
+by simp_rw [convolution_exists_at, ← integrable_comp_sub_left (λ t, L (f t) (g (x - t))) x,
+  sub_sub_cancel, flip_apply]
+
+lemma convolution_exists_at.integrable_swap (h : convolution_exists_at f g x L μ) :
+  integrable (λ t, L (f (x - t)) (g t)) μ :=
+by { convert h.comp_sub_left x, simp_rw [sub_sub_self] }
+
+lemma convolution_exists_at_iff_integrable_swap :
+  convolution_exists_at f g x L μ ↔ integrable (λ t, L (f (x - t)) (g t)) μ :=
+convolution_exists_at_flip.symm
+
+end measurable_group
+
+variables [topological_space G] [topological_add_group G] [borel_space G]
+  [second_countable_topology G] [is_add_left_invariant μ] [is_neg_invariant μ]
+  [sigma_compact_space G]
+
+lemma has_compact_support.convolution_exists_left
+  (hcf : has_compact_support f) (hf : continuous f) (hg : locally_integrable g μ) :
+  convolution_exists f g L μ :=
+λ x₀, convolution_exists_at_flip.mp $ hcf.convolution_exists_right L.flip hg hf x₀
+
+lemma has_compact_support.convolution_exists_right_of_continuous_left
+  (hcg : has_compact_support g) (hf : continuous f) (hg : locally_integrable g μ) :
+  convolution_exists f g L μ :=
+λ x₀, convolution_exists_at_flip.mp $
+  hcg.convolution_exists_left_of_continuous_right L.flip hg hf x₀
+
+end comm_group
+
+end convolution_exists
+
+end measurability
+
+end nondiscrete_normed_field