WIP: Lebesgue scheme step 2.

Equivalence between hypotheses of both forms.

Lebesgue/LInt_p.v

@@ -89,7 +89,6 @@ apply LInt_p_SFp_eq.
 intros x; simpl; auto with real.
 Qed.
 
-
 Lemma LInt_p_ge_0 : forall f, non_neg f -> Rbar_le 0 (LInt_p f).
 Proof.
 intros f Hf; unfold LInt_p, Rbar_lub.
@@ -1375,7 +1374,6 @@ rewrite charac_not.
 auto with real.
 Qed.
 
-
 Lemma LInt_p_const : forall a, Rbar_le 0 a ->
    LInt_p mu (fun _ => a) = Rbar_mult a (mu (fun _ => True)).
 Proof.
@@ -1391,7 +1389,6 @@ apply measurable_fun_charac.
 apply measurable_full.
 Qed.
 
-
 Lemma LInt_p_eq_meas_0 :
   forall f A,
     non_neg f -> measurable_fun_Rbar gen f ->
@@ -1921,6 +1918,7 @@ Qed.
 
 End LInt_p_plus_def.
 
+
 Section LInt_p_Dirac.
 
 Context {E : Type}.
@@ -1951,6 +1949,7 @@ End LInt_p_Dirac.
 Section Lebesgue_scheme.
 
 Context {E : Type}.
+Hypothesis Einhab : inhabited E.
 
 Variable genE : (E -> Prop) -> Prop.
 
@@ -1958,8 +1957,7 @@ Lemma P_ext :
   forall (P : (E -> Rbar) -> Prop) f1 f2,
     (forall x, f1 x = f2 x) -> P f1 -> P f2.
 Proof.
-intros P f1 f2 H1.
-now apply functional_extensionality in H1; subst.
+intros P f1 f2 H; apply functional_extensionality in H; now subst.
 Qed.
 
 Lemma Lebesgue_scheme :
@@ -2092,27 +2090,103 @@ apply measurable_fun_charac; easy.
 apply IHl.
 Qed.
 
+Lemma Lebesgue_scheme_step2_hyp_equiv :
+  forall (P : (E -> Rbar) -> Prop),
+    ((forall a A, 0 <= a -> measurable genE A -> P (fun x => a * 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 => Rbar_plus (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))).
+Proof.
+intros P; split; intros [H1 H2]; split.
+(* *)
+apply P_ext with (f1 := fun x => 0 * charac fullset x).
+intros; rewrite Rbar_finite_eq; apply Rmult_0_l.
+apply (H1 0 fullset); try lra; apply measurable_full.
+(* *)
+intros a A f Ha HA Hf1 Hf2 Hf3.
+apply P_ext with (f1 := fun x => Rbar_plus (a * charac A x) (f x)); try now simpl.
+apply H2; try easy.
+apply non_neg_ext with (f0 := fun x => Rbar_mult a (charac A x)); try now simpl.
+apply non_neg_scal_l; try now simpl.
+apply non_neg_charac.
+now apply SF_scal, SF_charac.
+now apply H1.
+(* *)
+intros a A Ha HA.
+apply P_ext with (f1 := fun x => a * charac A x + 0).
+intros; rewrite Rbar_finite_eq; lra.
+apply H2; try easy.
+intros x; simpl; lra.
+apply SF_0.
+
+admit. (* inversion Einhab. ne marche pas ! *)
+
+(* *)
+intros f g Hf1 [lf [Hlf Hf2]] Hg1 Hg2 Hf3 Hg3.
+generalize (finite_vals_sum_eq _ _ Hlf); intros Hf4.
+apply P_ext with (f1 := fun x =>
+    Rbar_plus (sum_Rbar_map lf (fun y => Finite (y * charac (fun t => f t = y) x)))
+              (Finite (g x))).
+intros; now rewrite <- Hf4.
+generalize f Hf1 Hlf Hf2 Hf3 Hf4; clear f Hf1 Hlf Hf2 Hf3 Hf4.
+induction lf as [ | v l].
+(* . *)
+intros; apply P_ext with (f1 := g); try easy.
+intros; simpl; apply Rbar_finite_eq; lra.
+(* . *)
+intros f Hf1 Hlf Hf2 Hf3 Hf4.
+assert (Hf2' : SF_aux genE f (v :: l)) by now split.
+generalize (SF_aux_cons Einhab genE f v l Hf1 Hf2').
+pose (h := fun x => f x - v * charac (fun t => f t = v) x); fold h; intros [Hh1 [Hh2 Hh3]].
+pose (f1 := fun x => h x + g x).
+apply P_ext with (f1 := fun x => v * charac (fun t => f t = v) x + f1 x).
+(* .. *)
+admit.
+(* .. *)
+apply H2; try easy.
+(* ... *)
+apply (In_finite_vals_non_neg _ _ _ Hf1 Hlf), in_eq.
+(* ... *)
+unfold f1.
+apply non_neg_ext with (f0 := fun x => Rbar_plus (h x) (g x)).
+intros x; now rewrite <- Rbar_finite_plus.
+now apply non_neg_plus.
+(* ... *)
+unfold f1; apply SF_plus; try easy; now exists l.
+(* ... *)
+apply P_ext with (f1 := fun x =>
+    Rbar_plus (sum_Rbar_map l (fun y => y * charac (fun t => h t = y) x)) (g x)).
+
+admit.
+
+apply IHl; try easy; try apply Hh2.
+
+Admitted.
+
 Lemma Lebesgue_scheme_step2 :
   forall (P : (E -> Rbar) -> Prop),
-    (forall l A, 0 <= l -> P (charac A) -> P (fun x => l * charac A x)) ->
+    (forall a A, 0 <= a -> P (fun x => a * 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 => Rbar_plus (f x) (g x))) ->
-    (forall A, measurable genE A -> P (charac A)) ->
     forall (f : E -> R), non_neg f -> SF genE f -> P f.
 Proof.
-intros P H1 H2 H f Hf1 [l [Hl Hf2]].
+intros P H1 H2 f Hf1 [l [Hl Hf2]].
+
 generalize (finite_vals_sum_eq _ _ Hl); intros Hf3.
 apply P_ext with (f1 := (fun x =>
     sum_Rbar_map l (fun a => Finite (a * (charac (fun x => real (f x) = a) x))))); try easy.
 induction l.
 (* *)
-apply P_ext with (f1 := fun _ => 0).
-intros x; unfold sum_Rbar_map; now simpl.
-apply P_ext with (f1 := (charac (fun _ => False))).
-intros x; now rewrite charac_is_0.
-apply H, measurable_Prop.
+apply P_ext with (f1 := fun x => 0 * charac emptyset x).
+intros; unfold sum_Rbar_map; simpl; apply Rbar_finite_eq; rewrite charac_is_0; [lra | easy].
+apply H1; lra.
 (* *)
 apply P_ext with (f1 := (fun x =>
     Rbar_plus (Finite (a * (charac (fun t => f t = a) x)))
@@ -2148,14 +2222,12 @@ admit.
 case (Rle_lt_dec 0 a); intros Ha.
 (* .. *)
 apply H1; try easy.
-apply H, Hf2.
 (* .. *)
-apply P_ext with (f1 := charac (fun _ => False)).
-intros x; f_equal; rewrite charac_is_0; try easy; symmetry.
-apply Rmult_eq_0_compat_l, charac_is_0, sym_not_eq, Rlt_not_eq.
-apply Rlt_le_trans with 0; try easy.
-apply Hf1.
-apply H, measurable_empty.
+apply P_ext with (f1 := fun x => 0 * charac emptyset x).
+intros; apply Rbar_finite_eq.
+rewrite Rmult_0_l; symmetry; apply Rmult_eq_0_compat_l, charac_is_0, sym_not_eq, Rlt_not_eq.
+apply Rlt_le_trans with 0; try easy; apply Hf1.
+apply H1; lra.
 (* . *)
 apply P_ext with (f1 :=
     fun x => sum_Rbar_map l (fun a0 => Finite (a0 * charac (fun t => f t = a0) x))).
@@ -2166,14 +2238,9 @@ admit.
 apply IHl.
 
 
-
-
-
-
 Admitted.
 
-(* This one should be really optimal. *)
-Lemma Lebesgue_scheme_step2' :
+Lemma Lebesgue_scheme_step2_alt :
   forall (P : (E -> Rbar) -> Prop),
     P (fun _ => 0) ->
     (forall a A (f : E -> R),
@@ -2294,7 +2361,7 @@ Lemma Lebesgue_scheme' :
 Proof.
 intros P H0 H1 H2.
 apply Lebesgue_scheme_step3; try easy.
-now apply Lebesgue_scheme_step2'.
+now apply Lebesgue_scheme_step2_alt.
 Qed.
 
 End Lebesgue_scheme.