WIP: optimal step 2 for Lebesgue scheme.

Lebesgue/LInt_p.v

@@ -30,6 +30,7 @@ From Flocq Require Import Core.
 Require Import subset_compl.
 Require Import Rbar_compl.
 Require Import sum_Rbar_nonneg.
+Require Import Subset.
 Require Import sigma_algebra.
 Require Import sigma_algebra_R_Rbar.
 Require Import measurable_fun.
@@ -2169,6 +2170,92 @@ apply IHl.
 
 
 
+Admitted.
+
+(* This one should be really optimal. *)
+Lemma Lebesgue_scheme_step2' :
+  forall (P : (E -> Rbar) -> Prop),
+    P (fun _ => 0) ->
+    (forall a A (f : E -> R),
+      0 <= a -> measurable genE A -> non_neg f -> SF genE f ->
+      P f -> P (fun x => a * charac A x + f x)) ->
+    forall (f : E -> R), non_neg f -> SF genE f -> P f.
+Proof.
+intros P H0 H1 f Hf1 [lf [Hlf Hf2]].
+generalize (finite_vals_sum_eq _ _ Hlf); intros Hf3.
+apply P_ext with (f1 := (fun x =>
+    sum_Rbar_map lf (fun y => Finite (y * (charac (fun x => f x = y) x))))); try easy.
+assert (Hv : forall v, In v lf -> 0 <= v) by (intros; now apply (In_finite_vals_non_neg f lf)).
+induction lf as [ | v lg]; try easy.
+pose (g := fun x => f x - v * charac (fun t => f t = v) x).
+destruct Hlf as [Hlf1 [Hlf2 Hlf3]].
+(* *)
+assert (Hg1 : forall x, ~ (g x = v)).
+intros x Hx.
+
+admit.
+
+(* *)
+assert (Hlg : finite_vals_canonic g lg).
+repeat split.
+(* . *)
+now apply (sort_compl.LocallySorted_cons _ v).
+(* . *)
+intros y Hy1.
+assert (Hy2 : v < y).
+  apply (sort_compl.LocallySorted_extends _ lg); try easy.
+  apply Rlt_trans.
+destruct (Hlf2 y) as [x Hx].
+now apply in_cons.
+exists x; unfold g; rewrite <- Hx.
+rewrite <- Rminus_0_r; f_equal.
+erewrite <- Rmult_0_r; f_equal.
+apply charac_is_0; rewrite Hx.
+now apply not_eq_sym, Rlt_not_eq.
+(* . *)
+intros x.
+
+admit.
+
+generalize (finite_vals_sum_eq _ _ Hlg); intros Hg3.
+destruct Hlg as [Hlg1 [Hlg2 Hlg3]].
+(* *)
+apply P_ext with (f1 := (fun x =>
+    Finite (v * (charac (fun t => f t = v) x) +
+      (real (sum_Rbar_map lg (fun y => y * (charac (fun t => g t = y) x))))))).
+(* *)
+intros x; unfold sum_Rbar_map; simpl; rewrite <- Rbar_finite_plus.
+rewrite sum_Rbar_l_is_finite.
+2: { intros y Hy; apply in_map_iff in Hy.
+    destruct Hy as [z [Hz _]]; now rewrite <- Hz. }
+f_equal; apply sum_Rbar_map_ext_f; intros y Hy.
+f_equal; f_equal.
+apply charac_ext; intros t; split; intros Ht; rewrite <- Ht; unfold g.
+
+admit.
+admit.
+
+(* *)
+apply H1.
+(* . *)
+apply Hv, in_eq.
+(* . *)
+apply Hf2.
+(* . *)
+intros y.
+rewrite sum_Rbar_map_is_finite; try easy.
+apply sum_Rbar_map_ge_0.
+intros z Hz; simpl.
+apply Rmult_le_pos; try now apply Hv, in_cons.
+apply non_neg_charac.
+(* . *)
+exists lg; split; repeat split.
+now apply (sort_compl.LocallySorted_cons _ v).
+intros y Hy; destruct (Hlg2 y) as [x Hx]; try easy;
+  exists x; rewrite <- Hx, <- finite_vals_sum_eq; try easy.
+intros x; rewrite <- (Hg3 x); now simpl.
+intros y.
+
 Admitted.
 
 Lemma Lebesgue_scheme_step3 :
@@ -2194,12 +2281,10 @@ Qed.
 
 Lemma Lebesgue_scheme' :
   forall (P : (E -> Rbar) -> Prop),
-    (forall A, measurable genE A -> P (charac A)) ->
-    (forall l A, 0 <= l -> P (charac A) -> P (fun x => l * charac A x)) ->
-    (forall (f g : E -> R),
-      non_neg f -> SF genE f ->
-      non_neg g -> SF genE g ->
-      P f -> P g -> P (fun x => f x + g x)) ->
+    P (fun _ => 0) ->
+    (forall a A (f : E -> R),
+      0 <= a -> measurable genE A -> non_neg f -> SF genE f ->
+      P f -> P (fun x => a * charac A x + f x)) ->
     (forall (f : nat -> E -> R),
       (forall n, non_neg (f n)) -> (forall n, SF genE (f n)) ->
       (forall x n, Rbar_le (f n x) (f (S n) x)) ->
@@ -2207,9 +2292,9 @@ Lemma Lebesgue_scheme' :
       (P (fun t => Sup_seq (fun n => f n t)))) ->
     forall f, non_neg f -> measurable_fun_Rbar genE f -> P f.
 Proof.
-intros P H1 H2 H3 H4.
+intros P H0 H1 H2.
 apply Lebesgue_scheme_step3; try easy.
-now apply Lebesgue_scheme_step2.
+now apply Lebesgue_scheme_step2'.
 Qed.
 
 End Lebesgue_scheme.