Lebesgue differentiation theorem and applications (#1065)

* lebesgue differentiation, ftc, lebesgue's density

---------

Co-authored-by: zstone1 <[email protected]>

CHANGELOG_UNRELEASED.md

@@ -10,6 +10,47 @@
 - in `lebesgue_integral.v`
   + lemma `ge0_integralZr`
 - file `function_spaces.v`
+- in `mathcomp_extra.v`
+  + lemma `invf_plt`
+
+- in `set_interval.v`
+  + lemmas `setDitv1r`, `setDitv1l`
+  + lemmas `set_itvxx`, `itv_bndbnd_setU`
+
+- in `reals.v`
+  + lemma `abs_ceil_ge`
+
+- in `topology.v`:
+  + lemmas `nbhs_infty_ger`, `nbhs0_ltW`, `nbhs0_lt`
+
+- in `normedtype.v`
+  + lemma `closed_ball_ball`
+
+- in `numfun.v`
+  + lemma `cvg_indic`
+
+- in `lebesgue_integral.v`
+  + lemma `locally_integrable_indic`
+  + definition `davg`,
+    lemmas `davg0`, `davg_ge0`, `davgD`, `continuous_cvg_davg`
+  + definition `lim_sup_davg`,
+    lemmas `lim_sup_davg_ge0`, `lim_sup_davg_le`,
+	`continuous_lim_sup_davg`, `lim_sup_davgB`, `lim_sup_davgT_HL_maximal`
+  + definition `lebesgue_pt`,
+    lemma `continuous_lebesgue_pt`
+  + lemma `integral_setU_EFin`
+  + lemmas `integral_set1`, `ge0_integral_closed_ball`, `integral_setD1_EFin`,
+    `integral_itv_bndo_bndc`, `integral_itv_obnd_cbnd`
+  + lemma `lebesgue_differentiation`
+  + lemma `lebesgue_density`
+  + definition `nicely_shrinking`,
+    lemmas `nicely_shrinking_gt0`, `nicely_shrinking_lty`, `nice_lebesgue_differentiation`
+
+- in `normedtype.v`:
+  + lemma `ball_open_nbhs`
+
+- new file `ftc.v`:
+  - lemmas `FTC1`, `continuous_FTC1`
 
 - in file `normedtype.v`,
   + new definition `completely_regular_space`.
@@ -78,8 +119,14 @@
   + `lte_addl` -> `lteDl`
   + `lte_addr` -> `lteDr`
 
+- in `lebesgue_integral.v`
+  + `integral_setU` -> `ge0_integral_setU`
+
 ### Generalized
 
+- in `realfun.v`
+  + lemma `lime_sup_le`
+
 ### Deprecated
 
 ### Removed

_CoqProject

@@ -41,6 +41,7 @@ theories/derive.v
 theories/measure.v
 theories/numfun.v
 theories/lebesgue_integral.v
+theories/ftc.v
 theories/hoelder.v
 theories/probability.v
 theories/summability.v

classical/mathcomp_extra.v

@@ -985,3 +985,10 @@ Qed.
 
 End path_lt.
 Arguments last_filterP {d T a} P s.
+
+(* TODO: in MathComp since version 2.3.0 *)
+Lemma invf_plt (F : numFieldType) :
+  {in Num.pos &, forall x y : F, (x^-1 < y)%R = (y^-1 < x)%R}.
+Proof.
+by move=> x y ? ?; rewrite -[in LHS](@invrK _ y) ltf_pV2// posrE invr_gt0.
+Qed.

classical/set_interval.v

@@ -121,23 +121,108 @@ Definition set_itvE := (set_itv1, set_itvoo0, set_itvoc0, set_itvco0, set_itvoo,
   set_itvcc, set_itvoc, set_itvco, set_itv_infty_infty, set_itv_o_infty,
   set_itv_c_infty, set_itv_infty_o, set_itv_infty_c, set_itv_infty_set0).
 
-Lemma setUitv1 (a : itv_bound T) (x : T) : (a <= BLeft x)%O ->
+Lemma set_itvxx a : [set` Interval a a] = set0.
+Proof. by move: a => [[|] a |[|]]; rewrite !set_itvE. Qed.
+
+Lemma setUitv1 a x : (a <= BLeft x)%O ->
   [set` Interval a (BLeft x)] `|` [set x] = [set` Interval a (BRight x)].
 Proof.
 move=> ax; apply/predeqP => z /=; rewrite itv_splitU1// [in X in _ <-> X]inE.
 by rewrite (rwP eqP) (rwP orP) orbC.
 Qed.
 
-Lemma setU1itv (a : itv_bound T) (x : T) : (BRight x <= a)%O ->
+Lemma setU1itv a x : (BRight x <= a)%O ->
   x |` [set` Interval (BRight x) a] = [set` Interval (BLeft x) a].
 Proof.
 move=> ax; apply/predeqP => z /=; rewrite itv_split1U// [in X in _ <-> X]inE.
 by rewrite (rwP eqP) (rwP orP) orbC.
 Qed.
 
+Lemma setDitv1r a x :
+  [set` Interval a (BRight x)] `\ x = [set` Interval a (BLeft x)].
+Proof.
+apply/seteqP; split => [z|z] /=; rewrite !in_itv/=.
+  by move=> [/andP[-> /= zx] /eqP xz]; rewrite lt_neqAle xz.
+by rewrite lt_neqAle => /andP[-> /andP[/eqP ? ->]].
+Qed.
+
+Lemma setDitv1l a x :
+  [set` Interval (BLeft x) a] `\ x = [set` Interval (BRight x) a].
+Proof.
+apply/seteqP; split => [z|z] /=; rewrite !in_itv/=.
+  move=> [/andP[xz ->]]; rewrite andbT => /eqP.
+  by rewrite lt_neqAle eq_sym => ->.
+move=> /andP[]; rewrite lt_neqAle => /andP[xz zx ->].
+by rewrite andbT; split => //; exact/nesym/eqP.
+Qed.
+
 End set_itv_porderType.
 Arguments neitv {d T} _.
 
+Section set_itv_orderType.
+Variables (d : unit) (T : orderType d).
+Implicit Types a x y : itv_bound T.
+Local Open Scope order_scope.
+
+Lemma itv_bndbnd_setU a x y : a <= x -> x <= y ->
+  ([set` Interval a y] = [set` Interval a x] `|` [set` Interval x y])%classic.
+Proof.
+rewrite le_eqVlt => /predU1P[<-{x} ay|]; first by rewrite set_itvxx set0U.
+move=> /[swap].
+rewrite le_eqVlt => /predU1P[-> ay|]; first by rewrite set_itvxx setU0.
+move: y => [yb y/=|[|]]; last 2 first.
+  by case: x => [|[|]].
+  move=> _ ax; apply/seteqP; split => [z|z] /=.
+    rewrite !in_itv/= !andbT => -> /=; apply/orP.
+    by move: x => [[|] x/=|[|]//] in ax *; rewrite leNgt ?(orbN,orNb).
+  rewrite !in_itv/= !andbT => -[/andP[]|]//.
+  move: x => [[|] x/=|[|]//] in ax *; move: a => [[|] a/=|[|]//] in ax * => //.
+  - by apply/le_trans; exact/ltW.
+  - exact/lt_le_trans.
+  - by move=> /(le_lt_trans ax) /ltW.
+  - exact/lt_trans.
+move=> xy ax; apply/seteqP; split => [z|z] /=.
+  rewrite !in_itv /= => /andP[].
+  move: a ax => [b t /=|[]//= oox _].
+    move=> tx -> zxy /=; rewrite zxy andbT/=; apply/orP.
+    by case: x xy tx => [[|] x/=|[|]//] xy tx; rewrite leNgt ?(orbN,orNb).
+  move=> ->; rewrite andbT; apply/orP.
+  by move: x => [[|] x/=|[|]//] in oox xy *; rewrite leNgt ?(orbN,orNb).
+rewrite !in_itv/=.
+move: a ax => [b t /= tx| [/= oox|/= oox]].
+- move=> [/andP[-> zx]|].
+    move: x => [[|] x|[|]//]/= in xy tx zx *.
+      case: yb => /= in xy *.
+        by rewrite (lt_trans zx _).
+      by rewrite (ltW (lt_le_trans zx _)).
+    rewrite bnd_simp in xy.
+    case: yb => /=.
+      by rewrite (le_lt_trans zx _).
+    by rewrite (ltW (le_lt_trans zx _)).
+  move: x => [[|] x|[|]//]/= in xy tx *; rewrite bnd_simp in xy tx.
+  + move=> /andP[xz ->]; rewrite andbT.
+    case: b => /=.
+      by rewrite (le_trans _ xz)// ltW.
+    by rewrite (lt_le_trans tx).
+  move=> /andP[xz ->]; rewrite andbT.
+  case: b tx => /= tx; rewrite bnd_simp in tx.
+    by rewrite ltW// (le_lt_trans _ xz).
+  by rewrite (lt_trans tx).
+- move: x => [[|] x|[|]//]/= in xy oox *; move=> [|].
+  + case: yb => /= in xy *.
+      by move=> /lt_trans; exact.
+    rewrite bnd_simp in xy.
+    by move=> /lt_le_trans => /(_ _ xy)/ltW.
+  + by move=> /andP[].
+  + case: yb => /= in xy *.
+      by move=> /le_lt_trans; apply.
+    by move=> /le_trans; apply; exact/ltW.
+  + by move=> /andP[].
+- by move: x => [[|] x|[|]//]/= in xy oox *.
+Qed.
+
+End set_itv_orderType.
+
 Lemma set_itv_ge [disp : unit] [T : porderType disp] [b1 b2 : itv_bound T] :
   ~~ (b1 < b2)%O -> [set` Interval b1 b2] = set0.
 Proof. by move=> Nb12; rewrite -subset0 => x /=; rewrite itv_ge. Qed.

theories/Make

@@ -30,6 +30,7 @@ derive.v
 measure.v
 numfun.v
 lebesgue_integral.v
+ftc.v
 hoelder.v
 probability.v
 lebesgue_stieltjes_measure.v

theories/charge.v

@@ -669,7 +669,7 @@ have [v [v0 Pv]] : {v : nat -> elt_type |
     v 0%N = exist _ (A0, d_ set0, A0) (And4 mA0 A0D (d_ge0 set0) A0d0) /\
     forall n, elt_rel (v n) (v n.+1)}.
   apply: dependent_choice_Type => -[[[A' ?] U] [/= mA' A'D]].
-  have [A1 [mA1 A1DU A1t1] ] := next_elt U.
+  have [A1 [mA1 A1DU A1t1]] := next_elt U.
   have A1D : A1 `<=` D by apply: (subset_trans A1DU); apply: subDsetl.
   by exists (exist _ (A1, d_ U, U `|` A1) (And4 mA1 A1D (d_ge0 U) A1t1)).
 have Ubig n : U_ (v n) = \big[setU/set0]_(i < n.+1) A_ (v i).