Réunion du 27/09/2021

Lebesgue/LInt.v

@@ -41,7 +41,7 @@ Definition non_neg_part :=
 Definition non_pos_part :=
   fun (f : E -> Rbar) (x : E) => Rbar_max 0 (Rbar_opp (f x)).
 
-(** integrale de Lebesgue *)
+(** Lebesgue integrability and integral *)
 Definition ex_LInt : (E -> Rbar) -> Prop := fun f =>
   let f_p := non_neg_part f in
   let f_m := non_pos_part f in
@@ -83,6 +83,14 @@ replace (LInt_p mu (fun x : E => Rbar_max 0 (Rbar_opp (f x)))) with (Finite 0).
     simpl; f_equal; ring.
 Qed.
 
+Lemma ex_LInt_equiv_abs :
+   forall f,
+    (ex_LInt f) <-> 
+       (measurable_fun gen gen_Rbar f /\
+          is_finite (LInt_p mu (fun t => Rbar_abs (f t)))).
+Admitted.
+
+
 End LInt_def.
 
 (*

Lebesgue/LInt_calc.v

@@ -29,9 +29,8 @@ Require Import LInt_p.
 Require Import LInt.
 Require Import measure_R.
 
+Definition l_meas : measure gen_R := Borel_Lebesgue_measure.
 
-Definition lambda : measure gen_R := Borel_Lebesgue_measure.
-(* SB râle un peu sur "lambda" *)
 
 Definition intcc : R -> R -> R -> Prop :=
   fun a b x => a <= x /\ x <= b.
@@ -40,7 +39,7 @@ Definition intcc : R -> R -> R -> Prop :=
 
 Lemma LInt_calc_constant_aux :
   forall a b c, a <= b -> (0 <= c) ->
-    LInt lambda (fun x => c * charac (intcc a b) x) = c * (b - a).
+    LInt l_meas (fun x => c * charac (intcc a b) x) = c * (b - a).
 Proof.
 intros a b c H1 H2.
 rewrite LInt_eq_p; try easy.
@@ -64,25 +63,82 @@ Qed.
 
 Lemma LInt_calc_constant :
   forall a b c, a <= b ->
-    LInt lambda (fun x => c * charac (intcc a b) x) = c * (b - a).
+    LInt l_meas (fun x => c * charac (intcc a b) x) = c * (b - a).
 Proof.
 intros a b c H.
 (* séparer cas c >= 0 ou non *)
 Admitted.
 
+Lemma LInt_p_calc_identity_0_1 :
+  LInt_p l_meas (fun x:R => Rbar_mult x (charac (intcc 0 1) x)) = 1/2.
+Proof.
+assert (KR: inhabited R).
+apply (inhabits 0%R).
+
+pose (f:= (fun x0 : R => Rbar_mult x0 (charac (intcc 0 1) x0))); fold f.
+assert (Hf1 : non_neg f).
+admit.
+assert (Hf2 : measurable_fun_Rbar gen_R f).
+apply measurable_fun_when_charac with (f':= fun x => Finite x).
+apply measurable_R_intcc.
+intros t; easy.
+intros A.
+apply measurable_Rbar_R.
+(* *)
+rewrite <- LInt_p_with_mk_adapted_seq; try easy.
+apply trans_eq with (Sup_seq (fun n => /2* (1-/pow 2 n))).
+(* Question pow or powerRZ or .. ? *)
+apply Sup_seq_ext.
+intros n.
+
+
+pose (Y:= (mk_adapted_seq_SF f Hf1 Hf2)).
+rewrite LInt_p_SFp_eq with (Hf:=Y n); try easy.
+unfold Y.
+
+(*
+unfold mk_adapted_seq_SF.
+
+needs mk_adapted_seq_SF to be Defined instead of Qed *)
+
+
+(* Stopped for now!
+Very unpractical as the lists are awful to handle
+=> not sure it is the good method...
+
+Other solution: prove that \phi_n = 
+  \Sum_{k=0}^{2^n-1} k/2^n * 
+    charac(fun t => k/2^n <= t < (k+1)/2^n)    +1_{x=1}
+
+then \int \phi_n = \Sum \int (constant funs) = ...
+
+=> maybe too compliacated for what it is worth
+
+Other solution: FTA (and \int x = x^2/2)
+
+Other solution by geometric transformations 
+  (Fubini, or change of variable, or...)
+*)
+
+
+
+Admitted.
+
+
+
 Lemma LInt_calc_identity_0_1 :
-  LInt lambda (fun x => x * charac (intcc 0 1) x) = 1/2.
+  LInt l_meas (fun x => x * charac (intcc 0 1) x) = 1/2.
 Proof.
 Admitted.
 
 Lemma LInt_p_calc_identity :
   forall a b, 0 <= a <= b ->
-    LInt_p lambda (fun x => x * charac (intcc a b) x) = (b - a) / 2.
+    LInt_p l_meas (fun x => x * charac (intcc a b) x) = (b - a) / 2.
 Proof.
 Admitted.
 
 Lemma LInt_calc_identity :
   forall a b, a <= b ->
-    LInt lambda (fun x => x * charac (intcc a b) x) = (b - a) / 2.
+    LInt l_meas (fun x => x * charac (intcc a b) x) = (b - a) / 2.
 Proof.
 Admitted.

Lebesgue/bochner_integral/BInt_LInt_p.v

@@ -24,6 +24,7 @@ From Coq Require Import
     Rdefinitions
     Rbasic_fun
     Raxioms
+    Reals
 .
 
 From Coquelicot Require Import
@@ -53,6 +54,7 @@ Require Import
     sigma_algebra
     sigma_algebra_R_Rbar_new
     subset_compl
+    LInt
 .
 
 Section BInt_to_LInt_p.
@@ -554,4 +556,111 @@ Section BInt_to_LInt_p.
         rewrite Rplus_comm => //.
     Qed.
 
+  Lemma Bif_measurable {f : X -> R} :
+        ∀ bf : Bif μ f,
+          measurable_fun_R gen f.
+  Proof.
+  intros bf.
+  generalize (measurable_Bif bf).
+  unfold fun_Bif, measurable_fun_R.
+  intros H A HA.
+  apply H.
+  apply measurable_R_equiv_oo; easy.
+  Qed.
+
+
+   Lemma Bif_ex_LInt {f : X -> R} :
+        ∀ bf : Bif μ f,
+        ex_LInt μ f.
+   Proof.
+   intros bf.
+   apply ex_LInt_equiv_abs.
+   apply bf.
+   split.
+   apply measurable_fun_R_Rbar.
+   apply Bif_measurable; easy.
+   (* *)
+   generalize bf.
+   destruct bf; intros bf.
+   destruct (proj2 (ax_lim_l1 (mkposreal _ Rlt_0_1))) as (N,HN).
+   simpl in HN; rewrite Rplus_0_l in HN.
+   eapply Rbar_bounded_is_finite.
+   apply LInt_p_ge_0; try easy.
+   intros t; apply Rbar_abs_ge_0.
+   2: easy.
+   eapply LInt_p_monotone.
+   intros t.
+   replace (Finite (f t)) with 
+     (Rbar_plus (Rbar_minus (f t) (seq N t)) (seq N t)).
+   2: apply sym_eq, Rbar_plus_minus_r; easy.
+   eapply Rbar_le_trans with (1:= Rbar_abs_triang _ _).
+   apply Rbar_le_refl.
+   rewrite LInt_p_plus; try easy;
+      try (intros t; apply Rbar_abs_ge_0).
+   assert (T1:is_finite ((LInt_p μ
+        (λ x : X,
+           Rbar_abs (Rbar_minus (f x) (seq N x)))))).
+  apply Rbar_bounded_is_finite with 0 1; try easy.
+  apply LInt_p_ge_0; try easy.
+  intros t; apply Rbar_abs_ge_0.
+  apply Rbar_lt_le.
+  replace (LInt_p μ  (λ x : X,
+        Rbar_abs (Rbar_minus (f x) (seq N x)))) with (LInt_p μ
+              (λ x : X, (‖ f - seq N ‖)%fn x)); try easy.
+  apply HN; auto with arith.
+  apply LInt_p_ext; intros t.
+  unfold fun_norm, norm; simpl.
+  unfold abs; simpl; f_equal; f_equal.
+  unfold fun_plus, fun_scal, opp; simpl.
+  unfold plus, scal, mult, one; simpl.
+  unfold mult; simpl; ring.
+  assert (T2: is_finite ((LInt_p μ (λ x : X, Rbar_abs (seq N x))))).
+  generalize (integrable_sf_norm (ax_int N)).
+  intros K; generalize (Bif_integrable_sf ax_notempty K).
+  intros K'; generalize (is_finite_LInt_p_Bif K').
+ 
+  unfold fun_Bif, fun_norm.
+  (*rewrite (fun_sf_norm (seq N) x).*)
+
+  (* problème de réécriture sous le lambda ! *)
+
+
+  (*rewrite <- BInt_LInt_p_eq.
+   BInt_sf_LInt_SFp*)
+  admit. (* dur *)
+
+  rewrite <- T1, <- T2; easy.
+   (* *)
+   apply measurable_fun_abs.
+   apply measurable_fun_plus.
+   apply measurable_fun_R_Rbar.
+   apply Bif_measurable; easy.
+  apply measurable_fun_opp.
+  apply measurable_fun_R_Rbar.
+   apply Bif_measurable.
+  apply Bif_integrable_sf; easy.
+  intros t; easy.
+ apply measurable_fun_abs.
+apply measurable_fun_R_Rbar.
+   apply Bif_measurable.
+  apply Bif_integrable_sf; easy.
+
+
+Admitted.
+
+
+     Lemma BInt_LInt_eq {f : X -> R} :
+        ∀ bf : Bif μ f,
+          BInt bf = LInt μ f.
+   Proof.
+  intros bf.
+  unfold LInt.
+  (*rewrite <- BInt_LInt_p_eq.*)
+
+
+Admitted.
+
+
+
+
 End BInt_to_LInt_p.
\ No newline at end of file