feat(analysis/convolution): integral of a convolution over positive r…

…eals (#18353)

This PR generalises `integral_convolution` to consider convolutions of functions on the positive real line. (This will be used in a follow-up PR to relate the gamma and beta functions).

src/analysis/convolution.lean

@@ -6,6 +6,7 @@ Authors: Floris van Doorn
 import measure_theory.group.integration
 import measure_theory.group.prod
 import measure_theory.function.locally_integrable
+import measure_theory.integral.interval_integral
 import analysis.calculus.specific_functions
 import analysis.calculus.parametric_integral
 
@@ -1562,3 +1563,75 @@ lemma has_compact_support.cont_diff_convolution_left [μ.is_add_left_invariant]
 by { rw [← convolution_flip], exact hcf.cont_diff_convolution_right L.flip hg hf }
 
 end with_param
+
+section nonneg
+
+variables [normed_space ℝ E] [normed_space ℝ E'] [normed_space ℝ F] [complete_space F]
+
+/-- The forward convolution of two functions `f` and `g` on `ℝ`, with respect to a continuous
+bilinear map `L` and measure `ν`. It is defined to be the function mapping `x` to
+`∫ t in 0..x, L (f t) (g (x - t)) ∂ν` if `0 < x`, and 0 otherwise. -/
+noncomputable def pos_convolution
+  (f : ℝ → E) (g : ℝ → E') (L : E →L[ℝ] E' →L[ℝ] F) (ν : measure ℝ . volume_tac) : ℝ → F :=
+indicator (Ioi (0:ℝ)) (λ x, ∫ t in 0..x, L (f t) (g (x - t)) ∂ν)
+
+lemma pos_convolution_eq_convolution_indicator
+  (f : ℝ → E) (g : ℝ → E') (L : E →L[ℝ] E' →L[ℝ] F) (ν : measure ℝ . volume_tac) [has_no_atoms ν] :
+  pos_convolution f g L ν = convolution (indicator (Ioi 0) f) (indicator (Ioi 0) g) L ν :=
+begin
+  ext1 x,
+  rw [convolution, pos_convolution, indicator],
+  split_ifs,
+  { rw [interval_integral.integral_of_le (le_of_lt h),
+      integral_Ioc_eq_integral_Ioo,
+      ←integral_indicator (measurable_set_Ioo : measurable_set (Ioo 0 x))],
+    congr' 1 with t : 1,
+    have : (t ≤ 0) ∨ (t ∈ Ioo 0 x) ∨ (x ≤ t),
+    { rcases le_or_lt t 0 with h | h,
+      { exact or.inl h },
+      { rcases lt_or_le t x with h' | h',
+        exacts [or.inr (or.inl ⟨h, h'⟩), or.inr (or.inr h')] } },
+    rcases this with ht|ht|ht,
+    { rw [indicator_of_not_mem (not_mem_Ioo_of_le ht), indicator_of_not_mem (not_mem_Ioi.mpr ht),
+        continuous_linear_map.map_zero, continuous_linear_map.zero_apply] },
+    { rw [indicator_of_mem ht, indicator_of_mem (mem_Ioi.mpr ht.1),
+        indicator_of_mem (mem_Ioi.mpr $ sub_pos.mpr ht.2)] },
+    { rw [indicator_of_not_mem (not_mem_Ioo_of_ge ht),
+        indicator_of_not_mem (not_mem_Ioi.mpr (sub_nonpos_of_le ht)),
+        continuous_linear_map.map_zero] } },
+  { convert (integral_zero ℝ F).symm,
+    ext1 t,
+    by_cases ht : 0 < t,
+    { rw [indicator_of_not_mem (_ : x - t ∉ Ioi 0), continuous_linear_map.map_zero],
+      rw not_mem_Ioi at h ⊢,
+      exact sub_nonpos.mpr (h.trans ht.le) },
+    { rw [indicator_of_not_mem (mem_Ioi.not.mpr ht), continuous_linear_map.map_zero,
+        continuous_linear_map.zero_apply] } }
+end
+
+lemma integrable_pos_convolution {f : ℝ → E} {g : ℝ → E'} {μ ν : measure ℝ}
+  [sigma_finite μ] [sigma_finite ν] [is_add_right_invariant μ] [has_no_atoms ν]
+  (hf : integrable_on f (Ioi 0) ν) (hg : integrable_on g (Ioi 0) μ) (L : E →L[ℝ] E' →L[ℝ] F) :
+  integrable (pos_convolution f g L ν) μ :=
+begin
+  rw ←integrable_indicator_iff (measurable_set_Ioi : measurable_set (Ioi (0:ℝ))) at hf hg,
+  rw pos_convolution_eq_convolution_indicator f g L ν,
+  exact (hf.convolution_integrand L hg).integral_prod_left,
+end
+
+/-- The integral over `Ioi 0` of a forward convolution of two functions is equal to the product
+of their integrals over this set. (Compare `integral_convolution` for the two-sided convolution.) -/
+lemma integral_pos_convolution [complete_space E] [complete_space E'] {μ ν : measure ℝ}
+  [sigma_finite μ] [sigma_finite ν] [is_add_right_invariant μ] [has_no_atoms ν]
+  {f : ℝ → E} {g : ℝ → E'} (hf : integrable_on f (Ioi 0) ν)
+  (hg : integrable_on g (Ioi 0) μ) (L : E →L[ℝ] E' →L[ℝ] F)  :
+  ∫ x:ℝ in Ioi 0, (∫ t:ℝ in 0..x, L (f t) (g (x - t)) ∂ν) ∂μ =
+    L (∫ x:ℝ in Ioi 0, f x ∂ν) (∫ x:ℝ in Ioi 0, g x ∂μ) :=
+begin
+  rw ←integrable_indicator_iff (measurable_set_Ioi : measurable_set (Ioi (0:ℝ))) at hf hg,
+  simp_rw ←integral_indicator measurable_set_Ioi,
+  convert integral_convolution L hf hg using 2,
+  apply pos_convolution_eq_convolution_indicator,
+end
+
+end nonneg