feat: improper integration by parts (#10874)

Co-authored-by: L Lllvvuu <git@llllvvuu.dev>
Co-authored-by: Moritz Firsching <firsching@google.com>
Co-authored-by: L <git@llllvvuu.dev>

Mathlib/MeasureTheory/Integral/FundThmCalculus.lean

@@ -1341,6 +1341,8 @@ section Parts
 
 variable [NormedRing A] [NormedAlgebra ℝ A] [CompleteSpace A]
 
+/-- For improper integrals, see `MeasureTheory.integral_deriv_mul_eq_sub`,
+`MeasureTheory.integral_Ioi_deriv_mul_eq_sub`, and `MeasureTheory.integral_Iic_deriv_mul_eq_sub`. -/
 theorem integral_deriv_mul_eq_sub {u v u' v' : ℝ → A} (hu : ∀ x ∈ uIcc a b, HasDerivAt u (u' x) x)
     (hv : ∀ x ∈ uIcc a b, HasDerivAt v (v' x) x) (hu' : IntervalIntegrable u' volume a b)
     (hv' : IntervalIntegrable v' volume a b) :
@@ -1350,6 +1352,10 @@ theorem integral_deriv_mul_eq_sub {u v u' v' : ℝ → A} (hu : ∀ x ∈ uIcc a
       (hv'.continuousOn_mul (HasDerivAt.continuousOn hu))
 #align interval_integral.integral_deriv_mul_eq_sub intervalIntegral.integral_deriv_mul_eq_sub
 
+/-- **Integration by parts**. For improper integrals, see
+`MeasureTheory.integral_mul_deriv_eq_deriv_mul`,
+`MeasureTheory.integral_Ioi_mul_deriv_eq_deriv_mul`,
+and `MeasureTheory.integral_Iic_mul_deriv_eq_deriv_mul`. -/
 theorem integral_mul_deriv_eq_deriv_mul {u v u' v' : ℝ → A}
     (hu : ∀ x ∈ uIcc a b, HasDerivAt u (u' x) x) (hv : ∀ x ∈ uIcc a b, HasDerivAt v (v' x) x)
     (hu' : IntervalIntegrable u' volume a b) (hv' : IntervalIntegrable v' volume a b) :

Mathlib/MeasureTheory/Integral/IntegralEqImproper.lean

@@ -1054,4 +1054,98 @@ theorem integrableOn_Ioi_comp_mul_right_iff (f : ℝ → E) (c : ℝ) {a : ℝ}
 
 end IoiIntegrability
 
+/-!
+## Integration by parts
+-/
+
+section IntegrationByParts
+
+variable {A : Type*} [NormedRing A] [NormedAlgebra ℝ A] [CompleteSpace A]
+  {a b : ℝ} {a' b' : A} {u : ℝ → A} {v : ℝ → A} {u' : ℝ → A} {v' : ℝ → A}
+
+/-- For finite intervals, see: `intervalIntegral.integral_deriv_mul_eq_sub`. -/
+theorem integral_deriv_mul_eq_sub
+    (hu : ∀ x, HasDerivAt u (u' x) x) (hv : ∀ x, HasDerivAt v (v' x) x)
+    (huv : Integrable (u' * v + u * v'))
+    (h_bot : Tendsto (u * v) atBot (𝓝 a')) (h_top : Tendsto (u * v) atTop (𝓝 b')) :
+    ∫ (x : ℝ), u' x * v x + u x * v' x = b' - a' :=
+  integral_of_hasDerivAt_of_tendsto (fun x ↦ (hu x).mul (hv x)) huv h_bot h_top
+
+/-- **Integration by parts on (-∞, ∞).**
+For finite intervals, see: `intervalIntegral.integral_mul_deriv_eq_deriv_mul`. -/
+theorem integral_mul_deriv_eq_deriv_mul
+    (hu : ∀ x, HasDerivAt u (u' x) x) (hv : ∀ x, HasDerivAt v (v' x) x)
+    (huv' : Integrable (u * v')) (hu'v : Integrable (u' * v))
+    (h_bot : Tendsto (u * v) atBot (𝓝 a')) (h_top : Tendsto (u * v) atTop (𝓝 b')) :
+    ∫ (x : ℝ), u x * v' x = b' - a' - ∫ (x : ℝ), u' x * v x := by
+  rw [Pi.mul_def] at huv' hu'v
+  rw [eq_sub_iff_add_eq, ← integral_add huv' hu'v]
+  simpa only [add_comm] using integral_deriv_mul_eq_sub hu hv (hu'v.add huv') h_bot h_top
+
+-- TODO: also apply `Tendsto _ (𝓝[>] a) (𝓝 a')` generalization to
+-- `integral_Ioi_of_hasDerivAt_of_tendsto` and `integral_Iic_of_hasDerivAt_of_tendsto`
+/-- For finite intervals, see: `intervalIntegral.integral_deriv_mul_eq_sub`. -/
+theorem integral_Ioi_deriv_mul_eq_sub
+    (hu : ∀ x ∈ Ioi a, HasDerivAt u (u' x) x) (hv : ∀ x ∈ Ioi a, HasDerivAt v (v' x) x)
+    (huv : IntegrableOn (u' * v + u * v') (Ioi a))
+    (h_zero : Tendsto (u * v) (𝓝[>] a) (𝓝 a')) (h_infty : Tendsto (u * v) atTop (𝓝 b')) :
+    ∫ (x : ℝ) in Ioi a, u' x * v x + u x * v' x = b' - a' := by
+  rw [← Ici_diff_left] at h_zero
+  let f := Function.update (u * v) a a'
+  have hderiv : ∀ x ∈ Ioi a, HasDerivAt f (u' x * v x + u x * v' x) x := by
+    intro x (hx : a < x)
+    apply ((hu x hx).mul (hv x hx)).congr_of_eventuallyEq
+    filter_upwards [eventually_ne_nhds hx.ne.symm] with y hy
+    exact Function.update_noteq hy a' (u * v)
+  have htendsto : Tendsto f atTop (𝓝 b') := by
+    apply h_infty.congr'
+    filter_upwards [eventually_ne_atTop a] with x hx
+    exact (Function.update_noteq hx a' (u * v)).symm
+  simpa using integral_Ioi_of_hasDerivAt_of_tendsto
+    (continuousWithinAt_update_same.mpr h_zero) hderiv huv htendsto
+
+/-- **Integration by parts on (a, ∞).**
+For finite intervals, see: `intervalIntegral.integral_mul_deriv_eq_deriv_mul`. -/
+theorem integral_Ioi_mul_deriv_eq_deriv_mul
+    (hu : ∀ x ∈ Ioi a, HasDerivAt u (u' x) x) (hv : ∀ x ∈ Ioi a, HasDerivAt v (v' x) x)
+    (huv' : IntegrableOn (u * v') (Ioi a)) (hu'v : IntegrableOn (u' * v) (Ioi a))
+    (h_zero : Tendsto (u * v) (𝓝[>] a) (𝓝 a')) (h_infty : Tendsto (u * v) atTop (𝓝 b')) :
+    ∫ (x : ℝ) in Ioi a, u x * v' x = b' - a' - ∫ (x : ℝ) in Ioi a, u' x * v x := by
+  rw [Pi.mul_def] at huv' hu'v
+  rw [eq_sub_iff_add_eq, ← integral_add huv' hu'v]
+  simpa only [add_comm] using integral_Ioi_deriv_mul_eq_sub hu hv (hu'v.add huv') h_zero h_infty
+
+/-- For finite intervals, see: `intervalIntegral.integral_deriv_mul_eq_sub`. -/
+theorem integral_Iic_deriv_mul_eq_sub
+    (hu : ∀ x ∈ Iio a, HasDerivAt u (u' x) x) (hv : ∀ x ∈ Iio a, HasDerivAt v (v' x) x)
+    (huv : IntegrableOn (u' * v + u * v') (Iic a))
+    (h_zero : Tendsto (u * v) (𝓝[<] a) (𝓝 a')) (h_infty : Tendsto (u * v) atBot (𝓝 b')) :
+    ∫ (x : ℝ) in Iic a, u' x * v x + u x * v' x = a' - b' := by
+  rw [← Iic_diff_right] at h_zero
+  let f := Function.update (u * v) a a'
+  have hderiv : ∀ x ∈ Iio a, HasDerivAt f (u' x * v x + u x * v' x) x := by
+    intro x hx
+    apply ((hu x hx).mul (hv x hx)).congr_of_eventuallyEq
+    filter_upwards [Iio_mem_nhds hx] with x (hx : x < a)
+    exact Function.update_noteq (ne_of_lt hx) a' (u * v)
+  have htendsto : Tendsto f atBot (𝓝 b') := by
+    apply h_infty.congr'
+    filter_upwards [Iio_mem_atBot a] with x (hx : x < a)
+    exact (Function.update_noteq (ne_of_lt hx) a' (u * v)).symm
+  simpa using integral_Iic_of_hasDerivAt_of_tendsto
+    (continuousWithinAt_update_same.mpr h_zero) hderiv huv htendsto
+
+/-- **Integration by parts on (∞, a].**
+For finite intervals, see: `intervalIntegral.integral_mul_deriv_eq_deriv_mul`. -/
+theorem integral_Iic_mul_deriv_eq_deriv_mul
+    (hu : ∀ x ∈ Iio a, HasDerivAt u (u' x) x) (hv : ∀ x ∈ Iio a, HasDerivAt v (v' x) x)
+    (huv' : IntegrableOn (u * v') (Iic a)) (hu'v : IntegrableOn (u' * v) (Iic a))
+    (h_zero : Tendsto (u * v) (𝓝[<] a) (𝓝 a')) (h_infty : Tendsto (u * v) atBot (𝓝 b')) :
+    ∫ (x : ℝ) in Iic a, u x * v' x = a' - b' - ∫ (x : ℝ) in Iic a, u' x * v x := by
+  rw [Pi.mul_def] at huv' hu'v
+  rw [eq_sub_iff_add_eq, ← integral_add huv' hu'v]
+  simpa only [add_comm] using integral_Iic_deriv_mul_eq_sub hu hv (hu'v.add huv') h_zero h_infty
+
+end IntegrationByParts
+
 end MeasureTheory