use powere_pos, fixes

CHANGELOG_UNRELEASED.md

@@ -76,66 +76,24 @@
     `powere_pose1`, `powere_posNyr` `powere_pos0r`, `powere_pos1r`,
     `powere_posNyr`, `fine_powere_pos`, `powere_pos_ge0`,
     `powere_pos_gt0`, `powere_pos_eq0`, `powere_posM`, `powere12_sqrt`
-- in `classical_sets.v`:
-  + canonical `unit_pointedType`
-- in `measure.v`:
-  + definition `finite_measure`
-  + mixin `isProbability`, structure `Probability`, type `probability`
-  + lemma `probability_le1`
-  + definition `discrete_measurable_unit`
-  + structures `sigma_finite_additive_measure` and `sigma_finite_measure`
-
-- in file `topology.v`,
-  + new definition `perfect_set`.
-  + new lemmas `perfectTP`, `perfect_prod`, and `perfect_diagonal`.
-
-- in `constructive_ereal.v`:
-  + lemma `oppe_inj`
-
-- in `mathcomp_extra.v`:
-  + lemma `add_onemK`
-  + function `swap`
-- in `classical_sets.v`:
-  + lemmas `setT0`, `set_unit`, `set_bool`
-  + lemmas `xsection_preimage_snd`, `ysection_preimage_fst`
-- in `exp.v`:
-  + lemma `expR_ge0`
-- in `measure.v`
-  + lemmas `measurable_curry`, `measurable_fun_fst`, `measurable_fun_snd`,
-    `measurable_fun_swap`, `measurable_fun_pair`, `measurable_fun_if_pair`
-  + lemmas `dirac0`, `diracT`
-  + lemma `finite_measure_sigma_finite`
-- in `lebesgue_measure.v`:
-  + lemma `measurable_fun_opp`
-- in `lebesgue_integral.v`
-  + lemmas `integral0_eq`, `fubini_tonelli`
-  + product measures now take `{measure _ -> _}` arguments and their
-    theory quantifies over a `{sigma_finite_measure _ -> _}`.
-
-- in `classical_sets.v`:
-  + lemma `trivIset_mkcond`
-- in `numfun.v`:
-  + lemmas `xsection_indic`, `ysection_indic`
-- in `classical_sets.v`:
-  + lemmas `xsectionI`, `ysectionI`
-- in `lebesgue_integral.v`:
-  + notations `\x`, `\x^` for `product_measure1` and `product_measure2`
 
 - file `ereal.v`:
   + lemmas `compreBr`, `compre_scale`
   + lemma `le_er_map`
+- file `lebesgue_measure.v`
+  + lemma `measurable_fun_er_map`
 - file `lebesgue_integral.v`:
   + instance of `isMeasurableFun` for `normr`
   + lemma `finite_measure_integrable_cst`
-  + lemma `measurable_fun_er_map`
   + lemma `ae_ge0_le_integral`
   + lemma `ae_eq_refl`
 - file `probability.v`:
   + mixin `isLfun`, structure `Lfun`, notation `LfunType`
   + canonicals `Lfun_eqType`, `Lfun_choiceType`, `Lequiv_canonical`
   + definition `LType`
+  + definitions `Lequiv`, `LspaceType`
   + definition `Lspace`, notation `.-Lspace`
-  + lemmas `LequivP`, `Lspace1`, `Lspace2`
+  + lemmas `LequivP`, `LType1_integrable`, `LType2_integrable_sqr`
   + definition `random_variable`, notation `{RV _ >-> _}`
   + lemmas `notin_range_measure`, `probability_range`
   + definition `distribution`, instance of `isProbability`
@@ -146,6 +104,7 @@
     `expectationB`
   + definition `variance`, `'V_P[X]`
   + lemma `varianceE`
+  + lemmas `variance_ge0`, `variance_cst`
   + lemmas `markov`, `chebyshev`,
   + mixin `MeasurableFun_isDiscrete`, structure `discreteMeasurableFun`,
     notation `{dmfun aT >-> T}`

theories/probability.v

@@ -5,6 +5,7 @@ Require Import boolp reals ereal.
 From HB Require Import structures.
 Require Import classical_sets signed functions topology normedtype cardinality.
 Require Import sequences esum measure numfun lebesgue_measure lebesgue_integral.
+Require Import exp.
 
 (******************************************************************************)
 (*                       Probability (experimental)                           *)
@@ -52,14 +53,14 @@ Local Open Scope classical_set_scope.
 Local Open Scope ring_scope.
 
 HB.mixin Record isLfun d (T : measurableType d) (R : realType)
-    (mu : {measure set T -> \bar R}) (p : nat) (f : T -> R) := {
+    (mu : {measure set T -> \bar R}) (p : R) (f : T -> R) := {
   measurable_lfun : measurable_fun [set: T] f ;
-  lfuny : (\int[mu]_x (`|f x| ^+ p)%:E < +oo)%E
+  lfuny : (\int[mu]_x (`|f x| `^ p)%:E < +oo)%E
 }.
 
 #[short(type=LfunType)]
-HB.structure Definition LFun d (T : measurableType d) (R : realType)
-    (mu : {measure set T -> \bar R}) (p : nat) :=
+HB.structure Definition Lfun d (T : measurableType d) (R : realType)
+    (mu : {measure set T -> \bar R}) (p : R) :=
   {f : T -> R & isLfun d T R mu p f}.
 
 #[global] Hint Resolve measurable_lfun : core.
@@ -68,15 +69,15 @@ Arguments lfuny {d} {T} {R} {mu} {p} _.
 
 Section Lfun_canonical.
 Context d (T : measurableType d) (R : realType).
-Variables (mu : {measure set T -> \bar R}) (p : nat).
+Variables (mu : {measure set T -> \bar R}) (p : R).
 
 Canonical Lfun_eqType := EqType (LfunType mu p) gen_eqMixin.
 Canonical Lfun_choiceType := ChoiceType (LfunType mu p) gen_choiceMixin.
 End Lfun_canonical.
 
 Section Lequiv.
 Context d (T : measurableType d) (R : realType).
-Variables (mu : {measure set T -> \bar R}) (p : nat).
+Variables (mu : {measure set T -> \bar R}) (p : R).
 
 Definition Lequiv (f g : LfunType mu p) := `[< {ae mu, forall x, f x = g x} >].
 
@@ -101,26 +102,20 @@ Canonical Lequiv_canonical :=
 
 Local Open Scope quotient_scope.
 
-Let Ltype := {eq_quot Lequiv}.
-Canonical Ltype_quotType := [quotType of Ltype].
-Canonical Ltype_eqType := [eqType of Ltype].
-Canonical Ltype_choiceType := [choiceType of Ltype].
-Canonical Ltype_eqQuotType := [eqQuotType Lequiv of Ltype].
-
-Record LType := MemLType { Lfun_class : Ltype }.
-Coercion LfunType_of_LType (f : LType) : LfunType mu p := repr (Lfun_class f).
-
-Canonical LType_subType' := [newType for Lfun_class].
-Canonical LType_subType := [subType Ltype of LfunType mu p by %/].
-Definition LType_eqMixin := Eval hnf in [eqMixin of LType by <:].
-Canonical LType_eqType := Eval hnf in EqType LType LType_eqMixin.
-Definition LType_choiceMixin := Eval hnf in [choiceMixin of LType by <:].
-Canonical LType_choiceType := Eval hnf in ChoiceType LType LType_choiceMixin.
+Definition LspaceType := {eq_quot Lequiv}.
+Canonical LspaceType_quotType := [quotType of LspaceType].
+Canonical LspaceType_eqType := [eqType of LspaceType].
+Canonical LspaceType_choiceType := [choiceType of LspaceType].
+Canonical LspaceType_eqQuotType := [eqQuotType Lequiv of LspaceType].
 
 Lemma LequivP (f g : LfunType mu p) :
-  reflect {ae mu, forall x, f x = g x} (f == g %[mod Ltype]).
+  reflect {ae mu, forall x, f x = g x} (f == g %[mod LspaceType]).
 Proof. by apply/(iffP idP); rewrite eqmodE// => /asboolP. Qed.
 
+Record LType := MemLType { Lfun_class : LspaceType }.
+Coercion LfunType_of_LType (f : LType) : LfunType mu p :=
+  repr (Lfun_class f).
+
 End Lequiv.
 
 Section Lspace.
@@ -130,20 +125,28 @@ Variable mu : {measure set T -> \bar R}.
 Definition Lspace p := [set: LType mu p].
 Arguments Lspace : clear implicits.
 
-Lemma Lspace1 (f : LType mu 1) : mu.-integrable setT (EFin \o f).
-Proof. by split; [exact/EFin_measurable_fun|exact: lfuny f]. Qed.
+Lemma LType1_integrable (f : LType mu 1) : mu.-integrable setT (EFin \o f).
+Proof.
+split; first exact/EFin_measurable_fun.
+under eq_integral.
+  move=> x _ /=.
+  rewrite -(@powere_pose1 _ `|f x|%:E)//.
+  over.
+exact: lfuny f.
+Qed.
 
-Lemma Lspace2 (f : LType mu 2%N) :
+Lemma LType2_integrable_sqr (f : LType mu 2) :
   mu.-integrable [set: T] (EFin \o (fun x => f x ^+ 2)).
 Proof.
-split.
-- exact/EFin_measurable_fun/measurable_fun_exprn.
-- rewrite (le_lt_trans _ (lfuny f))// ge0_le_integral//.
-  + apply: measurable_funT_comp => //.
-    exact/EFin_measurable_fun/measurable_fun_exprn.
-  + apply/EFin_measurable_fun/measurable_fun_exprn.
-    exact: measurable_funT_comp.
-  + by move=> t _/=; rewrite lee_fin normrX.
+split; first exact/EFin_measurable_fun/measurable_fun_exprn.
+rewrite (le_lt_trans _ (lfuny f))// ge0_le_integral//.
+- apply: measurable_funT_comp => //.
+  exact/EFin_measurable_fun/measurable_fun_exprn.
+- by move=> x _; rewrite lee_fin power_pos_ge0.
+- apply/EFin_measurable_fun.
+  under eq_fun do rewrite power_pos_mulrn//.
+  exact/measurable_fun_exprn/measurable_funT_comp.
+- by move=> t _/=; rewrite lee_fin normrX power_pos_mulrn.
 Qed.
 
 End Lspace.
@@ -363,9 +366,6 @@ have h (Y : {RV P >-> R}) :
     exact/measurable_fun_exprn/measurable_fun_id.
   - by move=> x /=; apply: sqr_ge0.
   - by move=> x /=; apply: sqr_ge0.
-simpl.
-
-
   - by apply/aeW => t /=; rewrite real_normK// num_real.
 have := h [the {mfun T >-> R} of (X \- cst (fine ('E_P[X])))%R].
 by move=> /le_trans; apply; rewrite lee_pmul2l// lte_fin invr_gt0 exprn_gt0.