feat(MeasureTheory.Integral.Bochner): drop completeness requirement f…

…rom the definition (#5910)

The notion of Bochner integral of a function taking values in a normed space `E` requires that `E` is complete. This means that whenever we write down an integral, the term contains the assertion that `E` is complete.

In this PR, we remove the completeness requirement from the definition, using the junk value `0` when the space is not complete. Mathematically this does not make any difference, as all reasonable applications will be with a complete `E`. But it means that terms involving integrals become a little bit simpler and that completeness will not have to be checked by the system when applying a bunch of basic lemmas on integrals.

Mathlib/Analysis/Convolution.lean

@@ -471,7 +471,7 @@ theorem convolution_lsmul [Sub G] {f : G → 𝕜} {g : G → F} :
 #align convolution_lsmul convolution_lsmul
 
 /-- The definition of convolution where the bilinear operator is multiplication. -/
-theorem convolution_mul [Sub G] [NormedSpace ℝ 𝕜] [CompleteSpace 𝕜] {f : G → 𝕜} {g : G → 𝕜} :
+theorem convolution_mul [Sub G] [NormedSpace ℝ 𝕜] {f : G → 𝕜} {g : G → 𝕜} :
     (f ⋆[mul 𝕜 𝕜, μ] g) x = ∫ t, f t * g (x - t) ∂μ :=
   rfl
 #align convolution_mul convolution_mul
@@ -793,7 +793,7 @@ theorem convolution_lsmul_swap {f : G → 𝕜} {g : G → F} :
 #align convolution_lsmul_swap convolution_lsmul_swap
 
 /-- The symmetric definition of convolution where the bilinear operator is multiplication. -/
-theorem convolution_mul_swap [NormedSpace ℝ 𝕜] [CompleteSpace 𝕜] {f : G → 𝕜} {g : G → 𝕜} :
+theorem convolution_mul_swap [NormedSpace ℝ 𝕜] {f : G → 𝕜} {g : G → 𝕜} :
     (f ⋆[mul 𝕜 𝕜, μ] g) x = ∫ t, f (x - t) * g t ∂μ :=
   convolution_eq_swap _
 #align convolution_mul_swap convolution_mul_swap

Mathlib/Analysis/Fourier/FourierTransform.lean

@@ -73,8 +73,6 @@ variable {𝕜 : Type _} [CommRing 𝕜] {V : Type _} [AddCommGroup V] [Module 
 
 section Defs
 
-variable [CompleteSpace E]
-
 /-- The Fourier transform integral for `f : V → E`, with respect to a bilinear form `L : V × W → 𝕜`
 and an additive character `e`. -/
 def fourierIntegral (e : Multiplicative 𝕜 →* 𝕊) (μ : Measure V) (L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜) (f : V → E)
@@ -249,7 +247,7 @@ theorem continuous_fourierChar : Continuous Real.fourierChar :=
   (map_continuous expMapCircle).comp (continuous_const.mul continuous_toAdd)
 #align real.continuous_fourier_char Real.continuous_fourierChar
 
-variable {E : Type _} [NormedAddCommGroup E] [CompleteSpace E] [NormedSpace ℂ E]
+variable {E : Type _} [NormedAddCommGroup E] [NormedSpace ℂ E]
 
 theorem vector_fourierIntegral_eq_integral_exp_smul {V : Type _} [AddCommGroup V] [Module ℝ V]
     [MeasurableSpace V] {W : Type _} [AddCommGroup W] [Module ℝ W] (L : V →ₗ[ℝ] W →ₗ[ℝ] ℝ)
@@ -272,8 +270,8 @@ theorem fourierIntegral_def (f : ℝ → E) (w : ℝ) :
 
 scoped[FourierTransform] notation "𝓕" => Real.fourierIntegral
 
-theorem fourierIntegral_eq_integral_exp_smul {E : Type _} [NormedAddCommGroup E] [CompleteSpace E]
-    [NormedSpace ℂ E] (f : ℝ → E) (w : ℝ) :
+theorem fourierIntegral_eq_integral_exp_smul {E : Type _} [NormedAddCommGroup E] [NormedSpace ℂ E]
+    (f : ℝ → E) (w : ℝ) :
     𝓕 f w = ∫ v : ℝ, Complex.exp (↑(-2 * π * v * w) * Complex.I) • f v := by
   simp_rw [fourierIntegral_def, Real.fourierChar_apply, mul_neg, neg_mul, mul_assoc]
 #align real.fourier_integral_eq_integral_exp_smul Real.fourierIntegral_eq_integral_exp_smul

Mathlib/Analysis/Fourier/RiemannLebesgueLemma.lean

@@ -100,7 +100,7 @@ theorem fourier_integral_half_period_translate {w : V} (hw : w ≠ 0) :
   -- rw [integral_add_right_eq_self (fun (x : V) ↦ -(e[-⟪x, w⟫]) • f x)
   --       ((fun w ↦ (1 / (2 * ‖w‖ ^ (2 : ℕ))) • w) w)]
   -- Unfortunately now we need to specify `volume`, and call `dsimp`.
-  have := @integral_add_right_eq_self _ _ _ _ _ _ volume _ _ _ (fun (x : V) ↦ -(e[-⟪x, w⟫]) • f x)
+  have := @integral_add_right_eq_self _ _ _ _ _ volume _ _ _ (fun (x : V) ↦ -(e[-⟪x, w⟫]) • f x)
     ((fun w ↦ (1 / (2 * ‖w‖ ^ (2 : ℕ))) • w) w)
   erw [this] -- Porting note, we can avoid `erw` by first calling `dsimp at this ⊢`.
   simp only [neg_smul, integral_neg]

Mathlib/Analysis/SpecialFunctions/Gamma/Beta.lean

@@ -272,7 +272,7 @@ theorem GammaSeq_eq_approx_Gamma_integral {s : ℂ} (hs : 0 < re s) {n : ℕ} (h
   have : ∀ x : ℝ, x = x / n * n := by intro x; rw [div_mul_cancel]; exact Nat.cast_ne_zero.mpr hn
   conv_rhs => enter [1, x, 2, 1]; rw [this x]
   rw [GammaSeq_eq_betaIntegral_of_re_pos hs]
-  have := @intervalIntegral.integral_comp_div _ _ _ _ 0 n _
+  have := intervalIntegral.integral_comp_div (a := 0) (b := n)
     (fun x => ↑((1 - x) ^ n) * ↑(x * ↑n) ^ (s - 1) : ℝ → ℂ) (Nat.cast_ne_zero.mpr hn)
   dsimp only at this
   rw [betaIntegral, this, real_smul, zero_div, div_self, add_sub_cancel,

Mathlib/Analysis/SpecialFunctions/Gaussian.lean

@@ -299,8 +299,8 @@ theorem integral_gaussian_complex_Ioi {b : ℂ} (hb : 0 < re b) :
   have : ∀ c : ℝ, ∫ x in (0 : ℝ)..c, cexp (-b * (x : ℂ) ^ 2) =
       ∫ x in -c..0, cexp (-b * (x : ℂ) ^ 2) := by
     intro c
-    have :=
-      @intervalIntegral.integral_comp_sub_left _ _ _ _ 0 c (fun x => cexp (-b * (x : ℂ) ^ 2)) 0
+    have := intervalIntegral.integral_comp_sub_left (a := 0) (b := c)
+      (fun x => cexp (-b * (x : ℂ) ^ 2)) 0
     simpa [zero_sub, neg_sq, neg_zero] using this
   have t1 :=
     intervalIntegral_tendsto_integral_Ioi 0 (integrable_cexp_neg_mul_sq hb).integrableOn tendsto_id