From 200dd03fb48b72423587c43147f408ab39d92e01 Mon Sep 17 00:00:00 2001
From: Reynald Affeldt <reynald.affeldt@aist.go.jp>
Date: Tue, 23 Jul 2024 15:21:59 +0900
Subject: [PATCH] a preliminary version of integration by parts

---
 CHANGELOG_UNRELEASED.md |  3 ++
 theories/ftc.v          | 71 +++++++++++++++++++++++++++++++++++++++++
 2 files changed, 74 insertions(+)

diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index 47607e4f96..5ae6f34593 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -91,6 +91,9 @@
     `parameterized_integral_continuous`
   + corollary `continuous_FTC2`
 
+- in `ftc.v`:
+  + lemma `continuous_integration_by_parts`
+
 ### Changed
 
 - in `topology.v`:
diff --git a/theories/ftc.v b/theories/ftc.v
index 38e865a94a..185afdaca9 100644
--- a/theories/ftc.v
+++ b/theories/ftc.v
@@ -536,3 +536,74 @@ exact: integral_fune_fin_num.
 Unshelve. all: by end_near. Qed.
 
 End corollary_FTC1.
+
+Section integration_by_parts.
+Context {R : realType}.
+Notation mu := lebesgue_measure.
+Local Open Scope ereal_scope.
+Implicit Types (F G f g : R -> R) (a b : R).
+
+Lemma integration_by_parts F G f g a b :
+    (a < b)%R ->
+    {in `[a, b], continuous f} -> {in `[a, b], continuous F} ->
+    derivable_oo_continuous_bnd F a b ->
+    {in `]a, b[, F^`() =1 f} ->
+    {in `[a, b], continuous g} -> {in `[a, b], continuous G} ->
+    derivable_oo_continuous_bnd G a b ->
+    {in `]a, b[, G^`() =1 g} ->
+  (\int[mu]_(x in `[a, b]) (F x * g x)%:E = (F b * G b - F a * G a)%:E -
+   \int[mu]_(x in `[a, b]) (f x * G x)%:E).
+Proof.
+move=> ab cf cF Fab Ff cg cG Gab Gg.
+have cfg : {in `[a, b], continuous (f * G + F * g)%R}.
+  move=> z zab.
+  apply: continuousD ; apply: continuousM.
+  exact: cf.
+  exact: cG.
+  exact: cF.
+  exact: cg.
+have FGab : derivable_oo_continuous_bnd (F * G)%R a b.
+  case: Fab => /= abF FFa FFb.
+  case: Gab => /= abG GGa GGb.
+  split => /=.
+  move=> z zab.
+  apply: derivableM.
+  exact: abF.
+  exact: abG.
+  exact: cvgM.
+  exact: cvgM.
+have FGfg : {in `]a, b[, (F * G)^`() =1 f * G + F * g}%R.
+  case: Fab => /= abF FFa FFb.
+  case: Gab => /= abG GGa GGb.
+  move=> z zb.
+  rewrite derive1E deriveM; last 2 first.
+    exact: abF.
+    exact: abG.
+  by rewrite -derive1E Gg// -derive1E Ff// addrC (mulrC f).
+have := continuous_FTC2 ab cfg FGab FGfg.
+rewrite -EFinB => <-.
+under [X in _ = X - _]eq_integral do rewrite EFinD.
+rewrite /= integralD//=; last 2 first.
+  apply: continuous_compact_integrable => //.
+  exact: segment_compact.
+  apply: continuous_in_subspaceT => z /[!inE] zab.
+  apply: continuousM.
+  exact: cf.
+  exact: cG.
+  apply: continuous_compact_integrable => //.
+  exact: segment_compact.
+  apply: continuous_in_subspaceT => z /[!inE] zab.
+  apply: continuousM.
+  exact: cF.
+  exact: cg.
+rewrite addeAC subee ?add0e//.
+apply: integral_fune_fin_num => //=.
+apply: continuous_compact_integrable => //.
+exact: segment_compact.
+apply: continuous_in_subspaceT => z /[!inE] zab.
+apply: continuousM.
+exact: cf.
+exact: cG.
+Qed.
+
+End integration_by_parts.