progress on cauchy schwartz

Author: hoheinzollern

theories/probability.v

@@ -213,36 +213,47 @@ split.
     exact: measurable_funT_comp.
   + by move=> t _/=; rewrite lee_fin normrX.
 Qed.
-
 End Lspace.
-Notation "`|| f ||_ p" := (Lp_norm p f) (at level 0).
 
 Section Lspace.
 Context d (T : measurableType d) (R : realType).
 Variable mu : {finite_measure set T -> \bar R}.
 
-Notation "`|| f ||_ p" := (Lp_norm mu p f) (at level 0).
+Lemma powere12_sqrt (a : \bar R) : (0 <= a)%E -> (a `^ (2^-1))%E = sqrte a.
+Admitted.
+
+Definition Lp_norm (p : nat) (f : T -> R) : \bar R :=
+  ((\int[mu]_x (`|f x| ^+ p)%:E) `^ (p%:R^-1))%E.
+  
+Local Notation "`|| f ||_ p" := (Lp_norm p f) (at level 0).
+
+Lemma hoelder (f g : T -> R) p q :
+  measurable_fun setT f -> measurable_fun setT g -> (p%:R^-1 + q%:R^-1 = 1 :> R) ->
+    (`|| (f \* g)%R ||_1 <= `|| f ||_p * `|| g ||_q)%E.
+Admitted.
+(* follow http://pi.math.cornell.edu/~erin/analysis/lectures.pdf version with convexity, not young inequality *)
 
 (* FROM https://ocw.mit.edu/courses/18-125-measure-and-integration-fall-2003/6f21af6c40de1eccd70349bd3a3b0095_18125_lec17.pdf *)
-Lemma Lspace2_Lspace1 :
-  Lspace mu 2 `<=` Lspace mu 1.
+Lemma Lspace2_Lspace1 (f : Ltype mu 2%N) : mu.-integrable [set: T] (EFin \o repr f).
 Proof.
-move => f [mf foo]; split => //.
+have mf := Lfun.mf (repr f).
+have foo := Lfun.intf (repr f).
+split; [exact/EFin_measurable_fun|].
 apply: (@le_lt_trans _ _
-    (sqrte (\int[mu]_x (`|f x| ^+ 2)%:E) * sqrte (mu setT)))%E; last first.
+    (sqrte (\int[mu]_x (`|repr f x| ^+ 2)%:E) * sqrte (mu setT)))%E; last first.
   rewrite muleC lte_mul_pinfty//.
   + by rewrite esqrt_ge0.
   + by rewrite fin_num_esqrt// fin_num_measure.
   + by rewrite -ge0_fin_numE ?esqrt_ge0// fin_num_esqrt// ge0_fin_numE// integral_ge0//.
 rewrite -[X in (_ * sqrte (mu X))%E](setTI setT).
 rewrite -integral_indic//.
 under [X in (_ * sqrte X)%E]eq_integral. move => x _. rewrite indicT. rewrite -(@ger0_norm _ (cst 1 x) _) //=. over.
-rewrite -expe12_sqrt; last by apply: integral_ge0.
-rewrite -expe12_sqrt; last by apply: integral_ge0.
+rewrite -powere12_sqrt; last by apply: integral_ge0.
+rewrite -powere12_sqrt; last by apply: integral_ge0.
 rewrite (_ : (\int[mu]__ `|1|%:E)%E = (\int[mu]_x `|cst 1 x| ^+ 2)%E); last first.
   by apply: eq_integral => t _ /=; rewrite normr1 mule1.
 have : 2^-1 + 2^-1 = 1 :> R by rewrite -div1r -splitr.
-move/(@hoelder _ _ _ mu _ (cst 1%R) _ _ mf (measurable_fun_cst _)).
+move/(@hoelder _ (cst 1%R) _ _ mf (measurable_fun_cst _)).
 rewrite /Lp_norm.
 apply: le_trans.
 rewrite /Lp_norm /=.
@@ -271,79 +282,10 @@ Lemma probability_range d (T : measurableType d) (R : realType)
   (P : probability T R) (X : {RV P >-> R}) : P (X @^-1` range X) = 1%E.
 Proof. by rewrite preimage_range probability_setT. Qed.
 
-Section tmp.
-Context d (T : measurableType d) (R : realType) (mu : {measure set T -> \bar R}).
-Lemma integral_ae_eq (g f : T -> \bar R) :
-  mu.-integrable setT f -> mu.-integrable setT g ->
-  (forall E, measurable E -> \int[mu]_(x in E) f x = \int[mu]_(x in E) g x)%E ->
-  ae_eq mu setT f g.
-Admitted.
-End tmp.
-
-Section covariance.
-Local Open Scope ereal_scope.
-Variables (d : _) (T : measurableType d) (R : realType) (P : probability T R).
-
-Definition covariance (X Y : {RV P >-> R}) :=
-  ('E_P [(X \- cst (fine 'E_P[X])) \* (Y \- cst (fine 'E_P[Y]))])%R.
-Local Notation "''Cov' [ X , Y ]" := (covariance X Y).
-
-Lemma square_X_0_ae (X : {RV P >-> R}) :
-  P.-Lspace 2 X -> 'E_P[(X ^+ 2)%R] = 0 -> ae_eq P setT (EFin \o X) (EFin \o cst 0%R).
-Proof.
-move => l2x xsqr0.
-apply integral_ae_eq => /=.
-Admitted.
-
-Lemma cauchy_schwarz (X Y : {RV P >-> R}) :
-  P.-Lspace 1 X -> P.-Lspace 1 Y ->
-  (* 'E X < +oo -> 'E Y < +oo -> TODO: use lspaces *)
-    'E_P[(X \* Y)%R] ^+2 <= 'E_P[(X ^+ 2)%R] + 'E_P[(Y ^+ 2)%R].
-Proof.
-move => hfinex hfiney.
-pose a := Num.sqrt (fine 'E_P[(Y ^+ 2)%R]).
-pose b := Num.sqrt (fine 'E_P[(X ^+ 2)%R]).
-have ex2_ge0 : 0 <= 'E_P[(X ^+ 2)%R] by apply expectation_ge0 => x /=; rewrite /mexp; exact: sqr_ge0.
-have ey2_ge0 : 0 <= 'E_P[(Y ^+ 2)%R] by apply expectation_ge0 => x /=; rewrite /mexp; exact: sqr_ge0.
-have [a0|a0] := eqVneq ('E_P[(Y ^+ 2)%R]) 0.
-- have: ae_eq P setT (EFin \o X) (EFin \o cst 0%R).
-  apply square_X_0_ae.
-  (* Here *)
-  Check (Lspace2_Lspace1).
-  rewrite a0 adde0.
-  have -> : 'E_P[(X \* Y)%R] = 0. admit.
-  rewrite /= mule0.
-  apply ex2_ge0.have [b0|b0] := eqVneq ('E (X`^+2)) 0.
-  rewrite b0 add0e.
-  have -> : 'E (X `* Y) = 0. admit.
-  rewrite /= mule0.
-  apply ey2_ge0.
-have H2ab : (2 * a * b * (b * a) = a * a * (fine 'E (X`^+2)) + b * b * (fine 'E (Y`^+2)))%R.
-  rewrite -(sqr_sqrtr (a:=fine 'E (X`^+2))); last (apply: fine_ge0; apply: expectation_ge0 => x; apply sqr_ge0).
-  rewrite -(sqr_sqrtr (a:=fine 'E (Y`^+2))); last (apply: fine_ge0; apply: expectation_ge0 => x; apply sqr_ge0).
-  rewrite -/a -/b /GRing.exp /=.
-  by rewrite mulrA (mulrC (_ * _) a)%R ![in LHS]mulrA (mulrC a) (mulrC _ (a * a)%R)
-             -![in LHS]mulrA mulrC mulr2n !mulrA mulrDr mulr1.
-Admitted.
-
-Lemma cauchy_schwarz' (X Y : {RV P >-> R}) :
-  ('Cov[ X , Y ])^+2 <= 'V X + 'V Y.
-Proof.
-rewrite /variance /covariance.
-apply cauchy_schwarz.
-Admitted.
-
-End covariance.
-Notation "''Cov' [ X , Y ]" := (covariance X Y).
-
 Definition distribution (d : _) (T : measurableType d) (R : realType)
     (P : probability T R) (X : {mfun T >-> R}) :=
   pushforward P (@measurable_funP _ _ _ X).
 
-Section distribution.
-Variables (d : _) (T : measurableType d) (R : realType) (P : probability T R)
-          (X : {mfun T >-> R}).
-
 Section distribution_is_probability.
 Context d (T : measurableType d) (R : realType) (P : probability T R)
         (X : {mfun T >-> R}).
@@ -544,6 +486,7 @@ Qed.
 
 End markov_chebyshev.
 
+
 HB.mixin Record MeasurableFun_isDiscrete d (T : measurableType d) (R : realType)
     (X : T -> R) of @MeasurableFun d T R X := {
   countable_range : countable (range X)
@@ -704,3 +647,83 @@ Qed.
 Local Close Scope ereal_scope.
 
 End discrete_distribution.
+
+Section covariance.
+Local Open Scope ereal_scope.
+Variables (d : _) (T : measurableType d) (R : realType) (P : probability T R).
+
+Definition covariance (X Y : {RV P >-> R}) :=
+  ('E_P [(X \- cst (fine 'E_P[X])) \* (Y \- cst (fine 'E_P[Y]))])%R.
+Local Notation "''Cov' [ X , Y ]" := (covariance X Y).
+
+Lemma expectation_sqr_eq0 (X : {RV P >-> R}) :
+  'E_P[X ^+ 2] = 0 -> ae_eq P setT (EFin \o X) (EFin \o cst 0%R).
+Proof.
+move => hx.
+have x20: ae_eq P setT (EFin \o (X ^+ 2)%R) (EFin \o cst 0%R).
+  apply ae_eq_integral_abs => //; first by apply/EFin_measurable_fun.
+    have -> : \int[P]_x `|(EFin \o (X ^+ 2)%R) x| = 'E_P[X ^+ 2] => //.
+      under eq_integral => x _. rewrite gee0_abs. over.
+      apply sqr_ge0.
+      reflexivity.
+apply: (ae_imply _ x20) => x /=.
+rewrite -expr2 => h0 _.
+apply EFin_inj in h0 => //.
+have: (X ^+ 2)%R x == 0%R. rewrite -h0 //.
+rewrite sqrf_eq0 /= => h1.
+rewrite (eqP h1) //.
+Qed.
+
+Lemma cauchy_schwarz (X Y : {RV P >-> R}) :
+  P.-integrable [set: T] (EFin \o X) -> P.-integrable [set: T] (EFin \o Y) ->
+  (* 'E X < +oo -> 'E Y < +oo -> TODO: use lspaces *)
+    'E_P[(X \* Y)%R] ^+2 <= 'E_P[(X ^+ 2)%R] + 'E_P[(Y ^+ 2)%R].
+Proof.
+move => hfinex hfiney.
+pose a := Num.sqrt (fine 'E_P[(Y ^+ 2)%R]).
+pose b := Num.sqrt (fine 'E_P[(X ^+ 2)%R]).
+have ex2_ge0 : 0 <= 'E_P[(X ^+ 2)%R] by apply expectation_ge0 => x /=; exact: sqr_ge0.
+have ey2_ge0 : 0 <= 'E_P[(Y ^+ 2)%R] by apply expectation_ge0 => x /=; exact: sqr_ge0.
+have [a0|a0] := eqVneq ('E_P[(Y ^+ 2)%R]) 0.
+- rewrite a0 adde0.
+  have y0: ae_eq P setT (EFin \o Y) (EFin \o cst 0%R) by apply expectation_sqr_eq0.
+  have -> : 'E_P[X \* Y] = 'E_P[cst 0%R].
+    apply: ae_eq_integral => //=.
+      apply measurable_funT_comp => //; apply measurable_funM => //.
+      apply measurable_fun_cst.
+      apply: (ae_imply _ y0) => x /= h _.
+      apply EFin_inj in h => //.
+      by rewrite h mulr0.
+  rewrite expectation_cst /= mule0.
+  apply expectation_ge0 => x.
+  apply sqr_ge0.
+have [b0|b0] := eqVneq ('E_P[(X ^+ 2)%R]) 0.
+- rewrite b0 add0e.
+  have x0: ae_eq P setT (EFin \o X) (EFin \o cst 0%R) by apply expectation_sqr_eq0.
+  have -> : 'E_P[X \* Y] = 'E_P[cst 0%R].
+    apply: ae_eq_integral => //=.
+      apply measurable_funT_comp => //; apply measurable_funM => //.
+      apply measurable_fun_cst.
+      apply: (ae_imply _ x0) => x /= h _.
+      apply EFin_inj in h => //.
+      by rewrite h mul0r.
+  rewrite expectation_cst /= mule0.
+  apply expectation_ge0 => x.
+  apply sqr_ge0.
+have H2ab : (2 * a * b * (b * a) = a * a * (fine 'E_P[X ^+ 2]) + b * b * (fine 'E_P[Y ^+ 2]))%R.
+  rewrite -(sqr_sqrtr (a:=fine 'E_P[X ^+ 2])); last (apply: fine_ge0; apply: expectation_ge0 => x; apply sqr_ge0).
+  rewrite -(sqr_sqrtr (a:=fine 'E_P[Y ^+ 2])); last (apply: fine_ge0; apply: expectation_ge0 => x; apply sqr_ge0).
+  rewrite -/a -/b /GRing.exp /=.
+  by rewrite mulrA (mulrC (_ * _) a)%R ![in LHS]mulrA (mulrC a) (mulrC _ (a * a)%R)
+             -![in LHS]mulrA mulrC mulr2n !mulrA mulrDr mulr1.
+Admitted.
+
+Lemma cauchy_schwarz' (X Y : {RV P >-> R}) :
+  ('Cov[ X , Y ])^+2 <= 'V_P[X] + 'V_P[Y].
+Proof.
+rewrite /variance /covariance.
+apply cauchy_schwarz.
+Admitted.
+
+End covariance.
+Notation "''Cov' [ X , Y ]" := (covariance X Y).