Skip to content

Commit 949b179

Browse files
IshiguroYoshihiroIshiguroYoshihiro
committed
integration_by_party
1 parent d8087fd commit 949b179

File tree

2 files changed

+326
-0
lines changed

2 files changed

+326
-0
lines changed

‎CHANGELOG_UNRELEASED.md‎

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -102,6 +102,12 @@
102102
- in `lebesgue_integral_nonneg.v`:
103103
+ lemma `ge0_integral_ereal_sup` (was a `Let`)
104104

105+
- in `ftc.v`:
106+
+ lemmas `integration_by_partsy_ge0_ge0`,
107+
`integration_by_partsy_le0_ge0`,
108+
`integration_by_partsy_le0_le0`,
109+
`integration_by_partsy_ge0_le0`
110+
105111
### Changed
106112

107113
- in `convex.v`:

‎theories/ftc.v‎

Lines changed: 320 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -836,6 +836,326 @@ Qed.
836836

837837
End integration_by_parts.
838838

839+
(* PR#1656 *)
840+
Lemma derivable_oy_continuous_within_itvcy {R : numFieldType}
841+
{V : normedModType R} (f : R -> V) (x : R) :
842+
derivable_oy_continuous_bnd f x -> {within `[x, +oo[, continuous f}.
843+
Proof.
844+
Admitted.
845+
846+
(* #PR1656 *)
847+
Lemma derivable_oy_continuous_bndW_oo {R : numFieldType} {V : normedModType R}
848+
(a c d : R) (f : R -> V) :
849+
(c < d) ->
850+
(a <= c) ->
851+
derivable_oy_continuous_bnd f a ->
852+
derivable_oo_continuous_bnd f c d.
853+
Proof.
854+
Admitted.
855+
856+
(* PR#1662 *)
857+
Lemma measurable_fun_itv_bndo_bndcP {R : realType} (a : itv_bound R) (b : R)
858+
(f : R -> R) :
859+
measurable_fun [set` Interval a (BLeft b)] f <->
860+
measurable_fun [set` Interval a (BRight b)] f.
861+
Proof.
862+
Admitted.
863+
864+
(* PR#1662 *)
865+
Lemma measurable_fun_itv_obnd_cbndP {R : realType} (a : R) (b : itv_bound R)
866+
(f : R -> R) :
867+
measurable_fun [set` Interval (BRight a) b] f <->
868+
measurable_fun [set` Interval (BLeft a) b] f.
869+
Proof.
870+
Admitted.
871+
872+
Section integration_by_partsy_ge0.
873+
Context {R : realType}.
874+
Notation mu := lebesgue_measure.
875+
Local Open Scope ereal_scope.
876+
Local Open Scope classical_set_scope.
877+
878+
Let itvSay {a : R} {n m} {b0 b1 : bool} :
879+
[set` Interval (BSide b0 (a + n%:R)) (BSide b1 (a + m%:R))] `<=`
880+
[set` Interval (BSide b0 a) (BInfty _ false)].
881+
Proof.
882+
move=> x/=; rewrite 2!in_itv/= andbT => /andP[+ _].
883+
by case: b0 => /= H; [apply: le_trans H|apply: le_lt_trans H]; rewrite lerDl.
884+
Qed.
885+
886+
Variables (F G f g : R -> R^o) (a FGoo : R).
887+
Hypothesis cf : {within `[a, +oo[, continuous f}.
888+
Hypothesis Foy : derivable_oy_continuous_bnd F a.
889+
Hypothesis Ff : {in `]a, +oo[%R, F^`() =1 f}.
890+
Hypothesis cg : {within `[a, +oo[, continuous g}.
891+
Hypothesis Goy : derivable_oy_continuous_bnd G a.
892+
Hypothesis Gg : {in `]a, +oo[%R, G^`() =1 g}.
893+
Hypothesis cvgFG : (F \* G)%R x @[x --> +oo%R] --> FGoo.
894+
895+
Let mFg : measurable_fun `]a, +oo[ (fun x => (F x * g x)%R).
896+
Proof.
897+
apply: (@measurable_funS _ _ _ _ `[a, +oo[) => //.
898+
by apply: subset_itvr; rewrite bnd_simp.
899+
apply: measurable_funM; apply: subspace_continuous_measurable_fun => //.
900+
exact: (@derivable_oy_continuous_within_itvcy _ R^o).
901+
Qed.
902+
903+
Let cfG : {within `[a, +oo[, continuous (fun x => (f x * G x)%R)}.
904+
Proof.
905+
have/continuous_within_itvcyP[aycf cfa] := cf.
906+
have/derivable_oy_continuous_within_itvcy/continuous_within_itvcyP[] := Goy.
907+
move=> aycG cGa.
908+
apply/continuous_within_itvcyP; split; last exact: cvgM.
909+
move=> x ax; apply: continuousM; first exact: aycf.
910+
exact: aycG.
911+
Qed.
912+
913+
Let mfG : measurable_fun `]a, +oo[ (fun x => (f x * G x)%R).
914+
Proof.
915+
apply/measurable_fun_itv_obnd_cbndP.
916+
exact: subspace_continuous_measurable_fun.
917+
Qed.
918+
919+
Let Ffai i : {in `]a + i%:R, a + i.+1%:R[%R, F^`() =1 f}.
920+
Proof. exact/(in1_subset_itv _ Ff)/itvSay. Qed.
921+
922+
Let Ggai i : {in `]a + i%:R, a + i.+1%:R[%R, G^`() =1 g}.
923+
Proof. exact/(in1_subset_itv _ Gg)/itvSay. Qed.
924+
925+
Let integral_sum_lim :
926+
\big[+%R/0%R]_(0 <= i <oo)
927+
\int[mu]_(x in seqDU (fun k : nat => `]a, (a + k%:R)]) i) (F x * g x)%:E
928+
= (limn (fun n => ((F (a + n.-1%:R) * G (a + n.-1%:R) - F a * G a)%:E
929+
+ \big[+%R/0%R]_(0 <= i < n) - \int[mu]_(x in
930+
seqDU (fun k : nat => `]a, (a + k%:R)]) i) (f x * G x)%:E))).
931+
Proof.
932+
apply: congr_lim.
933+
apply/funext => n.
934+
case: n.
935+
by rewrite big_nat_cond [in RHS]big_nat_cond 2?big_pred0//= 2!addr0 subrr.
936+
case.
937+
rewrite 2!big_nat1 seqDUE -pred_Sn addr0 subrr add0r.
938+
by rewrite set_itvoc0 2!integral_set0 oppe0.
939+
move=> n.
940+
rewrite big_nat_recl// [in RHS]big_nat_recl//=.
941+
rewrite seqDUE/= addr0 set_itvoc0 2!integral_set0 oppe0 2!add0r.
942+
have subset_ai_ay (b b' : bool) i :
943+
[set` Interval (BSide b (a + i%:R)) (BSide b' (a + i.+1%:R))] `<=`
944+
[set` Interval (BSide b a) (BInfty _ false)].
945+
by apply/subitvP; rewrite subitvE bnd_simp; rewrite ?ler_wpDr.
946+
under eq_bigr => i _.
947+
rewrite seqDUE/= integral_itv_obnd_cbnd; last first.
948+
exact: (@measurable_funS _ _ _ _ `]a, +oo[).
949+
rewrite (integration_by_parts _ _ _ (@Ffai i) _ _ (@Ggai i)); last 5 first.
950+
- by rewrite ltrD2l ltr_nat.
951+
- exact: continuous_subspaceW cf.
952+
- apply: derivable_oy_continuous_bndW_oo Foy.
953+
+ by rewrite ltrD2l ltr_nat.
954+
+ by rewrite lerDl.
955+
- exact: continuous_subspaceW cg.
956+
- apply: derivable_oy_continuous_bndW_oo Goy.
957+
+ by rewrite ltrD2l ltr_nat.
958+
+ by rewrite lerDl.
959+
over.
960+
rewrite big_split/=.
961+
under eq_bigr do rewrite EFinB.
962+
rewrite telescope_sume// addr0; congr +%E.
963+
apply: eq_bigr => k _; rewrite seqDUE/= integral_itv_obnd_cbnd//.
964+
exact: measurable_funS mfG.
965+
Qed.
966+
967+
Let FGaoo :
968+
(F (a + x.-1%:R)%E * G (a + x.-1%:R)%E - F a * G a)%:E @[x --> \oo] -->
969+
(FGoo - F a * G a)%:E.
970+
Proof.
971+
apply: cvg_EFin; first exact: nearW; apply: (@cvgB _ R^o); last exact: cvg_cst.
972+
rewrite -cvg_shiftS/=.
973+
apply: (@cvg_comp _ _ _ _ (F \* G)%R _ +oo%R); last exact: cvgFG; apply/cvgeryP.
974+
apply: (@cvge_pinftyP R (fun x => (a + x)%:E) +oo).1; last exact: cvgr_idn.
975+
by apply/cvgeryP; exact: cvg_addrl.
976+
Qed.
977+
978+
Let sumN_Nsum_fG n :
979+
(\sum_(0 <= i < n)
980+
(- (\int[mu]_(x in seqDU (fun k : nat => `]a, (a + k%:R)]%classic) i)
981+
(f x * G x)%:E))%E)%R =
982+
- (\sum_(0 <= i < n)
983+
(\int[mu]_(x in seqDU (fun k : nat => `]a, (a + k%:R)]%classic) i)
984+
(f x * G x)%:E)%E)%R.
985+
Proof.
986+
rewrite big_nat_cond fin_num_sumeN; rewrite -?big_nat_cond//; move=> m _.
987+
rewrite seqDUE integral_itv_obnd_cbnd; last exact: measurable_funS mfG.
988+
apply: integral_fune_fin_num => //=.
989+
apply: continuous_compact_integrable; first exact: segment_compact.
990+
exact: continuous_subspaceW cfG.
991+
Qed.
992+
993+
Let sumNint_sumintN_fG n :
994+
(\sum_(0 <= i < n)
995+
(- (\int[mu]_(x in seqDU (fun k : nat => `]a, (a + k%:R)]%classic) i)
996+
(f x * G x)%:E))%E)%R =
997+
\sum_(0 <= i < n)
998+
(\int[mu]_(x in seqDU (fun k : nat => `]a, (a + k%:R)]%classic) i)
999+
(- (f x * G x))%:E)%E.
1000+
Proof.
1001+
rewrite big_nat_cond [RHS]big_nat_cond.
1002+
apply: eq_bigr => i.
1003+
rewrite seqDUE andbT => i0n.
1004+
rewrite 2?integral_itv_obnd_cbnd; last exact: measurable_funS mfG; last first.
1005+
apply: measurableT_comp => //.
1006+
exact: measurable_funS mfG.
1007+
rewrite -integralN ?integrable_add_def ?continuous_compact_integrable//.
1008+
exact: segment_compact.
1009+
exact: continuous_subspaceW cfG.
1010+
Qed.
1011+
1012+
Lemma integration_by_partsy_ge0_ge0 :
1013+
{in `]a, +oo[, forall x, 0 <= (f x * G x)%:E} ->
1014+
{in `]a, +oo[, forall x, 0 <= (F x * g x)%:E} ->
1015+
\int[mu]_(x in `[a, +oo[) (F x * g x)%:E = (FGoo - F a * G a)%:E -
1016+
\int[mu]_(x in `[a, +oo[) (f x * G x)%:E.
1017+
Proof.
1018+
move=> fG0 Fg0.
1019+
rewrite -integral_itv_obnd_cbnd// -[in RHS]integral_itv_obnd_cbnd//.
1020+
rewrite itv_bndy_bigcup_BRight seqDU_bigcup_eq.
1021+
rewrite 2?ge0_integral_bigcup//= -?seqDU_bigcup_eq -?itv_bndy_bigcup_BRight;
1022+
last 6 first.
1023+
- by move=> k; apply: measurableD => //; apply: bigsetU_measurable.
1024+
- exact/measurable_EFinP.
1025+
- by move=> ? ?; rewrite fG0// inE.
1026+
- by move=> k; apply: measurableD => //; apply: bigsetU_measurable.
1027+
- exact/measurable_EFinP.
1028+
- by move=> ? ?; rewrite Fg0// inE.
1029+
rewrite integral_sum_lim; apply/cvg_lim => //.
1030+
apply: cvgeD; first exact: fin_num_adde_defr; first exact: FGaoo.
1031+
under eq_cvg do rewrite sumN_Nsum_fG; apply: cvgeN.
1032+
apply: is_cvg_nneseries_cond => n _ _; apply: integral_ge0 => x.
1033+
by rewrite seqDUE => anx; apply: fG0; rewrite inE/=; exact/itvSay/anx.
1034+
Qed.
1035+
1036+
Lemma integration_by_partsy_le0_ge0 :
1037+
{in `]a, +oo[, forall x, (f x * G x)%:E <= 0} ->
1038+
{in `]a, +oo[, forall x, 0 <= (F x * g x)%:E} ->
1039+
\int[mu]_(x in `[a, +oo[) (F x * g x)%:E = (FGoo - F a * G a)%:E +
1040+
\int[mu]_(x in `[a, +oo[) (- (f x * G x)%:E).
1041+
Proof.
1042+
move=> fG0 Fg0.
1043+
have mMfG : measurable_fun `]a, +oo[ (fun x => (- (f x * G x))%R).
1044+
exact: measurableT_comp.
1045+
rewrite -integral_itv_obnd_cbnd// -[in RHS]integral_itv_obnd_cbnd//.
1046+
rewrite itv_bndy_bigcup_BRight seqDU_bigcup_eq.
1047+
rewrite 2?ge0_integral_bigcup//= -?seqDU_bigcup_eq -?itv_bndy_bigcup_BRight;
1048+
last 6 first.
1049+
- by move=> k; apply: measurableD => //; apply: bigsetU_measurable.
1050+
- by apply/measurable_EFinP; exact: measurableT_comp.
1051+
- by move=> ? ?; rewrite EFinN oppe_ge0 fG0// inE.
1052+
- by move=> k; apply: measurableD => //; apply: bigsetU_measurable.
1053+
- exact/measurable_EFinP.
1054+
- by move=> ? ?; rewrite Fg0// inE.
1055+
rewrite integral_sum_lim; apply/cvg_lim => //.
1056+
apply: cvgeD; first exact: fin_num_adde_defr; first exact: FGaoo.
1057+
under eq_cvg do rewrite sumNint_sumintN_fG.
1058+
apply: is_cvg_nneseries_cond => n _ _; apply: integral_ge0 => x.
1059+
rewrite seqDUE => anx; rewrite EFinN oppe_ge0.
1060+
apply: fG0; rewrite inE/=; exact/itvSay/anx.
1061+
Qed.
1062+
1063+
End integration_by_partsy_ge0.
1064+
1065+
Section integration_by_partsy_le0.
1066+
Context {R: realType}.
1067+
Notation mu := lebesgue_measure.
1068+
Local Open Scope ereal_scope.
1069+
Local Open Scope classical_set_scope.
1070+
1071+
Lemma derivable_oy_continuous_bndN (F : R -> R^o) (a : R) :
1072+
derivable_oy_continuous_bnd F a ->
1073+
derivable_oy_continuous_bnd (- F)%R a.
1074+
Proof.
1075+
Admitted.
1076+
1077+
Variables (F G f g : R -> R^o) (a FGoo : R).
1078+
Hypothesis cf : {within `[a, +oo[, continuous f}.
1079+
Hypothesis Foy : derivable_oy_continuous_bnd F a.
1080+
Hypothesis Ff : {in `]a, +oo[%R, F^`() =1 f}.
1081+
Hypothesis cg : {within `[a, +oo[, continuous g}.
1082+
Hypothesis Goy : derivable_oy_continuous_bnd G a.
1083+
Hypothesis Gg : {in `]a, +oo[%R, G^`() =1 g}.
1084+
Hypothesis cvgFG : (F \* G)%R x @[x --> +oo%R] --> FGoo.
1085+
1086+
Let mFg : measurable_fun `]a, +oo[ (fun x : R => (F x * g x)%R).
1087+
Proof.
1088+
apply: subspace_continuous_measurable_fun => //.
1089+
rewrite continuous_open_subspace// => x ax.
1090+
apply: cvgM.
1091+
have [+ _]:= Foy; move/derivable_within_continuous.
1092+
by rewrite continuous_open_subspace//; apply.
1093+
have /continuous_within_itvcyP[+ _] := cg.
1094+
by apply; rewrite inE/= in ax.
1095+
Qed.
1096+
1097+
Let NintNFg :
1098+
{in `]a, +oo[, forall x, (F x * g x)%:E <= 0} ->
1099+
\int[mu]_(x in `[a, +oo[) (F x * g x)%:E =
1100+
- \int[mu]_(x in `[a, +oo[) (- F x * g x)%:E.
1101+
Proof.
1102+
move=> Fg0.
1103+
rewrite -integral_itv_obnd_cbnd//.
1104+
under eq_integral => x do rewrite -(opprK (F x)) mulNr EFinN.
1105+
rewrite integralN/=; last first.
1106+
apply: fin_num_adde_defl.
1107+
apply/EFin_fin_numP; exists 0%R.
1108+
apply/eqe_oppLRP; rewrite oppe0.
1109+
apply:integral0_eq => /= x ax.
1110+
apply: (@ge0_funenegE _ _ `]a, +oo[); last by rewrite inE/=.
1111+
move=> ?/= ?; rewrite mulNr EFinN oppe_ge0 Fg0//=.
1112+
by rewrite inE/=.
1113+
rewrite integral_itv_obnd_cbnd//.
1114+
under [X in _ _ X]eq_fun do rewrite mulNr; exact: measurableT_comp.
1115+
Qed.
1116+
1117+
Lemma integration_by_partsy_le0_le0 :
1118+
{in `]a, +oo[, forall x, (f x * G x)%:E <= 0} ->
1119+
{in `]a, +oo[, forall x, (F x * g x)%:E <= 0} ->
1120+
\int[mu]_(x in `[a, +oo[) (F x * g x)%:E = (FGoo - F a * G a)%:E +
1121+
\int[mu]_(x in `[a, +oo[) (- (f x * G x)%:E).
1122+
Proof.
1123+
move=> fG0 Fg0.
1124+
rewrite NintNFg//.
1125+
rewrite (@integration_by_partsy_ge0_ge0 R (- F)%R G (- f)%R g a (- FGoo))//; last 6 first.
1126+
- by move=> ?; apply: cvgN; exact: cf.
1127+
- exact: derivable_oy_continuous_bndN.
1128+
- by move=> ? ?; rewrite fctE derive1N ?Ff//; move: Foy => [+ _]; apply.
1129+
- by under eq_cvg do rewrite fctE/= mulNr; apply: cvgN.
1130+
- by move=> ? ?; rewrite mulNr EFinN oppe_ge0; apply: fG0.
1131+
- by move=> ? ?; rewrite mulNr EFinN oppe_ge0; apply: Fg0.
1132+
rewrite oppeB; last exact: fin_num_adde_defr.
1133+
rewrite -EFinN opprD 2!opprK mulNr.
1134+
by under eq_integral do rewrite mulNr EFinN.
1135+
Qed.
1136+
1137+
Lemma integration_by_partsy_ge0_le0 :
1138+
{in `]a, +oo[, forall x, 0 <= (f x * G x)%:E} ->
1139+
{in `]a, +oo[, forall x, (F x * g x)%:E <= 0} ->
1140+
\int[mu]_(x in `[a, +oo[) (F x * g x)%:E = (FGoo - F a * G a)%:E -
1141+
\int[mu]_(x in `[a, +oo[) (f x * G x)%:E.
1142+
Proof.
1143+
move=> fG0 Fg0.
1144+
rewrite NintNFg//.
1145+
rewrite (@integration_by_partsy_le0_ge0 R (- F)%R G (- f)%R g a (- FGoo))//; last 6 first.
1146+
- by move=> ?; apply: cvgN; exact: cf.
1147+
- exact: derivable_oy_continuous_bndN.
1148+
- by move=> ? ?; rewrite fctE derive1N ?Ff//; move: Foy => [+ _]; apply.
1149+
- by under eq_cvg do rewrite fctE/= mulNr; apply: cvgN.
1150+
- by move=> ? ?; rewrite mulNr EFinN oppe_le0; apply: fG0.
1151+
- by move=> ? ?; rewrite mulNr EFinN oppe_ge0; apply: Fg0.
1152+
rewrite oppeD; last exact: fin_num_adde_defr.
1153+
rewrite -EFinN opprD 2!opprK mulNr.
1154+
by under eq_integral do rewrite mulNr EFinN oppeK.
1155+
Qed.
1156+
1157+
End integration_by_partsy_le0.
1158+
8391159
Section Rintegration_by_parts.
8401160
Context {R : realType}.
8411161
Notation mu := lebesgue_measure.

0 commit comments

Comments
 (0)