Module mathcomp.analysis.ftc
From HB Require Import structures.From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint interval finmap.
From mathcomp Require Import mathcomp_extra boolp classical_sets functions.
From mathcomp Require Import cardinality fsbigop .
Require Import signed reals ereal topology normedtype sequences real_interval.
Require Import esum measure lebesgue_measure numfun realfun lebesgue_integral.
Require Import derive.
# Fundamental Theorem of Calculus for the Lebesgue Integral
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Import Order.TTheory GRing.Theory Num.Def Num.Theory.
Import numFieldTopology.Exports.
Local Open Scope classical_set_scope.
Local Open Scope ring_scope.
Section FTC.
Context {R : realType}.
Notation mu := lebesgue_measure.
Local Open Scope ereal_scope.
Implicit Types (f : R -> R) (a : itv_bound R).
Let FTC0 f a : mu.-integrable setT (EFin \o f) ->
let F x := (\int[mu]_(t in [set` Interval a (BRight x)]) f t)%R in
forall x, a < BRight x -> lebesgue_pt f x ->
h^-1 *: (F (h + x) - F x) @[h --> 0%R^'] --> f x.
Proof.
move=> intf F x ax fx.
have locf : locally_integrable setT f.
by apply: integrable_locally => //; exact: openT.
apply: cvg_at_right_left_dnbhs.
- apply/cvg_at_rightP => d [d_gt0 d0].
pose E x n := `[x, x + d n[%classic%R.
have muE y n : mu (E y n) = (d n)%:E.
rewrite /E lebesgue_measure_itv/= lte_fin ltrDl d_gt0.
by rewrite -EFinD addrAC subrr add0r.
have nice_E y : nicely_shrinking y (E y).
split=> [n|]; first exact: measurable_itv.
exists (2, (fun n => PosNum (d_gt0 n))); split => //= [n z|n].
rewrite /E/= in_itv/= /ball/= ltr_distlC => /andP[yz ->].
by rewrite (lt_le_trans _ yz)// ltrBlDr ltrDl.
rewrite (lebesgue_measure_ball _ (ltW _))// -/mu muE -EFinM lee_fin.
by rewrite mulr_natl.
have ixdf n : \int[mu]_(t in [set` Interval a (BRight (x + d n))]) (f t)%:E -
\int[mu]_(t in [set` Interval a (BRight x)]) (f t)%:E =
\int[mu]_(y in E x n) (f y)%:E.
rewrite -[in X in X - _]integral_itv_bndo_bndc//=; last first.
by case: locf => + _ _; exact: measurable_funS.
rewrite (@itv_bndbnd_setU _ _ _ (BLeft x))//=; last 2 first.
by case: a ax F => [[|] a|[|]]// /ltW.
by rewrite bnd_simp lerDl ltW.
rewrite integral_setU_EFin//=.
- rewrite addeAC -[X in _ - X]integral_itv_bndo_bndc//=; last first.
by case: locf => + _ _; exact: measurable_funS.
rewrite subee ?add0e//.
by apply: integral_fune_fin_num => //; exact: integrableS intf.
- by case: locf => + _ _; exact: measurable_funS.
- apply/disj_setPRL => z/=.
rewrite /E /= !in_itv/= => /andP[xz zxdn].
move: a ax {F} => [[|] t/=|[_ /=|//]].
- rewrite lte_fin => tx.
by apply/negP; rewrite negb_and -leNgt xz orbT.
- rewrite lte_fin => tx.
by apply/negP; rewrite negb_and -!leNgt xz orbT.
- by apply/negP; rewrite -leNgt.
rewrite [f in f n @[n --> _] --> _](_ : _ =
fun n => (d n)^-1 *: fine (\int[mu]_(t in E x n) (f t)%:E)); last first.
apply/funext => n; congr (_ *: _); rewrite -fineB/=.
by rewrite /= (addrC (d n) x) ixdf.
by apply: integral_fune_fin_num => //; exact: integrableS intf.
by apply: integral_fune_fin_num => //; exact: integrableS intf.
have := nice_lebesgue_differentiation nice_E locf fx.
rewrite {ixdf} -/mu.
rewrite [g in g n @[n --> _] --> _ -> _](_ : _ =
fun n => (d n)^-1%:E * \int[mu]_(y in E x n) (f y)%:E); last first.
by apply/funext => n; rewrite muE.
move/fine_cvgP => [_ /=].
set g := _ \o _ => gf.
set h := (f in f n @[n --> \oo] --> _).
suff : g = h by move=> <-.
apply/funext => n.
rewrite /g /h /= fineM//.
apply: integral_fune_fin_num => //; first exact: (nice_E _).1.
by apply: integrableS intf => //; exact: (nice_E _).1.
- apply/cvg_at_leftP => d [d_gt0 d0].
have {}Nd_gt0 n : (0 < - d n)%R by rewrite ltrNr oppr0.
pose E x n := `]x + d n, x]%classic%R.
have muE y n : mu (E y n) = (- d n)%:E.
rewrite /E lebesgue_measure_itv/= lte_fin -ltrBrDr.
by rewrite ltrDl Nd_gt0 -EFinD opprD addrA subrr add0r.
have nice_E y : nicely_shrinking y (E y).
split=> [n|]; first exact: measurable_itv.
exists (2, (fun n => PosNum (Nd_gt0 n))); split => //=.
by rewrite -oppr0; exact: cvgN.
move=> n z.
rewrite /E/= in_itv/= /ball/= => /andP[yz zy].
by rewrite ltr_distlC opprK yz /= (le_lt_trans zy)// ltrDl.
move=> n.
rewrite lebesgue_measure_ball//; last exact: ltW.
by rewrite -/mu muE -EFinM lee_fin mulr_natl.
have ixdf : {near \oo,
(fun n => \int[mu]_(t in [set` Interval a (BRight (x + d n))]) (f t)%:E -
\int[mu]_(t in [set` Interval a (BRight x)]) (f t)%:E) =1
(fun n => - \int[mu]_(y in E x n) (f y)%:E)}.
case: a ax {F}; last first.
move=> [_|//].
apply: nearW => n.
rewrite -[in LHS]integral_itv_bndo_bndc//=; last first.
by case: locf => + _ _; exact: measurable_funS.
rewrite -/mu -[LHS]oppeK; congr oppe.
rewrite oppeB; last first.
rewrite fin_num_adde_defl// fin_numN//.
by apply: integral_fune_fin_num => //; exact: integrableS intf.
rewrite addeC.
rewrite (_ : `]-oo, x] = `]-oo, (x + d n)%R] `|` E x n)%classic; last first.
by rewrite -itv_bndbnd_setU//= bnd_simp ler_wnDr// ltW.
rewrite integral_setU_EFin//=.
- rewrite addeAC.
rewrite -[X in X - _]integral_itv_bndo_bndc//; last first.
by case: locf => + _ _; exact: measurable_funS.
rewrite subee ?add0e//.
by apply: integral_fune_fin_num => //; exact: integrableS intf.
- exact: (nice_E _).1.
- by case: locf => + _ _; exact: measurable_funS.
- apply/disj_setPLR => z/=.
rewrite /E /= !in_itv/= leNgt => xdnz.
by apply/negP; rewrite negb_and xdnz.
move=> b a ax.
move/cvgrPdist_le : d0.
move/(_ (x - a)%R); rewrite subr_gt0 => /(_ ax)[m _ /=] h.
near=> n.
have mn : (m <= n)%N by near: n; exists m.
rewrite -[in X in X - _]integral_itv_bndo_bndc//=; last first.
by case: locf => + _ _; exact: measurable_funS.
rewrite -/mu -[LHS]oppeK; congr oppe.
rewrite oppeB; last first.
rewrite fin_num_adde_defl// fin_numN//.
by apply: integral_fune_fin_num => //; exact: integrableS intf.
rewrite addeC.
rewrite (@itv_bndbnd_setU _ _ _ (BRight (x - - d n)%R))//; last 2 first.
case: b in ax * => /=; rewrite bnd_simp.
rewrite lerBrDl addrC -lerBrDl.
by have := h _ mn; rewrite sub0r gtr0_norm.
rewrite lerBrDl -lerBrDr.
by have := h _ mn; rewrite sub0r gtr0_norm.
by rewrite opprK bnd_simp -lerBrDl subrr ltW.
rewrite integral_setU_EFin//=.
- rewrite addeAC -[X in X - _]integral_itv_bndo_bndc//; last first.
by case: locf => + _ _; exact: measurable_funS.
rewrite opprK subee ?add0e//.
by apply: integral_fune_fin_num => //; exact: integrableS intf.
- by case: locf => + _ _; exact: measurable_funS.
- apply/disj_setPLR => z/=.
rewrite /E /= !in_itv/= => /andP[az zxdn].
by apply/negP; rewrite negb_and -leNgt zxdn.
suff: ((d n)^-1 * - fine (\int[mu]_(y in E x n) (f y)%:E))%R
@[n --> \oo] --> f x.
apply: cvg_trans; apply: near_eq_cvg; near=> n; congr (_ *: _).
rewrite /F/= /Rintegral -fineN -fineB; last 2 first.
by apply: integral_fune_fin_num => //; exact: integrableS intf.
by apply: integral_fune_fin_num => //; exact: integrableS intf.
by congr fine => /=; apply/esym; rewrite (addrC _ x); near: n.
have := nice_lebesgue_differentiation nice_E locf fx.
rewrite {ixdf} -/mu.
move/fine_cvgP => [_ /=].
set g := _ \o _ => gf.
rewrite (@eq_cvg _ _ _ _ g)// => n.
rewrite /g /= fineM//=; last first.
apply: integral_fune_fin_num => //; first exact: (nice_E _).1.
by apply: integrableS intf => //; exact: (nice_E _).1.
by rewrite muE/= invrN mulNr -mulrN.
Unshelve. all: by end_near. Qed.
have locf : locally_integrable setT f.
by apply: integrable_locally => //; exact: openT.
apply: cvg_at_right_left_dnbhs.
- apply/cvg_at_rightP => d [d_gt0 d0].
pose E x n := `[x, x + d n[%classic%R.
have muE y n : mu (E y n) = (d n)%:E.
rewrite /E lebesgue_measure_itv/= lte_fin ltrDl d_gt0.
by rewrite -EFinD addrAC subrr add0r.
have nice_E y : nicely_shrinking y (E y).
split=> [n|]; first exact: measurable_itv.
exists (2, (fun n => PosNum (d_gt0 n))); split => //= [n z|n].
rewrite /E/= in_itv/= /ball/= ltr_distlC => /andP[yz ->].
by rewrite (lt_le_trans _ yz)// ltrBlDr ltrDl.
rewrite (lebesgue_measure_ball _ (ltW _))// -/mu muE -EFinM lee_fin.
by rewrite mulr_natl.
have ixdf n : \int[mu]_(t in [set` Interval a (BRight (x + d n))]) (f t)%:E -
\int[mu]_(t in [set` Interval a (BRight x)]) (f t)%:E =
\int[mu]_(y in E x n) (f y)%:E.
rewrite -[in X in X - _]integral_itv_bndo_bndc//=; last first.
by case: locf => + _ _; exact: measurable_funS.
rewrite (@itv_bndbnd_setU _ _ _ (BLeft x))//=; last 2 first.
by case: a ax F => [[|] a|[|]]// /ltW.
by rewrite bnd_simp lerDl ltW.
rewrite integral_setU_EFin//=.
- rewrite addeAC -[X in _ - X]integral_itv_bndo_bndc//=; last first.
by case: locf => + _ _; exact: measurable_funS.
rewrite subee ?add0e//.
by apply: integral_fune_fin_num => //; exact: integrableS intf.
- by case: locf => + _ _; exact: measurable_funS.
- apply/disj_setPRL => z/=.
rewrite /E /= !in_itv/= => /andP[xz zxdn].
move: a ax {F} => [[|] t/=|[_ /=|//]].
- rewrite lte_fin => tx.
by apply/negP; rewrite negb_and -leNgt xz orbT.
- rewrite lte_fin => tx.
by apply/negP; rewrite negb_and -!leNgt xz orbT.
- by apply/negP; rewrite -leNgt.
rewrite [f in f n @[n --> _] --> _](_ : _ =
fun n => (d n)^-1 *: fine (\int[mu]_(t in E x n) (f t)%:E)); last first.
apply/funext => n; congr (_ *: _); rewrite -fineB/=.
by rewrite /= (addrC (d n) x) ixdf.
by apply: integral_fune_fin_num => //; exact: integrableS intf.
by apply: integral_fune_fin_num => //; exact: integrableS intf.
have := nice_lebesgue_differentiation nice_E locf fx.
rewrite {ixdf} -/mu.
rewrite [g in g n @[n --> _] --> _ -> _](_ : _ =
fun n => (d n)^-1%:E * \int[mu]_(y in E x n) (f y)%:E); last first.
by apply/funext => n; rewrite muE.
move/fine_cvgP => [_ /=].
set g := _ \o _ => gf.
set h := (f in f n @[n --> \oo] --> _).
suff : g = h by move=> <-.
apply/funext => n.
rewrite /g /h /= fineM//.
apply: integral_fune_fin_num => //; first exact: (nice_E _).1.
by apply: integrableS intf => //; exact: (nice_E _).1.
- apply/cvg_at_leftP => d [d_gt0 d0].
have {}Nd_gt0 n : (0 < - d n)%R by rewrite ltrNr oppr0.
pose E x n := `]x + d n, x]%classic%R.
have muE y n : mu (E y n) = (- d n)%:E.
rewrite /E lebesgue_measure_itv/= lte_fin -ltrBrDr.
by rewrite ltrDl Nd_gt0 -EFinD opprD addrA subrr add0r.
have nice_E y : nicely_shrinking y (E y).
split=> [n|]; first exact: measurable_itv.
exists (2, (fun n => PosNum (Nd_gt0 n))); split => //=.
by rewrite -oppr0; exact: cvgN.
move=> n z.
rewrite /E/= in_itv/= /ball/= => /andP[yz zy].
by rewrite ltr_distlC opprK yz /= (le_lt_trans zy)// ltrDl.
move=> n.
rewrite lebesgue_measure_ball//; last exact: ltW.
by rewrite -/mu muE -EFinM lee_fin mulr_natl.
have ixdf : {near \oo,
(fun n => \int[mu]_(t in [set` Interval a (BRight (x + d n))]) (f t)%:E -
\int[mu]_(t in [set` Interval a (BRight x)]) (f t)%:E) =1
(fun n => - \int[mu]_(y in E x n) (f y)%:E)}.
case: a ax {F}; last first.
move=> [_|//].
apply: nearW => n.
rewrite -[in LHS]integral_itv_bndo_bndc//=; last first.
by case: locf => + _ _; exact: measurable_funS.
rewrite -/mu -[LHS]oppeK; congr oppe.
rewrite oppeB; last first.
rewrite fin_num_adde_defl// fin_numN//.
by apply: integral_fune_fin_num => //; exact: integrableS intf.
rewrite addeC.
rewrite (_ : `]-oo, x] = `]-oo, (x + d n)%R] `|` E x n)%classic; last first.
by rewrite -itv_bndbnd_setU//= bnd_simp ler_wnDr// ltW.
rewrite integral_setU_EFin//=.
- rewrite addeAC.
rewrite -[X in X - _]integral_itv_bndo_bndc//; last first.
by case: locf => + _ _; exact: measurable_funS.
rewrite subee ?add0e//.
by apply: integral_fune_fin_num => //; exact: integrableS intf.
- exact: (nice_E _).1.
- by case: locf => + _ _; exact: measurable_funS.
- apply/disj_setPLR => z/=.
rewrite /E /= !in_itv/= leNgt => xdnz.
by apply/negP; rewrite negb_and xdnz.
move=> b a ax.
move/cvgrPdist_le : d0.
move/(_ (x - a)%R); rewrite subr_gt0 => /(_ ax)[m _ /=] h.
near=> n.
have mn : (m <= n)%N by near: n; exists m.
rewrite -[in X in X - _]integral_itv_bndo_bndc//=; last first.
by case: locf => + _ _; exact: measurable_funS.
rewrite -/mu -[LHS]oppeK; congr oppe.
rewrite oppeB; last first.
rewrite fin_num_adde_defl// fin_numN//.
by apply: integral_fune_fin_num => //; exact: integrableS intf.
rewrite addeC.
rewrite (@itv_bndbnd_setU _ _ _ (BRight (x - - d n)%R))//; last 2 first.
case: b in ax * => /=; rewrite bnd_simp.
rewrite lerBrDl addrC -lerBrDl.
by have := h _ mn; rewrite sub0r gtr0_norm.
rewrite lerBrDl -lerBrDr.
by have := h _ mn; rewrite sub0r gtr0_norm.
by rewrite opprK bnd_simp -lerBrDl subrr ltW.
rewrite integral_setU_EFin//=.
- rewrite addeAC -[X in X - _]integral_itv_bndo_bndc//; last first.
by case: locf => + _ _; exact: measurable_funS.
rewrite opprK subee ?add0e//.
by apply: integral_fune_fin_num => //; exact: integrableS intf.
- by case: locf => + _ _; exact: measurable_funS.
- apply/disj_setPLR => z/=.
rewrite /E /= !in_itv/= => /andP[az zxdn].
by apply/negP; rewrite negb_and -leNgt zxdn.
suff: ((d n)^-1 * - fine (\int[mu]_(y in E x n) (f y)%:E))%R
@[n --> \oo] --> f x.
apply: cvg_trans; apply: near_eq_cvg; near=> n; congr (_ *: _).
rewrite /F/= /Rintegral -fineN -fineB; last 2 first.
by apply: integral_fune_fin_num => //; exact: integrableS intf.
by apply: integral_fune_fin_num => //; exact: integrableS intf.
by congr fine => /=; apply/esym; rewrite (addrC _ x); near: n.
have := nice_lebesgue_differentiation nice_E locf fx.
rewrite {ixdf} -/mu.
move/fine_cvgP => [_ /=].
set g := _ \o _ => gf.
rewrite (@eq_cvg _ _ _ _ g)// => n.
rewrite /g /= fineM//=; last first.
apply: integral_fune_fin_num => //; first exact: (nice_E _).1.
by apply: integrableS intf => //; exact: (nice_E _).1.
by rewrite muE/= invrN mulNr -mulrN.
Unshelve. all: by end_near. Qed.
Lemma FTC1 f a : mu.-integrable setT (EFin \o f) ->
let F x := (\int[mu]_(t in [set` Interval a (BRight x)]) (f t))%R in
forall x, a < BRight x -> lebesgue_pt f x ->
derivable F x 1 /\ F^`() x = f x.
Proof.
move=> intf F x ax fx; split; last first.
by apply/cvg_lim; [exact: Rhausdorff|exact: FTC0].
apply/cvg_ex; exists (f x).
have /= := FTC0 intf ax fx.
set g := (f in f n @[n --> _] --> _ -> _).
set h := (f in _ -> f n @[n --> _] --> _).
suff : g = h by move=> <-.
by apply/funext => y;rewrite /g /h /= [X in F (X + _)](mulr1).
Qed.
by apply/cvg_lim; [exact: Rhausdorff|exact: FTC0].
apply/cvg_ex; exists (f x).
have /= := FTC0 intf ax fx.
set g := (f in f n @[n --> _] --> _ -> _).
set h := (f in _ -> f n @[n --> _] --> _).
suff : g = h by move=> <-.
by apply/funext => y;rewrite /g /h /= [X in F (X + _)](mulr1).
Qed.
Corollary continuous_FTC1 f a : mu.-integrable setT (EFin \o f) ->
let F x := (\int[mu]_(t in [set` Interval a (BRight x)]) (f t))%R in
forall x, a < BRight x -> {for x, continuous f} ->
derivable F x 1 /\ F^`() x = f x.
Proof.
move=> fi F x ax fx.
have lfx : lebesgue_pt f x.
near (0%R:R)^'+ => e.
apply: (@continuous_lebesgue_pt _ _ _ (ball x e)).
- exact: ball_open_nbhs.
- exact: measurable_ball.
- case/integrableP : fi => + _.
by move/EFin_measurable_fun; exact: measurable_funS.
- exact: fx.
have lif : locally_integrable setT f.
by apply: integrable_locally => //; exact: openT.
have /= /(_ ax lfx)/= [dfx f'xE] := @FTC1 f a fi x.
by split; [exact: dfx|rewrite f'xE].
Unshelve. all: by end_near. Qed.
have lfx : lebesgue_pt f x.
near (0%R:R)^'+ => e.
apply: (@continuous_lebesgue_pt _ _ _ (ball x e)).
- exact: ball_open_nbhs.
- exact: measurable_ball.
- case/integrableP : fi => + _.
by move/EFin_measurable_fun; exact: measurable_funS.
- exact: fx.
have lif : locally_integrable setT f.
by apply: integrable_locally => //; exact: openT.
have /= /(_ ax lfx)/= [dfx f'xE] := @FTC1 f a fi x.
by split; [exact: dfx|rewrite f'xE].
Unshelve. all: by end_near. Qed.
End FTC.