From f8e1a1c7bc79275497914fcc8f43e24b839074d0 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Tue, 5 Nov 2024 11:35:42 +0900 Subject: [PATCH 01/10] expectation of product --- CHANGELOG_UNRELEASED.md | 325 +++++++++++ experimental_reals/discrete.v | 2 +- theories/measurable_realfun.v | 6 + theories/measure_theory/measurable_function.v | 11 + theories/numfun.v | 166 +++++- theories/probability.v | 542 +++++++++++++++++- 6 files changed, 1046 insertions(+), 6 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index dd5e81e1d5..6c0e1cb2fe 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -103,6 +103,173 @@ - in `lebesgue_integrable.v`: + lemma `integrable_set0` +- in `probability.v`: + + definition `ccdf` + + lemmas `lebesgue_stieltjes_cdf_id`, `cdf_ccdf_1`, `ccdf_nonincreasing`, `cvg_ccdfy0`, `cvg_ccdfNy1`, `ccdf_right_continuous`, `ge0_expectation_ccdf` + + corollaries `ccdf_cdf_1`, `ccdf_1_cdf`, `cdf_1_ccdf` + +- in `num_normedtype.v`: + + lemma `nbhs_infty_gtr` +- in `function_spaces.v`: + + lemmas `cvg_big`, `continuous_big` + +- in `realfun.v`: + + lemma `cvg_addrl_Ny` + +- in `constructive_ereal.v`: + + lemmas `mule_natr`, `dmule_natr` + + lemmas `inve_eqy`, `inve_eqNy` + +- in `uniform_structure.v`: + + lemma `continuous_injective_withinNx` + +- in `constructive_ereal.v`: + + variants `Ione`, `Idummy_placeholder` + + inductives `Inatmul`, `IEFin` + + definition `parse`, `print` + + number notations in scopes `ereal_dual_scope` and `ereal_scope` + + notation `- 1` in scopes `ereal_dual_scope` and `ereal_scope` +- in `pseudometric_normed_Zmodule.v`: + + lemma `le0_ball0` +- in `theories/landau.v`: + + lemma `littleoE0` + +- in `constructive_ereal.v`: + + lemma `lt0_adde` + +- in `unstable.v` + + lemmas `coprime_prodr`, `Gauss_dvd_prod`, `expn_prod`, `mono_leq_infl`, + `card_big_setU` + +- file `pnt.v` + + definitions `next_prime`, `prime_seq` + + lemmas `leq_prime_seq`, `mem_prime_seq` + + theorem `dvg_sum_inv_prime_seq` +- new directory `theories/measure_theory` with new files: + + `measurable_structure.v` + + `measure_function.v` + + `counting_measure.v` + + `dirac_measure.v` + + `probability_measure.v` + + `measure_negligible.v` + + `measure_extension.v` + + `measurable_function.v` + + `measure.v` + +- in `realfun.v`: + + lemmas `derivable_oy_continuous_within_itvcy`, + `derivable_oy_continuous_within_itvNyc` + + lemmas `derivable_oo_continuousW`, + `derivable_oy_continuousWoo`, + `derivable_oy_continuousW`, + `derivable_Nyo_continuousWoo`, + `derivable_Nyo_continuousW` +- in `probability.v`: + + lemmas `eq_bernoulli`, `eq_bernoulliV2` +- file `mathcomp_extra.v` + + lemmas `ge_trunc`, `lt_succ_trunc`, `trunc_ge_nat`, `trunc_lt_nat` + +- file `Rstruct.v` + + lemma `Pos_to_natE` (from `mathcomp_extra.v`) + + lemmas `RabsE`, `RdistE`, `sum_f_R0E`, `factE` + +- new file `internal_Eqdep_dec.v` (don't use, internal, to be removed) +- in `normedtype.v`: + + lemma `scaler1` + +- in `derive.v`: + + lemmas `horner0_ext`, `hornerD_ext`, `horner_scale_ext`, `hornerC_ext`, + `derivable_horner`, `derivE`, `continuous_horner` + + instance `is_derive_poly` +- in `mathcomp_extra.v`: + + lemma `partition_disjoint_bigfcup` +- in `lebesgue_measure.v`: + + lemma `measurable_indicP` +- in `constructive_ereal.v`: + + notation `\prod_( i <- r | P ) F` for extended real numbers and its variants + +- in `numfun.v`: + + defintions `funrpos`, `funrneg` with notations `^\+` and `^\-` + + lemmas `funrpos_ge0`, `funrneg_ge0`, `funrposN`, `funrnegN`, `ge0_funrposE`, + `ge0_funrnegE`, `le0_funrposE`, `le0_funrnegE`, `ge0_funrposM`, `ge0_funrnegM`, + `le0_funrposM`, `le0_funrnegM`, `funr_normr`, `funrposneg`, `funrD_Dpos`, + `funrD_posD`, `funrpos_le`, `funrneg_le` + + lemmas `funerpos`, `funerneg` + +- in `measure.v`: + + lemma `preimage_class_comp` + + defintions `mapping_display`, `g_sigma_algebra_mappingType`, `g_sigma_algebra_mapping`, + notations `.-mapping`, `.-mapping.-measurable` + +- in `lebesgue_measure.v`: + + lemma `measurable_indicP` + + lemmas `measurable_funrpos`, `measurable_funrneg` + +- in `lebesgue_integral.v`: + + lemmas `integral_fin_num_abs`, `Rintegral_cst`, `le_Rintegral` + +- new file `pi_irrational.v`: + + lemmas `measurable_poly` + + definition `rational` + + module `pi_irrational` + + lemma `pi_irrationnal` +- in `constructive_ereal.v`: + + notations `\prod` in scope ereal_scope + + lemmas `prode_ge0`, `prode_fin_num` +- in `probability.v`: + + lemma `expectation_def` + + notation `'M_` +- in `probability.v`: + + lemma `expectationM_ge0` + + definition `independent_events` + + definition `mutual_independence` + + definition `independent_RVs` + + definition `independent_RVs2` + + lemmas `g_sigma_algebra_mapping_comp`, `g_sigma_algebra_mapping_funrpos`, + `g_sigma_algebra_mapping_funrneg` + + lemmas `independent_RVs2_comp`, `independent_RVs2_funrposneg`, + `independent_RVs2_funrnegpos`, `independent_RVs2_funrnegneg`, + `independent_RVs2_funrpospos` + + lemma `expectationM_ge0`, `integrable_expectationM`, `independent_integrableM`, + ` expectation_prod` + +- in `numfun.v` + + lemmas `funeposE`, `funenegE`, `funepos_comp`, `funeneg_comp` + +- in `classical_sets.v`: + + lemmas `xsectionE`, `ysectionE` + +- file `constructive_ereal.v`: + + definition `iter_mule` + + lemma `prodEFin` + +- file `exp.v`: + + lemma `expR_sum` + +- file `lebesgue_integral.v`: + + lemma `measurable_fun_le` + +- in `trigo.v`: + + lemma `integral0oo_atan` + +- in `measure.v`: + + lemmas `mnormalize_id`, `measurable_fun_eqP` + +- in `ftc.v`: + + lemma `integrable_locally` + +- in `constructive_ereal.v`: + + lemma `EFin_bigmax` + +- in `mathcomp_extra.v`: + + lemmas `inr_inj`, `inl_inj` + +- in `classical_sets.v`: + + lemmas `in_set1`, `inr_in_set_inr`, `inl_in_set_inr`, `mem_image`, `mem_range`, `image_f` + + lemmas `inr_in_set_inl`, `inl_in_set_inl` + +- in `lebesgue_integral_approximation.v`: + + lemma `measurable_prod` - in `lebesgue_integrable.v`: + lemma `integrable_norm` @@ -172,6 +339,123 @@ - in `charge.v`: + `induced` -> `induced_charge` +- in `reals.v`: + + `sup_le_ub` -> `ge_sub` + + `le_inf` -> `inf_le` + + `le_sup` -> `sup_le` + + `sup_ubound` -> `ub_le_sup` + + `inf_lbound` -> `ge_inf` + + `ub_ereal_sup` -> `ge_ereal_sup` + + `ereal_inf_le` -> `ge_ereal_inf` + + `le_ereal_sup` -> `ereal_sup_le` + + `le_ereal_inf` -> `ereal_inf_le_tmp` + + `lb_ereal_inf` -> `le_ereal_inf_tmp` + + `ereal_sup_ge` -> `le_ereal_sup_tmp` +- in `kernel.v`: + + `isFiniteTransition` -> `isFiniteTransitionKernel` +- in `lebesgue_integral.v`: + + `fubini1a` -> `integrable12ltyP` + + `fubini1b` -> `integrable21ltyP` + + `measurable_funP` -> `measurable_funPT` (field of `isMeasurableFun` mixin) + +- in `mathcomp_extra.v` + + `comparable_min_le_min` -> `comparable_le_min2` + + `comparable_max_le_max` -> `comparable_le_max2` + + `min_le_min` -> `le_min2` + + `max_le_max` -> `le_max2` + + `real_sqrtC` -> `sqrtC_real` +- in `measure.v` + + `preimage_class` -> `preimage_set_system` + + `image_class` -> `image_set_system` + + `preimage_classes` -> `g_sigma_preimageU` + + `preimage_class_measurable_fun` -> `preimage_set_system_measurable_fun` + + `sigma_algebra_preimage_class` -> `sigma_algebra_preimage` + + `sigma_algebra_image_class` -> `sigma_algebra_image` + + `sigma_algebra_preimage_classE` -> `g_sigma_preimageE` + + `preimage_classes_comp` -> `g_sigma_preimageU_comp` + + +- in file `normedtype.v`, + changed `completely_regular_space` to depend on uniform separators + which removes the dependency on `R`. The old formulation can be + recovered easily with `uniform_separatorP`. + +- moved from `Rstruct.v` to `Rstruct_topology.v` + + lemmas `continuity_pt_nbhs`, `continuity_pt_cvg`, + `continuity_ptE`, `continuity_pt_cvg'`, `continuity_pt_dnbhs` + and `nbhs_pt_comp` + +- moved from `real_interval.v` to `normedtype.v` + + lemmas `set_itvK`, `RhullT`, `RhullK`, `set_itv_setT`, + `Rhull_smallest`, `le_Rhull`, `neitv_Rhull`, `Rhull_involutive`, + `disj_itv_Rhull` +- in `topology.v`: + + lemmas `subspace_pm_ball_center`, `subspace_pm_ball_sym`, + `subspace_pm_ball_triangle`, `subspace_pm_entourage` turned + into local `Let`'s + +- in `lebesgue_integral.v`: + + structure `SimpleFun` now inside a module `HBSimple` + + structure `NonNegSimpleFun` now inside a module `HBNNSimple` + + lemma `cst_nnfun_subproof` has now a different statement + + lemma `indic_nnfun_subproof` has now a different statement +- in `mathcomp_extra.v`: + + definition `idempotent_fun` + +- in `topology_structure.v`: + + definitions `regopen`, `regclosed` + + lemmas `closure_setC`, `interiorC`, `closureU`, `interiorU`, + `closureEbigcap`, `interiorEbigcup`, + `closure_open_regclosed`, `interior_closed_regopen`, + `closure_interior_idem`, `interior_closure_idem` + +- in file `topology_structure.v`, + + mixin `isContinuous`, type `continuousType`, structure `Continuous` + + new lemma `continuousEP`. + + new definition `mkcts`. + +- in file `subspace_topology.v`, + + new lemmas `continuous_subspace_setT`, `nbhs_prodX_subspace_inE`, and + `continuous_subspace_prodP`. + + type `continuousFunType`, HB structure `ContinuousFun` + +- in file `subtype_topology.v`, + + new lemmas `subspace_subtypeP`, `subspace_sigL_continuousP`, + `subspace_valL_continuousP'`, `subspace_valL_continuousP`, `sigT_of_setXK`, + `setX_of_sigTK`, `setX_of_sigT_continuous`, and `sigT_of_setX_continuous`. + +- in `lebesgue_integrale.v` + + change implicits of `measurable_funP` + +### Changed + +### Renamed + +- in `lebesgue_measure.v`: + + `measurable_fun_indic` -> `measurable_indic` + + `emeasurable_fun_sum` -> `emeasurable_sum` + + `emeasurable_fun_fsum` -> `emeasurable_fsum` + + `ge0_emeasurable_fun_sum` -> `ge0_emeasurable_sum` +- in `probability.v`: + + `expectationM` -> `expectationZl` + +- in `classical_sets.v`: + + `preimage_itv_o_infty` -> `preimage_itvoy` + + `preimage_itv_c_infty` -> `preimage_itvcy` + + `preimage_itv_infty_o` -> `preimage_itvNyo` + + `preimage_itv_infty_c` -> `preimage_itvNyc` + +- in `constructive_ereal.v`: + + `maxeMr` -> `maxe_pMr` + + `maxeMl` -> `maxe_pMl` + + `mineMr` -> `mine_pMr` + + `mineMl` -> `mine_pMl` + +- in `probability.v`: + + `integral_distribution` -> `ge0_integral_distribution` + + `expectationM` -> `expectationMl` + +- file `homotopy_theory/path.v` -> `homotopy_theory/continuous_path.v` ### Generalized @@ -256,6 +540,47 @@ - in `set_interval.v`: + lemma `interval_set1` (use `set_itv1` instead) +- in `ereal.v`: + + notation `ereal_sup_le` (was deprecated since 1.11.0) +- file `mathcomp_extra.v` + + lemma `Pos_to_natE` (moved to `Rstruct.v`) + + lemma `deg_le2_ge0` (available as `deg_le2_poly_ge0` in `ssrnum.v` + since MathComp 2.1.0) +- in `sequences.v`: + + notations `nneseries_pred0`, `eq_nneseries`, `nneseries0`, + `ereal_cvgPpinfty`, `ereal_cvgPninfty` (were deprecated since 0.6.0) +- in `topology_structure.v`: + + lemma `closureC` + +- in file `lebesgue_integral.v`: + + lemma `approximation` + +### Removed + +- in `lebesgue_integral.v`: + + definition `cst_mfun` + + lemma `mfun_cst` + +- in `cardinality.v`: + + lemma `cst_fimfun_subproof` + +- in `lebesgue_integral.v`: + + lemma `cst_mfun_subproof` (use lemma `measurable_cst` instead) + + lemma `cst_nnfun_subproof` (turned into a `Let`) + + lemma `indic_mfun_subproof` (use lemma `measurable_fun_indic` instead) + +- in `lebesgue_integral.v`: + + lemma `measurable_indic` (was uselessly specializing `measurable_fun_indic` (now `measurable_indic`) from `lebesgue_measure.v`) + + notation `measurable_fun_indic` (deprecation since 0.6.3) +- in `constructive_ereal.v` + + notation `lee_opp` (deprecated since 0.6.5) + + notation `lte_opp` (deprecated since 0.6.5) +- in `measure.v`: + + `dynkin_setI_bigsetI` (use `big_ind` instead) + +- in `lebesgue_measurable.v`: + + notation `measurable_fun_power_pos` (deprecated since 0.6.3) + + notation `measurable_power_pos` (deprecated since 0.6.4) ### Infrastructure diff --git a/experimental_reals/discrete.v b/experimental_reals/discrete.v index 63ca0e73b8..412877a07b 100644 --- a/experimental_reals/discrete.v +++ b/experimental_reals/discrete.v @@ -4,7 +4,7 @@ (* Copyright (c) - 2016--2018 - Polytechnique *) (* -------------------------------------------------------------------- *) -From Corelib Require Setoid. +From Coq Require Setoid. From HB Require Import structures. From mathcomp Require Import all_ssreflect all_algebra. From mathcomp.classical Require Import boolp. diff --git a/theories/measurable_realfun.v b/theories/measurable_realfun.v index 0e7947c120..fcd121560e 100644 --- a/theories/measurable_realfun.v +++ b/theories/measurable_realfun.v @@ -991,6 +991,12 @@ by move=> mf mg mD; move: (mD); apply: measurable_fun_if => //; [exact: measurable_fun_ltr|exact: measurable_funS mg|exact: measurable_funS mf]. Qed. +Lemma measurable_funrpos D f : measurable_fun D f -> measurable_fun D f^\+. +Proof. by move=> mf; exact: measurable_maxr. Qed. + +Lemma measurable_funrneg D f : measurable_fun D f -> measurable_fun D f^\-. +Proof. by move=> mf; apply: measurable_maxr => //; exact: measurableT_comp. Qed. + Lemma measurable_minr D f g : measurable_fun D f -> measurable_fun D g -> measurable_fun D (f \min g). Proof. diff --git a/theories/measure_theory/measurable_function.v b/theories/measure_theory/measurable_function.v index ce3f705fd3..300cce8b9f 100644 --- a/theories/measure_theory/measurable_function.v +++ b/theories/measure_theory/measurable_function.v @@ -331,6 +331,17 @@ HB.instance Definition _ := isMeasurableFun.Build _ _ _ _ (f \o g) End mfun_measurableType. +Lemma preimage_set_system_compS (aT : Type) + d (rT : measurableType d) d' (T : sigmaRingType d') + (g : rT -> T) (f : aT -> rT) (D : set aT) : + measurable_fun setT g -> + preimage_set_system D (g \o f) measurable `<=` + preimage_set_system D f measurable. +Proof. +move=> mg A; rewrite /preimage_set_system => -[B GB]; exists (g @^-1` B) => //. +by rewrite -[X in measurable X]setTI; exact: mg. +Qed. + Section measurability. (* f is measurable on the sigma-algebra generated by itself *) diff --git a/theories/numfun.v b/theories/numfun.v index 0ce6da7b8e..cd037679ae 100644 --- a/theories/numfun.v +++ b/theories/numfun.v @@ -25,12 +25,15 @@ From mathcomp Require Import sequences function_spaces. (* bounded_variation a b f == all variations of f are bounded *) (* {nnfun T >-> R} == type of non-negative functions *) (* f ^\+ == the function formed by the non-negative outputs *) -(* of f (from a type to the type of extended real *) -(* numbers) and 0 otherwise *) -(* rendered as f ⁺ with company-coq (U+207A) *) +(* of f and 0 otherwise *) +(* The codomain of f is the real numbers in scope *) +(* ring_scope and the extended real numbers in *) +(* scope ereal_scope. *) +(* Rendered as f ⁺ with company-coq (U+207A). *) (* f ^\- == the function formed by the non-positive outputs *) (* of f and 0 o.w. *) -(* rendered as f ⁻ with company-coq (U+207B) *) +(* Similar to ^\+. *) +(* Rendered as f ⁻ with company-coq (U+207B). *) (* \1_ A == indicator function 1_A *) (* ``` *) (* *) @@ -679,6 +682,149 @@ Proof. by apply/funext=> x; rewrite /patch/=; case: ifP; rewrite ?mule0. Qed. End erestrict_lemmas. +Section funrposneg. +Local Open Scope ring_scope. + +Definition funrpos T (R : realDomainType) (f : T -> R) := + fun x => Num.max (f x) 0. +Definition funrneg T (R : realDomainType) (f : T -> R) := + fun x => Num.max (- f x) 0. + +End funrposneg. + +Notation "f ^\+" := (funrpos f) : ring_scope. +Notation "f ^\-" := (funrneg f) : ring_scope. + +Section funrposneg_lemmas. +Local Open Scope ring_scope. +Variables (T : Type) (R : realDomainType) (D : set T). +Implicit Types (f g : T -> R) (r : R). + +Lemma funrpos_ge0 f x : 0 <= f^\+ x. +Proof. by rewrite /funrpos /= le_max lexx orbT. Qed. + +Lemma funrneg_ge0 f x : 0 <= f^\- x. +Proof. by rewrite /funrneg le_max lexx orbT. Qed. + +Lemma funrposN f : (\- f)^\+ = f^\-. Proof. exact/funext. Qed. + +Lemma funrnegN f : (\- f)^\- = f^\+. +Proof. by apply/funext => x; rewrite /funrneg opprK. Qed. + +(* TODO: the following lemmas require a pointed type and realDomainType does +not seem to be at this point + +Lemma funrpos_restrict f : (f \_ D)^\+ = (f^\+) \_ D. +Proof. +by apply/funext => x; rewrite /patch/_^\+; case: ifP; rewrite //= maxxx. +Qed. + +Lemma funrneg_restrict f : (f \_ D)^\- = (f^\-) \_ D. +Proof. +by apply/funext => x; rewrite /patch/_^\-; case: ifP; rewrite //= oppr0 maxxx. +Qed.*) + +Lemma ge0_funrposE f : (forall x, D x -> 0 <= f x) -> {in D, f^\+ =1 f}. +Proof. by move=> f0 x; rewrite inE => Dx; apply/max_idPl/f0. Qed. + +Lemma ge0_funrnegE f : (forall x, D x -> 0 <= f x) -> {in D, f^\- =1 cst 0}. +Proof. +by move=> f0 x; rewrite inE => Dx; apply/max_idPr; rewrite lerNl oppr0 f0. +Qed. + +Lemma le0_funrposE f : (forall x, D x -> f x <= 0) -> {in D, f^\+ =1 cst 0}. +Proof. by move=> f0 x; rewrite inE => Dx; exact/max_idPr/f0. Qed. + +Lemma le0_funrnegE f : (forall x, D x -> f x <= 0) -> {in D, f^\- =1 \- f}. +Proof. +by move=> f0 x; rewrite inE => Dx; apply/max_idPl; rewrite lerNr oppr0 f0. +Qed. + +Lemma ge0_funrposM r f : (0 <= r)%R -> + (fun x => r * f x)^\+ = (fun x => r * (f^\+ x)). +Proof. by move=> ?; rewrite funeqE => x; rewrite /funrpos maxr_pMr// mulr0. Qed. + +Lemma ge0_funrnegM r f : (0 <= r)%R -> + (fun x => r * f x)^\- = (fun x => r * (f^\- x)). +Proof. +by move=> r0; rewrite funeqE => x; rewrite /funrneg -mulrN maxr_pMr// mulr0. +Qed. + +Lemma le0_funrposM r f : (r <= 0)%R -> + (fun x => r * f x)^\+ = (fun x => - r * (f^\- x)). +Proof. +move=> r0; rewrite -[in LHS](opprK r); under eq_fun do rewrite mulNr. +by rewrite funrposN ge0_funrnegM ?oppr_ge0. +Qed. + +Lemma le0_funrnegM r f : (r <= 0)%R -> + (fun x => r * f x)^\- = (fun x => - r * (f^\+ x)). +Proof. +move=> r0; rewrite -[in LHS](opprK r); under eq_fun do rewrite mulNr. +by rewrite funrnegN ge0_funrposM ?oppr_ge0. +Qed. + +Lemma funr_normr f : Num.norm \o f = f^\+ \+ f^\-. +Proof. +rewrite funeqE => x /=; have [fx0|/ltW fx0] := leP (f x) 0. +- rewrite ler0_norm// /funrpos /funrneg. + move/max_idPr : (fx0) => ->; rewrite add0r. + by move: fx0; rewrite -{1}oppr0 lerNr => /max_idPl ->. +- rewrite ger0_norm// /funrpos /funrneg; move/max_idPl : (fx0) => ->. + by move: fx0; rewrite -{1}oppr0 lerNl => /max_idPr ->; rewrite addr0. +Qed. + +Lemma funrposneg f : f = (fun x => f^\+ x - f^\- x). +Proof. +rewrite funeqE => x; rewrite /funrpos /funrneg; have [|/ltW] := leP (f x) 0. + by rewrite -{1}oppr0 -lerNr => /max_idPl ->; rewrite opprK add0r. +by rewrite -{1}oppr0 -lerNl => /max_idPr ->; rewrite subr0. +Qed. + +Lemma funrD_Dpos f g : f \+ g = (f \+ g)^\+ \- (f \+ g)^\-. +Proof. +apply/funext => x; rewrite /funrpos /funrneg/=; have [|/ltW] := lerP 0 (f x + g x). +- by rewrite -{1}oppr0 -lerNl => /max_idPr ->; rewrite subr0. +- by rewrite -{1}oppr0 -lerNr => /max_idPl ->; rewrite opprK add0r. +Qed. + +Lemma funrD_posD f g : f \+ g = (f^\+ \+ g^\+) \- (f^\- \+ g^\-). +Proof. +apply/funext => x; rewrite /funrpos /funrneg/=. +have [|fx0] := lerP 0 (f x); last rewrite add0r. +- rewrite -{1}oppr0 lerNl => /max_idPr ->; have [|/ltW] := lerP 0 (g x). + by rewrite -{1}oppr0 lerNl => /max_idPr ->; rewrite addr0 subr0. + by rewrite -{1}oppr0 -lerNr => /max_idPl ->; rewrite addr0 sub0r opprK. +- move/ltW : (fx0); rewrite -{1}oppr0 lerNr => /max_idPl ->. + have [|]/= := lerP 0 (g x); last rewrite add0r. + by rewrite -{1}oppr0 lerNl => /max_idPr ->; rewrite addr0 opprK addrC. + by rewrite -oppr0 ltrNr -{1}oppr0 => /ltW/max_idPl ->; rewrite opprD !opprK. +Qed. + +Lemma funrpos_le f g : + {in D, forall x, f x <= g x} -> {in D, forall x, f^\+ x <= g^\+ x}. +Proof. +move=> fg x Dx; rewrite /funrpos /Num.max; case: ifPn => fx; case: ifPn => gx//. +- by rewrite leNgt. +- by move: fx; rewrite -leNgt => /(lt_le_trans gx); rewrite ltNge fg. +- exact: fg. +Qed. + +Lemma funrneg_le f g : + {in D, forall x, f x <= g x} -> {in D, forall x, g^\- x <= f^\- x}. +Proof. +move=> fg x Dx; rewrite /funrneg /Num.max; case: ifPn => gx; case: ifPn => fx//. +- by rewrite leNgt. +- by move: gx; rewrite -leNgt => /(lt_le_trans fx); rewrite ltrN2 ltNge fg. +- by rewrite lerN2; exact: fg. +Qed. + +End funrposneg_lemmas. +#[global] +Hint Extern 0 (is_true (0%R <= _ ^\+ _)%R) => solve [apply: funrpos_ge0] : core. +#[global] +Hint Extern 0 (is_true (0%R <= _ ^\- _)%R) => solve [apply: funrneg_ge0] : core. + HB.lock Definition funepos T (R : realDomainType) (f : T -> \bar R) := fun x => maxe (f x) 0. @@ -844,7 +990,19 @@ Hint Extern 0 (is_true (0%R <= _ ^\+ _)%E) => solve [apply: funepos_ge0] : core. #[global] Hint Extern 0 (is_true (0%R <= _ ^\- _)%E) => solve [apply: funeneg_ge0] : core. +Section funrpos_funepos_lemmas. +Context {T : Type} {R : realDomainType}. + +Lemma funerpos (f : T -> R) : (EFin \o f)^\+%E = (EFin \o f^\+). +Proof. by apply/funext => x; rewrite funeposE /funrpos/= EFin_max. Qed. + +Lemma funerneg (f : T -> R) : (EFin \o f)^\-%E = (EFin \o f^\-). +Proof. by apply/funext => x; rewrite funenegE /funrneg/= EFin_max. Qed. + +End funrpos_funepos_lemmas. + Definition indic {T} {R : pzRingType} (A : set T) (x : T) : R := (x \in A)%:R. + Reserved Notation "'\1_' A" (at level 8, A at level 2, format "'\1_' A") . Notation "'\1_' A" := (indic A) : ring_scope. diff --git a/theories/probability.v b/theories/probability.v index 0c87621819..28e4d28ddb 100644 --- a/theories/probability.v +++ b/theories/probability.v @@ -45,6 +45,10 @@ From mathcomp Require Import charge ftc gauss_integral hoelder. (* ccdf X r == complementary cumulative distribution function of X *) (* := distribution P X `]r, +oo[ *) (* enum_prob X k == probability of the kth value in the range of X *) +(* independent_events I F == the events F indexed by I are independent *) +(* mutual_independence I F == the classes F indexed by I are independent *) +(* independent_RVs I X == the random variables X indexed by I are independent *) +(* independent_RVs2 X Y == the random variables X and Y are independent *) (* ``` *) (* *) (* ``` *) @@ -842,6 +846,24 @@ Definition mmt_gen_fun d (T : measurableType d) (R : realType) (P : probability T R) (X : T -> R) (t : R) := ('E_P[expR \o t \o* X])%E. Notation "'M_ P X" := (@mmt_gen_fun _ _ _ P X). +(* TODO: move earlier *) +Section mfun_measurable_realType. +Context {d} {aT : measurableType d} {rT : realType}. + +HB.instance Definition _ (f : {mfun aT >-> rT}) := + @isMeasurableFun.Build d _ _ _ f^\+ + (measurable_funrpos (@measurable_funPT _ _ _ _ f)). + +HB.instance Definition _ (f : {mfun aT >-> rT}) := + @isMeasurableFun.Build d _ _ _ f^\- + (measurable_funrneg (@measurable_funPT _ _ _ _ f)). + +HB.instance Definition _ (f : {mfun aT >-> rT}) := + @isMeasurableFun.Build d _ _ _ (@normr _ _ \o f) + (measurableT_comp (@normr_measurable _ _) (@measurable_funPT _ _ _ _ f)). + +End mfun_measurable_realType. + Section markov_chebyshev_cantelli. Local Open Scope ereal_scope. Context d (T : measurableType d) (R : realType) (P : probability T R). @@ -1134,6 +1156,524 @@ Qed. End discrete_distribution. +Section independent_events. +Context {R : realType} d {T : measurableType d}. +Variable P : probability T R. +Local Open Scope ereal_scope. + +Definition independent_events (I0 : choiceType) (I : set I0) (A : I0 -> set T) := + forall J : {fset I0}, [set` J] `<=` I -> + P (\bigcap_(i in [set` J]) A i) = \prod_(i <- J) P (A i). + +End independent_events. + +Section mutual_independence. +Context {R : realType} d {T : measurableType d}. +Variable P : probability T R. +Local Open Scope ereal_scope. + +Definition mutual_independence (I0 : choiceType) (I : set I0) + (F : I0 -> set (set T)) := + (forall i : I0, I i -> F i `<=` @measurable _ T) /\ + forall J : {fset I0}, + [set` J] `<=` I -> + forall E : I0 -> set T, + (forall i : I0, i \in J -> E i \in F i) -> + P (\big[setI/setT]_(j <- J) E j) = \prod_(j <- J) P (E j). + +End mutual_independence. + +(* g_sigma_algebra_mapping f == sigma-algebra generated by the mapping f *) +(* g_sigma_algebra_mappingType f == the measurableType corresponding to *) +(* g_sigma_algebra_mapping f *) +(* This is an HB alias. *) +(* f.-mapping.-measurable A == A is measurable for g_sigma_algebra_mapping f *) + +Definition mapping_display {T T'} : (T -> T') -> measure_display. +Proof. exact. Qed. + +Definition g_sigma_algebra_mappingType d' (T : pointedType) + (T' : measurableType d') (f : T -> T') : Type := T. + +Definition g_sigma_algebra_mapping d' (T : pointedType) + (T' : measurableType d') (f : T -> T') := + preimage_set_system setT f (@measurable _ T'). + +Section mapping_generated_sigma_algebra. +Context {d'} (T : pointedType) (T' : measurableType d'). +Variable f : T -> T'. + +Let mapping_set0 : g_sigma_algebra_mapping f set0. +Proof. +rewrite /g_sigma_algebra_mapping /preimage_set_system/=. +by exists set0 => //; rewrite preimage_set0 setI0. +Qed. + +Let mapping_setC A : + g_sigma_algebra_mapping f A -> g_sigma_algebra_mapping f (~` A). +Proof. +rewrite /g_sigma_algebra_mapping /preimage_set_system/= => -[B mB] <-{A}. +by exists (~` B); [exact: measurableC|rewrite !setTI preimage_setC]. +Qed. + +Let mapping_bigcup (F : (set T)^nat) : + (forall i, g_sigma_algebra_mapping f (F i)) -> + g_sigma_algebra_mapping f (\bigcup_i (F i)). +Proof. +move=> mF; rewrite /g_sigma_algebra_mapping /preimage_set_system/=. +pose g := fun i => sval (cid2 (mF i)). +pose mg := fun i => svalP (cid2 (mF i)). +exists (\bigcup_i g i). + by apply: bigcup_measurable => k; case: (mg k). +rewrite setTI /g preimage_bigcup; apply: eq_bigcupr => k _. +by case: (mg k) => _; rewrite setTI. +Qed. + +HB.instance Definition _ := Pointed.on (g_sigma_algebra_mappingType f). + +HB.instance Definition _ := @isMeasurable.Build (mapping_display f) + (g_sigma_algebra_mappingType f) (g_sigma_algebra_mapping f) + mapping_set0 mapping_setC mapping_bigcup. + +End mapping_generated_sigma_algebra. + +Notation "f .-mapping" := (mapping_display f) : measure_display_scope. +Notation "f .-mapping.-measurable" := + (measurable : set (set (g_sigma_algebra_mappingType f))) : classical_set_scope. + +Section independent_RVs. +Context {R : realType} d d' (T : measurableType d) (T' : measurableType d'). +Variable P : probability T R. + +Definition independent_RVs (I0 : choiceType) (I : set I0) + (X : I0 -> {mfun T >-> T'}) : Prop := + mutual_independence P I (fun i => g_sigma_algebra_mapping (X i)). + +Definition independent_RVs2 (X Y : {mfun T >-> T'}) := + independent_RVs [set 0%N; 1%N] + [eta (fun=> cst point) with 0%N |-> X, 1%N |-> Y]. + +End independent_RVs. + +Section g_sigma_algebra_mapping_lemmas. +Context d {T : measurableType d} {R : realType}. + +Lemma g_sigma_algebra_mapping_comp (X : {mfun T >-> R}) (f : R -> R) : + measurable_fun setT f -> + g_sigma_algebra_mapping (f \o X)%R `<=` g_sigma_algebra_mapping X. +Proof. exact: preimage_set_system_compS. Qed. + +Lemma g_sigma_algebra_mapping_funrpos (X : {mfun T >-> R}) : + g_sigma_algebra_mapping X^\+%R `<=` d.-measurable. +Proof. +by move=> A/= -[B mB] <-; have := measurable_funrpos (measurable_funP X); exact. +Qed. + +Lemma g_sigma_algebra_mapping_funrneg (X : {mfun T >-> R}) : + g_sigma_algebra_mapping X^\-%R `<=` d.-measurable. +Proof. +by move=> A/= -[B mB] <-; have := measurable_funrneg (measurable_funP X); exact. +Qed. + +End g_sigma_algebra_mapping_lemmas. +Arguments g_sigma_algebra_mapping_comp {d T R X} f. + +Section independent_RVs_lemmas. +Context {R : realType} d d' (T : measurableType d) (T' : measurableType d'). +Variable P : probability T R. +Local Open Scope ring_scope. + +Lemma independent_RVs2_comp (X Y : {RV P >-> R}) (f g : {mfun R >-> R}) : + independent_RVs2 P X Y -> independent_RVs2 P (f \o X) (g \o Y). +Proof. +move=> indeXY; split => [i [|]->{i}/= Z/=|J J01 E JE]. +- by rewrite /g_sigma_algebra_mapping/= /preimage_set_system/= => -[B mB <-]; + exact/measurableT_comp. +- by rewrite /g_sigma_algebra_mapping/= /preimage_set_system/= => -[B mB <-]; + exact/measurableT_comp. +- apply indeXY => //= i iJ; have := JE _ iJ. + have : i \in [set 0%N; 1%N] by rewrite inE; apply: J01. + rewrite inE/= => -[|] /eqP ->/=; rewrite !inE. + + exact: g_sigma_algebra_mapping_comp. + + by case: ifPn => [/eqP ->|i0]; exact: g_sigma_algebra_mapping_comp. +Qed. + +Lemma independent_RVs2_funrposneg (X Y : {RV P >-> R}) : + independent_RVs2 P X Y -> independent_RVs2 P X^\+ Y^\-. +Proof. +move=> indeXY; split=> [/= i [|] -> /=|J J01 E JE]. +- exact: g_sigma_algebra_mapping_funrpos. +- exact: g_sigma_algebra_mapping_funrneg. +- apply indeXY => //= i iJ; have := JE _ iJ. + move/J01 : (iJ) => /= -[|] ->//=; rewrite !inE. + + apply: (g_sigma_algebra_mapping_comp (fun x => maxr x 0)%R). + exact: measurable_funrpos. + + apply: (g_sigma_algebra_mapping_comp (fun x => maxr (- x) 0)%R). + exact: measurable_funrneg. +Qed. + +Lemma independent_RVs2_funrnegpos (X Y : {RV P >-> R}) : + independent_RVs2 P X Y -> independent_RVs2 P X^\- Y^\+. +Proof. +move=> indeXY; split=> [/= i [|] -> /=|J J01 E JE]. +- exact: g_sigma_algebra_mapping_funrneg. +- exact: g_sigma_algebra_mapping_funrpos. +- apply indeXY => //= i iJ; have := JE _ iJ. + move/J01 : (iJ) => /= -[|] ->//=; rewrite !inE. + + apply: (g_sigma_algebra_mapping_comp (fun x => maxr (- x) 0)%R). + exact: measurable_funrneg. + + apply: (g_sigma_algebra_mapping_comp (fun x => maxr x 0)%R). + exact: measurable_funrpos. +Qed. + +Lemma independent_RVs2_funrnegneg (X Y : {RV P >-> R}) : + independent_RVs2 P X Y -> independent_RVs2 P X^\- Y^\-. +Proof. +move=> indeXY; split=> [/= i [|] -> /=|J J01 E JE]. +- exact: g_sigma_algebra_mapping_funrneg. +- exact: g_sigma_algebra_mapping_funrneg. +- apply indeXY => //= i iJ; have := JE _ iJ. + move/J01 : (iJ) => /= -[|] ->//=; rewrite !inE. + + apply: (g_sigma_algebra_mapping_comp (fun x => maxr (- x) 0)%R). + exact: measurable_funrneg. + + apply: (g_sigma_algebra_mapping_comp (fun x => maxr (- x) 0)%R). + exact: measurable_funrneg. +Qed. + +Lemma independent_RVs2_funrpospos (X Y : {RV P >-> R}) : + independent_RVs2 P X Y -> independent_RVs2 P X^\+ Y^\+. +Proof. +move=> indeXY; split=> [/= i [|] -> /=|J J01 E JE]. +- exact: g_sigma_algebra_mapping_funrpos. +- exact: g_sigma_algebra_mapping_funrpos. +- apply indeXY => //= i iJ; have := JE _ iJ. + move/J01 : (iJ) => /= -[|] ->//=; rewrite !inE. + + apply: (g_sigma_algebra_mapping_comp (fun x => maxr x 0)%R). + exact: measurable_funrpos. + + apply: (g_sigma_algebra_mapping_comp (fun x => maxr x 0)%R). + exact: measurable_funrpos. +Qed. + +End independent_RVs_lemmas. + +Section product_expectation. +Context {R : realType} d (T : measurableType d). +Variable P : probability T R. +Local Open Scope ereal_scope. + +Import HBNNSimple. + +Let expectationM_nnsfun (f g : {nnsfun T >-> R}) : + (forall y y', y \in range f -> y' \in range g -> + P (f @^-1` [set y] `&` g @^-1` [set y']) = + P (f @^-1` [set y]) * P (g @^-1` [set y'])) -> + 'E_P [f \* g] = 'E_P [f] * 'E_P [g]. +Proof. +move=> fg; transitivity + ('E_P [(fun x => (\sum_(y \in range f) y * \1_(f @^-1` [set y]) x)%R) + \* (fun x => (\sum_(y \in range g) y * \1_(g @^-1` [set y]) x)%R)]). + by congr ('E_P [_]); apply/funext => t/=; rewrite (fimfunE f) (fimfunE g). +transitivity ('E_P [(fun x => (\sum_(y \in range f) \sum_(y' \in range g) y * y' + * \1_(f @^-1` [set y] `&` g @^-1` [set y']) x)%R)]). + congr ('E_P [_]); apply/funext => t/=. + rewrite mulrC; rewrite fsbig_distrr//=. (* TODO: lemma fsbig_distrl *) + apply: eq_fsbigr => y yf; rewrite mulrC; rewrite fsbig_distrr//=. + by apply: eq_fsbigr => y' y'g; rewrite indicI mulrCA !mulrA (mulrC y'). +rewrite unlock. +under eq_integral do rewrite -fsumEFin//. +transitivity (\sum_(y \in range f) (\sum_(y' \in range g) + ((y * y')%:E * \int[P]_w (\1_(f @^-1` [set y] `&` g @^-1` [set y']) w)%:E))). + rewrite ge0_integral_fsum//=; last 2 first. + - move=> r; under eq_fun do rewrite -fsumEFin//. + apply: emeasurable_fun_fsum => // s. + apply/measurable_EFinP/measurable_funM => //. + exact/measurable_indic/measurableI. + - move=> r t _; rewrite lee_fin sumr_ge0 // => s _; rewrite -lee_fin. + by rewrite indicI/= indicE -mulrACA EFinM mule_ge0// nnfun_muleindic_ge0. + apply: eq_fsbigr => y yf. + under eq_integral do rewrite -fsumEFin//. + rewrite ge0_integral_fsum//=; last 2 first. + - move=> r; apply/measurable_EFinP; apply: measurable_funM => //. + exact/measurable_indic/measurableI. + - move=> r t _. + by rewrite indicI/= indicE -mulrACA EFinM mule_ge0// nnfun_muleindic_ge0. + apply: eq_fsbigr => y' y'g. + under eq_integral do rewrite EFinM. + by rewrite integralZl//; exact/integrable_indic/measurableI. +transitivity (\sum_(y \in range f) (\sum_(y' \in range g) + ((y * y')%:E * (\int[P]_w (\1_(f @^-1` [set y]) w)%:E * + \int[P]_w (\1_(g @^-1` [set y']) w)%:E)))). + apply: eq_fsbigr => y fy; apply: eq_fsbigr => y' gy'; congr *%E. + transitivity ('E_P[\1_(f @^-1` [set y] `&` g @^-1` [set y'])]). + by rewrite unlock. + transitivity ('E_P[\1_(f @^-1` [set y])] * 'E_P[\1_(g @^-1` [set y'])]); + last by rewrite unlock. + rewrite expectation_indic//; last exact: measurableI. + by rewrite !expectation_indic// fg. +transitivity ( + (\sum_(y \in range f) (y%:E * (\int[P]_w (\1_(f @^-1` [set y]) w)%:E))) * + (\sum_(y' \in range g) (y'%:E * \int[P]_w (\1_(g @^-1` [set y']) w)%:E))). + transitivity (\sum_(y \in range f) (\sum_(y' \in range g) + (y'%:E * \int[P]_w (\1_(g @^-1` [set y']) w)%:E)%E)%R * + (y%:E * \int[P]_w (\1_(f @^-1` [set y]) w)%:E)%E%R); last first. + rewrite !fsbig_finite//= ge0_sume_distrl//; last first. + move=> r _; rewrite -integralZl//; last exact: integrable_indic. + by apply: integral_ge0 => t _; rewrite nnfun_muleindic_ge0. + by apply: eq_bigr => r _; rewrite muleC. + apply: eq_fsbigr => y fy. + rewrite !fsbig_finite//= ge0_sume_distrl//; last first. + move=> r _; rewrite -integralZl//; last exact: integrable_indic. + by apply: integral_ge0 => t _; rewrite nnfun_muleindic_ge0. + apply: eq_bigr => r _; rewrite (mulrC y) EFinM. + by rewrite [X in _ * X]muleC muleACA. +suff: forall h : {nnsfun T >-> R}, + (\sum_(y \in range h) (y%:E * \int[P]_w (\1_(h @^-1` [set y]) w)%:E)%E)%R + = \int[P]_w (h w)%:E. + by move=> suf; congr *%E; rewrite suf. +move=> h. +apply/esym. +under eq_integral do rewrite (fimfunE h). +under eq_integral do rewrite -fsumEFin//. +rewrite ge0_integral_fsum//; last 2 first. +- by move=> r; exact/measurable_EFinP/measurable_funM. +- by move=> r t _; rewrite lee_fin -lee_fin nnfun_muleindic_ge0. +by apply: eq_fsbigr => y fy; rewrite -integralZl//; exact/integrable_indic. +Qed. + +Lemma expectationM_ge0 (X Y : {RV P >-> R}) : + independent_RVs2 P X Y -> + 'E_P[X] *? 'E_P[Y] -> + (forall t, 0 <= X t)%R -> (forall t, 0 <= Y t)%R -> + 'E_P [X * Y] = 'E_P [X] * 'E_P [Y]. +Proof. +move=> indeXY defXY X0 Y0. +have mX : measurable_fun setT (EFin \o X) by exact/measurable_EFinP. +have mY : measurable_fun setT (EFin \o Y) by exact/measurable_EFinP. +pose X_ := nnsfun_approx measurableT mX. +pose Y_ := nnsfun_approx measurableT mY. +have EXY : 'E_P[X_ n \* Y_ n] @[n --> \oo] --> 'E_P [X * Y]. + rewrite unlock; have -> : \int[P]_w ((X * Y) w)%:E = + \int[P]_x limn (fun n => (EFin \o (X_ n \* Y_ n)%R) x). + apply: eq_integral => t _; apply/esym/cvg_lim => //=. + rewrite fctE EFinM; under eq_fun do rewrite EFinM. + by apply: cvgeM; [rewrite mule_def_fin//| + apply: cvg_nnsfun_approx => //= x _; rewrite lee_fin..]. + apply: cvg_monotone_convergence => //. + - by move=> n; apply/measurable_EFinP; exact: measurable_funM. + - by move=> n t _; rewrite lee_fin. + - move=> t _ m n mn. + by rewrite lee_fin/= ler_pM//; exact/lefP/nd_nnsfun_approx. +have EX : 'E_P[X_ n] @[n --> \oo] --> 'E_P [X]. + rewrite unlock. + have -> : \int[P]_w (X w)%:E = \int[P]_x limn (fun n => (EFin \o X_ n) x). + by apply: eq_integral => t _; apply/esym/cvg_lim => //=; + apply: cvg_nnsfun_approx => // x _; rewrite lee_fin. + apply: cvg_monotone_convergence => //. + - by move=> n; exact/measurable_EFinP. + - by move=> n t _; rewrite lee_fin. + - by move=> t _ m n mn; rewrite lee_fin/=; exact/lefP/nd_nnsfun_approx. +have EY : 'E_P[Y_ n] @[n --> \oo] --> 'E_P [Y]. + rewrite unlock. + have -> : \int[P]_w (Y w)%:E = \int[P]_x limn (fun n => (EFin \o Y_ n) x). + by apply: eq_integral => t _; apply/esym/cvg_lim => //=; + apply: cvg_nnsfun_approx => // x _; rewrite lee_fin. + apply: cvg_monotone_convergence => //. + - by move=> n; exact/measurable_EFinP. + - by move=> n t _; rewrite lee_fin. + - by move=> t _ m n mn; rewrite lee_fin/=; exact/lefP/nd_nnsfun_approx. +have {EX EY}EXY' : 'E_P[X_ n] * 'E_P[Y_ n] @[n --> \oo] --> 'E_P[X] * 'E_P[Y]. + apply: cvgeM => //. +suff : forall n, 'E_P[X_ n \* Y_ n] = 'E_P[X_ n] * 'E_P[Y_ n]. + by move=> suf; apply: (cvg_unique _ EXY) => //=; under eq_fun do rewrite suf. +move=> n; apply: expectationM_nnsfun => x y xX_ yY_. +suff : P (\big[setI/setT]_(j <- [fset 0%N; 1%N]%fset) + [eta fun=> set0 with 0%N |-> X_ n @^-1` [set x], + 1%N |-> Y_ n @^-1` [set y]] j) = + \prod_(j <- [fset 0%N; 1%N]%fset) + P ([eta fun=> set0 with 0%N |-> X_ n @^-1` [set x], + 1%N |-> Y_ n @^-1` [set y]] j). + by rewrite !big_fsetU1/= ?inE//= !big_seq_fset1/=. +move: indeXY => [/= _]; apply => // i. + by rewrite /= !inE => /orP[|]/eqP ->; auto. +pose AX := dyadic_approx setT (EFin \o X). +pose AY := dyadic_approx setT (EFin \o Y). +pose BX := integer_approx setT (EFin \o X). +pose BY := integer_approx setT (EFin \o Y). +have mA (Z : {RV P >-> R}) m k : (k < m * 2 ^ m)%N -> + g_sigma_algebra_mapping Z (dyadic_approx setT (EFin \o Z) m k). + move=> mk; rewrite /g_sigma_algebra_mapping /dyadic_approx mk setTI. + rewrite /preimage_class/=; exists [set` dyadic_itv R m k] => //. + rewrite setTI/=; apply/seteqP; split => z/=. + by rewrite inE/= => Zz; exists (Z z). + by rewrite inE/= => -[r rmk] [<-]. +have mB (Z : {RV P >-> R}) k : + g_sigma_algebra_mapping Z (integer_approx setT (EFin \o Z) k). + rewrite /g_sigma_algebra_mapping /integer_approx setTI /preimage_set_system/=. + by exists `[k%:R, +oo[%classic => //; rewrite setTI preimage_itvcy. +have m1A (Z : {RV P >-> R}) : forall k, (k < n * 2 ^ n)%N -> + measurable_fun setT + (\1_(dyadic_approx setT (EFin \o Z) n k) : g_sigma_algebra_mappingType Z -> R). + move=> k kn. + exact/(@measurable_indicP _ (g_sigma_algebra_mappingType Z))/mA. +rewrite !inE => /orP[|]/eqP->{i} //=. + have : @measurable_fun _ _ (g_sigma_algebra_mappingType X) _ setT (X_ n). + rewrite nnsfun_approxE//. + apply: measurable_funD => //=. + apply: measurable_sum => //= k'; apply: measurable_funM => //. + by apply: measurable_indic; exact: mA. + apply: measurable_funM => //. + by apply: measurable_indic; exact: mB. + rewrite /measurable_fun => /(_ measurableT _ (measurable_set1 x)). + by rewrite setTI. +have : @measurable_fun _ _ (g_sigma_algebra_mappingType Y) _ setT (Y_ n). + rewrite nnsfun_approxE//. + apply: measurable_funD => //=. + apply: measurable_sum => //= k'; apply: measurable_funM => //. + by apply: measurable_indic; exact: mA. + apply: measurable_funM => //. + by apply: measurable_indic; exact: mB. +move=> /(_ measurableT [set y] (measurable_set1 y)). +by rewrite setTI. +Qed. + +Lemma integrable_expectationM (X Y : {RV P >-> R}) : + independent_RVs2 P X Y -> + (X : T -> R) \in Lfun P 1 -> (Y : T -> R) \in Lfun P 1 -> + `|'E_P [X * Y]| < +oo. +Proof. +move=> indeXY iX iY. +apply: (@le_lt_trans _ _ 'E_P[(@normr _ _ \o X) * (@normr _ _ \o Y)]). + rewrite unlock/=. + rewrite (le_trans (le_abse_integral _ _ _))//. + apply/measurable_EFinP/measurable_funM. + by move/Lfun1_integrable : iX => /measurable_int. + by move/Lfun1_integrable : iY => /measurable_int. + apply: ge0_le_integral => //=. + - by apply/measurable_EFinP; exact/measurableT_comp. + - by move=> x _; rewrite lee_fin/= mulr_ge0/=. + - by apply/measurable_EFinP; apply/measurable_funM; exact/measurableT_comp. + - by move=> t _; rewrite lee_fin/= normrM. +rewrite expectationM_ge0//=. +- rewrite lte_mul_pinfty//. + + by rewrite expectation_ge0/=. + + rewrite expectation_fin_num//=. + exact: Lfun_norm. + move/Lfun_norm : iY => /expectation_fin_num. + by rewrite fin_numElt => /andP[_]. +- exact: independent_RVs2_comp. +- apply: mule_def_fin; rewrite unlock integrable_fin_num//. + + by move/Lfun_norm : iX => /Lfun1_integrable. + + by move/Lfun_norm : iY => /Lfun1_integrable. +Qed. + +Lemma independent_integrableM (X Y : {RV P >-> R}) : + independent_RVs2 P X Y -> + P.-integrable setT (EFin \o X) -> P.-integrable setT (EFin \o Y) -> + P.-integrable setT (EFin \o (X \* Y)%R). +Proof. +move=> indeXY iX iY. +apply/integrableP; split; first exact/measurable_EFinP/measurable_funM. +move/Lfun1_integrable in iX. +move/Lfun1_integrable in iY. +have := integrable_expectationM indeXY iX iY. +rewrite unlock => /abse_integralP; apply => //. +apply/measurable_EFinP. +by apply: measurable_funM. +Qed. + +(* TODO: rename to expectationM when deprecation is removed *) +Lemma expectation_prod (X Y : {RV P >-> R}) : + independent_RVs2 P X Y -> + (X : _ -> _) \in Lfun P 1 -> (Y : _ -> _) \in Lfun P 1 -> + 'E_P [X * Y] = 'E_P [X] * 'E_P [Y]. +Proof. +move=> XY iX iY. +transitivity ('E_P[(X^\+ - X^\-) * (Y^\+ - Y^\-)]). + congr ('E_P[_]). + apply/funext => /=t. + by rewrite [in LHS](funrposneg X)/= [in LHS](funrposneg Y). +have ? : P.-integrable [set: T] (EFin \o X^\-%R). + rewrite -funerneg; apply/integrable_funeneg => //. + exact/Lfun1_integrable. +have ? : P.-integrable [set: T] (EFin \o X^\+%R). + rewrite -funerpos; apply/integrable_funepos => //. + exact/Lfun1_integrable. +have ? : P.-integrable [set: T] (EFin \o Y^\+%R). + rewrite -funerpos; apply/integrable_funepos => //. + exact/Lfun1_integrable. +have ? : P.-integrable [set: T] (EFin \o Y^\-%R). + rewrite -funerneg; apply/integrable_funeneg => //. + exact/Lfun1_integrable. +have ? : P.-integrable [set: T] (EFin \o (X^\+ \* Y^\+)%R). + by apply: independent_integrableM => //=; exact: independent_RVs2_funrpospos. +have ? : P.-integrable [set: T] (EFin \o (X^\- \* Y^\+)%R). + by apply: independent_integrableM => //=; exact: independent_RVs2_funrnegpos. +have ? : P.-integrable [set: T] (EFin \o (X^\+ \* Y^\-)%R). + by apply: independent_integrableM => //=; exact: independent_RVs2_funrposneg. +have ? : P.-integrable [set: T] (EFin \o (X^\- \* Y^\-)%R). + by apply: independent_integrableM => //=; exact: independent_RVs2_funrnegneg. +transitivity ('E_P[X^\+ * Y^\+] - 'E_P[X^\- * Y^\+] + - 'E_P[X^\+ * Y^\-] + 'E_P[X^\- * Y^\-]). + rewrite mulrDr !mulrDl -expectationB//=; last 2 first. + exact/Lfun1_integrable. + exact/Lfun1_integrable. + rewrite -expectationB//; last 2 first. + rewrite rpredB//=. + exact/Lfun1_integrable. + exact/Lfun1_integrable. + exact/Lfun1_integrable. + rewrite -expectationD//=; last 2 first. + rewrite rpredB//=. + rewrite rpredB//=. + exact/Lfun1_integrable. + exact/Lfun1_integrable. + exact/Lfun1_integrable. + exact/Lfun1_integrable. + congr ('E_P[_]); apply/funext => t/=. + by rewrite !fctE !(mulNr,mulrN,opprK,addrA)/=. +rewrite [in LHS]expectationM_ge0//=; last 2 first. + exact: independent_RVs2_funrpospos. + rewrite mule_def_fin// expectation_fin_num//; exact/Lfun1_integrable. +rewrite [in LHS]expectationM_ge0//=; last 2 first. + exact: independent_RVs2_funrnegpos. + rewrite mule_def_fin// expectation_fin_num//; exact/Lfun1_integrable. +rewrite [in LHS]expectationM_ge0//=; last 2 first. + exact: independent_RVs2_funrposneg. + rewrite mule_def_fin// expectation_fin_num//; exact/Lfun1_integrable. +rewrite [in LHS]expectationM_ge0//=; last 2 first. + exact: independent_RVs2_funrnegneg. + rewrite mule_def_fin// expectation_fin_num//; exact/Lfun1_integrable. +transitivity ('E_P[X^\+ - X^\-] * 'E_P[Y^\+ - Y^\-]). + rewrite -addeA -addeACA -muleBr; last 2 first. + rewrite expectation_fin_num//; exact/Lfun1_integrable. + rewrite fin_num_adde_defr// expectation_fin_num//. + exact/Lfun1_integrable. + rewrite -oppeB; last first. + rewrite fin_num_adde_defr// fin_numM// expectation_fin_num//. + exact/Lfun1_integrable. + exact/Lfun1_integrable. + rewrite -muleBr; last 2 first. + rewrite expectation_fin_num//. + exact/Lfun1_integrable. + rewrite fin_num_adde_defr// expectation_fin_num//. + exact/Lfun1_integrable. + rewrite -muleBl; last 2 first. + rewrite fin_numB// !expectation_fin_num//. + exact/Lfun1_integrable. + exact/Lfun1_integrable. + rewrite fin_num_adde_defr// expectation_fin_num//. + exact/Lfun1_integrable. + rewrite -expectationB//=; last 2 first. + exact/Lfun1_integrable. + exact/Lfun1_integrable. + rewrite -expectationB//. + exact/Lfun1_integrable. + exact/Lfun1_integrable. +by congr *%E; congr ('E_P[_]); rewrite [RHS]funrposneg. +Qed. + +End product_expectation. + Section bernoulli_pmf. Context {R : realType} (p : R). Local Open Scope ring_scope. @@ -1646,7 +2186,7 @@ pose f_ := nnsfun_approx measurableT mf. transitivity (lim (\int[uniform_prob ab]_x (f_ n x)%:E @[n --> \oo])%E). rewrite -monotone_convergence//=. - apply: eq_integral => ? /[!inE] xD; apply/esym/cvg_lim => //=. - exact: cvg_nnsfun_approx. + exact/cvg_nnsfun_approx. - by move=> n; exact/measurable_EFinP/measurable_funTS. - by move=> n ? _; rewrite lee_fin. - by move=> ? _ ? ? mn; rewrite lee_fin; exact/lefP/nd_nnsfun_approx. From b2a28d967073e718cd7d797d0607265c8b3315cd Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Tue, 19 Nov 2024 10:35:23 +0900 Subject: [PATCH 02/10] use bool instead of I_2 --- theories/probability.v | 62 ++++++++++++++++++++---------------------- 1 file changed, 30 insertions(+), 32 deletions(-) diff --git a/theories/probability.v b/theories/probability.v index 28e4d28ddb..7794975db9 100644 --- a/theories/probability.v +++ b/theories/probability.v @@ -1245,13 +1245,12 @@ Section independent_RVs. Context {R : realType} d d' (T : measurableType d) (T' : measurableType d'). Variable P : probability T R. -Definition independent_RVs (I0 : choiceType) (I : set I0) - (X : I0 -> {mfun T >-> T'}) : Prop := +Definition independent_RVs (I0 : choiceType) + (I : set I0) (X : I0 -> {mfun T >-> T'}) : Prop := mutual_independence P I (fun i => g_sigma_algebra_mapping (X i)). Definition independent_RVs2 (X Y : {mfun T >-> T'}) := - independent_RVs [set 0%N; 1%N] - [eta (fun=> cst point) with 0%N |-> X, 1%N |-> Y]. + independent_RVs [set: bool] [eta (fun=> cst point) with false |-> X, true |-> Y]. End independent_RVs. @@ -1286,54 +1285,54 @@ Local Open Scope ring_scope. Lemma independent_RVs2_comp (X Y : {RV P >-> R}) (f g : {mfun R >-> R}) : independent_RVs2 P X Y -> independent_RVs2 P (f \o X) (g \o Y). Proof. -move=> indeXY; split => [i [|]->{i}/= Z/=|J J01 E JE]. -- by rewrite /g_sigma_algebra_mapping/= /preimage_set_system/= => -[B mB <-]; - exact/measurableT_comp. -- by rewrite /g_sigma_algebra_mapping/= /preimage_set_system/= => -[B mB <-]; - exact/measurableT_comp. -- apply indeXY => //= i iJ; have := JE _ iJ. - have : i \in [set 0%N; 1%N] by rewrite inE; apply: J01. - rewrite inE/= => -[|] /eqP ->/=; rewrite !inE. - + exact: g_sigma_algebra_mapping_comp. - + by case: ifPn => [/eqP ->|i0]; exact: g_sigma_algebra_mapping_comp. +move=> indeXY; split => /=. +- move=> [] _ /= A. + + by rewrite /g_sigma_algebra_mapping/= /preimage_set_system/= => -[B mB <-]; + exact/measurableT_comp. + + by rewrite /g_sigma_algebra_mapping/= /preimage_set_system/= => -[B mB <-]; + exact/measurableT_comp. +- move=> J _ E JE. + apply indeXY => //= i iJ; have := JE _ iJ. + by move: i {iJ} =>[|]//=; rewrite !inE => Eg; + exact: g_sigma_algebra_mapping_comp Eg. Qed. Lemma independent_RVs2_funrposneg (X Y : {RV P >-> R}) : independent_RVs2 P X Y -> independent_RVs2 P X^\+ Y^\-. Proof. -move=> indeXY; split=> [/= i [|] -> /=|J J01 E JE]. -- exact: g_sigma_algebra_mapping_funrpos. +move=> indeXY; split=> [[|]/= _|J J2 E JE]. - exact: g_sigma_algebra_mapping_funrneg. +- exact: g_sigma_algebra_mapping_funrpos. - apply indeXY => //= i iJ; have := JE _ iJ. - move/J01 : (iJ) => /= -[|] ->//=; rewrite !inE. - + apply: (g_sigma_algebra_mapping_comp (fun x => maxr x 0)%R). - exact: measurable_funrpos. + move/J2 : iJ; move: i => [|]// _; rewrite !inE. + apply: (g_sigma_algebra_mapping_comp (fun x => maxr (- x) 0)%R). exact: measurable_funrneg. + + apply: (g_sigma_algebra_mapping_comp (fun x => maxr x 0)%R) => //. + exact: measurable_funrpos. Qed. Lemma independent_RVs2_funrnegpos (X Y : {RV P >-> R}) : independent_RVs2 P X Y -> independent_RVs2 P X^\- Y^\+. Proof. -move=> indeXY; split=> [/= i [|] -> /=|J J01 E JE]. -- exact: g_sigma_algebra_mapping_funrneg. +move=> indeXY; split=> [/= [|]// _ |J J2 E JE]. - exact: g_sigma_algebra_mapping_funrpos. +- exact: g_sigma_algebra_mapping_funrneg. - apply indeXY => //= i iJ; have := JE _ iJ. - move/J01 : (iJ) => /= -[|] ->//=; rewrite !inE. - + apply: (g_sigma_algebra_mapping_comp (fun x => maxr (- x) 0)%R). - exact: measurable_funrneg. + move/J2 : iJ; move: i => [|]// _; rewrite !inE. + apply: (g_sigma_algebra_mapping_comp (fun x => maxr x 0)%R). exact: measurable_funrpos. + + apply: (g_sigma_algebra_mapping_comp (fun x => maxr (- x) 0)%R). + exact: measurable_funrneg. Qed. Lemma independent_RVs2_funrnegneg (X Y : {RV P >-> R}) : independent_RVs2 P X Y -> independent_RVs2 P X^\- Y^\-. Proof. -move=> indeXY; split=> [/= i [|] -> /=|J J01 E JE]. +move=> indeXY; split=> [/= [|]// _ |J J2 E JE]. - exact: g_sigma_algebra_mapping_funrneg. - exact: g_sigma_algebra_mapping_funrneg. - apply indeXY => //= i iJ; have := JE _ iJ. - move/J01 : (iJ) => /= -[|] ->//=; rewrite !inE. + move/J2 : iJ; move: i => [|]// _; rewrite !inE. + apply: (g_sigma_algebra_mapping_comp (fun x => maxr (- x) 0)%R). exact: measurable_funrneg. + apply: (g_sigma_algebra_mapping_comp (fun x => maxr (- x) 0)%R). @@ -1343,11 +1342,11 @@ Qed. Lemma independent_RVs2_funrpospos (X Y : {RV P >-> R}) : independent_RVs2 P X Y -> independent_RVs2 P X^\+ Y^\+. Proof. -move=> indeXY; split=> [/= i [|] -> /=|J J01 E JE]. +move=> indeXY; split=> [/= [|]//= _ |J J2 E JE]. - exact: g_sigma_algebra_mapping_funrpos. - exact: g_sigma_algebra_mapping_funrpos. - apply indeXY => //= i iJ; have := JE _ iJ. - move/J01 : (iJ) => /= -[|] ->//=; rewrite !inE. + move/J2 : iJ; move: i => [|]// _; rewrite !inE. + apply: (g_sigma_algebra_mapping_comp (fun x => maxr x 0)%R). exact: measurable_funrpos. + apply: (g_sigma_algebra_mapping_comp (fun x => maxr x 0)%R). @@ -1486,15 +1485,14 @@ have {EX EY}EXY' : 'E_P[X_ n] * 'E_P[Y_ n] @[n --> \oo] --> 'E_P[X] * 'E_P[Y]. suff : forall n, 'E_P[X_ n \* Y_ n] = 'E_P[X_ n] * 'E_P[Y_ n]. by move=> suf; apply: (cvg_unique _ EXY) => //=; under eq_fun do rewrite suf. move=> n; apply: expectationM_nnsfun => x y xX_ yY_. -suff : P (\big[setI/setT]_(j <- [fset 0%N; 1%N]%fset) +suff : P (\big[setI/setT]_(j <- [fset false; true]%fset) [eta fun=> set0 with 0%N |-> X_ n @^-1` [set x], 1%N |-> Y_ n @^-1` [set y]] j) = - \prod_(j <- [fset 0%N; 1%N]%fset) + \prod_(j <- [fset false; true]%fset) P ([eta fun=> set0 with 0%N |-> X_ n @^-1` [set x], 1%N |-> Y_ n @^-1` [set y]] j). by rewrite !big_fsetU1/= ?inE//= !big_seq_fset1/=. move: indeXY => [/= _]; apply => // i. - by rewrite /= !inE => /orP[|]/eqP ->; auto. pose AX := dyadic_approx setT (EFin \o X). pose AY := dyadic_approx setT (EFin \o Y). pose BX := integer_approx setT (EFin \o X). @@ -1502,7 +1500,7 @@ pose BY := integer_approx setT (EFin \o Y). have mA (Z : {RV P >-> R}) m k : (k < m * 2 ^ m)%N -> g_sigma_algebra_mapping Z (dyadic_approx setT (EFin \o Z) m k). move=> mk; rewrite /g_sigma_algebra_mapping /dyadic_approx mk setTI. - rewrite /preimage_class/=; exists [set` dyadic_itv R m k] => //. + rewrite /preimage_set_system/=; exists [set` dyadic_itv R m k] => //. rewrite setTI/=; apply/seteqP; split => z/=. by rewrite inE/= => Zz; exists (Z z). by rewrite inE/= => -[r rmk] [<-]. From 82937d5a49b714c7a9683ac327ad73315fbac794 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Tue, 19 Nov 2024 10:45:03 +0900 Subject: [PATCH 03/10] complete thm 2.13 --- CHANGELOG_UNRELEASED.md | 62 +-- _CoqProject | 1 + theories/Make | 1 + theories/independence.v | 1167 +++++++++++++++++++++++++++++++++++++++ theories/probability.v | 2 +- 5 files changed, 1172 insertions(+), 61 deletions(-) create mode 100644 theories/independence.v diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 6c0e1cb2fe..c114dedb54 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -185,8 +185,6 @@ + lemma `partition_disjoint_bigfcup` - in `lebesgue_measure.v`: + lemma `measurable_indicP` -- in `constructive_ereal.v`: - + notation `\prod_( i <- r | P ) F` for extended real numbers and its variants - in `numfun.v`: + defintions `funrpos`, `funrneg` with notations `^\+` and `^\-` @@ -202,7 +200,6 @@ notations `.-mapping`, `.-mapping.-measurable` - in `lebesgue_measure.v`: - + lemma `measurable_indicP` + lemmas `measurable_funrpos`, `measurable_funrneg` - in `lebesgue_integral.v`: @@ -219,7 +216,8 @@ - in `probability.v`: + lemma `expectation_def` + notation `'M_` -- in `probability.v`: + +- new file `independence.v`: + lemma `expectationM_ge0` + definition `independent_events` + definition `mutual_independence` @@ -374,61 +372,6 @@ + `sigma_algebra_preimage_classE` -> `g_sigma_preimageE` + `preimage_classes_comp` -> `g_sigma_preimageU_comp` - -- in file `normedtype.v`, - changed `completely_regular_space` to depend on uniform separators - which removes the dependency on `R`. The old formulation can be - recovered easily with `uniform_separatorP`. - -- moved from `Rstruct.v` to `Rstruct_topology.v` - + lemmas `continuity_pt_nbhs`, `continuity_pt_cvg`, - `continuity_ptE`, `continuity_pt_cvg'`, `continuity_pt_dnbhs` - and `nbhs_pt_comp` - -- moved from `real_interval.v` to `normedtype.v` - + lemmas `set_itvK`, `RhullT`, `RhullK`, `set_itv_setT`, - `Rhull_smallest`, `le_Rhull`, `neitv_Rhull`, `Rhull_involutive`, - `disj_itv_Rhull` -- in `topology.v`: - + lemmas `subspace_pm_ball_center`, `subspace_pm_ball_sym`, - `subspace_pm_ball_triangle`, `subspace_pm_entourage` turned - into local `Let`'s - -- in `lebesgue_integral.v`: - + structure `SimpleFun` now inside a module `HBSimple` - + structure `NonNegSimpleFun` now inside a module `HBNNSimple` - + lemma `cst_nnfun_subproof` has now a different statement - + lemma `indic_nnfun_subproof` has now a different statement -- in `mathcomp_extra.v`: - + definition `idempotent_fun` - -- in `topology_structure.v`: - + definitions `regopen`, `regclosed` - + lemmas `closure_setC`, `interiorC`, `closureU`, `interiorU`, - `closureEbigcap`, `interiorEbigcup`, - `closure_open_regclosed`, `interior_closed_regopen`, - `closure_interior_idem`, `interior_closure_idem` - -- in file `topology_structure.v`, - + mixin `isContinuous`, type `continuousType`, structure `Continuous` - + new lemma `continuousEP`. - + new definition `mkcts`. - -- in file `subspace_topology.v`, - + new lemmas `continuous_subspace_setT`, `nbhs_prodX_subspace_inE`, and - `continuous_subspace_prodP`. - + type `continuousFunType`, HB structure `ContinuousFun` - -- in file `subtype_topology.v`, - + new lemmas `subspace_subtypeP`, `subspace_sigL_continuousP`, - `subspace_valL_continuousP'`, `subspace_valL_continuousP`, `sigT_of_setXK`, - `setX_of_sigTK`, `setX_of_sigT_continuous`, and `sigT_of_setX_continuous`. - -- in `lebesgue_integrale.v` - + change implicits of `measurable_funP` - -### Changed - ### Renamed - in `lebesgue_measure.v`: @@ -453,7 +396,6 @@ - in `probability.v`: + `integral_distribution` -> `ge0_integral_distribution` - + `expectationM` -> `expectationMl` - file `homotopy_theory/path.v` -> `homotopy_theory/continuous_path.v` diff --git a/_CoqProject b/_CoqProject index aaec25f6d1..32999d79aa 100644 --- a/_CoqProject +++ b/_CoqProject @@ -124,6 +124,7 @@ theories/lebesgue_integral_theory/giry.v theories/ftc.v theories/hoelder.v theories/probability.v +theories/independence.v theories/convex.v theories/charge.v theories/kernel.v diff --git a/theories/Make b/theories/Make index d67f6b5447..727b5ddff5 100644 --- a/theories/Make +++ b/theories/Make @@ -91,6 +91,7 @@ lebesgue_integral_theory/giry.v ftc.v hoelder.v probability.v +independence.v convex.v charge.v kernel.v diff --git a/theories/independence.v b/theories/independence.v new file mode 100644 index 0000000000..034f15aa89 --- /dev/null +++ b/theories/independence.v @@ -0,0 +1,1167 @@ +(* mathcomp analysis (c) 2022 Inria and AIST. License: CeCILL-C. *) +From mathcomp Require Import all_ssreflect interval_inference. +From mathcomp Require Import ssralg poly ssrnum ssrint interval finmap. +From mathcomp Require Import mathcomp_extra boolp classical_sets functions. +From mathcomp Require Import cardinality fsbigop. +From HB Require Import structures. +From mathcomp Require Import exp numfun lebesgue_measure lebesgue_integral. +From mathcomp Require Import reals ereal topology normedtype sequences. +From mathcomp Require Import esum measure exp numfun lebesgue_measure. +From mathcomp Require Import lebesgue_integral kernel probability. +From mathcomp Require Import hoelder. + +(**md**************************************************************************) +(* # Independence *) +(* *) +(* ``` *) +(* independent_events I F == the events F indexed by I are independent *) +(* mutual_independence I F == the set systems F indexed by I are independent *) +(* independent_RVs I X == the random variables X indexed by I are independent *) +(* independent_RVs2 X Y == the random variables X and Y are independent *) +(* ``` *) +(* *) +(******************************************************************************) + +Set Implicit Arguments. +Unset Strict Implicit. +Unset Printing Implicit Defensive. + +Import Order.TTheory GRing.Theory Num.Def Num.Theory. +Import numFieldTopology.Exports. + +Local Open Scope classical_set_scope. +Local Open Scope ring_scope. + +Section independent_events. +Context {R : realType} d {T : measurableType d} (P : probability T R) + {I0 : choiceType}. +Local Open Scope ereal_scope. + +Definition independent_events (I : set I0) (E : I0 -> set T) := + (forall i, I i -> measurable (E i)) /\ + forall J : {fset I0}, [set` J] `<=` I -> + P (\bigcap_(i in [set` J]) E i) = \prod_(i <- J) P (E i). + +End independent_events. + +Section mutual_independence. +Context {R : realType} d {T : measurableType d} (P : probability T R) + {I0 : choiceType}. +Local Open Scope ereal_scope. + +Definition g_sigma_family (I : set I0) (F : I0 -> set_system T) + : set_system T := + <>. + +Definition mutual_independence (I : set I0) (F : I0 -> set_system T) := + (forall i, I i -> F i `<=` measurable) /\ + forall J : {fset I0}, [set` J] `<=` I -> + forall E, (forall i, i \in J -> E i \in F i) -> + P (\big[setI/setT]_(j <- J) E j) = \prod_(j <- J) P (E j). + +Lemma eq_mutual_independence (I : set I0) (F F' : I0 -> set_system T) : + (forall i, I i -> F i = F' i) -> + mutual_independence I F -> mutual_independence I F'. +Proof. +move=> FF' IF; split => [i Ii|J JI E EF']. + by rewrite -FF'//; apply IF. +apply IF => // i iJ. +by rewrite FF' ?EF'//; exact: JI. +Qed. + +End mutual_independence. + +Section independence. +Context {R : realType} d {T : measurableType d} (P : probability T R). +Local Open Scope ereal_scope. + +Definition independence (F G : set_system T) := + [/\ F `<=` measurable , G `<=` measurable & + forall A B, A \in F -> B \in G -> P (A `&` B) = P A * P B]. + +Lemma independenceP (F G : set_system T) : independence F G <-> + mutual_independence P [set: bool] (fun b => if b then F else G). +Proof. +split=> [[mF mG FG]|/= indeF]. + split=> [/= [|]//|/= J Jbool E EF]. + have [/eqP Jtrue|/eqP Jfalse| |] := set_bool [set` J]. + - rewrite -bigcap_fset Jtrue bigcap_set1. + by rewrite fsbig_seq ?Jtrue ?fsbig_set1. + - rewrite -bigcap_fset Jfalse bigcap_set1. + by rewrite fsbig_seq// ?Jfalse fsbig_set1. + - rewrite set_seq_eq0 => /eqP ->. + by rewrite !big_nil probability_setT. + - rewrite setT_bool => /eqP {}Jbool. + rewrite -bigcap_fset Jbool bigcap_setU1 bigcap_set1. + rewrite FG//. + + rewrite -(set_fsetK J) Jbool. + rewrite fset_setU1//= fset_set1. + rewrite big_fsetU1 ?inE//=. + by rewrite big_seq_fset1. + + rewrite EF//. + rewrite -(set_fsetK J) Jbool. + by rewrite in_fset_set// !inE/=; left. + + rewrite EF//. + rewrite -(set_fsetK J) Jbool. + by rewrite in_fset_set// !inE/=; right. +split. +- by case: indeF => /= [+ _] => /(_ true); exact. +- by case: indeF => /= [+ _] => /(_ false); exact. +- move=> A B AF BG. + case: indeF => _ /= /(_ [fset true; false]%fset _ (fun b => if b then A else B)). + do 2 rewrite big_fsetU1/= ?inE//= big_seq_fset1. + by apply => // -[]. +Qed. + +End independence. + +Lemma setI_closed_setT T (F : set_system T) : + setI_closed F -> setI_closed (F `|` [set setT]). +Proof. +move=> IF=> C D [FC|/= ->{C}]. +- move=> [FD|/= ->{D}]. + by left; exact: IF. + by rewrite setIT; left. +- move=> [FD|->{D}]. + by rewrite setTI; left. + by rewrite !setTI; right. +Qed. + +Lemma setI_closed_set0 T (F : set_system T) : + setI_closed F -> setI_closed (F `|` [set set0]). +Proof. +move=> IF=> C D [FC|/= ->{C}]. +- move=> [FD|/= ->{D}]. + by left; exact: IF. + by rewrite setI0; right. +- move=> [FD|->{D}]. + by rewrite set0I; right. + by rewrite !set0I; right. +Qed. + +Lemma setI_closed_set0' T (F : set_system T) : + F set0 -> + setI_closed (F `|` [set set0]) -> setI_closed F. +Proof. +move=> F0 IF C D FC FD. +have [//|/= ->//] : (F `|` [set set0]) (C `&` D). +by apply: IF; left. +Qed. + +Lemma g_sigma_setU d {T : measurableType d} (F : set_system T) A : + <> A -> + <> = @measurable _ T -> + <> = <>. +Proof. +move=> FA sFT; apply/seteqP; split=> [B|B]. + by apply: sub_sigma_algebra2; exact: subsetUl. +apply: smallest_sub => // C [FC|/= ->//]. +exact: sub_gen_smallest. +Qed. + +Lemma g_sigma_algebra_finite_measure_unique {d} {T : measurableType d} + {R : realType} (G : set_system T) : + G `<=` d.-measurable -> + setI_closed G -> + forall m1 m2 : {finite_measure set T -> \bar R}, + m1 [set: T] = m2 [set: T] -> + (forall A : set T, G A -> m1 A = m2 A) -> + forall E : set T, <> E -> m1 E = m2 E. +Proof. +move=> Gm IG m1 m2 m1m2T m1m2 E sGE. +apply: (@g_sigma_algebra_measure_unique _ _ _ + (G `|` [set setT]) _ (fun=> setT)) => //. +- by move=> A [/Gm//|/= ->//]. +- by right. +- by rewrite bigcup_const. +- exact: setI_closed_setT. +- by move=> B [/m1m2 //|/= ->]. +- by move=> n; apply: fin_num_fun_lty; exact: fin_num_measure. +- move: E sGE; apply: smallest_sub => // C GC. + by apply: sub_gen_smallest; left. +Qed. + +(*Section lem142b. +Context d {T : measurableType d} {R : realType}. +Variable mu : {finite_measure set T -> \bar R}. +Variable F : set_system T. +Hypothesis setI_closed_F : setI_closed F. (* pi-system *) +Hypothesis FT : F `<=` @measurable _ T. +Hypothesis sFT : <> = @measurable _ T. + +Lemma lem142b : forall nu : {finite_measure set T -> \bar R}, + (mu setT = nu setT) -> + (forall E, F E -> nu E = mu E) -> + forall A, measurable A -> mu A = nu A. +Proof. +move=> nu munu numu A mA. +apply: (measure_unique (F `|` [set setT]) (fun=> setT)) => //. +- rewrite -sFT; apply: g_sigma_setU => //. + by rewrite sFT. +- exact: setI_closed_setT. +- by move=> n /=; right. +- by rewrite bigcup_const. +- move=> E [/numu //|/= ->]. + by rewrite munu. +- move=> n. + apply: fin_num_fun_lty. + exact: fin_num_measure. +Qed. + +End lem142b.*) + +Section mutual_independence_properties. +Context {R : realType} d {T : measurableType d} (P : probability T R). +Local Open Scope ereal_scope. + +(**md see Achim Klenke's Probability Thery, Ch.2, sec.2.1, thm.2.13(i) *) +Lemma mutual_independence_fset {I0 : choiceType} (I : {fset I0}) + (F : I0 -> set_system T) : + (forall i, i \in I -> F i `<=` measurable /\ (F i) [set: T]) -> + mutual_independence P [set` I] F <-> + forall E, (forall i, i \in I -> E i \in F i) -> + P (\big[setI/setT]_(j <- I) E j) = \prod_(j <- I) P (E j). +Proof. +move=> mF; split=> [indeF E EF|indeF]; first by apply indeF. +split=> [i /mF[]//|J JI E EF]. +pose E' i := if i \in J then E i else [set: T]. +have /indeF : forall i, i \in I -> E' i \in F i. + move=> i iI; rewrite /E'; case: ifPn => [|iJ]; first exact: EF. + by rewrite inE; apply mF. +move/fsubsetP : (JI) => /(big_fset_incl _) <- /=; last first. + by move=> j jI jJ; rewrite /E' (negbTE jJ). +move/fsubsetP : (JI) => /(big_fset_incl _) <- /=; last first. + by move=> j jI jJ; rewrite /E' (negbTE jJ); rewrite probability_setT. +rewrite big_seq [in X in X = _ -> _](eq_bigr E); last first. + by move=> i iJ; rewrite /E' iJ. +rewrite -big_seq => ->. +by rewrite !big_seq; apply: eq_bigr => i iJ; rewrite /E' iJ. +Qed. + +(**md see Achim Klenke's Probability Thery, Ch.2, sec.2.1, thm.2.13(ii) *) +Lemma mutual_independence_finiteS {I0 : choiceType} (I : set I0) + (F : I0 -> set_system T) : + mutual_independence P I F <-> + (forall J : {fset I0}%fset, [set` J] `<=` I -> + mutual_independence P [set` J] F). +Proof. +split=> [indeF J JI|indeF]. + split=> [i /JI Ii|K KJ E EF]. + by apply indeF. + by apply indeF => // i /KJ /JI. +split=> [i Ii|J JI E EF]. + have : [set` [fset i]%fset] `<=` I. + by move=> j; rewrite /= inE => /eqP ->. + by move/indeF => [+ _]; apply; rewrite /= inE. +by have [_] := indeF _ JI; exact. +Qed. + +(**md see Achim Klenke's Probability Thery, Ch.2, sec.2.1, thm.2.13(iii) *) +Theorem mutual_independence_finite_g_sigma {I0 : choiceType} (I : set I0) + (F : I0 -> set_system T) : + (forall i, i \in I -> setI_closed (F i `|` [set set0])) -> + mutual_independence P I F <-> mutual_independence P I (fun i => <>). +Proof. +split=> indeF; last first. + split=> [i Ii|J JI E EF]. + case: indeF => /(_ _ Ii) + _. + by apply: subset_trans; exact: sub_gen_smallest. + apply indeF => // i iJ; rewrite inE. + by apply: sub_gen_smallest; exact/set_mem/EF. +split=> [i Ii|K KI E EF]. + case: indeF => + _ => /(_ _ Ii). + by apply: smallest_sub; exact: sigma_algebra_measurable. +suff: forall J J' : {fset I0}%fset, (J `<=` J')%fset -> [set` J'] `<=` I -> + forall E, (forall i, i \in J -> E i \in <>) -> + (forall i, i \in [set` J'] `\` [set` J] -> E i \in F i) -> + P (\big[setI/setT]_(j <- J') E j) = \prod_(j <- J') P (E j). + move=> /(_ K K (@fsubset_refl _ _) KI E); apply. + - by move=> i iK; exact: EF. + - by move=> i; rewrite setDv inE. +move=> {E EF K KI}. +apply: finSet_rect => K ih J' KJ' J'I E EsF EF. +have [K0|/fset0Pn[j jK]] := eqVneq K fset0. + apply indeF => // i iJ'. + by apply: EF; rewrite !inE; split => //=; rewrite K0 inE. +pose J := (K `\ j)%fset. +have jI : j \in I by apply/mem_set/J'I => /=; move/fsubsetP : KJ'; exact. +have JK : (J `<` K)%fset by rewrite fproperD1. +have JjJ' : (j |` J `<=` J')%fset by apply: fsubset_trans KJ'; rewrite fsetD1K. +have JJ' : (J `<=` J')%fset by apply: fsubset_trans JjJ'; exact: fsubsetU1. +have J'mE i : i \in J' -> d.-measurable (E i). + move=> iJ'. + case: indeF => + _ => /(_ i (J'I _ iJ')) Fim. + suff: <> (E i). + by apply: smallest_sub => //; exact: sigma_algebra_measurable. + apply/set_mem. + have [iK|iK] := boolP (i \in K); first by rewrite EsF. + have /set_mem : E i \in F i. + by rewrite EF// !inE/=; split => //; exact/negP. + by move/sub_sigma_algebra => /(_ setT)/mem_set. +have mmu : measurable (\big[setI/[set: T]]_(j0 <- (J' `\ j)%fset) (E j0)). + rewrite big_seq; apply: bigsetI_measurable => i /[!inE] /andP[_ iJ']. + exact: J'mE. +pose mu0 A := P (A `&` \big[setI/[set: T]]_(j0 <- (J' `\ j)%fset) (E j0)). +pose mu := [the {finite_measure set _ -> \bar _} of mrestr P mmu]. +pose nu0 A := P A * \prod_(j0 <- (J' `\ j)%fset) P (E j0). +have nuk : (0 <= fine (\prod_(j0 <- (J' `\ j)%fset) P (E j0)))%R. + by rewrite fine_ge0// prode_ge0. +pose nu := [the measure _ _ of mscale (NngNum nuk) P]. +have nuEj A : nu A = P A * \prod_(j0 <- (J' `\ j)%fset) P (E j0). + rewrite /nu/= /mscale muleC/= fineK// big_seq. + rewrite prode_fin_num// => i /[!inE]/= /andP[ij iJ']. + by rewrite fin_num_measure//; exact: J'mE. +have JJ'j : (J `<=` J' `\ j)%fset by exact: fsetSD. +have J'jI : [set` (J' `\ j)%fset] `<=` I. + by apply: subset_trans J'I; apply/fsubsetP; exact: fsubsetDl. +have jJ' : j \in J' by move/fsubsetP : JjJ'; apply; rewrite !inE eqxx. +have Fjmunu A : (F j `|` [set set0; setT]) A -> mu A = nu A. + move=> [FjA|[->|->]]. + - rewrite nuEj. + pose E' i := if i == j then A else E i. + transitivity (P (\big[setI/[set: T]]_(j <- J') E' j)). + rewrite [in RHS](big_fsetD1 j)//= {1}/E' eqxx//; congr (P (_ `&` _)). + rewrite !big_seq; apply: eq_bigr => i /[!inE] /andP[ij _]. + by rewrite /E' (negbTE ij). + transitivity (\prod_(j <- J') P (E' j)); last first. + rewrite [in LHS](big_fsetD1 j)//= {1}/E' eqxx//; congr (P _ * _). + rewrite !big_seq; apply: eq_bigr => i /[!inE] /andP[ij _]. + by rewrite /E' (negbTE ij). + apply: (ih _ JK _ JJ' J'I). + + move=> i iJ. + rewrite /E'; case: ifPn => [/eqP ->|ij]. + by rewrite inE; exact: sub_sigma_algebra. + rewrite EsF//. + by move/fproper_sub : JK => /fsubsetP; apply. + + move=> i. + rewrite ![in X in X -> _]inE /= ![in X in X -> _]inE => -[] iJ' /negP. + rewrite negb_and negbK => /predU1P[ij|iK]. + by rewrite /E' ij eqxx inE. + rewrite /E' ifF//; last first. + apply/negP => /eqP ij. + by rewrite ij jK in iK. + by rewrite EF// !inE/=; split => //; exact/negP. + - by rewrite !measure0. + - rewrite /mu /= /mrestr /= nuEj setTI probability_setT mul1e. + apply: (ih _ JK _ JJ'j J'jI). + + move=> i iJ. + rewrite EsF//. + by move/fproper_sub : JK => /fsubsetP; apply. + + move=> i. + rewrite ![in X in X -> _]inE /= ![in X in X -> _]inE => -[]. + move=> /andP[-> iJ'] iK. + by rewrite EF// !inE. +have sFjmunu A : <> A -> mu A = nu A. + move=> sFjA. + apply: (@g_sigma_algebra_finite_measure_unique _ _ _ (F j `|` [set set0])). + - move=> B /= [|->//]. + move: B. + case: indeF => + _. + by apply; exact/set_mem. + - exact: H. + - rewrite /mu/= /mrestr/= nuEj setTI probability_setT mul1e. + apply: (ih _ JK _ JJ'j J'jI). + + move=> i iJ. + rewrite EsF//. + by move/fproper_sub : JK => /fsubsetP; apply. + + move=> i. + rewrite ![in X in X -> _]inE /= ![in X in X -> _]inE => -[]. + move=> /andP[ij iJ']. + rewrite ij/= => iK. + by rewrite EF// !inE. + - move=> B FjB; apply: Fjmunu. + case: FjB => [|->//]; first by left. + by right; left. + - by move: sFjA; exact: sub_smallest2r. +rewrite [in LHS](big_fsetD1 j)//= [in RHS](big_fsetD1 j)//=. +have /sFjmunu : <> (E j) by apply/set_mem; rewrite EsF. +by rewrite /mu/= /mrestr/= nuEj. +Qed. + +(* pick an i from I_ k s.t. E k \in F (f k) *) +Local Definition f (K0 : choiceType) (K : {fset K0}) + (I0 : pointedType) (F : I0 -> set_system T) E I_ + (EF : forall k, k \in K -> E k \in \bigcup_(i in I_ k) F i) k := + if pselect (k \in K) is left kK then + sval (cid2 (set_mem (EF _ kK))) + else + point. + +Local Lemma f_prop (K0 : choiceType) (K : {fset K0}) + (I0 : pointedType) (F : I0 -> set_system T) E I_ + (EF : forall k, k \in K -> E k \in \bigcup_(i in I_ k) F i) k : + k \in K -> E k \in F (f EF k). +Proof. +move=> kK; rewrite /f; case: pselect => [kK_/=|//]. +by case: cid2 => // i/= ? /mem_set. +Qed. + +Local Lemma f_inj (K0 : choiceType) (K K' : {fset K0}) + (K'K : [set` K'] `<=` [set` K]) (I0 : pointedType) (F : I0 -> set_system T) + E I_ (EF : forall k, k \in K' -> E k \in \bigcup_(i in I_ k) F i) + (KI : trivIset [set` K] I_) k1 k2 : + k1 \in K' -> k2 \in K'-> k1 != k2 -> + ([fset f EF k1] `&` [fset f EF k2] = fset0)%fset. +Proof. +move=> k1K' k2K' k1k2; apply/eqP; rewrite -fsubset0. +apply/fsubsetP => i /[!inE] /andP[]. +rewrite /f; case: pselect => // k1K'_. +case: cid2 => // i' i'k1 Fi' /eqP ->{i}. +case: pselect => // k2K'_. +case: cid2 => // j ik2 FjEk2 /eqP/= i'j. +rewrite -{j}i'j in ik2 FjEk2 *. +move/trivIsetP : KI => /(_ _ _ (K'K _ k1K') (K'K _ k2K') k1k2). +by move/seteqP => [+ _] => /(_ i')/=; rewrite -falseE; exact. +Qed. + +Local Definition g (K0 : pointedType) (K' : {fset K0}) + (I0 : Type) (I_ : K0 -> set I0) (i : I0) : K0 := + if pselect (exists2 k, k \in K' & i \in I_ k) is left e then + sval (cid2 e) + else + point. + +Local Lemma gf (K0 I0 : pointedType) (F : I0 -> set_system T) + (K K' : {fset K0}) (K'K : [set` K'] `<=` [set` K]) + E I_ (EF : forall k, k \in K' -> E k \in \bigcup_(i in I_ k) F i) + (KI : trivIset [set` K] (fun i => I_ i)) i : i \in K' -> g K I_ (f EF i) = i. +Proof. +move=> iK'; rewrite /f; case: pselect => // iK'_. +case: cid2 => // j jIi FjEi. +rewrite /g; case: pselect => // k'; last first. + exfalso; apply: k'. + by exists i => //; [exact: K'K|exact/mem_set]. +case: cid2 => //= k'' k''K jIk'. +apply/eqP/negP => /negP k'i. +move/trivIsetP : KI => /(_ k'' i) /= /(_ k''K (K'K _ iK') k'i)/= /eqP. +apply/negP/set0P; exists j; split => //. +exact/set_mem. +Qed. + +(**md see Achim Klenke's Probability Thery, Ch.2, sec.2.1, thm.2.13(iv) *) +Lemma mutual_independence_bigcup (K0 I0 : pointedType) (K : {fset K0}) + (I_ : K0 -> set I0) (I : set I0) (F : I0 -> set_system T) : + trivIset [set` K] (fun i => I_ i) -> + (forall k, k \in K -> I_ k `<=` I) -> + mutual_independence P I F -> + mutual_independence P [set` K] (fun k => \bigcup_(i in I_ k) F i). +Proof. +move=> KI I_I PIF. +split=> [i Ki A [j ij FjA]|K' K'K E EF]. + by case: PIF => + _ => /(_ j); apply => //; exact: (I_I _ Ki). +case: PIF => Fm PIF. +pose f' := f EF. +pose g' := g K I_. +pose J' := (\bigcup_(k <- K') [fset f' k])%fset. +pose E' := E \o g'. +suff: P (\big[setI/[set: T]]_(j <- J') E' j) = \prod_(j <- J') P (E' j). + move=> suf. + transitivity (P (\big[setI/[set: T]]_(j <- J') E' j)). + congr (P _). + apply/seteqP; split=> [t|]. + rewrite -!bigcap_fset => L j => /bigfcupP[k] /[!andbT] kK'. + rewrite !inE => /eqP ->{j}. + apply: L => //=. + by rewrite /g' /f' gf. + move=> t. + rewrite -!bigcap_fset => L j/= jK'. + have /= := L (f' j). + rewrite /E' /g' /f'/= gf//. + by apply; apply/bigfcupP; exists j;[rewrite jK'|rewrite inE]. + rewrite suf partition_disjoint_bigfcup//=. + rewrite [LHS]big_seq [RHS]big_seq; apply: eq_big => // k kK'. + by rewrite big_seq_fset1 /E' /g' /f' /= gf. + move=> k1 k2 k1K' k2K' k1k2 /=. + by rewrite -fsetI_eq0 -fsubset0 (f_inj K'K). +apply: PIF. +- move=> i/= /bigfcupP[k] /[!andbT] kK' /[!inE] /eqP ->. + apply: (I_I k) => /=; first exact: K'K. + by rewrite /f' /f; case: pselect => // kK'_; case: cid2. +- move=> i /bigfcupP[k'] /[!andbT] k'K /[!inE] /eqP ->{i}. + by rewrite /E' /g' /f'/= gf//; exact/set_mem/f_prop. +Qed. + +End mutual_independence_properties. + +Section g_sigma_algebra_mapping_lemmas. +Context d {T : measurableType d} {R : realType}. + +Lemma g_sigma_algebra_mapping_comp (X : {mfun T >-> R}) (f : R -> R) : + measurable_fun setT f -> + g_sigma_algebra_mapping (f \o X)%R `<=` g_sigma_algebra_mapping X. +Proof. +move=> mf. +rewrite /g_sigma_algebra_mapping. +rewrite preimage_set_system_comp. +move=> A /= [] B [C mC <-{B}] <-{A}. +red. +exists ([set: R] `&` f @^-1` C) => //. +by apply: mf. +Qed. + +Lemma g_sigma_algebra_mapping_funrpos (X : {mfun T >-> R}) : + g_sigma_algebra_mapping X^\+%R `<=` d.-measurable. +Proof. +by move=> A/= -[B mB] <-; have := measurable_funrpos (measurable_funP X); exact. +Qed. + +Lemma g_sigma_algebra_mapping_funrneg (X : {mfun T >-> R}) : + g_sigma_algebra_mapping X^\-%R `<=` d.-measurable. +Proof. +by move=> A/= -[B mB] <-; have := measurable_funrneg (measurable_funP X); exact. +Qed. + +End g_sigma_algebra_mapping_lemmas. +Arguments g_sigma_algebra_mapping_comp {d T R X} f. + +Section independent_RVs. +Context {R : realType} d (T : measurableType d). +Context {I0 : choiceType}. +Context {d' : I0 -> _} (T' : forall i : I0, measurableType (d' i)). +Variable P : probability T R. + +Definition independent_RVs (I : set I0) + (X : forall i : I0, {mfun T >-> T' i}) : Prop := + mutual_independence P I (fun i => g_sigma_algebra_mapping (X i)). + +End independent_RVs. + +Section independent_RVs2. +Context {R : realType} d d' (T : measurableType d) (T' : measurableType d'). +Variable P : probability T R. + +Definition independent_RVs2 (X Y : {mfun T >-> T'}) := + independent_RVs P [set: bool] (fun b => if b then Y else X). + +End independent_RVs2. + +Section independent_generators. +Context {R : realType} d (T : measurableType d). +Context {I0 : choiceType}. +Context {d' : I0 -> _} (T' : forall i : I0, measurableType (d' i)). +Variable P : probability T R. + +(**md see Achim Klenke's Probability Thery, Ch.2, sec.2.1, thm.2.16 *) +Theorem independent_generators (I : set I0) (F : forall i : I0, set_system (T' i)) + (X : forall i, {RV P >-> T' i}) : + (forall i, i \in I -> setI_closed (F i)) -> + (forall i, i \in I -> F i `<=` @measurable _ (T' i)) -> + (forall i, i \in I -> @measurable _ (T' i) = <>) -> + mutual_independence P I (fun i => preimage_set_system setT (X i) (F i)) -> + independent_RVs P I X. +Proof. +move=> IF FA AsF indeX1. +have closed_preimage i : I i -> setI_closed (preimage_set_system setT (X i) (F i)). + move=> Ii A B [A' FiA']; rewrite setTI => <-{A}. + move=> [B' FiB']; rewrite setTI => <-{B}. + rewrite /preimage_set_system/=; exists (A' `&` B'). + apply: IF => //. + - exact/mem_set. + - by rewrite setTI. +have gen_preimage i : I i -> + <> = g_sigma_algebra_mapping (X i). + move=> Ii. + rewrite /g_sigma_algebra_mapping AsF; last exact/mem_set. + by rewrite -g_sigma_preimageE. +rewrite /independent_RVs. +suff: mutual_independence P I (fun i => <>). + exact: eq_mutual_independence. +apply: (mutual_independence_finite_g_sigma _ _).1. +- by move=> i Ii; apply: setI_closed_set0; exact/closed_preimage/set_mem. +- split => [i Ii A [A' mA'] <-{A}|J JI E EF]. + by apply/measurable_funP => //; apply: FA => //; exact/mem_set. + by apply indeX1. +Qed. + +End independent_generators. + +Section independent_RVs_lemmas. +Context {R : realType} d d' (T : measurableType d) (T' : measurableType d'). +Variable P : probability T R. +Local Open Scope ring_scope. + +Lemma independent_RVs2_comp (X Y : {RV P >-> R}) (f g : {mfun R >-> R}) : + independent_RVs2 P X Y -> independent_RVs2 P (f \o X) (g \o Y). +Proof. +move=> indeXY; split => /=. +- move=> [] _ /= A. + + by rewrite /g_sigma_algebra_mapping/= /preimage_set_system/= => -[B mB <-]; + exact/measurableT_comp. + + by rewrite /g_sigma_algebra_mapping/= /preimage_set_system/= => -[B mB <-]; + exact/measurableT_comp. +- move=> J _ E JE. + apply indeXY => //= i iJ; have := JE _ iJ. + by move: i {iJ} =>[|]//=; rewrite !inE => Eg; + exact: g_sigma_algebra_mapping_comp Eg. +Qed. + +Lemma independent_RVs2_funrposneg (X Y : {RV P >-> R}) : + independent_RVs2 P X Y -> independent_RVs2 P X^\+ Y^\-. +Proof. +move=> indeXY; split=> [[|]/= _|J J2 E JE]. +- exact: g_sigma_algebra_mapping_funrneg. +- exact: g_sigma_algebra_mapping_funrpos. +- apply indeXY => //= i iJ; have := JE _ iJ. + move/J2 : iJ; move: i => [|]// _; rewrite !inE. + + apply: (g_sigma_algebra_mapping_comp (fun x => maxr (- x) 0)%R). + exact: measurable_funrneg. + + apply: (g_sigma_algebra_mapping_comp (fun x => maxr x 0)%R) => //. + exact: measurable_funrpos. +Qed. + +Lemma independent_RVs2_funrnegpos (X Y : {RV P >-> R}) : + independent_RVs2 P X Y -> independent_RVs2 P X^\- Y^\+. +Proof. +move=> indeXY; split=> [/= [|]// _ |J J2 E JE]. +- exact: g_sigma_algebra_mapping_funrpos. +- exact: g_sigma_algebra_mapping_funrneg. +- apply indeXY => //= i iJ; have := JE _ iJ. + move/J2 : iJ; move: i => [|]// _; rewrite !inE. + + apply: (g_sigma_algebra_mapping_comp (fun x => maxr x 0)%R). + exact: measurable_funrpos. + + apply: (g_sigma_algebra_mapping_comp (fun x => maxr (- x) 0)%R). + exact: measurable_funrneg. +Qed. + +Lemma independent_RVs2_funrnegneg (X Y : {RV P >-> R}) : + independent_RVs2 P X Y -> independent_RVs2 P X^\- Y^\-. +Proof. +move=> indeXY; split=> [/= [|]// _ |J J2 E JE]. +- exact: g_sigma_algebra_mapping_funrneg. +- exact: g_sigma_algebra_mapping_funrneg. +- apply indeXY => //= i iJ; have := JE _ iJ. + move/J2 : iJ; move: i => [|]// _; rewrite !inE. + + apply: (g_sigma_algebra_mapping_comp (fun x => maxr (- x) 0)%R). + exact: measurable_funrneg. + + apply: (g_sigma_algebra_mapping_comp (fun x => maxr (- x) 0)%R). + exact: measurable_funrneg. +Qed. + +Lemma independent_RVs2_funrpospos (X Y : {RV P >-> R}) : + independent_RVs2 P X Y -> independent_RVs2 P X^\+ Y^\+. +Proof. +move=> indeXY; split=> [/= [|]//= _ |J J2 E JE]. +- exact: g_sigma_algebra_mapping_funrpos. +- exact: g_sigma_algebra_mapping_funrpos. +- apply indeXY => //= i iJ; have := JE _ iJ. + move/J2 : iJ; move: i => [|]// _; rewrite !inE. + + apply: (g_sigma_algebra_mapping_comp (fun x => maxr x 0)%R). + exact: measurable_funrpos. + + apply: (g_sigma_algebra_mapping_comp (fun x => maxr x 0)%R). + exact: measurable_funrpos. +Qed. + +End independent_RVs_lemmas. + +Definition preimage_classes I (d : I -> measure_display) + (Tn : forall k, semiRingOfSetsType (d k)) (T : Type) (fn : forall k, T -> Tn k) := + <>. +Arguments preimage_classes {I} d Tn {T} fn. + +Lemma measurable_prod d [T : measurableType d] [R : realType] [D : set T] [I : eqType] + (s : seq I) [h : I -> T -> R] : + (forall i, i \in s -> measurable_fun D (h i)) -> + measurable_fun D (fun x => (\prod_(i <- s) h i x)%R). +Proof. +elim: s => [mh|x y ih mh]. + under eq_fun do rewrite big_nil//=. + exact: measurable_cst. +under eq_fun do rewrite big_cons//=. +apply: measurable_funM => //. + apply: mh. + by rewrite mem_head. +apply: ih => n ny. +apply: mh. +by rewrite inE orbC ny. +Qed. + +Section pairRV. +Context d d' {T : measurableType d} {T' : measurableType d'} {R : realType} + (P : probability T R). + +Definition pairRV (X Y : {RV P >-> T'}) : T * T -> T' * T' := + (fun x => (X x.1, Y x.2)). + +Lemma pairM (X Y : {RV P >-> T'}) : measurable_fun setT (pairRV X Y). +Proof. +rewrite /pairRV. +apply/prod_measurable_funP; split => //=. + rewrite (_ : (fst \o (fun x : T * T => (X x.1, Y x.2))) = (fun x => X x.1))//. + by apply/measurableT_comp => //=. +rewrite (_ : (snd \o (fun x : T * T => (X x.1, Y x.2))) = (fun x => Y x.2))//. +by apply/measurableT_comp => //=. +Qed. + +HB.instance Definition _ (X Y : {RV P >-> T'}) := + @isMeasurableFun.Build _ _ _ _ (pairRV X Y) (pairM X Y). + +End pairRV. + +Section product_expectation. +Context {R : realType} d (T : measurableType d). +Variable P : probability T R. +Local Open Scope ereal_scope. + +Let mu := @lebesgue_measure R. + +Let mprod_m (X Y : {RV P >-> R}) (A1 : set R) (A2 : set R) : + measurable A1 -> measurable A2 -> + (distribution P X \x distribution P Y) (A1 `*` A2) = + ((distribution P X) A1 * (distribution P Y) A2)%E. +Proof. +move=> mA1 mA2. +etransitivity. + by apply: product_measure1E. +rewrite /=. +done. +Qed. + +Lemma tmp0 (X Y : {RV P >-> R}) (B1 B2 : set R) : + measurable B1 -> measurable B2 -> + independent_RVs2 P X Y -> + P (X @^-1` B1 `&` Y @^-1` B2) = P (X @^-1` B1) * P (Y @^-1` B2). +Proof. +move=> mB1 mB2. +rewrite /independent_RVs2 /independent_RVs /mutual_independence /= => -[_]. +move/(_ [fset false; true]%fset (@subsetT _ _) + (fun b => if b then Y @^-1` B2 else X @^-1` B1)). +rewrite !big_fsetU1 ?inE//= !big_seq_fset1/=. +apply => -[|] /= _; rewrite !inE; rewrite /g_sigma_algebra_mapping. +by exists B2 => //; rewrite setTI. +by exists B1 => //; rewrite setTI. +Qed. + +Lemma tmp1 (X Y : {RV P >-> R}) (B1 B2 : set R) : + measurable B1 -> measurable B2 -> + independent_RVs2 P X Y -> + P (X @^-1` B1 `&` Y @^-1` B2) = (P \x P) (pairRV X Y @^-1` (B1 `*` B2)). +Proof. +move=> mB1 mB2 XY. +rewrite (_ : ((fun x : T * T => (X x.1, Y x.2)) @^-1` (B1 `*` B2)) = + (X @^-1` B1) `*` (Y @^-1` B2)); last first. + by apply/seteqP; split => [[x1 x2]|[x1 x2]]//. +rewrite product_measure1E; last 2 first. + rewrite -[_ @^-1` _]setTI. + by apply: (measurable_funP X). + rewrite -[_ @^-1` _]setTI. + by apply: (measurable_funP Y). +by rewrite tmp0//. +Qed. + +Let phi (x : R * R) := (x.1 * x.2)%R. +Let mphi : measurable_fun setT phi. +Proof. +rewrite /= /phi. +by apply: measurable_funM. +Qed. + +Lemma PP : (P \x P) setT = 1. +Proof. +rewrite /product_measure1 /=. +rewrite /xsection/=. +under eq_integral. + move=> t _. + rewrite (_ : [set y | (t, y) \in [set: T * T]] = setT); last first. + apply/seteqP; split => [x|x]// _ /=. + by rewrite in_setT. + rewrite probability_setT. + over. +rewrite integral_cst // mul1e. +apply: probability_setT. +Qed. + +HB.instance Definition _ := @Measure_isProbability.Build _ _ R (P \x P) PP. + +Lemma integrable_expectationM (X Y : {RV P >-> R}) : + independent_RVs2 P X Y -> + P.-integrable setT (EFin \o X) -> P.-integrable setT (EFin \o Y) -> + 'E_(P \x P) [(fun x => `|X x.1 * Y x.2|)%R] < +oo +(* `|'E_(P) [(fun x => X x * Y x)%R]| < +oo *) . +Proof. +move=> indeXY iX iY. +(*apply: (@le_lt_trans _ _ 'E_(P \x P)[(fun x => `|(X x.1 * Y x.2)|%R)] + (* 'E_(P)[(fun x => `|(X x * Y x)|%R)] *) ). + rewrite unlock/=. + rewrite (le_trans (le_abse_integral _ _ _))//. + apply/measurable_EFinP/measurable_funM. + by apply/measurableT_comp => //. + by apply/measurableT_comp => //.*) +rewrite unlock. +rewrite [ltLHS](_ : _ = + \int[distribution (P \x P) (pairRV X Y)%R]_x `|x.1 * x.2|%:E); last first. + rewrite ge0_integral_distribution//=; last first. + apply/measurable_EFinP => //=. + by apply/measurableT_comp => //=. +rewrite [ltLHS](_ : _ = + \int[distribution P X \x distribution P Y]_x `|x.1 * x.2|%:E); last first. + apply: eq_measure_integral => // A mA _. + apply/esym. + apply: product_measure_unique => //= A1 A2 mA1 mA2. + rewrite /pushforward/=. + rewrite -tmp1//. + by rewrite tmp0//. +rewrite fubini_tonelli1//=; last first. + by apply/measurable_EFinP => /=; apply/measurableT_comp => //=. +rewrite /fubini_F/= -/mu. +rewrite [ltLHS](_ : _ = \int[distribution P X]_x `|x|%:E * + \int[distribution P Y]_y `|y|%:E); last first. + rewrite -ge0_integralZr//=; last 2 first. + exact/measurable_EFinP. + by apply: integral_ge0 => //. + apply: eq_integral => x _. + rewrite -ge0_integralZl//=. + by under eq_integral do rewrite normrM. + exact/measurable_EFinP. +rewrite ge0_integral_distribution//=; last exact/measurable_EFinP. +rewrite ge0_integral_distribution//=; last exact/measurable_EFinP. +rewrite lte_mul_pinfty//. + by apply: integral_ge0 => //. + apply: integral_fune_fin_num => //=. + by move/integrable_abse : iX => //. +apply: integral_fune_lt_pinfty => //. +by move/integrable_abse : iY => //. +Qed. + +End product_expectation. + +Section product_expectation. +Context {R : realType} d (T : measurableType d). +Variable P : probability T R. +Local Open Scope ereal_scope. + +Import HBNNSimple. + +Let expectationM_nnsfun (f g : {nnsfun T >-> R}) : + (forall y y', y \in range f -> y' \in range g -> + P (f @^-1` [set y] `&` g @^-1` [set y']) = + P (f @^-1` [set y]) * P (g @^-1` [set y'])) -> + 'E_P [f \* g] = 'E_P [f] * 'E_P [g]. +Proof. +move=> fg; transitivity + ('E_P [(fun x => (\sum_(y \in range f) y * \1_(f @^-1` [set y]) x)%R) + \* (fun x => (\sum_(y \in range g) y * \1_(g @^-1` [set y]) x)%R)]). + by congr ('E_P [_]); apply/funext => t/=; rewrite (fimfunE f) (fimfunE g). +transitivity ('E_P [(fun x => (\sum_(y \in range f) \sum_(y' \in range g) y * y' + * \1_(f @^-1` [set y] `&` g @^-1` [set y']) x)%R)]). + congr ('E_P [_]); apply/funext => t/=. + rewrite mulrC; rewrite fsbig_distrr//=. (* TODO: lemma fsbig_distrl *) + apply: eq_fsbigr => y yf; rewrite mulrC; rewrite fsbig_distrr//=. + by apply: eq_fsbigr => y' y'g; rewrite indicI mulrCA !mulrA (mulrC y'). +rewrite unlock. +under eq_integral do rewrite -fsumEFin//. +transitivity (\sum_(y \in range f) (\sum_(y' \in range g) + ((y * y')%:E * \int[P]_w (\1_(f @^-1` [set y] `&` g @^-1` [set y']) w)%:E))). + rewrite ge0_integral_fsum//=; last 2 first. + - move=> r; under eq_fun do rewrite -fsumEFin//. + apply: emeasurable_fsum => // s. + apply/measurable_EFinP/measurable_funM => //. + exact/measurable_indic/measurableI. + - move=> r t _; rewrite lee_fin sumr_ge0 // => s _; rewrite -lee_fin. + by rewrite indicI/= indicE -mulrACA EFinM mule_ge0// nnfun_muleindic_ge0. + apply: eq_fsbigr => y yf. + under eq_integral do rewrite -fsumEFin//. + rewrite ge0_integral_fsum//=; last 2 first. + - move=> r; apply/measurable_EFinP; apply: measurable_funM => //. + exact/measurable_indic/measurableI. + - move=> r t _. + by rewrite indicI/= indicE -mulrACA EFinM mule_ge0// nnfun_muleindic_ge0. + apply: eq_fsbigr => y' y'g. + under eq_integral do rewrite EFinM. + by rewrite integralZl//; exact/integrable_indic/measurableI. +transitivity (\sum_(y \in range f) (\sum_(y' \in range g) + ((y * y')%:E * (\int[P]_w (\1_(f @^-1` [set y]) w)%:E * + \int[P]_w (\1_(g @^-1` [set y']) w)%:E)))). + apply: eq_fsbigr => y fy; apply: eq_fsbigr => y' gy'; congr *%E. + transitivity ('E_P[\1_(f @^-1` [set y] `&` g @^-1` [set y'])]). + by rewrite unlock. + transitivity ('E_P[\1_(f @^-1` [set y])] * 'E_P[\1_(g @^-1` [set y'])]); + last by rewrite unlock. + rewrite expectation_indic//; last exact: measurableI. + by rewrite !expectation_indic// fg. +transitivity ( + (\sum_(y \in range f) (y%:E * (\int[P]_w (\1_(f @^-1` [set y]) w)%:E))) * + (\sum_(y' \in range g) (y'%:E * \int[P]_w (\1_(g @^-1` [set y']) w)%:E))). + transitivity (\sum_(y \in range f) (\sum_(y' \in range g) + (y'%:E * \int[P]_w (\1_(g @^-1` [set y']) w)%:E)%E)%R * + (y%:E * \int[P]_w (\1_(f @^-1` [set y]) w)%:E)%E%R); last first. + rewrite !fsbig_finite//= ge0_sume_distrl//; last first. + move=> r _; rewrite -integralZl//; last exact: integrable_indic. + by apply: integral_ge0 => t _; rewrite nnfun_muleindic_ge0. + by apply: eq_bigr => r _; rewrite muleC. + apply: eq_fsbigr => y fy. + rewrite !fsbig_finite//= ge0_sume_distrl//; last first. + move=> r _; rewrite -integralZl//; last exact: integrable_indic. + by apply: integral_ge0 => t _; rewrite nnfun_muleindic_ge0. + apply: eq_bigr => r _; rewrite (mulrC y) EFinM. + by rewrite [X in _ * X]muleC muleACA. +suff: forall h : {nnsfun T >-> R}, + (\sum_(y \in range h) (y%:E * \int[P]_w (\1_(h @^-1` [set y]) w)%:E)%E)%R + = \int[P]_w (h w)%:E. + by move=> suf; congr *%E; rewrite suf. +move=> h. +apply/esym. +under eq_integral do rewrite (fimfunE h). +under eq_integral do rewrite -fsumEFin//. +rewrite ge0_integral_fsum//; last 2 first. +- by move=> r; exact/measurable_EFinP/measurable_funM. +- by move=> r t _; rewrite lee_fin -lee_fin nnfun_muleindic_ge0. +by apply: eq_fsbigr => y fy; rewrite -integralZl//; exact/integrable_indic. +Qed. + +Lemma expectationM_ge0 (X Y : {RV P >-> R}) : + independent_RVs2 P X Y -> + 'E_P[X] *? 'E_P[Y] -> + (forall t, 0 <= X t)%R -> (forall t, 0 <= Y t)%R -> + 'E_P [X * Y] = 'E_P [X] * 'E_P [Y]. +Proof. +move=> indeXY defXY X0 Y0. +have mX : measurable_fun setT (EFin \o X) by exact/measurable_EFinP. +have mY : measurable_fun setT (EFin \o Y) by exact/measurable_EFinP. +pose X_ := nnsfun_approx measurableT mX. +pose Y_ := nnsfun_approx measurableT mY. +have EXY : 'E_P[X_ n \* Y_ n] @[n --> \oo] --> 'E_P [X * Y]. + rewrite unlock; have -> : \int[P]_w ((X * Y) w)%:E = + \int[P]_x limn (fun n => (EFin \o (X_ n \* Y_ n)%R) x). + apply: eq_integral => t _; apply/esym/cvg_lim => //=. + rewrite fctE EFinM; under eq_fun do rewrite EFinM. + by apply: cvgeM; [rewrite mule_def_fin//| + apply: cvg_nnsfun_approx => //= x _; rewrite lee_fin..]. + apply: cvg_monotone_convergence => //. + - by move=> n; apply/measurable_EFinP; exact: measurable_funM. + - by move=> n t _; rewrite lee_fin. + - move=> t _ m n mn. + by rewrite lee_fin/= ler_pM//; exact/lefP/nd_nnsfun_approx. +have EX : 'E_P[X_ n] @[n --> \oo] --> 'E_P [X]. + rewrite unlock. + have -> : \int[P]_w (X w)%:E = \int[P]_x limn (fun n => (EFin \o X_ n) x). + by apply: eq_integral => t _; apply/esym/cvg_lim => //=; + apply: cvg_nnsfun_approx => // x _; rewrite lee_fin. + apply: cvg_monotone_convergence => //. + - by move=> n; exact/measurable_EFinP. + - by move=> n t _; rewrite lee_fin. + - by move=> t _ m n mn; rewrite lee_fin/=; exact/lefP/nd_nnsfun_approx. +have EY : 'E_P[Y_ n] @[n --> \oo] --> 'E_P [Y]. + rewrite unlock. + have -> : \int[P]_w (Y w)%:E = \int[P]_x limn (fun n => (EFin \o Y_ n) x). + by apply: eq_integral => t _; apply/esym/cvg_lim => //=; + apply: cvg_nnsfun_approx => // x _; rewrite lee_fin. + apply: cvg_monotone_convergence => //. + - by move=> n; exact/measurable_EFinP. + - by move=> n t _; rewrite lee_fin. + - by move=> t _ m n mn; rewrite lee_fin/=; exact/lefP/nd_nnsfun_approx. +have {EX EY}EXY' : 'E_P[X_ n] * 'E_P[Y_ n] @[n --> \oo] --> 'E_P[X] * 'E_P[Y]. + apply: cvgeM => //. +suff : forall n, 'E_P[X_ n \* Y_ n] = 'E_P[X_ n] * 'E_P[Y_ n]. + by move=> suf; apply: (cvg_unique _ EXY) => //=; under eq_fun do rewrite suf. +move=> n; apply: expectationM_nnsfun => x y xX_ yY_. +suff : P (\big[setI/setT]_(j <- [fset false; true]%fset) + [eta fun=> set0 with 0%N |-> X_ n @^-1` [set x], + 1%N |-> Y_ n @^-1` [set y]] j) = + \prod_(j <- [fset false; true]%fset) + P ([eta fun=> set0 with 0%N |-> X_ n @^-1` [set x], + 1%N |-> Y_ n @^-1` [set y]] j). + by rewrite !big_fsetU1/= ?inE//= !big_seq_fset1/=. +move: indeXY => [/= _]; apply => // i. +pose AX := dyadic_approx setT (EFin \o X). +pose AY := dyadic_approx setT (EFin \o Y). +pose BX := integer_approx setT (EFin \o X). +pose BY := integer_approx setT (EFin \o Y). +have mA (Z : {RV P >-> R}) m k : (k < m * 2 ^ m)%N -> + g_sigma_algebra_mapping Z (dyadic_approx setT (EFin \o Z) m k). + move=> mk; rewrite /g_sigma_algebra_mapping /dyadic_approx mk setTI. + rewrite /preimage_set_system/=; exists [set` dyadic_itv R m k] => //. + rewrite setTI/=; apply/seteqP; split => z/=. + by rewrite inE/= => Zz; exists (Z z). + by rewrite inE/= => -[r rmk] [<-]. +have mB (Z : {RV P >-> R}) k : + g_sigma_algebra_mapping Z (integer_approx setT (EFin \o Z) k). + rewrite /g_sigma_algebra_mapping /integer_approx setTI /preimage_set_system/=. + by exists `[k%:R, +oo[%classic => //; rewrite setTI preimage_itvcy. +have m1A (Z : {RV P >-> R}) : forall k, (k < n * 2 ^ n)%N -> + measurable_fun setT + (\1_(dyadic_approx setT (EFin \o Z) n k) : g_sigma_algebra_mappingType Z -> R). + move=> k kn. + exact/(@measurable_indicP _ (g_sigma_algebra_mappingType Z))/mA. +rewrite !inE => /orP[|]/eqP->{i} //=. + have : @measurable_fun _ _ (g_sigma_algebra_mappingType X) _ setT (X_ n). + rewrite nnsfun_approxE//. + apply: measurable_funD => //=. + apply: measurable_sum => //= k'; apply: measurable_funM => //. + by apply: measurable_indic; exact: mA. + apply: measurable_funM => //. + by apply: measurable_indic; exact: mB. + rewrite /measurable_fun => /(_ measurableT _ (measurable_set1 x)). + by rewrite setTI. +have : @measurable_fun _ _ (g_sigma_algebra_mappingType Y) _ setT (Y_ n). + rewrite nnsfun_approxE//. + apply: measurable_funD => //=. + apply: measurable_sum => //= k'; apply: measurable_funM => //. + by apply: measurable_indic; exact: mA. + apply: measurable_funM => //. + by apply: measurable_indic; exact: mB. +move=> /(_ measurableT [set y] (measurable_set1 y)). +by rewrite setTI. +Qed. + +Lemma integrable_expectationM000 (X Y : {RV P >-> R}) : + independent_RVs2 P X Y -> + (X : _ -> _) \in Lfun P 1 -> (Y : _ -> _) \in Lfun P 1 -> + `|'E_P [X * Y]| < +oo. +Proof. +move=> indeXY iX iY. +apply: (@le_lt_trans _ _ 'E_P[(@normr _ _ \o X) * (@normr _ _ \o Y)]). + rewrite unlock/=. + rewrite (le_trans (le_abse_integral _ _ _))//. + apply/measurable_EFinP/measurable_funM. + by move/Lfun1_integrable : iX => /measurable_int/measurable_EFinP. + by move/Lfun1_integrable : iY => /measurable_int/measurable_EFinP. + apply: ge0_le_integral => //=. + - by apply/measurable_EFinP; exact/measurableT_comp. + - by move=> x _; rewrite lee_fin/= mulr_ge0/=. + - by apply/measurable_EFinP; apply/measurable_funM; exact/measurableT_comp. + - by move=> t _; rewrite lee_fin/= normrM. +rewrite expectationM_ge0//=. +- rewrite lte_mul_pinfty//. + + by rewrite expectation_ge0/=. + + rewrite expectation_fin_num//=. + by move: iX => /Lfun_norm. + + move : iY => /Lfun1_integrable. + move=> /integrableP[_]. + by rewrite unlock. +- exact: independent_RVs2_comp. +- apply: mule_def_fin; rewrite unlock integrable_fin_num//. + + by move/Lfun_norm : iX => /Lfun1_integrable. + + by move/Lfun_norm : iY => /Lfun1_integrable. +Qed. + +Lemma independent_integrableM (X Y : {RV P >-> R}) : + independent_RVs2 P X Y -> + (X : _ -> _) \in Lfun P 1 -> (Y : _ -> _) \in Lfun P 1 -> + (X \* Y)%R \in Lfun P 1. +Proof. +move=> indeXY iX iY. +apply/Lfun1_integrable. +apply/integrableP; split => //. + move/Lfun1_integrable : iX => /integrableP[iX _]. + move/Lfun1_integrable : iY => /integrableP[iY _]. + apply/measurable_EFinP. + by apply/measurable_funM; apply/measurable_EFinP. +have := integrable_expectationM000 indeXY iX iY. +rewrite unlock => /abse_integralP. +apply => //. +exact/measurable_EFinP/measurable_funM. +Qed. + +(* TODO: rename to expectationM when deprecation is removed *) +Lemma expectation_prod (X Y : {RV P >-> R}) : + independent_RVs2 P X Y -> + (X : _ -> _) \in Lfun P 1 -> (Y : _ -> _) \in Lfun P 1 -> + 'E_P [X * Y] = 'E_P [X] * 'E_P [Y]. +Proof. +move=> XY iX iY. +transitivity ('E_P[(X^\+ - X^\-) * (Y^\+ - Y^\-)]). + congr ('E_P[_]). + apply/funext => /=t. + by rewrite [in LHS](funrposneg X)/= [in LHS](funrposneg Y). +have ? : P.-integrable [set: T] (EFin \o X^\-%R). + rewrite -funerneg; apply/integrable_funeneg => //. + exact/Lfun1_integrable. +have ? : P.-integrable [set: T] (EFin \o X^\+%R). + rewrite -funerpos; apply/integrable_funepos => //. + exact/Lfun1_integrable. +have ? : P.-integrable [set: T] (EFin \o Y^\+%R). + rewrite -funerpos; apply/integrable_funepos => //. + exact/Lfun1_integrable. +have ? : P.-integrable [set: T] (EFin \o Y^\-%R). + rewrite -funerneg; apply/integrable_funeneg => //. + exact/Lfun1_integrable. +have ? : P.-integrable [set: T] (EFin \o (X^\+ \* Y^\+)%R). + apply/Lfun1_integrable. + apply: independent_integrableM => //=. + exact: independent_RVs2_funrpospos. + by apply/Lfun1_integrable. + by apply/Lfun1_integrable. +have ? : P.-integrable [set: T] (EFin \o (X^\- \* Y^\+)%R). + apply/Lfun1_integrable. + apply: independent_integrableM => //=. + exact: independent_RVs2_funrnegpos. + by apply/Lfun1_integrable. + by apply/Lfun1_integrable. +have ? : P.-integrable [set: T] (EFin \o (X^\+ \* Y^\-)%R). + apply/Lfun1_integrable. + apply: independent_integrableM => //=. + exact: independent_RVs2_funrposneg. + by apply/Lfun1_integrable. + by apply/Lfun1_integrable. +have ? : P.-integrable [set: T] (EFin \o (X^\- \* Y^\-)%R). + apply/Lfun1_integrable. + apply: independent_integrableM => //=. + exact: independent_RVs2_funrnegneg. + by apply/Lfun1_integrable. + by apply/Lfun1_integrable. +transitivity ('E_P[X^\+ * Y^\+] - 'E_P[X^\- * Y^\+] + - 'E_P[X^\+ * Y^\-] + 'E_P[X^\- * Y^\-]). + rewrite mulrDr !mulrDl -expectationB//=; [|exact/Lfun1_integrable..]. + rewrite -expectationB//=; last 2 first. + by rewrite rpredB//; exact/Lfun1_integrable. + exact/Lfun1_integrable. + rewrite -expectationD//=; last 2 first. + rewrite rpredB//; last exact/Lfun1_integrable. + by rewrite rpredB//; exact/Lfun1_integrable. + exact/Lfun1_integrable. + congr ('E_P[_]); apply/funext => t/=. + by rewrite !fctE !(mulNr,mulrN,opprK,addrA)/=. +rewrite [in LHS]expectationM_ge0//=; last 2 first. + exact: independent_RVs2_funrpospos. + by rewrite mule_def_fin// expectation_fin_num//; exact/Lfun1_integrable. +rewrite [in LHS]expectationM_ge0//=; last 2 first. + exact: independent_RVs2_funrnegpos. + by rewrite mule_def_fin// expectation_fin_num//; exact/Lfun1_integrable. +rewrite [in LHS]expectationM_ge0//=; last 2 first. + exact: independent_RVs2_funrposneg. + by rewrite mule_def_fin// expectation_fin_num//; exact/Lfun1_integrable. +rewrite [in LHS]expectationM_ge0//=; last 2 first. + exact: independent_RVs2_funrnegneg. + by rewrite mule_def_fin// expectation_fin_num//=; exact/Lfun1_integrable. +transitivity ('E_P[X^\+ - X^\-] * 'E_P[Y^\+ - Y^\-]). + rewrite -addeA -addeACA -muleBr; last 2 first. + by rewrite expectation_fin_num//; exact/Lfun1_integrable. + by rewrite fin_num_adde_defr// expectation_fin_num//; exact/Lfun1_integrable. + rewrite -oppeB; last first. + by rewrite fin_num_adde_defr// fin_numM// expectation_fin_num//; exact/Lfun1_integrable. + rewrite -muleBr; last 2 first. + by rewrite expectation_fin_num//; exact/Lfun1_integrable. + by rewrite fin_num_adde_defr// expectation_fin_num//; exact/Lfun1_integrable. + rewrite -muleBl; last 2 first. + by rewrite fin_numB// !expectation_fin_num//; exact/Lfun1_integrable. + by rewrite fin_num_adde_defr// expectation_fin_num//; exact/Lfun1_integrable. + rewrite -expectationB//=; [|exact/Lfun1_integrable..]. + by rewrite -expectationB//; exact/Lfun1_integrable. +by congr *%E; congr ('E_P[_]); rewrite [RHS]funrposneg. +Qed. + +Lemma prodE (s : seq nat) (X : {RV P >-> R}^nat) (t : T) : + (\prod_(i <- s) X i t)%R = ((\prod_(j <- s) X j)%R t). +Proof. +by elim/big_ind2 : _ => //= {}X x {}Y y -> ->. +Qed. + +Lemma set_cons2 (I : eqType) (x y : I) : [set` [:: x; y]] = [set x ; y]. +Proof. +apply/seteqP; split => z /=; rewrite !inE. + move=> /orP[|] /eqP ->; auto. +by move=> [|] ->; rewrite eqxx// orbT. +Qed. + +Lemma independent_RVsD1 (I : {fset nat}) i0 (X : {RV P >-> R}^nat) : + independent_RVs P [set` I] X -> independent_RVs P [set` (I `\ i0)%fset] X. +Proof. +move=> H. +split => [/= i|/= J JIi0 E EK]. + rewrite !inE => /andP[ii0 iI]. + by apply H. +apply H => //. +by move=> /= x /JIi0 /=; rewrite !inE => /andP[]. +Qed. + +End product_expectation. diff --git a/theories/probability.v b/theories/probability.v index 7794975db9..74feaf83bf 100644 --- a/theories/probability.v +++ b/theories/probability.v @@ -1384,7 +1384,7 @@ transitivity (\sum_(y \in range f) (\sum_(y' \in range g) ((y * y')%:E * \int[P]_w (\1_(f @^-1` [set y] `&` g @^-1` [set y']) w)%:E))). rewrite ge0_integral_fsum//=; last 2 first. - move=> r; under eq_fun do rewrite -fsumEFin//. - apply: emeasurable_fun_fsum => // s. + apply: emeasurable_fsum => // s. apply/measurable_EFinP/measurable_funM => //. exact/measurable_indic/measurableI. - move=> r t _; rewrite lee_fin sumr_ge0 // => s _; rewrite -lee_fin. From e14e8710bebccb3709a2fe21b6c39b5c9b490327 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Thu, 26 Dec 2024 22:49:36 +0900 Subject: [PATCH 04/10] renaming --- CHANGELOG_UNRELEASED.md | 36 ++----------- theories/independence.v | 113 +++++++++++++++++++--------------------- theories/probability.v | 78 +++++++++++++-------------- 3 files changed, 97 insertions(+), 130 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index c114dedb54..5c26a33f18 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -174,17 +174,6 @@ + lemmas `RabsE`, `RdistE`, `sum_f_R0E`, `factE` - new file `internal_Eqdep_dec.v` (don't use, internal, to be removed) -- in `normedtype.v`: - + lemma `scaler1` - -- in `derive.v`: - + lemmas `horner0_ext`, `hornerD_ext`, `horner_scale_ext`, `hornerC_ext`, - `derivable_horner`, `derivE`, `continuous_horner` - + instance `is_derive_poly` -- in `mathcomp_extra.v`: - + lemma `partition_disjoint_bigfcup` -- in `lebesgue_measure.v`: - + lemma `measurable_indicP` - in `numfun.v`: + defintions `funrpos`, `funrneg` with notations `^\+` and `^\-` @@ -196,35 +185,20 @@ - in `measure.v`: + lemma `preimage_class_comp` - + defintions `mapping_display`, `g_sigma_algebra_mappingType`, `g_sigma_algebra_mapping`, - notations `.-mapping`, `.-mapping.-measurable` + + defintions `preimage_display`, `g_sigma_algebra_preimageType`, `g_sigma_algebra_preimage`, + notations `.-preimage`, `.-preimage.-measurable` -- in `lebesgue_measure.v`: +- in `measurable_realfun.v`: + lemmas `measurable_funrpos`, `measurable_funrneg` -- in `lebesgue_integral.v`: - + lemmas `integral_fin_num_abs`, `Rintegral_cst`, `le_Rintegral` - -- new file `pi_irrational.v`: - + lemmas `measurable_poly` - + definition `rational` - + module `pi_irrational` - + lemma `pi_irrationnal` -- in `constructive_ereal.v`: - + notations `\prod` in scope ereal_scope - + lemmas `prode_ge0`, `prode_fin_num` -- in `probability.v`: - + lemma `expectation_def` - + notation `'M_` - - new file `independence.v`: + lemma `expectationM_ge0` + definition `independent_events` + definition `mutual_independence` + definition `independent_RVs` + definition `independent_RVs2` - + lemmas `g_sigma_algebra_mapping_comp`, `g_sigma_algebra_mapping_funrpos`, - `g_sigma_algebra_mapping_funrneg` + + lemmas `g_sigma_algebra_preimage_comp`, `g_sigma_algebra_preimage_funrpos`, + `g_sigma_algebra_preimage_funrneg` + lemmas `independent_RVs2_comp`, `independent_RVs2_funrposneg`, `independent_RVs2_funrnegpos`, `independent_RVs2_funrnegneg`, `independent_RVs2_funrpospos` diff --git a/theories/independence.v b/theories/independence.v index 034f15aa89..07c86ed445 100644 --- a/theories/independence.v +++ b/theories/independence.v @@ -2,7 +2,7 @@ From mathcomp Require Import all_ssreflect interval_inference. From mathcomp Require Import ssralg poly ssrnum ssrint interval finmap. From mathcomp Require Import mathcomp_extra boolp classical_sets functions. -From mathcomp Require Import cardinality fsbigop. +From mathcomp Require Import cardinality fsbigop interval_inference. From HB Require Import structures. From mathcomp Require Import exp numfun lebesgue_measure lebesgue_integral. From mathcomp Require Import reals ereal topology normedtype sequences. @@ -214,7 +214,7 @@ Section mutual_independence_properties. Context {R : realType} d {T : measurableType d} (P : probability T R). Local Open Scope ereal_scope. -(**md see Achim Klenke's Probability Thery, Ch.2, sec.2.1, thm.2.13(i) *) +(**md see Achim Klenke's Probability Theory, Ch.2, sec.2.1, thm.2.13(i) *) Lemma mutual_independence_fset {I0 : choiceType} (I : {fset I0}) (F : I0 -> set_system T) : (forall i, i \in I -> F i `<=` measurable /\ (F i) [set: T]) -> @@ -238,7 +238,7 @@ rewrite -big_seq => ->. by rewrite !big_seq; apply: eq_bigr => i iJ; rewrite /E' iJ. Qed. -(**md see Achim Klenke's Probability Thery, Ch.2, sec.2.1, thm.2.13(ii) *) +(**md see Achim Klenke's Probability Theory, Ch.2, sec.2.1, thm.2.13(ii) *) Lemma mutual_independence_finiteS {I0 : choiceType} (I : set I0) (F : I0 -> set_system T) : mutual_independence P I F <-> @@ -256,7 +256,7 @@ split=> [i Ii|J JI E EF]. by have [_] := indeF _ JI; exact. Qed. -(**md see Achim Klenke's Probability Thery, Ch.2, sec.2.1, thm.2.13(iii) *) +(**md see Achim Klenke's Probability Theory, Ch.2, sec.2.1, thm.2.13(iii) *) Theorem mutual_independence_finite_g_sigma {I0 : choiceType} (I : set I0) (F : I0 -> set_system T) : (forall i, i \in I -> setI_closed (F i `|` [set set0])) -> @@ -438,7 +438,7 @@ apply/negP/set0P; exists j; split => //. exact/set_mem. Qed. -(**md see Achim Klenke's Probability Thery, Ch.2, sec.2.1, thm.2.13(iv) *) +(**md see Achim Klenke's Probability Theory, Ch.2, sec.2.1, thm.2.13(iv) *) Lemma mutual_independence_bigcup (K0 I0 : pointedType) (K : {fset K0}) (I_ : K0 -> set I0) (I : set I0) (F : I0 -> set_system T) : trivIset [set` K] (fun i => I_ i) -> @@ -483,36 +483,28 @@ Qed. End mutual_independence_properties. -Section g_sigma_algebra_mapping_lemmas. +Section g_sigma_algebra_preimage_lemmas. Context d {T : measurableType d} {R : realType}. -Lemma g_sigma_algebra_mapping_comp (X : {mfun T >-> R}) (f : R -> R) : +Lemma g_sigma_algebra_preimage_comp (X : {mfun T >-> R}) (f : R -> R) : measurable_fun setT f -> - g_sigma_algebra_mapping (f \o X)%R `<=` g_sigma_algebra_mapping X. -Proof. -move=> mf. -rewrite /g_sigma_algebra_mapping. -rewrite preimage_set_system_comp. -move=> A /= [] B [C mC <-{B}] <-{A}. -red. -exists ([set: R] `&` f @^-1` C) => //. -by apply: mf. -Qed. + g_sigma_algebra_preimage (f \o X)%R `<=` g_sigma_algebra_preimage X. +Proof. exact: preimage_set_system_compS. Qed. -Lemma g_sigma_algebra_mapping_funrpos (X : {mfun T >-> R}) : - g_sigma_algebra_mapping X^\+%R `<=` d.-measurable. +Lemma g_sigma_algebra_preimage_funrpos (X : {mfun T >-> R}) : + g_sigma_algebra_preimage X^\+%R `<=` d.-measurable. Proof. by move=> A/= -[B mB] <-; have := measurable_funrpos (measurable_funP X); exact. Qed. -Lemma g_sigma_algebra_mapping_funrneg (X : {mfun T >-> R}) : - g_sigma_algebra_mapping X^\-%R `<=` d.-measurable. +Lemma g_sigma_algebra_preimage_funrneg (X : {mfun T >-> R}) : + g_sigma_algebra_preimage X^\-%R `<=` d.-measurable. Proof. by move=> A/= -[B mB] <-; have := measurable_funrneg (measurable_funP X); exact. Qed. -End g_sigma_algebra_mapping_lemmas. -Arguments g_sigma_algebra_mapping_comp {d T R X} f. +End g_sigma_algebra_preimage_lemmas. +Arguments g_sigma_algebra_preimage_comp {d T R X} f. Section independent_RVs. Context {R : realType} d (T : measurableType d). @@ -522,7 +514,7 @@ Variable P : probability T R. Definition independent_RVs (I : set I0) (X : forall i : I0, {mfun T >-> T' i}) : Prop := - mutual_independence P I (fun i => g_sigma_algebra_mapping (X i)). + mutual_independence P I (fun i => g_sigma_algebra_preimage (X i)). End independent_RVs. @@ -541,7 +533,7 @@ Context {I0 : choiceType}. Context {d' : I0 -> _} (T' : forall i : I0, measurableType (d' i)). Variable P : probability T R. -(**md see Achim Klenke's Probability Thery, Ch.2, sec.2.1, thm.2.16 *) +(**md see Achim Klenke's Probability Theory, Ch.2, sec.2.1, thm.2.16 *) Theorem independent_generators (I : set I0) (F : forall i : I0, set_system (T' i)) (X : forall i, {RV P >-> T' i}) : (forall i, i \in I -> setI_closed (F i)) -> @@ -559,9 +551,9 @@ have closed_preimage i : I i -> setI_closed (preimage_set_system setT (X i) (F i - exact/mem_set. - by rewrite setTI. have gen_preimage i : I i -> - <> = g_sigma_algebra_mapping (X i). + <> = g_sigma_algebra_preimage (X i). move=> Ii. - rewrite /g_sigma_algebra_mapping AsF; last exact/mem_set. + rewrite /g_sigma_algebra_preimage AsF; last exact/mem_set. by rewrite -g_sigma_preimageE. rewrite /independent_RVs. suff: mutual_independence P I (fun i => <>). @@ -585,27 +577,27 @@ Lemma independent_RVs2_comp (X Y : {RV P >-> R}) (f g : {mfun R >-> R}) : Proof. move=> indeXY; split => /=. - move=> [] _ /= A. - + by rewrite /g_sigma_algebra_mapping/= /preimage_set_system/= => -[B mB <-]; + + by rewrite /g_sigma_algebra_preimage/= /preimage_set_system/= => -[B mB <-]; exact/measurableT_comp. - + by rewrite /g_sigma_algebra_mapping/= /preimage_set_system/= => -[B mB <-]; + + by rewrite /g_sigma_algebra_preimage/= /preimage_set_system/= => -[B mB <-]; exact/measurableT_comp. - move=> J _ E JE. apply indeXY => //= i iJ; have := JE _ iJ. by move: i {iJ} =>[|]//=; rewrite !inE => Eg; - exact: g_sigma_algebra_mapping_comp Eg. + exact: g_sigma_algebra_preimage_comp Eg. Qed. Lemma independent_RVs2_funrposneg (X Y : {RV P >-> R}) : independent_RVs2 P X Y -> independent_RVs2 P X^\+ Y^\-. Proof. move=> indeXY; split=> [[|]/= _|J J2 E JE]. -- exact: g_sigma_algebra_mapping_funrneg. -- exact: g_sigma_algebra_mapping_funrpos. +- exact: g_sigma_algebra_preimage_funrneg. +- exact: g_sigma_algebra_preimage_funrpos. - apply indeXY => //= i iJ; have := JE _ iJ. move/J2 : iJ; move: i => [|]// _; rewrite !inE. - + apply: (g_sigma_algebra_mapping_comp (fun x => maxr (- x) 0)%R). + + apply: (g_sigma_algebra_preimage_comp (fun x => maxr (- x) 0)%R). exact: measurable_funrneg. - + apply: (g_sigma_algebra_mapping_comp (fun x => maxr x 0)%R) => //. + + apply: (g_sigma_algebra_preimage_comp (fun x => maxr x 0)%R) => //. exact: measurable_funrpos. Qed. @@ -613,13 +605,13 @@ Lemma independent_RVs2_funrnegpos (X Y : {RV P >-> R}) : independent_RVs2 P X Y -> independent_RVs2 P X^\- Y^\+. Proof. move=> indeXY; split=> [/= [|]// _ |J J2 E JE]. -- exact: g_sigma_algebra_mapping_funrpos. -- exact: g_sigma_algebra_mapping_funrneg. +- exact: g_sigma_algebra_preimage_funrpos. +- exact: g_sigma_algebra_preimage_funrneg. - apply indeXY => //= i iJ; have := JE _ iJ. move/J2 : iJ; move: i => [|]// _; rewrite !inE. - + apply: (g_sigma_algebra_mapping_comp (fun x => maxr x 0)%R). + + apply: (g_sigma_algebra_preimage_comp (fun x => maxr x 0)%R). exact: measurable_funrpos. - + apply: (g_sigma_algebra_mapping_comp (fun x => maxr (- x) 0)%R). + + apply: (g_sigma_algebra_preimage_comp (fun x => maxr (- x) 0)%R). exact: measurable_funrneg. Qed. @@ -627,13 +619,13 @@ Lemma independent_RVs2_funrnegneg (X Y : {RV P >-> R}) : independent_RVs2 P X Y -> independent_RVs2 P X^\- Y^\-. Proof. move=> indeXY; split=> [/= [|]// _ |J J2 E JE]. -- exact: g_sigma_algebra_mapping_funrneg. -- exact: g_sigma_algebra_mapping_funrneg. +- exact: g_sigma_algebra_preimage_funrneg. +- exact: g_sigma_algebra_preimage_funrneg. - apply indeXY => //= i iJ; have := JE _ iJ. move/J2 : iJ; move: i => [|]// _; rewrite !inE. - + apply: (g_sigma_algebra_mapping_comp (fun x => maxr (- x) 0)%R). + + apply: (g_sigma_algebra_preimage_comp (fun x => maxr (- x) 0)%R). exact: measurable_funrneg. - + apply: (g_sigma_algebra_mapping_comp (fun x => maxr (- x) 0)%R). + + apply: (g_sigma_algebra_preimage_comp (fun x => maxr (- x) 0)%R). exact: measurable_funrneg. Qed. @@ -641,22 +633,23 @@ Lemma independent_RVs2_funrpospos (X Y : {RV P >-> R}) : independent_RVs2 P X Y -> independent_RVs2 P X^\+ Y^\+. Proof. move=> indeXY; split=> [/= [|]//= _ |J J2 E JE]. -- exact: g_sigma_algebra_mapping_funrpos. -- exact: g_sigma_algebra_mapping_funrpos. +- exact: g_sigma_algebra_preimage_funrpos. +- exact: g_sigma_algebra_preimage_funrpos. - apply indeXY => //= i iJ; have := JE _ iJ. move/J2 : iJ; move: i => [|]// _; rewrite !inE. - + apply: (g_sigma_algebra_mapping_comp (fun x => maxr x 0)%R). + + apply: (g_sigma_algebra_preimage_comp (fun x => maxr x 0)%R). exact: measurable_funrpos. - + apply: (g_sigma_algebra_mapping_comp (fun x => maxr x 0)%R). + + apply: (g_sigma_algebra_preimage_comp (fun x => maxr x 0)%R). exact: measurable_funrpos. Qed. End independent_RVs_lemmas. -Definition preimage_classes I (d : I -> measure_display) - (Tn : forall k, semiRingOfSetsType (d k)) (T : Type) (fn : forall k, T -> Tn k) := - <>. -Arguments preimage_classes {I} d Tn {T} fn. +Definition preimage_classes I0 (I : set I0) (d_ : forall i : I, measure_display) + (T_ : forall k : I, semiRingOfSetsType (d_ k)) (T : Type) + (f_ : forall k : I, T -> T_ k) := + <>. +Arguments preimage_classes {I0} I d_ T_ {T} f_. Lemma measurable_prod d [T : measurableType d] [R : realType] [D : set T] [I : eqType] (s : seq I) [h : I -> T -> R] : @@ -726,7 +719,7 @@ rewrite /independent_RVs2 /independent_RVs /mutual_independence /= => -[_]. move/(_ [fset false; true]%fset (@subsetT _ _) (fun b => if b then Y @^-1` B2 else X @^-1` B1)). rewrite !big_fsetU1 ?inE//= !big_seq_fset1/=. -apply => -[|] /= _; rewrite !inE; rewrite /g_sigma_algebra_mapping. +apply => -[|] /= _; rewrite !inE; rewrite /g_sigma_algebra_preimage. by exists B2 => //; rewrite setTI. by exists B1 => //; rewrite setTI. Qed. @@ -967,23 +960,23 @@ pose AY := dyadic_approx setT (EFin \o Y). pose BX := integer_approx setT (EFin \o X). pose BY := integer_approx setT (EFin \o Y). have mA (Z : {RV P >-> R}) m k : (k < m * 2 ^ m)%N -> - g_sigma_algebra_mapping Z (dyadic_approx setT (EFin \o Z) m k). - move=> mk; rewrite /g_sigma_algebra_mapping /dyadic_approx mk setTI. + g_sigma_algebra_preimage Z (dyadic_approx setT (EFin \o Z) m k). + move=> mk; rewrite /g_sigma_algebra_preimage /dyadic_approx mk setTI. rewrite /preimage_set_system/=; exists [set` dyadic_itv R m k] => //. rewrite setTI/=; apply/seteqP; split => z/=. by rewrite inE/= => Zz; exists (Z z). by rewrite inE/= => -[r rmk] [<-]. have mB (Z : {RV P >-> R}) k : - g_sigma_algebra_mapping Z (integer_approx setT (EFin \o Z) k). - rewrite /g_sigma_algebra_mapping /integer_approx setTI /preimage_set_system/=. + g_sigma_algebra_preimage Z (integer_approx setT (EFin \o Z) k). + rewrite /g_sigma_algebra_preimage /integer_approx setTI /preimage_set_system/=. by exists `[k%:R, +oo[%classic => //; rewrite setTI preimage_itvcy. have m1A (Z : {RV P >-> R}) : forall k, (k < n * 2 ^ n)%N -> measurable_fun setT - (\1_(dyadic_approx setT (EFin \o Z) n k) : g_sigma_algebra_mappingType Z -> R). + (\1_(dyadic_approx setT (EFin \o Z) n k) : g_sigma_algebra_preimageType Z -> R). move=> k kn. - exact/(@measurable_indicP _ (g_sigma_algebra_mappingType Z))/mA. + exact/(@measurable_indicP _ (g_sigma_algebra_preimageType Z))/mA. rewrite !inE => /orP[|]/eqP->{i} //=. - have : @measurable_fun _ _ (g_sigma_algebra_mappingType X) _ setT (X_ n). + have : @measurable_fun _ _ (g_sigma_algebra_preimageType X) _ setT (X_ n). rewrite nnsfun_approxE//. apply: measurable_funD => //=. apply: measurable_sum => //= k'; apply: measurable_funM => //. @@ -992,7 +985,7 @@ rewrite !inE => /orP[|]/eqP->{i} //=. by apply: measurable_indic; exact: mB. rewrite /measurable_fun => /(_ measurableT _ (measurable_set1 x)). by rewrite setTI. -have : @measurable_fun _ _ (g_sigma_algebra_mappingType Y) _ setT (Y_ n). +have : @measurable_fun _ _ (g_sigma_algebra_preimageType Y) _ setT (Y_ n). rewrite nnsfun_approxE//. apply: measurable_funD => //=. apply: measurable_sum => //= k'; apply: measurable_funM => //. @@ -1053,7 +1046,7 @@ exact/measurable_EFinP/measurable_funM. Qed. (* TODO: rename to expectationM when deprecation is removed *) -Lemma expectation_prod (X Y : {RV P >-> R}) : +Lemma expectation_mul (X Y : {RV P >-> R}) : independent_RVs2 P X Y -> (X : _ -> _) \in Lfun P 1 -> (Y : _ -> _) \in Lfun P 1 -> 'E_P [X * Y] = 'E_P [X] * 'E_P [Y]. diff --git a/theories/probability.v b/theories/probability.v index 74feaf83bf..f9105f7653 100644 --- a/theories/probability.v +++ b/theories/probability.v @@ -1183,44 +1183,44 @@ Definition mutual_independence (I0 : choiceType) (I : set I0) End mutual_independence. -(* g_sigma_algebra_mapping f == sigma-algebra generated by the mapping f *) -(* g_sigma_algebra_mappingType f == the measurableType corresponding to *) -(* g_sigma_algebra_mapping f *) +(* g_sigma_algebra_preimage f == sigma-algebra generated by the function f *) +(* g_sigma_algebra_preimageType f == the measurableType corresponding to *) +(* g_sigma_algebra_preimage f *) (* This is an HB alias. *) -(* f.-mapping.-measurable A == A is measurable for g_sigma_algebra_mapping f *) +(* f.-preimage.-measurable A == A is measurable for g_sigma_algebra_preimage f *) -Definition mapping_display {T T'} : (T -> T') -> measure_display. +Definition preimage_display {T T'} : (T -> T') -> measure_display. Proof. exact. Qed. -Definition g_sigma_algebra_mappingType d' (T : pointedType) +Definition g_sigma_algebra_preimageType d' (T : pointedType) (T' : measurableType d') (f : T -> T') : Type := T. -Definition g_sigma_algebra_mapping d' (T : pointedType) +Definition g_sigma_algebra_preimage d' (T : pointedType) (T' : measurableType d') (f : T -> T') := preimage_set_system setT f (@measurable _ T'). -Section mapping_generated_sigma_algebra. +Section preimage_generated_sigma_algebra. Context {d'} (T : pointedType) (T' : measurableType d'). Variable f : T -> T'. -Let mapping_set0 : g_sigma_algebra_mapping f set0. +Let preimage_set0 : g_sigma_algebra_preimage f set0. Proof. -rewrite /g_sigma_algebra_mapping /preimage_set_system/=. +rewrite /g_sigma_algebra_preimage /preimage_set_system/=. by exists set0 => //; rewrite preimage_set0 setI0. Qed. -Let mapping_setC A : - g_sigma_algebra_mapping f A -> g_sigma_algebra_mapping f (~` A). +Let preimage_setC A : + g_sigma_algebra_preimage f A -> g_sigma_algebra_preimage f (~` A). Proof. -rewrite /g_sigma_algebra_mapping /preimage_set_system/= => -[B mB] <-{A}. +rewrite /g_sigma_algebra_preimage /preimage_set_system/= => -[B mB] <-{A}. by exists (~` B); [exact: measurableC|rewrite !setTI preimage_setC]. Qed. -Let mapping_bigcup (F : (set T)^nat) : - (forall i, g_sigma_algebra_mapping f (F i)) -> - g_sigma_algebra_mapping f (\bigcup_i (F i)). +Let preimage_bigcup (F : (set T)^nat) : + (forall i, g_sigma_algebra_preimage f (F i)) -> + g_sigma_algebra_preimage f (\bigcup_i (F i)). Proof. -move=> mF; rewrite /g_sigma_algebra_mapping /preimage_set_system/=. +move=> mF; rewrite /g_sigma_algebra_preimage /preimage_set_system/=. pose g := fun i => sval (cid2 (mF i)). pose mg := fun i => svalP (cid2 (mF i)). exists (\bigcup_i g i). @@ -1229,17 +1229,17 @@ rewrite setTI /g preimage_bigcup; apply: eq_bigcupr => k _. by case: (mg k) => _; rewrite setTI. Qed. -HB.instance Definition _ := Pointed.on (g_sigma_algebra_mappingType f). +HB.instance Definition _ := Pointed.on (g_sigma_algebra_preimageType f). -HB.instance Definition _ := @isMeasurable.Build (mapping_display f) - (g_sigma_algebra_mappingType f) (g_sigma_algebra_mapping f) - mapping_set0 mapping_setC mapping_bigcup. +HB.instance Definition _ := @isMeasurable.Build (preimage_display f) + (g_sigma_algebra_preimageType f) (g_sigma_algebra_preimage f) + preimage_set0 preimage_setC preimage_bigcup. -End mapping_generated_sigma_algebra. +End preimage_generated_sigma_algebra. -Notation "f .-mapping" := (mapping_display f) : measure_display_scope. -Notation "f .-mapping.-measurable" := - (measurable : set (set (g_sigma_algebra_mappingType f))) : classical_set_scope. +Notation "f .-preimage" := (preimage_display f) : measure_display_scope. +Notation "f .-preimage.-measurable" := + (measurable : set (set (g_sigma_algebra_preimageType f))) : classical_set_scope. Section independent_RVs. Context {R : realType} d d' (T : measurableType d) (T' : measurableType d'). @@ -1247,7 +1247,7 @@ Variable P : probability T R. Definition independent_RVs (I0 : choiceType) (I : set I0) (X : I0 -> {mfun T >-> T'}) : Prop := - mutual_independence P I (fun i => g_sigma_algebra_mapping (X i)). + mutual_independence P I (fun i => g_sigma_algebra_preimage (X i)). Definition independent_RVs2 (X Y : {mfun T >-> T'}) := independent_RVs [set: bool] [eta (fun=> cst point) with false |-> X, true |-> Y]. @@ -1259,17 +1259,17 @@ Context d {T : measurableType d} {R : realType}. Lemma g_sigma_algebra_mapping_comp (X : {mfun T >-> R}) (f : R -> R) : measurable_fun setT f -> - g_sigma_algebra_mapping (f \o X)%R `<=` g_sigma_algebra_mapping X. + g_sigma_algebra_preimage (f \o X)%R `<=` g_sigma_algebra_preimage X. Proof. exact: preimage_set_system_compS. Qed. Lemma g_sigma_algebra_mapping_funrpos (X : {mfun T >-> R}) : - g_sigma_algebra_mapping X^\+%R `<=` d.-measurable. + g_sigma_algebra_preimage X^\+%R `<=` d.-measurable. Proof. by move=> A/= -[B mB] <-; have := measurable_funrpos (measurable_funP X); exact. Qed. Lemma g_sigma_algebra_mapping_funrneg (X : {mfun T >-> R}) : - g_sigma_algebra_mapping X^\-%R `<=` d.-measurable. + g_sigma_algebra_preimage X^\-%R `<=` d.-measurable. Proof. by move=> A/= -[B mB] <-; have := measurable_funrneg (measurable_funP X); exact. Qed. @@ -1287,9 +1287,9 @@ Lemma independent_RVs2_comp (X Y : {RV P >-> R}) (f g : {mfun R >-> R}) : Proof. move=> indeXY; split => /=. - move=> [] _ /= A. - + by rewrite /g_sigma_algebra_mapping/= /preimage_set_system/= => -[B mB <-]; + + by rewrite /g_sigma_algebra_preimage/= /preimage_set_system/= => -[B mB <-]; exact/measurableT_comp. - + by rewrite /g_sigma_algebra_mapping/= /preimage_set_system/= => -[B mB <-]; + + by rewrite /g_sigma_algebra_preimage/= /preimage_set_system/= => -[B mB <-]; exact/measurableT_comp. - move=> J _ E JE. apply indeXY => //= i iJ; have := JE _ iJ. @@ -1498,23 +1498,23 @@ pose AY := dyadic_approx setT (EFin \o Y). pose BX := integer_approx setT (EFin \o X). pose BY := integer_approx setT (EFin \o Y). have mA (Z : {RV P >-> R}) m k : (k < m * 2 ^ m)%N -> - g_sigma_algebra_mapping Z (dyadic_approx setT (EFin \o Z) m k). - move=> mk; rewrite /g_sigma_algebra_mapping /dyadic_approx mk setTI. + g_sigma_algebra_preimage Z (dyadic_approx setT (EFin \o Z) m k). + move=> mk; rewrite /g_sigma_algebra_preimage /dyadic_approx mk setTI. rewrite /preimage_set_system/=; exists [set` dyadic_itv R m k] => //. rewrite setTI/=; apply/seteqP; split => z/=. by rewrite inE/= => Zz; exists (Z z). by rewrite inE/= => -[r rmk] [<-]. have mB (Z : {RV P >-> R}) k : - g_sigma_algebra_mapping Z (integer_approx setT (EFin \o Z) k). - rewrite /g_sigma_algebra_mapping /integer_approx setTI /preimage_set_system/=. + g_sigma_algebra_preimage Z (integer_approx setT (EFin \o Z) k). + rewrite /g_sigma_algebra_preimage /integer_approx setTI /preimage_set_system/=. by exists `[k%:R, +oo[%classic => //; rewrite setTI preimage_itvcy. have m1A (Z : {RV P >-> R}) : forall k, (k < n * 2 ^ n)%N -> measurable_fun setT - (\1_(dyadic_approx setT (EFin \o Z) n k) : g_sigma_algebra_mappingType Z -> R). + (\1_(dyadic_approx setT (EFin \o Z) n k) : g_sigma_algebra_preimageType Z -> R). move=> k kn. - exact/(@measurable_indicP _ (g_sigma_algebra_mappingType Z))/mA. + exact/(@measurable_indicP _ (g_sigma_algebra_preimageType Z))/mA. rewrite !inE => /orP[|]/eqP->{i} //=. - have : @measurable_fun _ _ (g_sigma_algebra_mappingType X) _ setT (X_ n). + have : @measurable_fun _ _ (g_sigma_algebra_preimageType X) _ setT (X_ n). rewrite nnsfun_approxE//. apply: measurable_funD => //=. apply: measurable_sum => //= k'; apply: measurable_funM => //. @@ -1523,7 +1523,7 @@ rewrite !inE => /orP[|]/eqP->{i} //=. by apply: measurable_indic; exact: mB. rewrite /measurable_fun => /(_ measurableT _ (measurable_set1 x)). by rewrite setTI. -have : @measurable_fun _ _ (g_sigma_algebra_mappingType Y) _ setT (Y_ n). +have : @measurable_fun _ _ (g_sigma_algebra_preimageType Y) _ setT (Y_ n). rewrite nnsfun_approxE//. apply: measurable_funD => //=. apply: measurable_sum => //= k'; apply: measurable_funM => //. From 96b15370fd7febdb233b9205268dd45aa65fdd6a Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Wed, 30 Apr 2025 15:49:23 +0900 Subject: [PATCH 05/10] rebase and fix - fix changelog - mv defs to appropriate files --- CHANGELOG_UNRELEASED.md | 104 +----------------- experimental_reals/discrete.v | 2 +- .../measure_theory/measurable_structure.v | 71 +++++++++++- theories/probability.v | 58 ---------- 4 files changed, 71 insertions(+), 164 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 5c26a33f18..8f56fa9795 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -164,16 +164,9 @@ `derivable_oy_continuousW`, `derivable_Nyo_continuousWoo`, `derivable_Nyo_continuousW` -- in `probability.v`: - + lemmas `eq_bernoulli`, `eq_bernoulliV2` -- file `mathcomp_extra.v` - + lemmas `ge_trunc`, `lt_succ_trunc`, `trunc_ge_nat`, `trunc_lt_nat` - -- file `Rstruct.v` - + lemma `Pos_to_natE` (from `mathcomp_extra.v`) - + lemmas `RabsE`, `RdistE`, `sum_f_R0E`, `factE` -- new file `internal_Eqdep_dec.v` (don't use, internal, to be removed) +- in `measurable_function.v`: + + lemma `preimage_set_system_compS` - in `numfun.v`: + defintions `funrpos`, `funrneg` with notations `^\+` and `^\-` @@ -183,9 +176,8 @@ `funrD_posD`, `funrpos_le`, `funrneg_le` + lemmas `funerpos`, `funerneg` -- in `measure.v`: - + lemma `preimage_class_comp` - + defintions `preimage_display`, `g_sigma_algebra_preimageType`, `g_sigma_algebra_preimage`, +- in `measurable_structure.v`: + + definitions `preimage_display`, `g_sigma_algebra_preimageType`, `g_sigma_algebra_preimage`, notations `.-preimage`, `.-preimage.-measurable` - in `measurable_realfun.v`: @@ -323,55 +315,6 @@ + `le_ereal_inf` -> `ereal_inf_le_tmp` + `lb_ereal_inf` -> `le_ereal_inf_tmp` + `ereal_sup_ge` -> `le_ereal_sup_tmp` -- in `kernel.v`: - + `isFiniteTransition` -> `isFiniteTransitionKernel` -- in `lebesgue_integral.v`: - + `fubini1a` -> `integrable12ltyP` - + `fubini1b` -> `integrable21ltyP` - + `measurable_funP` -> `measurable_funPT` (field of `isMeasurableFun` mixin) - -- in `mathcomp_extra.v` - + `comparable_min_le_min` -> `comparable_le_min2` - + `comparable_max_le_max` -> `comparable_le_max2` - + `min_le_min` -> `le_min2` - + `max_le_max` -> `le_max2` - + `real_sqrtC` -> `sqrtC_real` -- in `measure.v` - + `preimage_class` -> `preimage_set_system` - + `image_class` -> `image_set_system` - + `preimage_classes` -> `g_sigma_preimageU` - + `preimage_class_measurable_fun` -> `preimage_set_system_measurable_fun` - + `sigma_algebra_preimage_class` -> `sigma_algebra_preimage` - + `sigma_algebra_image_class` -> `sigma_algebra_image` - + `sigma_algebra_preimage_classE` -> `g_sigma_preimageE` - + `preimage_classes_comp` -> `g_sigma_preimageU_comp` - -### Renamed - -- in `lebesgue_measure.v`: - + `measurable_fun_indic` -> `measurable_indic` - + `emeasurable_fun_sum` -> `emeasurable_sum` - + `emeasurable_fun_fsum` -> `emeasurable_fsum` - + `ge0_emeasurable_fun_sum` -> `ge0_emeasurable_sum` -- in `probability.v`: - + `expectationM` -> `expectationZl` - -- in `classical_sets.v`: - + `preimage_itv_o_infty` -> `preimage_itvoy` - + `preimage_itv_c_infty` -> `preimage_itvcy` - + `preimage_itv_infty_o` -> `preimage_itvNyo` - + `preimage_itv_infty_c` -> `preimage_itvNyc` - -- in `constructive_ereal.v`: - + `maxeMr` -> `maxe_pMr` - + `maxeMl` -> `maxe_pMl` - + `mineMr` -> `mine_pMr` - + `mineMl` -> `mine_pMl` - -- in `probability.v`: - + `integral_distribution` -> `ge0_integral_distribution` - -- file `homotopy_theory/path.v` -> `homotopy_theory/continuous_path.v` ### Generalized @@ -458,45 +401,6 @@ + lemma `interval_set1` (use `set_itv1` instead) - in `ereal.v`: + notation `ereal_sup_le` (was deprecated since 1.11.0) -- file `mathcomp_extra.v` - + lemma `Pos_to_natE` (moved to `Rstruct.v`) - + lemma `deg_le2_ge0` (available as `deg_le2_poly_ge0` in `ssrnum.v` - since MathComp 2.1.0) -- in `sequences.v`: - + notations `nneseries_pred0`, `eq_nneseries`, `nneseries0`, - `ereal_cvgPpinfty`, `ereal_cvgPninfty` (were deprecated since 0.6.0) -- in `topology_structure.v`: - + lemma `closureC` - -- in file `lebesgue_integral.v`: - + lemma `approximation` - -### Removed - -- in `lebesgue_integral.v`: - + definition `cst_mfun` - + lemma `mfun_cst` - -- in `cardinality.v`: - + lemma `cst_fimfun_subproof` - -- in `lebesgue_integral.v`: - + lemma `cst_mfun_subproof` (use lemma `measurable_cst` instead) - + lemma `cst_nnfun_subproof` (turned into a `Let`) - + lemma `indic_mfun_subproof` (use lemma `measurable_fun_indic` instead) - -- in `lebesgue_integral.v`: - + lemma `measurable_indic` (was uselessly specializing `measurable_fun_indic` (now `measurable_indic`) from `lebesgue_measure.v`) - + notation `measurable_fun_indic` (deprecation since 0.6.3) -- in `constructive_ereal.v` - + notation `lee_opp` (deprecated since 0.6.5) - + notation `lte_opp` (deprecated since 0.6.5) -- in `measure.v`: - + `dynkin_setI_bigsetI` (use `big_ind` instead) - -- in `lebesgue_measurable.v`: - + notation `measurable_fun_power_pos` (deprecated since 0.6.3) - + notation `measurable_power_pos` (deprecated since 0.6.4) ### Infrastructure diff --git a/experimental_reals/discrete.v b/experimental_reals/discrete.v index 412877a07b..63ca0e73b8 100644 --- a/experimental_reals/discrete.v +++ b/experimental_reals/discrete.v @@ -4,7 +4,7 @@ (* Copyright (c) - 2016--2018 - Polytechnique *) (* -------------------------------------------------------------------- *) -From Coq Require Setoid. +From Corelib Require Setoid. From HB Require Import structures. From mathcomp Require Import all_ssreflect all_algebra. From mathcomp.classical Require Import boolp. diff --git a/theories/measure_theory/measurable_structure.v b/theories/measure_theory/measurable_structure.v index d9196e229f..faeed5a702 100644 --- a/theories/measure_theory/measurable_structure.v +++ b/theories/measure_theory/measurable_structure.v @@ -90,11 +90,20 @@ From mathcomp Require Import ereal topology normedtype sequences. (* ## Other measure-theoretic definitions *) (* *) (* ``` *) -(* preimage_set_system D f G == set system of the preimages by f of sets in G *) -(* image_set_system D f G == set system of the sets with a preimage by f *) -(* in G *) -(* subset_sigma_subadditive mu == alternative predicate defining *) -(* sigma-subadditivity *) +(* preimage_set_system D f G == set system of the preimages by f of sets *) +(* in G *) +(* g_sigma_algebra_preimage f == sigma-algebra generated by the *) +(* function f *) +(* g_sigma_algebra_preimageType f == the measurableType corresponding to *) +(* g_sigma_algebra_preimage f *) +(* This is an HB alias. *) +(* f.-preimage.-measurable A == A is measurable for *) +(* g_sigma_algebra_preimage f *) +(* image_set_system D f G == set system of the sets with a preimage *) +(* by f in G *) +(* *) +(* subset_sigma_subadditive mu == alternative predicate defining *) +(* sigma-subadditivity *) (* ``` *) (* *) (* ## Product of measurable spaces *) @@ -1343,6 +1352,58 @@ case=> h0 hC hU; split; first by exists set0 => //; rewrite preimage_set0 setI0. exact: (mF' i).2. Qed. +Definition preimage_display {T T'} : (T -> T') -> measure_display. +Proof. exact. Qed. + +Definition g_sigma_algebra_preimageType d' (T : pointedType) + (T' : measurableType d') (f : T -> T') : Type := T. + +Definition g_sigma_algebra_preimage d' (T : pointedType) + (T' : measurableType d') (f : T -> T') := + preimage_set_system setT f (@measurable _ T'). + +Section preimage_generated_sigma_algebra. +Context {d'} (T : pointedType) (T' : measurableType d'). +Variable f : T -> T'. + +Let preimage_set0 : g_sigma_algebra_preimage f set0. +Proof. +rewrite /g_sigma_algebra_preimage /preimage_set_system/=. +by exists set0 => //; rewrite preimage_set0 setI0. +Qed. + +Let preimage_setC A : + g_sigma_algebra_preimage f A -> g_sigma_algebra_preimage f (~` A). +Proof. +rewrite /g_sigma_algebra_preimage /preimage_set_system/= => -[B mB] <-{A}. +by exists (~` B); [exact: measurableC|rewrite !setTI preimage_setC]. +Qed. + +Let preimage_bigcup (F : (set T)^nat) : + (forall i, g_sigma_algebra_preimage f (F i)) -> + g_sigma_algebra_preimage f (\bigcup_i (F i)). +Proof. +move=> mF; rewrite /g_sigma_algebra_preimage /preimage_set_system/=. +pose g := fun i => sval (cid2 (mF i)). +pose mg := fun i => svalP (cid2 (mF i)). +exists (\bigcup_i g i). + by apply: bigcup_measurable => k; case: (mg k). +rewrite setTI /g preimage_bigcup; apply: eq_bigcupr => k _. +by case: (mg k) => _; rewrite setTI. +Qed. + +HB.instance Definition _ := Pointed.on (g_sigma_algebra_preimageType f). + +HB.instance Definition _ := @isMeasurable.Build (preimage_display f) + (g_sigma_algebra_preimageType f) (g_sigma_algebra_preimage f) + preimage_set0 preimage_setC preimage_bigcup. + +End preimage_generated_sigma_algebra. + +Notation "f .-preimage" := (preimage_display f) : measure_display_scope. +Notation "f .-preimage.-measurable" := + (measurable : set (set (g_sigma_algebra_preimageType f))) : classical_set_scope. + Definition image_set_system (aT rT : Type) (D : set aT) (f : aT -> rT) (G : set (set aT)) : set (set rT) := [set B : set rT | G (D `&` f @^-1` B)]. diff --git a/theories/probability.v b/theories/probability.v index f9105f7653..2c2c7bbb2d 100644 --- a/theories/probability.v +++ b/theories/probability.v @@ -1183,64 +1183,6 @@ Definition mutual_independence (I0 : choiceType) (I : set I0) End mutual_independence. -(* g_sigma_algebra_preimage f == sigma-algebra generated by the function f *) -(* g_sigma_algebra_preimageType f == the measurableType corresponding to *) -(* g_sigma_algebra_preimage f *) -(* This is an HB alias. *) -(* f.-preimage.-measurable A == A is measurable for g_sigma_algebra_preimage f *) - -Definition preimage_display {T T'} : (T -> T') -> measure_display. -Proof. exact. Qed. - -Definition g_sigma_algebra_preimageType d' (T : pointedType) - (T' : measurableType d') (f : T -> T') : Type := T. - -Definition g_sigma_algebra_preimage d' (T : pointedType) - (T' : measurableType d') (f : T -> T') := - preimage_set_system setT f (@measurable _ T'). - -Section preimage_generated_sigma_algebra. -Context {d'} (T : pointedType) (T' : measurableType d'). -Variable f : T -> T'. - -Let preimage_set0 : g_sigma_algebra_preimage f set0. -Proof. -rewrite /g_sigma_algebra_preimage /preimage_set_system/=. -by exists set0 => //; rewrite preimage_set0 setI0. -Qed. - -Let preimage_setC A : - g_sigma_algebra_preimage f A -> g_sigma_algebra_preimage f (~` A). -Proof. -rewrite /g_sigma_algebra_preimage /preimage_set_system/= => -[B mB] <-{A}. -by exists (~` B); [exact: measurableC|rewrite !setTI preimage_setC]. -Qed. - -Let preimage_bigcup (F : (set T)^nat) : - (forall i, g_sigma_algebra_preimage f (F i)) -> - g_sigma_algebra_preimage f (\bigcup_i (F i)). -Proof. -move=> mF; rewrite /g_sigma_algebra_preimage /preimage_set_system/=. -pose g := fun i => sval (cid2 (mF i)). -pose mg := fun i => svalP (cid2 (mF i)). -exists (\bigcup_i g i). - by apply: bigcup_measurable => k; case: (mg k). -rewrite setTI /g preimage_bigcup; apply: eq_bigcupr => k _. -by case: (mg k) => _; rewrite setTI. -Qed. - -HB.instance Definition _ := Pointed.on (g_sigma_algebra_preimageType f). - -HB.instance Definition _ := @isMeasurable.Build (preimage_display f) - (g_sigma_algebra_preimageType f) (g_sigma_algebra_preimage f) - preimage_set0 preimage_setC preimage_bigcup. - -End preimage_generated_sigma_algebra. - -Notation "f .-preimage" := (preimage_display f) : measure_display_scope. -Notation "f .-preimage.-measurable" := - (measurable : set (set (g_sigma_algebra_preimageType f))) : classical_set_scope. - Section independent_RVs. Context {R : realType} d d' (T : measurableType d) (T' : measurableType d'). Variable P : probability T R. From d311bbd52f8df8c006c99e9766d3dd2537458232 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Wed, 31 Dec 2025 19:36:33 +0900 Subject: [PATCH 06/10] rebase, rm warnings --- theories/independence.v | 13 ++++++------- theories/probability.v | 1 - 2 files changed, 6 insertions(+), 8 deletions(-) diff --git a/theories/independence.v b/theories/independence.v index 07c86ed445..65ae6066fe 100644 --- a/theories/independence.v +++ b/theories/independence.v @@ -1,4 +1,4 @@ -(* mathcomp analysis (c) 2022 Inria and AIST. License: CeCILL-C. *) +(* mathcomp analysis (c) 2025 Inria and AIST. License: CeCILL-C. *) From mathcomp Require Import all_ssreflect interval_inference. From mathcomp Require Import ssralg poly ssrnum ssrint interval finmap. From mathcomp Require Import mathcomp_extra boolp classical_sets functions. @@ -678,7 +678,7 @@ Definition pairRV (X Y : {RV P >-> T'}) : T * T -> T' * T' := Lemma pairM (X Y : {RV P >-> T'}) : measurable_fun setT (pairRV X Y). Proof. rewrite /pairRV. -apply/prod_measurable_funP; split => //=. +apply/measurable_fun_pairP; split => //=. rewrite (_ : (fst \o (fun x : T * T => (X x.1, Y x.2))) = (fun x => X x.1))//. by apply/measurableT_comp => //=. rewrite (_ : (snd \o (fun x : T * T => (X x.1, Y x.2))) = (fun x => Y x.2))//. @@ -808,10 +808,10 @@ rewrite [ltLHS](_ : _ = \int[distribution P X]_x `|x|%:E * rewrite ge0_integral_distribution//=; last exact/measurable_EFinP. rewrite ge0_integral_distribution//=; last exact/measurable_EFinP. rewrite lte_mul_pinfty//. - by apply: integral_ge0 => //. - apply: integral_fune_fin_num => //=. - by move/integrable_abse : iX => //. -apply: integral_fune_lt_pinfty => //. + exact: integral_ge0. + apply: integrable_fin_num => //=. + by move/integrable_abse : iX. +apply: integrable_lty => //. by move/integrable_abse : iY => //. Qed. @@ -1010,7 +1010,6 @@ apply: (@le_lt_trans _ _ 'E_P[(@normr _ _ \o X) * (@normr _ _ \o Y)]). by move/Lfun1_integrable : iY => /measurable_int/measurable_EFinP. apply: ge0_le_integral => //=. - by apply/measurable_EFinP; exact/measurableT_comp. - - by move=> x _; rewrite lee_fin/= mulr_ge0/=. - by apply/measurable_EFinP; apply/measurable_funM; exact/measurableT_comp. - by move=> t _; rewrite lee_fin/= normrM. rewrite expectationM_ge0//=. diff --git a/theories/probability.v b/theories/probability.v index 2c2c7bbb2d..147ad69bd0 100644 --- a/theories/probability.v +++ b/theories/probability.v @@ -1490,7 +1490,6 @@ apply: (@le_lt_trans _ _ 'E_P[(@normr _ _ \o X) * (@normr _ _ \o Y)]). by move/Lfun1_integrable : iY => /measurable_int. apply: ge0_le_integral => //=. - by apply/measurable_EFinP; exact/measurableT_comp. - - by move=> x _; rewrite lee_fin/= mulr_ge0/=. - by apply/measurable_EFinP; apply/measurable_funM; exact/measurableT_comp. - by move=> t _; rewrite lee_fin/= normrM. rewrite expectationM_ge0//=. From b6c474c3e4364aac96b861644dfb42700740aa1a Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Mon, 5 Jan 2026 18:59:21 +0900 Subject: [PATCH 07/10] fix changelog --- CHANGELOG_UNRELEASED.md | 75 ----------------------------------------- 1 file changed, 75 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 8f56fa9795..071caf4a5b 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -103,67 +103,6 @@ - in `lebesgue_integrable.v`: + lemma `integrable_set0` -- in `probability.v`: - + definition `ccdf` - + lemmas `lebesgue_stieltjes_cdf_id`, `cdf_ccdf_1`, `ccdf_nonincreasing`, `cvg_ccdfy0`, `cvg_ccdfNy1`, `ccdf_right_continuous`, `ge0_expectation_ccdf` - + corollaries `ccdf_cdf_1`, `ccdf_1_cdf`, `cdf_1_ccdf` - -- in `num_normedtype.v`: - + lemma `nbhs_infty_gtr` -- in `function_spaces.v`: - + lemmas `cvg_big`, `continuous_big` - -- in `realfun.v`: - + lemma `cvg_addrl_Ny` - -- in `constructive_ereal.v`: - + lemmas `mule_natr`, `dmule_natr` - + lemmas `inve_eqy`, `inve_eqNy` - -- in `uniform_structure.v`: - + lemma `continuous_injective_withinNx` - -- in `constructive_ereal.v`: - + variants `Ione`, `Idummy_placeholder` - + inductives `Inatmul`, `IEFin` - + definition `parse`, `print` - + number notations in scopes `ereal_dual_scope` and `ereal_scope` - + notation `- 1` in scopes `ereal_dual_scope` and `ereal_scope` -- in `pseudometric_normed_Zmodule.v`: - + lemma `le0_ball0` -- in `theories/landau.v`: - + lemma `littleoE0` - -- in `constructive_ereal.v`: - + lemma `lt0_adde` - -- in `unstable.v` - + lemmas `coprime_prodr`, `Gauss_dvd_prod`, `expn_prod`, `mono_leq_infl`, - `card_big_setU` - -- file `pnt.v` - + definitions `next_prime`, `prime_seq` - + lemmas `leq_prime_seq`, `mem_prime_seq` - + theorem `dvg_sum_inv_prime_seq` -- new directory `theories/measure_theory` with new files: - + `measurable_structure.v` - + `measure_function.v` - + `counting_measure.v` - + `dirac_measure.v` - + `probability_measure.v` - + `measure_negligible.v` - + `measure_extension.v` - + `measurable_function.v` - + `measure.v` - -- in `realfun.v`: - + lemmas `derivable_oy_continuous_within_itvcy`, - `derivable_oy_continuous_within_itvNyc` - + lemmas `derivable_oo_continuousW`, - `derivable_oy_continuousWoo`, - `derivable_oy_continuousW`, - `derivable_Nyo_continuousWoo`, - `derivable_Nyo_continuousW` - in `measurable_function.v`: + lemma `preimage_set_system_compS` @@ -303,18 +242,6 @@ - in `charge.v`: + `induced` -> `induced_charge` -- in `reals.v`: - + `sup_le_ub` -> `ge_sub` - + `le_inf` -> `inf_le` - + `le_sup` -> `sup_le` - + `sup_ubound` -> `ub_le_sup` - + `inf_lbound` -> `ge_inf` - + `ub_ereal_sup` -> `ge_ereal_sup` - + `ereal_inf_le` -> `ge_ereal_inf` - + `le_ereal_sup` -> `ereal_sup_le` - + `le_ereal_inf` -> `ereal_inf_le_tmp` - + `lb_ereal_inf` -> `le_ereal_inf_tmp` - + `ereal_sup_ge` -> `le_ereal_sup_tmp` ### Generalized @@ -399,8 +326,6 @@ - in `set_interval.v`: + lemma `interval_set1` (use `set_itv1` instead) -- in `ereal.v`: - + notation `ereal_sup_le` (was deprecated since 1.11.0) ### Infrastructure From 65bcc24e29fa1277b932aeaad5a96cd8271f5f6f Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Mon, 5 Jan 2026 19:01:02 +0900 Subject: [PATCH 08/10] fix changelog --- CHANGELOG_UNRELEASED.md | 50 +++++------------------------------------ 1 file changed, 6 insertions(+), 44 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 071caf4a5b..d38f6e7b3c 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -104,6 +104,12 @@ - in `lebesgue_integrable.v`: + lemma `integrable_set0` +- in `lebesgue_integrable.v`: + + lemma `integrable_norm` +- in `order_topology.v`: + + structures `POrderedNbhs`, `POrderedTopological`, `POrderedUniform`, `POrderedPseudoMetric`, + `POrderedPointedTopological` + - in `measurable_function.v`: + lemma `preimage_set_system_compS` @@ -136,50 +142,6 @@ + lemma `expectationM_ge0`, `integrable_expectationM`, `independent_integrableM`, ` expectation_prod` -- in `numfun.v` - + lemmas `funeposE`, `funenegE`, `funepos_comp`, `funeneg_comp` - -- in `classical_sets.v`: - + lemmas `xsectionE`, `ysectionE` - -- file `constructive_ereal.v`: - + definition `iter_mule` - + lemma `prodEFin` - -- file `exp.v`: - + lemma `expR_sum` - -- file `lebesgue_integral.v`: - + lemma `measurable_fun_le` - -- in `trigo.v`: - + lemma `integral0oo_atan` - -- in `measure.v`: - + lemmas `mnormalize_id`, `measurable_fun_eqP` - -- in `ftc.v`: - + lemma `integrable_locally` - -- in `constructive_ereal.v`: - + lemma `EFin_bigmax` - -- in `mathcomp_extra.v`: - + lemmas `inr_inj`, `inl_inj` - -- in `classical_sets.v`: - + lemmas `in_set1`, `inr_in_set_inr`, `inl_in_set_inr`, `mem_image`, `mem_range`, `image_f` - + lemmas `inr_in_set_inl`, `inl_in_set_inl` - -- in `lebesgue_integral_approximation.v`: - + lemma `measurable_prod` - -- in `lebesgue_integrable.v`: - + lemma `integrable_norm` -- in `order_topology.v`: - + structures `POrderedNbhs`, `POrderedTopological`, `POrderedUniform`, `POrderedPseudoMetric`, - `POrderedPointedTopological` - ### Changed - in `charge.v`: From d998efb077ff353c082f4afdd19a294e5f4440c9 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Tue, 6 Jan 2026 13:10:48 +0900 Subject: [PATCH 09/10] rm duplicates and clean --- CHANGELOG_UNRELEASED.md | 29 ++- theories/independence.v | 424 ++++++++++++------------------------ theories/probability.v | 461 ---------------------------------------- 3 files changed, 159 insertions(+), 755 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index d38f6e7b3c..a4c77c6613 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -122,25 +122,40 @@ + lemmas `funerpos`, `funerneg` - in `measurable_structure.v`: - + definitions `preimage_display`, `g_sigma_algebra_preimageType`, `g_sigma_algebra_preimage`, - notations `.-preimage`, `.-preimage.-measurable` + + definitions `preimage_display`, `g_sigma_algebra_preimageType`, + `g_sigma_algebra_preimage` + + notations `.-preimage`, `.-preimage.-measurable` - in `measurable_realfun.v`: + lemmas `measurable_funrpos`, `measurable_funrneg` - new file `independence.v`: - + lemma `expectationM_ge0` + definition `independent_events` + definition `mutual_independence` - + definition `independent_RVs` - + definition `independent_RVs2` + + lemma `eq_mutual_independence` + + definition `independence2`, `independence2P` + + lemmas `setI_closed_setT`, `setI_closed_set0` + + lemma `g_sigma_algebra_finite_measure_unique` + + lemma `mutual_independence_fset` + + lemma `mutual_independence_finiteS` + + theorem `mutual_independence_finite_g_sigma` + + lemma `mutual_dependence_bigcup` + lemmas `g_sigma_algebra_preimage_comp`, `g_sigma_algebra_preimage_funrpos`, `g_sigma_algebra_preimage_funrneg` + + definition `independent_RVs` + + lemma `independent_RVsD1` + + theorem `independent_generators` + + definition `independent_RVs2` + lemmas `independent_RVs2_comp`, `independent_RVs2_funrposneg`, `independent_RVs2_funrnegpos`, `independent_RVs2_funrnegneg`, `independent_RVs2_funrpospos` - + lemma `expectationM_ge0`, `integrable_expectationM`, `independent_integrableM`, - ` expectation_prod` + + definition `pairRV`, lemma `measurable_pairRV` + + lemmas `independent_RVs2_product_measure1` + + lemmas `independent_RVs2_setI_preimage`, + `independent_Lfun1_expectation_product_measure_lty` + + lemmas `expectationM_nnsfun`, `expectationM_ge0`, + `ge0_independent_expectationM`, `independent_Lfun1_expectationM_lty`, + `independent_Lfun1M`, `independent_expectationM` ### Changed diff --git a/theories/independence.v b/theories/independence.v index 65ae6066fe..329368d0dc 100644 --- a/theories/independence.v +++ b/theories/independence.v @@ -1,4 +1,4 @@ -(* mathcomp analysis (c) 2025 Inria and AIST. License: CeCILL-C. *) +(* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C. *) From mathcomp Require Import all_ssreflect interval_inference. From mathcomp Require Import ssralg poly ssrnum ssrint interval finmap. From mathcomp Require Import mathcomp_extra boolp classical_sets functions. @@ -14,10 +14,11 @@ From mathcomp Require Import hoelder. (* # Independence *) (* *) (* ``` *) -(* independent_events I F == the events F indexed by I are independent *) -(* mutual_independence I F == the set systems F indexed by I are independent *) -(* independent_RVs I X == the random variables X indexed by I are independent *) -(* independent_RVs2 X Y == the random variables X and Y are independent *) +(* independent_events I F == the events F indexed by I are independent *) +(* mutual_independence I F == the set systems F indexed by I are independent *) +(* independent_RVs I X == the random variables X indexed by I are *) +(* independent *) +(* independent_RVs2 X Y == the random variables X and Y are independent *) (* ``` *) (* *) (******************************************************************************) @@ -49,10 +50,6 @@ Context {R : realType} d {T : measurableType d} (P : probability T R) {I0 : choiceType}. Local Open Scope ereal_scope. -Definition g_sigma_family (I : set I0) (F : I0 -> set_system T) - : set_system T := - <>. - Definition mutual_independence (I : set I0) (F : I0 -> set_system T) := (forall i, I i -> F i `<=` measurable) /\ forall J : {fset I0}, [set` J] `<=` I -> @@ -75,11 +72,11 @@ Section independence. Context {R : realType} d {T : measurableType d} (P : probability T R). Local Open Scope ereal_scope. -Definition independence (F G : set_system T) := +Definition independence2 (F G : set_system T) := [/\ F `<=` measurable , G `<=` measurable & forall A B, A \in F -> B \in G -> P (A `&` B) = P A * P B]. -Lemma independenceP (F G : set_system T) : independence F G <-> +Lemma independence2P (F G : set_system T) : independence2 F G <-> mutual_independence P [set: bool] (fun b => if b then F else G). Proof. split=> [[mF mG FG]|/= indeF]. @@ -139,26 +136,6 @@ move=> IF=> C D [FC|/= ->{C}]. by rewrite !set0I; right. Qed. -Lemma setI_closed_set0' T (F : set_system T) : - F set0 -> - setI_closed (F `|` [set set0]) -> setI_closed F. -Proof. -move=> F0 IF C D FC FD. -have [//|/= ->//] : (F `|` [set set0]) (C `&` D). -by apply: IF; left. -Qed. - -Lemma g_sigma_setU d {T : measurableType d} (F : set_system T) A : - <> A -> - <> = @measurable _ T -> - <> = <>. -Proof. -move=> FA sFT; apply/seteqP; split=> [B|B]. - by apply: sub_sigma_algebra2; exact: subsetUl. -apply: smallest_sub => // C [FC|/= ->//]. -exact: sub_gen_smallest. -Qed. - Lemma g_sigma_algebra_finite_measure_unique {d} {T : measurableType d} {R : realType} (G : set_system T) : G `<=` d.-measurable -> @@ -181,35 +158,6 @@ apply: (@g_sigma_algebra_measure_unique _ _ _ by apply: sub_gen_smallest; left. Qed. -(*Section lem142b. -Context d {T : measurableType d} {R : realType}. -Variable mu : {finite_measure set T -> \bar R}. -Variable F : set_system T. -Hypothesis setI_closed_F : setI_closed F. (* pi-system *) -Hypothesis FT : F `<=` @measurable _ T. -Hypothesis sFT : <> = @measurable _ T. - -Lemma lem142b : forall nu : {finite_measure set T -> \bar R}, - (mu setT = nu setT) -> - (forall E, F E -> nu E = mu E) -> - forall A, measurable A -> mu A = nu A. -Proof. -move=> nu munu numu A mA. -apply: (measure_unique (F `|` [set setT]) (fun=> setT)) => //. -- rewrite -sFT; apply: g_sigma_setU => //. - by rewrite sFT. -- exact: setI_closed_setT. -- by move=> n /=; right. -- by rewrite bigcup_const. -- move=> E [/numu //|/= ->]. - by rewrite munu. -- move=> n. - apply: fin_num_fun_lty. - exact: fin_num_measure. -Qed. - -End lem142b.*) - Section mutual_independence_properties. Context {R : realType} d {T : measurableType d} (P : probability T R). Local Open Scope ereal_scope. @@ -518,14 +466,19 @@ Definition independent_RVs (I : set I0) End independent_RVs. -Section independent_RVs2. +Section independent_RVs_properties. Context {R : realType} d d' (T : measurableType d) (T' : measurableType d'). Variable P : probability T R. -Definition independent_RVs2 (X Y : {mfun T >-> T'}) := - independent_RVs P [set: bool] (fun b => if b then Y else X). +Lemma independent_RVsD1 (I : {fset nat}) i0 (X : {RV P >-> T'}^nat) : + independent_RVs P [set` I] X -> independent_RVs P [set` (I `\ i0)%fset] X. +Proof. +move=> PIX; split => [/= i|/= J JIi0 E EK]. + by rewrite !inE => /andP[ii0 iI]; exact: PIX.1. +by apply: PIX.2 => //= x /JIi0 /=; rewrite !inE => /andP[]. +Qed. -End independent_RVs2. +End independent_RVs_properties. Section independent_generators. Context {R : realType} d (T : measurableType d). @@ -551,12 +504,14 @@ have closed_preimage i : I i -> setI_closed (preimage_set_system setT (X i) (F i - exact/mem_set. - by rewrite setTI. have gen_preimage i : I i -> - <> = g_sigma_algebra_preimage (X i). + <> = + g_sigma_algebra_preimage (X i). move=> Ii. rewrite /g_sigma_algebra_preimage AsF; last exact/mem_set. by rewrite -g_sigma_preimageE. rewrite /independent_RVs. -suff: mutual_independence P I (fun i => <>). +suff: mutual_independence P I + (fun i => <>). exact: eq_mutual_independence. apply: (mutual_independence_finite_g_sigma _ _).1. - by move=> i Ii; apply: setI_closed_set0; exact/closed_preimage/set_mem. @@ -567,7 +522,16 @@ Qed. End independent_generators. -Section independent_RVs_lemmas. +Section independent_RVs2. +Context {R : realType} d d' (T : measurableType d) (T' : measurableType d'). +Variable P : probability T R. + +Definition independent_RVs2 (X Y : {mfun T >-> T'}) := + independent_RVs P [set: bool] (fun b => if b then Y else X). + +End independent_RVs2. + +Section independent_RVs2_properties. Context {R : realType} d d' (T : measurableType d) (T' : measurableType d'). Variable P : probability T R. Local Open Scope ring_scope. @@ -643,30 +607,7 @@ move=> indeXY; split=> [/= [|]//= _ |J J2 E JE]. exact: measurable_funrpos. Qed. -End independent_RVs_lemmas. - -Definition preimage_classes I0 (I : set I0) (d_ : forall i : I, measure_display) - (T_ : forall k : I, semiRingOfSetsType (d_ k)) (T : Type) - (f_ : forall k : I, T -> T_ k) := - <>. -Arguments preimage_classes {I0} I d_ T_ {T} f_. - -Lemma measurable_prod d [T : measurableType d] [R : realType] [D : set T] [I : eqType] - (s : seq I) [h : I -> T -> R] : - (forall i, i \in s -> measurable_fun D (h i)) -> - measurable_fun D (fun x => (\prod_(i <- s) h i x)%R). -Proof. -elim: s => [mh|x y ih mh]. - under eq_fun do rewrite big_nil//=. - exact: measurable_cst. -under eq_fun do rewrite big_cons//=. -apply: measurable_funM => //. - apply: mh. - by rewrite mem_head. -apply: ih => n ny. -apply: mh. -by rewrite inE orbC ny. -Qed. +End independent_RVs2_properties. Section pairRV. Context d d' {T : measurableType d} {T' : measurableType d'} {R : realType} @@ -675,132 +616,90 @@ Context d d' {T : measurableType d} {T' : measurableType d'} {R : realType} Definition pairRV (X Y : {RV P >-> T'}) : T * T -> T' * T' := (fun x => (X x.1, Y x.2)). -Lemma pairM (X Y : {RV P >-> T'}) : measurable_fun setT (pairRV X Y). +Lemma measurable_pairM (X Y : {RV P >-> T'}) : measurable_fun setT (pairRV X Y). Proof. rewrite /pairRV. apply/measurable_fun_pairP; split => //=. - rewrite (_ : (fst \o (fun x : T * T => (X x.1, Y x.2))) = (fun x => X x.1))//. - by apply/measurableT_comp => //=. -rewrite (_ : (snd \o (fun x : T * T => (X x.1, Y x.2))) = (fun x => Y x.2))//. -by apply/measurableT_comp => //=. +- rewrite [X in measurable_fun _ X](_ : _ = X \o fst)//. + exact/measurableT_comp. +- rewrite [X in measurable_fun _ X](_ : _ = Y \o snd)//. + exact/measurableT_comp. Qed. HB.instance Definition _ (X Y : {RV P >-> T'}) := - @isMeasurableFun.Build _ _ _ _ (pairRV X Y) (pairM X Y). + @isMeasurableFun.Build _ _ _ _ (pairRV X Y) (measurable_pairM X Y). End pairRV. -Section product_expectation. +Section independent_RVs2_properties_realType. Context {R : realType} d (T : measurableType d). Variable P : probability T R. Local Open Scope ereal_scope. -Let mu := @lebesgue_measure R. - -Let mprod_m (X Y : {RV P >-> R}) (A1 : set R) (A2 : set R) : +Lemma independent_RVs2_setI_preimage (X Y : {mfun T >-> R}) (A1 A2 : set R) : measurable A1 -> measurable A2 -> - (distribution P X \x distribution P Y) (A1 `*` A2) = - ((distribution P X) A1 * (distribution P Y) A2)%E. -Proof. -move=> mA1 mA2. -etransitivity. - by apply: product_measure1E. -rewrite /=. -done. -Qed. - -Lemma tmp0 (X Y : {RV P >-> R}) (B1 B2 : set R) : - measurable B1 -> measurable B2 -> independent_RVs2 P X Y -> - P (X @^-1` B1 `&` Y @^-1` B2) = P (X @^-1` B1) * P (Y @^-1` B2). + P (X @^-1` A1 `&` Y @^-1` A2) = P (X @^-1` A1) * P (Y @^-1` A2). Proof. -move=> mB1 mB2. +move=> mA1 mA2. rewrite /independent_RVs2 /independent_RVs /mutual_independence /= => -[_]. move/(_ [fset false; true]%fset (@subsetT _ _) - (fun b => if b then Y @^-1` B2 else X @^-1` B1)). + (fun b => if b then Y @^-1` A2 else X @^-1` A1)). rewrite !big_fsetU1 ?inE//= !big_seq_fset1/=. apply => -[|] /= _; rewrite !inE; rewrite /g_sigma_algebra_preimage. -by exists B2 => //; rewrite setTI. -by exists B1 => //; rewrite setTI. +by exists A2 => //; rewrite setTI. +by exists A1 => //; rewrite setTI. Qed. -Lemma tmp1 (X Y : {RV P >-> R}) (B1 B2 : set R) : - measurable B1 -> measurable B2 -> +Lemma independent_RVs2_product_measure1 (X Y : {RV P >-> R}) (A1 A2 : set R) : + measurable A1 -> measurable A2 -> independent_RVs2 P X Y -> - P (X @^-1` B1 `&` Y @^-1` B2) = (P \x P) (pairRV X Y @^-1` (B1 `*` B2)). -Proof. -move=> mB1 mB2 XY. -rewrite (_ : ((fun x : T * T => (X x.1, Y x.2)) @^-1` (B1 `*` B2)) = - (X @^-1` B1) `*` (Y @^-1` B2)); last first. - by apply/seteqP; split => [[x1 x2]|[x1 x2]]//. -rewrite product_measure1E; last 2 first. - rewrite -[_ @^-1` _]setTI. - by apply: (measurable_funP X). - rewrite -[_ @^-1` _]setTI. - by apply: (measurable_funP Y). -by rewrite tmp0//. -Qed. - -Let phi (x : R * R) := (x.1 * x.2)%R. -Let mphi : measurable_fun setT phi. + (P \x P) (pairRV X Y @^-1` (A1 `*` A2)) = P (X @^-1` A1 `&` Y @^-1` A2). Proof. -rewrite /= /phi. -by apply: measurable_funM. +move=> mA1 mA2 iPXY. +rewrite (_ : (pairRV X Y @^-1` (A1 `*` A2)) = + (X @^-1` A1) `*` (Y @^-1` A2)); last first. + by apply/seteqP; split => [[x1 x2]|[x1 x2]]. +rewrite product_measure1E. +- by rewrite independent_RVs2_setI_preimage. +- by rewrite -[_ @^-1` _]setTI; exact: (measurable_funP X). +- by rewrite -[_ @^-1` _]setTI; exact: (measurable_funP Y). Qed. -Lemma PP : (P \x P) setT = 1. -Proof. -rewrite /product_measure1 /=. -rewrite /xsection/=. -under eq_integral. - move=> t _. - rewrite (_ : [set y | (t, y) \in [set: T * T]] = setT); last first. - apply/seteqP; split => [x|x]// _ /=. - by rewrite in_setT. - rewrite probability_setT. - over. -rewrite integral_cst // mul1e. -apply: probability_setT. -Qed. +End independent_RVs2_properties_realType. -HB.instance Definition _ := @Measure_isProbability.Build _ _ R (P \x P) PP. +Section product_expectation_over_product_measure. +Context {R : realType} d (T : measurableType d). +Variable P : probability T R. +Local Open Scope ereal_scope. -Lemma integrable_expectationM (X Y : {RV P >-> R}) : +Lemma independent_Lfun1_expectation_product_measure_lty (X Y : {RV P >-> R}) : independent_RVs2 P X Y -> - P.-integrable setT (EFin \o X) -> P.-integrable setT (EFin \o Y) -> - 'E_(P \x P) [(fun x => `|X x.1 * Y x.2|)%R] < +oo -(* `|'E_(P) [(fun x => X x * Y x)%R]| < +oo *) . + (X : _ -> _) \in Lfun P 1 -> (Y : _ -> _) \in Lfun P 1 -> + 'E_(P \x P) [(fun x => `|X x.1 * Y x.2|)%R] < +oo. Proof. move=> indeXY iX iY. -(*apply: (@le_lt_trans _ _ 'E_(P \x P)[(fun x => `|(X x.1 * Y x.2)|%R)] - (* 'E_(P)[(fun x => `|(X x * Y x)|%R)] *) ). - rewrite unlock/=. - rewrite (le_trans (le_abse_integral _ _ _))//. - apply/measurable_EFinP/measurable_funM. - by apply/measurableT_comp => //. - by apply/measurableT_comp => //.*) rewrite unlock. rewrite [ltLHS](_ : _ = \int[distribution (P \x P) (pairRV X Y)%R]_x `|x.1 * x.2|%:E); last first. rewrite ge0_integral_distribution//=; last first. apply/measurable_EFinP => //=. - by apply/measurableT_comp => //=. + by apply/measurableT_comp => //=; exact/measurable_funM. rewrite [ltLHS](_ : _ = \int[distribution P X \x distribution P Y]_x `|x.1 * x.2|%:E); last first. apply: eq_measure_integral => // A mA _. - apply/esym. + apply/esym. (* NB: don't simpl here! *) apply: product_measure_unique => //= A1 A2 mA1 mA2. - rewrite /pushforward/=. - rewrite -tmp1//. - by rewrite tmp0//. + by rewrite independent_RVs2_product_measure1// independent_RVs2_setI_preimage. rewrite fubini_tonelli1//=; last first. - by apply/measurable_EFinP => /=; apply/measurableT_comp => //=. -rewrite /fubini_F/= -/mu. + apply/measurable_EFinP => /=; apply/measurableT_comp => //=. + exact/measurable_funM. +rewrite /fubini_F/=. rewrite [ltLHS](_ : _ = \int[distribution P X]_x `|x|%:E * \int[distribution P Y]_y `|y|%:E); last first. rewrite -ge0_integralZr//=; last 2 first. exact/measurable_EFinP. - by apply: integral_ge0 => //. + exact: integral_ge0. apply: eq_integral => x _. rewrite -ge0_integralZl//=. by under eq_integral do rewrite normrM. @@ -808,14 +707,14 @@ rewrite [ltLHS](_ : _ = \int[distribution P X]_x `|x|%:E * rewrite ge0_integral_distribution//=; last exact/measurable_EFinP. rewrite ge0_integral_distribution//=; last exact/measurable_EFinP. rewrite lte_mul_pinfty//. - exact: integral_ge0. - apply: integrable_fin_num => //=. - by move/integrable_abse : iX. -apply: integrable_lty => //. -by move/integrable_abse : iY => //. +- exact: integral_ge0. +- apply: integrable_fin_num => //=. + by move/Lfun1_integrable : iX => /integrable_abse. +- apply: integrable_lty => //. + by move/Lfun1_integrable : iY => /integrable_abse. Qed. -End product_expectation. +End product_expectation_over_product_measure. Section product_expectation. Context {R : realType} d (T : measurableType d). @@ -824,7 +723,7 @@ Local Open Scope ereal_scope. Import HBNNSimple. -Let expectationM_nnsfun (f g : {nnsfun T >-> R}) : +Lemma expectationM_nnsfun (f g : {nnsfun T >-> R}) : (forall y y', y \in range f -> y' \in range g -> P (f @^-1` [set y] `&` g @^-1` [set y']) = P (f @^-1` [set y]) * P (g @^-1` [set y'])) -> @@ -901,7 +800,7 @@ rewrite ge0_integral_fsum//; last 2 first. by apply: eq_fsbigr => y fy; rewrite -integralZl//; exact/integrable_indic. Qed. -Lemma expectationM_ge0 (X Y : {RV P >-> R}) : +Lemma ge0_independent_expectationM (X Y : {RV P >-> R}) : independent_RVs2 P X Y -> 'E_P[X] *? 'E_P[Y] -> (forall t, 0 <= X t)%R -> (forall t, 0 <= Y t)%R -> @@ -976,7 +875,7 @@ have m1A (Z : {RV P >-> R}) : forall k, (k < n * 2 ^ n)%N -> move=> k kn. exact/(@measurable_indicP _ (g_sigma_algebra_preimageType Z))/mA. rewrite !inE => /orP[|]/eqP->{i} //=. - have : @measurable_fun _ _ (g_sigma_algebra_preimageType X) _ setT (X_ n). +- have : @measurable_fun _ _ (g_sigma_algebra_preimageType X) _ setT (X_ n). rewrite nnsfun_approxE//. apply: measurable_funD => //=. apply: measurable_sum => //= k'; apply: measurable_funM => //. @@ -985,26 +884,25 @@ rewrite !inE => /orP[|]/eqP->{i} //=. by apply: measurable_indic; exact: mB. rewrite /measurable_fun => /(_ measurableT _ (measurable_set1 x)). by rewrite setTI. -have : @measurable_fun _ _ (g_sigma_algebra_preimageType Y) _ setT (Y_ n). - rewrite nnsfun_approxE//. - apply: measurable_funD => //=. - apply: measurable_sum => //= k'; apply: measurable_funM => //. - by apply: measurable_indic; exact: mA. - apply: measurable_funM => //. - by apply: measurable_indic; exact: mB. -move=> /(_ measurableT [set y] (measurable_set1 y)). -by rewrite setTI. +- have : @measurable_fun _ _ (g_sigma_algebra_preimageType Y) _ setT (Y_ n). + rewrite nnsfun_approxE//. + apply: measurable_funD => //=. + apply: measurable_sum => //= k'; apply: measurable_funM => //. + by apply: measurable_indic; exact: mA. + apply: measurable_funM => //. + by apply: measurable_indic; exact: mB. + move=> /(_ measurableT [set y] (measurable_set1 y)). + by rewrite setTI. Qed. -Lemma integrable_expectationM000 (X Y : {RV P >-> R}) : +Lemma independent_Lfun1_expectationM_lty (X Y : {RV P >-> R}) : independent_RVs2 P X Y -> (X : _ -> _) \in Lfun P 1 -> (Y : _ -> _) \in Lfun P 1 -> `|'E_P [X * Y]| < +oo. Proof. move=> indeXY iX iY. apply: (@le_lt_trans _ _ 'E_P[(@normr _ _ \o X) * (@normr _ _ \o Y)]). - rewrite unlock/=. - rewrite (le_trans (le_abse_integral _ _ _))//. + rewrite unlock/= (le_trans (le_abse_integral _ _ _))//. apply/measurable_EFinP/measurable_funM. by move/Lfun1_integrable : iX => /measurable_int/measurable_EFinP. by move/Lfun1_integrable : iY => /measurable_int/measurable_EFinP. @@ -1012,13 +910,12 @@ apply: (@le_lt_trans _ _ 'E_P[(@normr _ _ \o X) * (@normr _ _ \o Y)]). - by apply/measurable_EFinP; exact/measurableT_comp. - by apply/measurable_EFinP; apply/measurable_funM; exact/measurableT_comp. - by move=> t _; rewrite lee_fin/= normrM. -rewrite expectationM_ge0//=. +rewrite ge0_independent_expectationM//=. - rewrite lte_mul_pinfty//. + by rewrite expectation_ge0/=. + rewrite expectation_fin_num//=. by move: iX => /Lfun_norm. - + move : iY => /Lfun1_integrable. - move=> /integrableP[_]. + + move : iY => /Lfun1_integrable/integrableP[_]. by rewrite unlock. - exact: independent_RVs2_comp. - apply: mule_def_fin; rewrite unlock integrable_fin_num//. @@ -1026,7 +923,7 @@ rewrite expectationM_ge0//=. + by move/Lfun_norm : iY => /Lfun1_integrable. Qed. -Lemma independent_integrableM (X Y : {RV P >-> R}) : +Lemma independent_Lfun1M (X Y : {RV P >-> R}) : independent_RVs2 P X Y -> (X : _ -> _) \in Lfun P 1 -> (Y : _ -> _) \in Lfun P 1 -> (X \* Y)%R \in Lfun P 1. @@ -1036,16 +933,13 @@ apply/Lfun1_integrable. apply/integrableP; split => //. move/Lfun1_integrable : iX => /integrableP[iX _]. move/Lfun1_integrable : iY => /integrableP[iY _]. - apply/measurable_EFinP. - by apply/measurable_funM; apply/measurable_EFinP. -have := integrable_expectationM000 indeXY iX iY. -rewrite unlock => /abse_integralP. -apply => //. + exact/measurable_EFinP/measurable_funM/measurable_EFinP. +have := independent_Lfun1_expectationM_lty indeXY iX iY. +rewrite unlock => /abse_integralP; apply => //. exact/measurable_EFinP/measurable_funM. Qed. -(* TODO: rename to expectationM when deprecation is removed *) -Lemma expectation_mul (X Y : {RV P >-> R}) : +Lemma independent_expectationM (X Y : {RV P >-> R}) : independent_RVs2 P X Y -> (X : _ -> _) \in Lfun P 1 -> (Y : _ -> _) \in Lfun P 1 -> 'E_P [X * Y] = 'E_P [X] * 'E_P [Y]. @@ -1055,105 +949,61 @@ transitivity ('E_P[(X^\+ - X^\-) * (Y^\+ - Y^\-)]). congr ('E_P[_]). apply/funext => /=t. by rewrite [in LHS](funrposneg X)/= [in LHS](funrposneg Y). -have ? : P.-integrable [set: T] (EFin \o X^\-%R). - rewrite -funerneg; apply/integrable_funeneg => //. +have ? : X^\-%R \in Lfun P 1. + apply/Lfun1_integrable; rewrite -funerneg; apply/integrable_funeneg => //. + exact/Lfun1_integrable. +have ? : X^\-%R \in Lfun P 1. + apply/Lfun1_integrable; rewrite -funerneg; apply/integrable_funeneg => //. exact/Lfun1_integrable. -have ? : P.-integrable [set: T] (EFin \o X^\+%R). - rewrite -funerpos; apply/integrable_funepos => //. +have ? : X^\+%R \in Lfun P 1. + apply/Lfun1_integrable; rewrite -funerpos; apply/integrable_funepos => //. exact/Lfun1_integrable. -have ? : P.-integrable [set: T] (EFin \o Y^\+%R). - rewrite -funerpos; apply/integrable_funepos => //. +have ? : Y^\+%R \in Lfun P 1. + apply/Lfun1_integrable; rewrite -funerpos; apply/integrable_funepos => //. exact/Lfun1_integrable. -have ? : P.-integrable [set: T] (EFin \o Y^\-%R). - rewrite -funerneg; apply/integrable_funeneg => //. +have ? : Y^\-%R \in Lfun P 1. + apply/Lfun1_integrable; rewrite -funerneg; apply/integrable_funeneg => //. exact/Lfun1_integrable. -have ? : P.-integrable [set: T] (EFin \o (X^\+ \* Y^\+)%R). - apply/Lfun1_integrable. - apply: independent_integrableM => //=. - exact: independent_RVs2_funrpospos. - by apply/Lfun1_integrable. - by apply/Lfun1_integrable. -have ? : P.-integrable [set: T] (EFin \o (X^\- \* Y^\+)%R). - apply/Lfun1_integrable. - apply: independent_integrableM => //=. - exact: independent_RVs2_funrnegpos. - by apply/Lfun1_integrable. - by apply/Lfun1_integrable. -have ? : P.-integrable [set: T] (EFin \o (X^\+ \* Y^\-)%R). - apply/Lfun1_integrable. - apply: independent_integrableM => //=. - exact: independent_RVs2_funrposneg. - by apply/Lfun1_integrable. - by apply/Lfun1_integrable. -have ? : P.-integrable [set: T] (EFin \o (X^\- \* Y^\-)%R). - apply/Lfun1_integrable. - apply: independent_integrableM => //=. - exact: independent_RVs2_funrnegneg. - by apply/Lfun1_integrable. - by apply/Lfun1_integrable. +have ? : (X^\+ \* Y^\+)%R \in Lfun P 1. + by apply: independent_Lfun1M => //=; exact: independent_RVs2_funrpospos. +have ? : (X^\- \* Y^\+)%R \in Lfun P 1. + by apply: independent_Lfun1M => //=; exact: independent_RVs2_funrnegpos. +have ? : (X^\+ \* Y^\-)%R \in Lfun P 1. + by apply: independent_Lfun1M => //=; exact: independent_RVs2_funrposneg. +have ? : (X^\- \* Y^\-)%R \in Lfun P 1. + by apply: independent_Lfun1M => //=; exact: independent_RVs2_funrnegneg. transitivity ('E_P[X^\+ * Y^\+] - 'E_P[X^\- * Y^\+] - 'E_P[X^\+ * Y^\-] + 'E_P[X^\- * Y^\-]). - rewrite mulrDr !mulrDl -expectationB//=; [|exact/Lfun1_integrable..]. - rewrite -expectationB//=; last 2 first. - by rewrite rpredB//; exact/Lfun1_integrable. - exact/Lfun1_integrable. - rewrite -expectationD//=; last 2 first. - rewrite rpredB//; last exact/Lfun1_integrable. - by rewrite rpredB//; exact/Lfun1_integrable. - exact/Lfun1_integrable. + rewrite mulrDr !mulrDl -!expectationB//=; last by rewrite rpredB. + rewrite -expectationD//=; last by rewrite !rpredB. congr ('E_P[_]); apply/funext => t/=. - by rewrite !fctE !(mulNr,mulrN,opprK,addrA)/=. -rewrite [in LHS]expectationM_ge0//=; last 2 first. + by rewrite !fctE !(mulNr,mulrN,opprK,addrA). +rewrite [in LHS]ge0_independent_expectationM//=; last 2 first. exact: independent_RVs2_funrpospos. - by rewrite mule_def_fin// expectation_fin_num//; exact/Lfun1_integrable. -rewrite [in LHS]expectationM_ge0//=; last 2 first. + by rewrite mule_def_fin// expectation_fin_num. +rewrite [in LHS]ge0_independent_expectationM//=; last 2 first. exact: independent_RVs2_funrnegpos. - by rewrite mule_def_fin// expectation_fin_num//; exact/Lfun1_integrable. -rewrite [in LHS]expectationM_ge0//=; last 2 first. + by rewrite mule_def_fin// expectation_fin_num. +rewrite [in LHS]ge0_independent_expectationM//=; last 2 first. exact: independent_RVs2_funrposneg. - by rewrite mule_def_fin// expectation_fin_num//; exact/Lfun1_integrable. -rewrite [in LHS]expectationM_ge0//=; last 2 first. + by rewrite mule_def_fin// expectation_fin_num. +rewrite [in LHS]ge0_independent_expectationM//=; last 2 first. exact: independent_RVs2_funrnegneg. - by rewrite mule_def_fin// expectation_fin_num//=; exact/Lfun1_integrable. + by rewrite mule_def_fin// expectation_fin_num. transitivity ('E_P[X^\+ - X^\-] * 'E_P[Y^\+ - Y^\-]). rewrite -addeA -addeACA -muleBr; last 2 first. - by rewrite expectation_fin_num//; exact/Lfun1_integrable. - by rewrite fin_num_adde_defr// expectation_fin_num//; exact/Lfun1_integrable. + by rewrite expectation_fin_num. + by rewrite fin_num_adde_defr// expectation_fin_num. rewrite -oppeB; last first. - by rewrite fin_num_adde_defr// fin_numM// expectation_fin_num//; exact/Lfun1_integrable. + by rewrite fin_num_adde_defr// fin_numM// expectation_fin_num. rewrite -muleBr; last 2 first. - by rewrite expectation_fin_num//; exact/Lfun1_integrable. - by rewrite fin_num_adde_defr// expectation_fin_num//; exact/Lfun1_integrable. - rewrite -muleBl; last 2 first. - by rewrite fin_numB// !expectation_fin_num//; exact/Lfun1_integrable. - by rewrite fin_num_adde_defr// expectation_fin_num//; exact/Lfun1_integrable. - rewrite -expectationB//=; [|exact/Lfun1_integrable..]. - by rewrite -expectationB//; exact/Lfun1_integrable. + by rewrite expectation_fin_num. + by rewrite fin_num_adde_defr// expectation_fin_num. + rewrite -muleBl. + - by rewrite -!expectationB. + - by rewrite fin_numB// !expectation_fin_num. + - by rewrite fin_num_adde_defr// expectation_fin_num. by congr *%E; congr ('E_P[_]); rewrite [RHS]funrposneg. Qed. -Lemma prodE (s : seq nat) (X : {RV P >-> R}^nat) (t : T) : - (\prod_(i <- s) X i t)%R = ((\prod_(j <- s) X j)%R t). -Proof. -by elim/big_ind2 : _ => //= {}X x {}Y y -> ->. -Qed. - -Lemma set_cons2 (I : eqType) (x y : I) : [set` [:: x; y]] = [set x ; y]. -Proof. -apply/seteqP; split => z /=; rewrite !inE. - move=> /orP[|] /eqP ->; auto. -by move=> [|] ->; rewrite eqxx// orbT. -Qed. - -Lemma independent_RVsD1 (I : {fset nat}) i0 (X : {RV P >-> R}^nat) : - independent_RVs P [set` I] X -> independent_RVs P [set` (I `\ i0)%fset] X. -Proof. -move=> H. -split => [/= i|/= J JIi0 E EK]. - rewrite !inE => /andP[ii0 iI]. - by apply H. -apply H => //. -by move=> /= x /JIi0 /=; rewrite !inE => /andP[]. -Qed. - End product_expectation. diff --git a/theories/probability.v b/theories/probability.v index 147ad69bd0..ca1f83d4e5 100644 --- a/theories/probability.v +++ b/theories/probability.v @@ -45,10 +45,6 @@ From mathcomp Require Import charge ftc gauss_integral hoelder. (* ccdf X r == complementary cumulative distribution function of X *) (* := distribution P X `]r, +oo[ *) (* enum_prob X k == probability of the kth value in the range of X *) -(* independent_events I F == the events F indexed by I are independent *) -(* mutual_independence I F == the classes F indexed by I are independent *) -(* independent_RVs I X == the random variables X indexed by I are independent *) -(* independent_RVs2 X Y == the random variables X and Y are independent *) (* ``` *) (* *) (* ``` *) @@ -1156,463 +1152,6 @@ Qed. End discrete_distribution. -Section independent_events. -Context {R : realType} d {T : measurableType d}. -Variable P : probability T R. -Local Open Scope ereal_scope. - -Definition independent_events (I0 : choiceType) (I : set I0) (A : I0 -> set T) := - forall J : {fset I0}, [set` J] `<=` I -> - P (\bigcap_(i in [set` J]) A i) = \prod_(i <- J) P (A i). - -End independent_events. - -Section mutual_independence. -Context {R : realType} d {T : measurableType d}. -Variable P : probability T R. -Local Open Scope ereal_scope. - -Definition mutual_independence (I0 : choiceType) (I : set I0) - (F : I0 -> set (set T)) := - (forall i : I0, I i -> F i `<=` @measurable _ T) /\ - forall J : {fset I0}, - [set` J] `<=` I -> - forall E : I0 -> set T, - (forall i : I0, i \in J -> E i \in F i) -> - P (\big[setI/setT]_(j <- J) E j) = \prod_(j <- J) P (E j). - -End mutual_independence. - -Section independent_RVs. -Context {R : realType} d d' (T : measurableType d) (T' : measurableType d'). -Variable P : probability T R. - -Definition independent_RVs (I0 : choiceType) - (I : set I0) (X : I0 -> {mfun T >-> T'}) : Prop := - mutual_independence P I (fun i => g_sigma_algebra_preimage (X i)). - -Definition independent_RVs2 (X Y : {mfun T >-> T'}) := - independent_RVs [set: bool] [eta (fun=> cst point) with false |-> X, true |-> Y]. - -End independent_RVs. - -Section g_sigma_algebra_mapping_lemmas. -Context d {T : measurableType d} {R : realType}. - -Lemma g_sigma_algebra_mapping_comp (X : {mfun T >-> R}) (f : R -> R) : - measurable_fun setT f -> - g_sigma_algebra_preimage (f \o X)%R `<=` g_sigma_algebra_preimage X. -Proof. exact: preimage_set_system_compS. Qed. - -Lemma g_sigma_algebra_mapping_funrpos (X : {mfun T >-> R}) : - g_sigma_algebra_preimage X^\+%R `<=` d.-measurable. -Proof. -by move=> A/= -[B mB] <-; have := measurable_funrpos (measurable_funP X); exact. -Qed. - -Lemma g_sigma_algebra_mapping_funrneg (X : {mfun T >-> R}) : - g_sigma_algebra_preimage X^\-%R `<=` d.-measurable. -Proof. -by move=> A/= -[B mB] <-; have := measurable_funrneg (measurable_funP X); exact. -Qed. - -End g_sigma_algebra_mapping_lemmas. -Arguments g_sigma_algebra_mapping_comp {d T R X} f. - -Section independent_RVs_lemmas. -Context {R : realType} d d' (T : measurableType d) (T' : measurableType d'). -Variable P : probability T R. -Local Open Scope ring_scope. - -Lemma independent_RVs2_comp (X Y : {RV P >-> R}) (f g : {mfun R >-> R}) : - independent_RVs2 P X Y -> independent_RVs2 P (f \o X) (g \o Y). -Proof. -move=> indeXY; split => /=. -- move=> [] _ /= A. - + by rewrite /g_sigma_algebra_preimage/= /preimage_set_system/= => -[B mB <-]; - exact/measurableT_comp. - + by rewrite /g_sigma_algebra_preimage/= /preimage_set_system/= => -[B mB <-]; - exact/measurableT_comp. -- move=> J _ E JE. - apply indeXY => //= i iJ; have := JE _ iJ. - by move: i {iJ} =>[|]//=; rewrite !inE => Eg; - exact: g_sigma_algebra_mapping_comp Eg. -Qed. - -Lemma independent_RVs2_funrposneg (X Y : {RV P >-> R}) : - independent_RVs2 P X Y -> independent_RVs2 P X^\+ Y^\-. -Proof. -move=> indeXY; split=> [[|]/= _|J J2 E JE]. -- exact: g_sigma_algebra_mapping_funrneg. -- exact: g_sigma_algebra_mapping_funrpos. -- apply indeXY => //= i iJ; have := JE _ iJ. - move/J2 : iJ; move: i => [|]// _; rewrite !inE. - + apply: (g_sigma_algebra_mapping_comp (fun x => maxr (- x) 0)%R). - exact: measurable_funrneg. - + apply: (g_sigma_algebra_mapping_comp (fun x => maxr x 0)%R) => //. - exact: measurable_funrpos. -Qed. - -Lemma independent_RVs2_funrnegpos (X Y : {RV P >-> R}) : - independent_RVs2 P X Y -> independent_RVs2 P X^\- Y^\+. -Proof. -move=> indeXY; split=> [/= [|]// _ |J J2 E JE]. -- exact: g_sigma_algebra_mapping_funrpos. -- exact: g_sigma_algebra_mapping_funrneg. -- apply indeXY => //= i iJ; have := JE _ iJ. - move/J2 : iJ; move: i => [|]// _; rewrite !inE. - + apply: (g_sigma_algebra_mapping_comp (fun x => maxr x 0)%R). - exact: measurable_funrpos. - + apply: (g_sigma_algebra_mapping_comp (fun x => maxr (- x) 0)%R). - exact: measurable_funrneg. -Qed. - -Lemma independent_RVs2_funrnegneg (X Y : {RV P >-> R}) : - independent_RVs2 P X Y -> independent_RVs2 P X^\- Y^\-. -Proof. -move=> indeXY; split=> [/= [|]// _ |J J2 E JE]. -- exact: g_sigma_algebra_mapping_funrneg. -- exact: g_sigma_algebra_mapping_funrneg. -- apply indeXY => //= i iJ; have := JE _ iJ. - move/J2 : iJ; move: i => [|]// _; rewrite !inE. - + apply: (g_sigma_algebra_mapping_comp (fun x => maxr (- x) 0)%R). - exact: measurable_funrneg. - + apply: (g_sigma_algebra_mapping_comp (fun x => maxr (- x) 0)%R). - exact: measurable_funrneg. -Qed. - -Lemma independent_RVs2_funrpospos (X Y : {RV P >-> R}) : - independent_RVs2 P X Y -> independent_RVs2 P X^\+ Y^\+. -Proof. -move=> indeXY; split=> [/= [|]//= _ |J J2 E JE]. -- exact: g_sigma_algebra_mapping_funrpos. -- exact: g_sigma_algebra_mapping_funrpos. -- apply indeXY => //= i iJ; have := JE _ iJ. - move/J2 : iJ; move: i => [|]// _; rewrite !inE. - + apply: (g_sigma_algebra_mapping_comp (fun x => maxr x 0)%R). - exact: measurable_funrpos. - + apply: (g_sigma_algebra_mapping_comp (fun x => maxr x 0)%R). - exact: measurable_funrpos. -Qed. - -End independent_RVs_lemmas. - -Section product_expectation. -Context {R : realType} d (T : measurableType d). -Variable P : probability T R. -Local Open Scope ereal_scope. - -Import HBNNSimple. - -Let expectationM_nnsfun (f g : {nnsfun T >-> R}) : - (forall y y', y \in range f -> y' \in range g -> - P (f @^-1` [set y] `&` g @^-1` [set y']) = - P (f @^-1` [set y]) * P (g @^-1` [set y'])) -> - 'E_P [f \* g] = 'E_P [f] * 'E_P [g]. -Proof. -move=> fg; transitivity - ('E_P [(fun x => (\sum_(y \in range f) y * \1_(f @^-1` [set y]) x)%R) - \* (fun x => (\sum_(y \in range g) y * \1_(g @^-1` [set y]) x)%R)]). - by congr ('E_P [_]); apply/funext => t/=; rewrite (fimfunE f) (fimfunE g). -transitivity ('E_P [(fun x => (\sum_(y \in range f) \sum_(y' \in range g) y * y' - * \1_(f @^-1` [set y] `&` g @^-1` [set y']) x)%R)]). - congr ('E_P [_]); apply/funext => t/=. - rewrite mulrC; rewrite fsbig_distrr//=. (* TODO: lemma fsbig_distrl *) - apply: eq_fsbigr => y yf; rewrite mulrC; rewrite fsbig_distrr//=. - by apply: eq_fsbigr => y' y'g; rewrite indicI mulrCA !mulrA (mulrC y'). -rewrite unlock. -under eq_integral do rewrite -fsumEFin//. -transitivity (\sum_(y \in range f) (\sum_(y' \in range g) - ((y * y')%:E * \int[P]_w (\1_(f @^-1` [set y] `&` g @^-1` [set y']) w)%:E))). - rewrite ge0_integral_fsum//=; last 2 first. - - move=> r; under eq_fun do rewrite -fsumEFin//. - apply: emeasurable_fsum => // s. - apply/measurable_EFinP/measurable_funM => //. - exact/measurable_indic/measurableI. - - move=> r t _; rewrite lee_fin sumr_ge0 // => s _; rewrite -lee_fin. - by rewrite indicI/= indicE -mulrACA EFinM mule_ge0// nnfun_muleindic_ge0. - apply: eq_fsbigr => y yf. - under eq_integral do rewrite -fsumEFin//. - rewrite ge0_integral_fsum//=; last 2 first. - - move=> r; apply/measurable_EFinP; apply: measurable_funM => //. - exact/measurable_indic/measurableI. - - move=> r t _. - by rewrite indicI/= indicE -mulrACA EFinM mule_ge0// nnfun_muleindic_ge0. - apply: eq_fsbigr => y' y'g. - under eq_integral do rewrite EFinM. - by rewrite integralZl//; exact/integrable_indic/measurableI. -transitivity (\sum_(y \in range f) (\sum_(y' \in range g) - ((y * y')%:E * (\int[P]_w (\1_(f @^-1` [set y]) w)%:E * - \int[P]_w (\1_(g @^-1` [set y']) w)%:E)))). - apply: eq_fsbigr => y fy; apply: eq_fsbigr => y' gy'; congr *%E. - transitivity ('E_P[\1_(f @^-1` [set y] `&` g @^-1` [set y'])]). - by rewrite unlock. - transitivity ('E_P[\1_(f @^-1` [set y])] * 'E_P[\1_(g @^-1` [set y'])]); - last by rewrite unlock. - rewrite expectation_indic//; last exact: measurableI. - by rewrite !expectation_indic// fg. -transitivity ( - (\sum_(y \in range f) (y%:E * (\int[P]_w (\1_(f @^-1` [set y]) w)%:E))) * - (\sum_(y' \in range g) (y'%:E * \int[P]_w (\1_(g @^-1` [set y']) w)%:E))). - transitivity (\sum_(y \in range f) (\sum_(y' \in range g) - (y'%:E * \int[P]_w (\1_(g @^-1` [set y']) w)%:E)%E)%R * - (y%:E * \int[P]_w (\1_(f @^-1` [set y]) w)%:E)%E%R); last first. - rewrite !fsbig_finite//= ge0_sume_distrl//; last first. - move=> r _; rewrite -integralZl//; last exact: integrable_indic. - by apply: integral_ge0 => t _; rewrite nnfun_muleindic_ge0. - by apply: eq_bigr => r _; rewrite muleC. - apply: eq_fsbigr => y fy. - rewrite !fsbig_finite//= ge0_sume_distrl//; last first. - move=> r _; rewrite -integralZl//; last exact: integrable_indic. - by apply: integral_ge0 => t _; rewrite nnfun_muleindic_ge0. - apply: eq_bigr => r _; rewrite (mulrC y) EFinM. - by rewrite [X in _ * X]muleC muleACA. -suff: forall h : {nnsfun T >-> R}, - (\sum_(y \in range h) (y%:E * \int[P]_w (\1_(h @^-1` [set y]) w)%:E)%E)%R - = \int[P]_w (h w)%:E. - by move=> suf; congr *%E; rewrite suf. -move=> h. -apply/esym. -under eq_integral do rewrite (fimfunE h). -under eq_integral do rewrite -fsumEFin//. -rewrite ge0_integral_fsum//; last 2 first. -- by move=> r; exact/measurable_EFinP/measurable_funM. -- by move=> r t _; rewrite lee_fin -lee_fin nnfun_muleindic_ge0. -by apply: eq_fsbigr => y fy; rewrite -integralZl//; exact/integrable_indic. -Qed. - -Lemma expectationM_ge0 (X Y : {RV P >-> R}) : - independent_RVs2 P X Y -> - 'E_P[X] *? 'E_P[Y] -> - (forall t, 0 <= X t)%R -> (forall t, 0 <= Y t)%R -> - 'E_P [X * Y] = 'E_P [X] * 'E_P [Y]. -Proof. -move=> indeXY defXY X0 Y0. -have mX : measurable_fun setT (EFin \o X) by exact/measurable_EFinP. -have mY : measurable_fun setT (EFin \o Y) by exact/measurable_EFinP. -pose X_ := nnsfun_approx measurableT mX. -pose Y_ := nnsfun_approx measurableT mY. -have EXY : 'E_P[X_ n \* Y_ n] @[n --> \oo] --> 'E_P [X * Y]. - rewrite unlock; have -> : \int[P]_w ((X * Y) w)%:E = - \int[P]_x limn (fun n => (EFin \o (X_ n \* Y_ n)%R) x). - apply: eq_integral => t _; apply/esym/cvg_lim => //=. - rewrite fctE EFinM; under eq_fun do rewrite EFinM. - by apply: cvgeM; [rewrite mule_def_fin//| - apply: cvg_nnsfun_approx => //= x _; rewrite lee_fin..]. - apply: cvg_monotone_convergence => //. - - by move=> n; apply/measurable_EFinP; exact: measurable_funM. - - by move=> n t _; rewrite lee_fin. - - move=> t _ m n mn. - by rewrite lee_fin/= ler_pM//; exact/lefP/nd_nnsfun_approx. -have EX : 'E_P[X_ n] @[n --> \oo] --> 'E_P [X]. - rewrite unlock. - have -> : \int[P]_w (X w)%:E = \int[P]_x limn (fun n => (EFin \o X_ n) x). - by apply: eq_integral => t _; apply/esym/cvg_lim => //=; - apply: cvg_nnsfun_approx => // x _; rewrite lee_fin. - apply: cvg_monotone_convergence => //. - - by move=> n; exact/measurable_EFinP. - - by move=> n t _; rewrite lee_fin. - - by move=> t _ m n mn; rewrite lee_fin/=; exact/lefP/nd_nnsfun_approx. -have EY : 'E_P[Y_ n] @[n --> \oo] --> 'E_P [Y]. - rewrite unlock. - have -> : \int[P]_w (Y w)%:E = \int[P]_x limn (fun n => (EFin \o Y_ n) x). - by apply: eq_integral => t _; apply/esym/cvg_lim => //=; - apply: cvg_nnsfun_approx => // x _; rewrite lee_fin. - apply: cvg_monotone_convergence => //. - - by move=> n; exact/measurable_EFinP. - - by move=> n t _; rewrite lee_fin. - - by move=> t _ m n mn; rewrite lee_fin/=; exact/lefP/nd_nnsfun_approx. -have {EX EY}EXY' : 'E_P[X_ n] * 'E_P[Y_ n] @[n --> \oo] --> 'E_P[X] * 'E_P[Y]. - apply: cvgeM => //. -suff : forall n, 'E_P[X_ n \* Y_ n] = 'E_P[X_ n] * 'E_P[Y_ n]. - by move=> suf; apply: (cvg_unique _ EXY) => //=; under eq_fun do rewrite suf. -move=> n; apply: expectationM_nnsfun => x y xX_ yY_. -suff : P (\big[setI/setT]_(j <- [fset false; true]%fset) - [eta fun=> set0 with 0%N |-> X_ n @^-1` [set x], - 1%N |-> Y_ n @^-1` [set y]] j) = - \prod_(j <- [fset false; true]%fset) - P ([eta fun=> set0 with 0%N |-> X_ n @^-1` [set x], - 1%N |-> Y_ n @^-1` [set y]] j). - by rewrite !big_fsetU1/= ?inE//= !big_seq_fset1/=. -move: indeXY => [/= _]; apply => // i. -pose AX := dyadic_approx setT (EFin \o X). -pose AY := dyadic_approx setT (EFin \o Y). -pose BX := integer_approx setT (EFin \o X). -pose BY := integer_approx setT (EFin \o Y). -have mA (Z : {RV P >-> R}) m k : (k < m * 2 ^ m)%N -> - g_sigma_algebra_preimage Z (dyadic_approx setT (EFin \o Z) m k). - move=> mk; rewrite /g_sigma_algebra_preimage /dyadic_approx mk setTI. - rewrite /preimage_set_system/=; exists [set` dyadic_itv R m k] => //. - rewrite setTI/=; apply/seteqP; split => z/=. - by rewrite inE/= => Zz; exists (Z z). - by rewrite inE/= => -[r rmk] [<-]. -have mB (Z : {RV P >-> R}) k : - g_sigma_algebra_preimage Z (integer_approx setT (EFin \o Z) k). - rewrite /g_sigma_algebra_preimage /integer_approx setTI /preimage_set_system/=. - by exists `[k%:R, +oo[%classic => //; rewrite setTI preimage_itvcy. -have m1A (Z : {RV P >-> R}) : forall k, (k < n * 2 ^ n)%N -> - measurable_fun setT - (\1_(dyadic_approx setT (EFin \o Z) n k) : g_sigma_algebra_preimageType Z -> R). - move=> k kn. - exact/(@measurable_indicP _ (g_sigma_algebra_preimageType Z))/mA. -rewrite !inE => /orP[|]/eqP->{i} //=. - have : @measurable_fun _ _ (g_sigma_algebra_preimageType X) _ setT (X_ n). - rewrite nnsfun_approxE//. - apply: measurable_funD => //=. - apply: measurable_sum => //= k'; apply: measurable_funM => //. - by apply: measurable_indic; exact: mA. - apply: measurable_funM => //. - by apply: measurable_indic; exact: mB. - rewrite /measurable_fun => /(_ measurableT _ (measurable_set1 x)). - by rewrite setTI. -have : @measurable_fun _ _ (g_sigma_algebra_preimageType Y) _ setT (Y_ n). - rewrite nnsfun_approxE//. - apply: measurable_funD => //=. - apply: measurable_sum => //= k'; apply: measurable_funM => //. - by apply: measurable_indic; exact: mA. - apply: measurable_funM => //. - by apply: measurable_indic; exact: mB. -move=> /(_ measurableT [set y] (measurable_set1 y)). -by rewrite setTI. -Qed. - -Lemma integrable_expectationM (X Y : {RV P >-> R}) : - independent_RVs2 P X Y -> - (X : T -> R) \in Lfun P 1 -> (Y : T -> R) \in Lfun P 1 -> - `|'E_P [X * Y]| < +oo. -Proof. -move=> indeXY iX iY. -apply: (@le_lt_trans _ _ 'E_P[(@normr _ _ \o X) * (@normr _ _ \o Y)]). - rewrite unlock/=. - rewrite (le_trans (le_abse_integral _ _ _))//. - apply/measurable_EFinP/measurable_funM. - by move/Lfun1_integrable : iX => /measurable_int. - by move/Lfun1_integrable : iY => /measurable_int. - apply: ge0_le_integral => //=. - - by apply/measurable_EFinP; exact/measurableT_comp. - - by apply/measurable_EFinP; apply/measurable_funM; exact/measurableT_comp. - - by move=> t _; rewrite lee_fin/= normrM. -rewrite expectationM_ge0//=. -- rewrite lte_mul_pinfty//. - + by rewrite expectation_ge0/=. - + rewrite expectation_fin_num//=. - exact: Lfun_norm. - move/Lfun_norm : iY => /expectation_fin_num. - by rewrite fin_numElt => /andP[_]. -- exact: independent_RVs2_comp. -- apply: mule_def_fin; rewrite unlock integrable_fin_num//. - + by move/Lfun_norm : iX => /Lfun1_integrable. - + by move/Lfun_norm : iY => /Lfun1_integrable. -Qed. - -Lemma independent_integrableM (X Y : {RV P >-> R}) : - independent_RVs2 P X Y -> - P.-integrable setT (EFin \o X) -> P.-integrable setT (EFin \o Y) -> - P.-integrable setT (EFin \o (X \* Y)%R). -Proof. -move=> indeXY iX iY. -apply/integrableP; split; first exact/measurable_EFinP/measurable_funM. -move/Lfun1_integrable in iX. -move/Lfun1_integrable in iY. -have := integrable_expectationM indeXY iX iY. -rewrite unlock => /abse_integralP; apply => //. -apply/measurable_EFinP. -by apply: measurable_funM. -Qed. - -(* TODO: rename to expectationM when deprecation is removed *) -Lemma expectation_prod (X Y : {RV P >-> R}) : - independent_RVs2 P X Y -> - (X : _ -> _) \in Lfun P 1 -> (Y : _ -> _) \in Lfun P 1 -> - 'E_P [X * Y] = 'E_P [X] * 'E_P [Y]. -Proof. -move=> XY iX iY. -transitivity ('E_P[(X^\+ - X^\-) * (Y^\+ - Y^\-)]). - congr ('E_P[_]). - apply/funext => /=t. - by rewrite [in LHS](funrposneg X)/= [in LHS](funrposneg Y). -have ? : P.-integrable [set: T] (EFin \o X^\-%R). - rewrite -funerneg; apply/integrable_funeneg => //. - exact/Lfun1_integrable. -have ? : P.-integrable [set: T] (EFin \o X^\+%R). - rewrite -funerpos; apply/integrable_funepos => //. - exact/Lfun1_integrable. -have ? : P.-integrable [set: T] (EFin \o Y^\+%R). - rewrite -funerpos; apply/integrable_funepos => //. - exact/Lfun1_integrable. -have ? : P.-integrable [set: T] (EFin \o Y^\-%R). - rewrite -funerneg; apply/integrable_funeneg => //. - exact/Lfun1_integrable. -have ? : P.-integrable [set: T] (EFin \o (X^\+ \* Y^\+)%R). - by apply: independent_integrableM => //=; exact: independent_RVs2_funrpospos. -have ? : P.-integrable [set: T] (EFin \o (X^\- \* Y^\+)%R). - by apply: independent_integrableM => //=; exact: independent_RVs2_funrnegpos. -have ? : P.-integrable [set: T] (EFin \o (X^\+ \* Y^\-)%R). - by apply: independent_integrableM => //=; exact: independent_RVs2_funrposneg. -have ? : P.-integrable [set: T] (EFin \o (X^\- \* Y^\-)%R). - by apply: independent_integrableM => //=; exact: independent_RVs2_funrnegneg. -transitivity ('E_P[X^\+ * Y^\+] - 'E_P[X^\- * Y^\+] - - 'E_P[X^\+ * Y^\-] + 'E_P[X^\- * Y^\-]). - rewrite mulrDr !mulrDl -expectationB//=; last 2 first. - exact/Lfun1_integrable. - exact/Lfun1_integrable. - rewrite -expectationB//; last 2 first. - rewrite rpredB//=. - exact/Lfun1_integrable. - exact/Lfun1_integrable. - exact/Lfun1_integrable. - rewrite -expectationD//=; last 2 first. - rewrite rpredB//=. - rewrite rpredB//=. - exact/Lfun1_integrable. - exact/Lfun1_integrable. - exact/Lfun1_integrable. - exact/Lfun1_integrable. - congr ('E_P[_]); apply/funext => t/=. - by rewrite !fctE !(mulNr,mulrN,opprK,addrA)/=. -rewrite [in LHS]expectationM_ge0//=; last 2 first. - exact: independent_RVs2_funrpospos. - rewrite mule_def_fin// expectation_fin_num//; exact/Lfun1_integrable. -rewrite [in LHS]expectationM_ge0//=; last 2 first. - exact: independent_RVs2_funrnegpos. - rewrite mule_def_fin// expectation_fin_num//; exact/Lfun1_integrable. -rewrite [in LHS]expectationM_ge0//=; last 2 first. - exact: independent_RVs2_funrposneg. - rewrite mule_def_fin// expectation_fin_num//; exact/Lfun1_integrable. -rewrite [in LHS]expectationM_ge0//=; last 2 first. - exact: independent_RVs2_funrnegneg. - rewrite mule_def_fin// expectation_fin_num//; exact/Lfun1_integrable. -transitivity ('E_P[X^\+ - X^\-] * 'E_P[Y^\+ - Y^\-]). - rewrite -addeA -addeACA -muleBr; last 2 first. - rewrite expectation_fin_num//; exact/Lfun1_integrable. - rewrite fin_num_adde_defr// expectation_fin_num//. - exact/Lfun1_integrable. - rewrite -oppeB; last first. - rewrite fin_num_adde_defr// fin_numM// expectation_fin_num//. - exact/Lfun1_integrable. - exact/Lfun1_integrable. - rewrite -muleBr; last 2 first. - rewrite expectation_fin_num//. - exact/Lfun1_integrable. - rewrite fin_num_adde_defr// expectation_fin_num//. - exact/Lfun1_integrable. - rewrite -muleBl; last 2 first. - rewrite fin_numB// !expectation_fin_num//. - exact/Lfun1_integrable. - exact/Lfun1_integrable. - rewrite fin_num_adde_defr// expectation_fin_num//. - exact/Lfun1_integrable. - rewrite -expectationB//=; last 2 first. - exact/Lfun1_integrable. - exact/Lfun1_integrable. - rewrite -expectationB//. - exact/Lfun1_integrable. - exact/Lfun1_integrable. -by congr *%E; congr ('E_P[_]); rewrite [RHS]funrposneg. -Qed. - -End product_expectation. - Section bernoulli_pmf. Context {R : realType} (p : R). Local Open Scope ring_scope. From a5018df1ff879f9b553edf01b925945aa6271777 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Tue, 6 Jan 2026 23:38:37 +0900 Subject: [PATCH 10/10] addressing comments --- CHANGELOG_UNRELEASED.md | 13 +++- classical/functions.v | 6 +- classical/unstable.v | 2 +- reals/constructive_ereal.v | 2 +- theories/charge.v | 6 +- theories/ereal.v | 11 +++- theories/esum.v | 28 ++++---- theories/independence.v | 8 +-- .../lebesgue_integrable.v | 36 +++++----- .../lebesgue_integral_dominated_convergence.v | 6 +- .../lebesgue_integral_fubini.v | 10 +-- .../lebesgue_integral_nonneg.v | 19 +++--- .../measurable_fun_approximation.v | 4 +- theories/measurable_realfun.v | 15 ++++- theories/measure_theory/measure_negligible.v | 15 +++-- theories/numfun.v | 65 ++++++------------- theories/probability.v | 20 +----- 17 files changed, 128 insertions(+), 138 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index a4c77c6613..dac6ec1835 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -117,7 +117,7 @@ + defintions `funrpos`, `funrneg` with notations `^\+` and `^\-` + lemmas `funrpos_ge0`, `funrneg_ge0`, `funrposN`, `funrnegN`, `ge0_funrposE`, `ge0_funrnegE`, `le0_funrposE`, `le0_funrnegE`, `ge0_funrposM`, `ge0_funrnegM`, - `le0_funrposM`, `le0_funrnegM`, `funr_normr`, `funrposneg`, `funrD_Dpos`, + `le0_funrposM`, `le0_funrnegM`, `funrposDneg`, `funrposBneg`, `funrD_posD`, `funrpos_le`, `funrneg_le` + lemmas `funerpos`, `funerneg` @@ -157,6 +157,12 @@ `ge0_independent_expectationM`, `independent_Lfun1_expectationM_lty`, `independent_Lfun1M`, `independent_expectationM` +- in `functions.v`: + + lemma `addBrfctE` + +- in `ereal.v`: + + lemma `ge0_addBefctE` + ### Changed - in `charge.v`: @@ -210,6 +216,11 @@ `bounded_variationN`, `bounded_variationl`, `bounded_variationr`, `variations_opp`, `nondecreasing_bounded_variation` +- in `numfun.v`: + + `fune_abse` renamed to `funeposDneg` and direction of the equality changed + + `funeposneg` renamed to `funeposBneg` and direction of the equality changed + + `funeD_posD` renamed to `funeDB` and direction of the equality changed + ### Renamed - in `probability.v`: diff --git a/classical/functions.v b/classical/functions.v index 9f5b894c34..823d4c8a82 100644 --- a/classical/functions.v +++ b/classical/functions.v @@ -1,4 +1,4 @@ -(* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C. *) +(* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C. *) From mathcomp Require Import all_ssreflect finmap ssralg ssrnum ssrint rat. From HB Require Import structures. From mathcomp Require Import mathcomp_extra unstable boolp classical_sets. @@ -2700,6 +2700,10 @@ Proof. by elim: n => [//|n h]; rewrite funeqE=> ?; rewrite !mulrSr h. Qed. Lemma opprfctE (T : Type) (K : zmodType) (f : T -> K) : - f = (fun x => - f x). Proof. by []. Qed. +Lemma addBrfctE (U : Type) (K : zmodType) : + @interchange (U -> K) (fun a b => a - b) (fun a b => a + b). +Proof. by move=> a b c d; apply/funext => x; rewrite addrACA -opprD. Qed. + Lemma mulrfctE (T : Type) (K : pzRingType) (f g : T -> K) : f * g = (fun x => f x * g x). Proof. by []. Qed. diff --git a/classical/unstable.v b/classical/unstable.v index b12853ecc9..b452fd14af 100644 --- a/classical/unstable.v +++ b/classical/unstable.v @@ -1,4 +1,4 @@ -(* mathcomp analysis (c) 2022 Inria and AIST. License: CeCILL-C. *) +(* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C. *) From mathcomp Require Import all_ssreflect finmap ssralg ssrnum ssrint. From mathcomp Require Import archimedean interval mathcomp_extra. diff --git a/reals/constructive_ereal.v b/reals/constructive_ereal.v index d9cd247e12..830b08c36a 100644 --- a/reals/constructive_ereal.v +++ b/reals/constructive_ereal.v @@ -1,4 +1,4 @@ -(* mathcomp analysis (c) 2025 Inria and AIST. License: CeCILL-C. *) +(* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C. *) (* -------------------------------------------------------------------- *) (* Copyright (c) - 2015--2016 - IMDEA Software Institute *) (* Copyright (c) - 2015--2018 - Inria *) diff --git a/theories/charge.v b/theories/charge.v index 2b4c9a09cc..83bc873e4f 100644 --- a/theories/charge.v +++ b/theories/charge.v @@ -1,4 +1,4 @@ -(* mathcomp analysis (c) 2025 Inria and AIST. License: CeCILL-C. *) +(* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C. *) From HB Require Import structures. From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint interval. From mathcomp Require Import finmap fingroup perm rat. @@ -2174,7 +2174,7 @@ Lemma Radon_Nikodym_change_of_variables f E : measurable E -> \int[mu]_(x in E) (f x * ('d (charge_of_finite_measure nu) '/d mu) x) = \int[nu]_(x in E) f x. Proof. -move=> mE mf; rewrite [in RHS](funeposneg f) integralB //; last 2 first. +move=> mE mf; rewrite -[in RHS](funeposBneg f) integralB //; last 2 first. - exact: integrable_funepos. - exact: integrable_funeneg. transitivity (\int[mu]_(x in E) (f x * Radon_Nikodym_SigmaFinite.f nu mu x)). @@ -2186,7 +2186,7 @@ transitivity (\int[mu]_(x in E) (f x * Radon_Nikodym_SigmaFinite.f nu mu x)). exact: measurable_int (Radon_Nikodym_SigmaFinite.f_integrable _). - apply: ae_eqe_mul2l. exact/ae_eq_sym/ae_eq_Radon_Nikodym_SigmaFinite. -rewrite [in LHS](funeposneg f). +rewrite -[in LHS](funeposBneg f). under [in LHS]eq_integral => x xE. rewrite muleBl; last 2 first. - exact: Radon_Nikodym_SigmaFinite.f_fin_num. - exact: add_def_funeposneg. diff --git a/theories/ereal.v b/theories/ereal.v index 8c0eb51a68..d7d4dc4c3b 100644 --- a/theories/ereal.v +++ b/theories/ereal.v @@ -1,4 +1,4 @@ -(* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C. *) +(* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C. *) (* -------------------------------------------------------------------- *) (* Copyright (c) - 2015--2016 - IMDEA Software Institute *) (* Copyright (c) - 2015--2018 - Inria *) @@ -58,11 +58,16 @@ Import numFieldTopology.Exports. From mathcomp Require Import mathcomp_extra unstable. Local Open Scope ring_scope. - Local Open Scope ereal_scope. - Local Open Scope classical_set_scope. +Lemma ge0_addBefctE (T : Type) (R : realDomainType) (a b c d : T -> \bar R) : + (forall x, 0 <= c x) -> (forall x, 0 <= d x) -> + a + b \- (c + d) = a \- c + (b \- d). +Proof. +by move=> ? ?; apply/funext=> x; rewrite !fctE addeACA oppeD ?ge0_adde_def ?inE. +Qed. + Lemma EFin_bigcup T (F : nat -> set T) : EFin @` (\bigcup_i F i) = \bigcup_i (EFin @` F i). Proof. diff --git a/theories/esum.v b/theories/esum.v index a25e061a86..9d4e14a756 100644 --- a/theories/esum.v +++ b/theories/esum.v @@ -1,4 +1,4 @@ -(* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C. *) +(* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C. *) From mathcomp Require Import all_ssreflect ssralg ssrnum finmap. From mathcomp Require Import mathcomp_extra boolp classical_sets functions. From mathcomp Require Import cardinality fsbigop reals ereal interval_inference. @@ -507,14 +507,14 @@ Proof. by move=> Df; rewrite summableN; exact: summableD. Qed. Lemma summable_funepos D f : summable D f -> summable D f^\+. Proof. -apply: le_lt_trans; apply le_esum => t Dt. -by rewrite -/((abse \o f) t) fune_abse gee0_abs// leeDl. +apply: le_lt_trans; apply: le_esum => t Dt. +by rewrite -/((abse \o f) t) -funeposDneg gee0_abs// leeDl. Qed. Lemma summable_funeneg D f : summable D f -> summable D f^\-. Proof. -apply: le_lt_trans; apply le_esum => t Dt. -by rewrite -/((abse \o f) t) fune_abse gee0_abs// leeDr. +apply: le_lt_trans; apply: le_esum => t Dt. +by rewrite -/((abse \o f) t) -funeposDneg gee0_abs// leeDr. Qed. End summable_lemmas. @@ -596,7 +596,7 @@ have -> : (C_ = A_ \- B_)%R. apply/funext => k. rewrite /= /A_ /C_ /B_ -sumrN -big_split/= -summable_fine_sum//. apply eq_bigr => i Pi; rewrite -fineB//. - - by rewrite [in LHS](funeposneg f). + - by rewrite -[in LHS](funeposBneg f). - by rewrite fin_num_abs (@summable_pinfty _ _ P) //; exact/summable_funepos. - by rewrite fin_num_abs (@summable_pinfty _ _ P) //; exact/summable_funeneg. by rewrite distrC; apply: hN; near: n; exists N. @@ -653,14 +653,14 @@ rewrite [X in _ == X -> _]addeC -sube_eq; last 2 first. - rewrite fin_num_adde_defr// ge0_esum_posneg//. rewrite (@eq_esum _ _ _ _ (abse \o f))// -?summableE// => i Di. by rewrite /= gee0_abs// f0. -rewrite -addeA addeCA eq_sym [X in _ == X -> _]addeC -sube_eq; last 2 first. - - rewrite ge0_esum_posneg//. - rewrite (@eq_esum _ _ _ _ (abse \o f))// -?summableE// => i Di. - by rewrite /= gee0_abs// f0. - - rewrite fin_num_adde_defl// ge0_esum_posneg//. - rewrite (@eq_esum _ _ _ _ (abse \o g))// -?summableE// => i Di. - by rewrite /= gee0_abs// g0. -by rewrite ge0_esum_posneg// ge0_esum_posneg// => /eqP ->. +rewrite -addeA addeCA eq_sym [X in _ == X -> _]addeC -sube_eq. +- by rewrite ge0_esum_posneg// ge0_esum_posneg// => /eqP ->. +- rewrite ge0_esum_posneg//. + rewrite (@eq_esum _ _ _ _ (abse \o f))// -?summableE// => i Di. + by rewrite /= gee0_abs// f0. +- rewrite fin_num_adde_defl// ge0_esum_posneg//. + rewrite (@eq_esum _ _ _ _ (abse \o g))// -?summableE// => i Di. + by rewrite /= gee0_abs// g0. Qed. End esumB. diff --git a/theories/independence.v b/theories/independence.v index 329368d0dc..4bb172f636 100644 --- a/theories/independence.v +++ b/theories/independence.v @@ -13,6 +13,8 @@ From mathcomp Require Import hoelder. (**md**************************************************************************) (* # Independence *) (* *) +(* The status of this file is experimental. *) +(* *) (* ``` *) (* independent_events I F == the events F indexed by I are independent *) (* mutual_independence I F == the set systems F indexed by I are independent *) @@ -946,9 +948,7 @@ Lemma independent_expectationM (X Y : {RV P >-> R}) : Proof. move=> XY iX iY. transitivity ('E_P[(X^\+ - X^\-) * (Y^\+ - Y^\-)]). - congr ('E_P[_]). - apply/funext => /=t. - by rewrite [in LHS](funrposneg X)/= [in LHS](funrposneg Y). + by rewrite !funrposBneg. have ? : X^\-%R \in Lfun P 1. apply/Lfun1_integrable; rewrite -funerneg; apply/integrable_funeneg => //. exact/Lfun1_integrable. @@ -1003,7 +1003,7 @@ transitivity ('E_P[X^\+ - X^\-] * 'E_P[Y^\+ - Y^\-]). - by rewrite -!expectationB. - by rewrite fin_numB// !expectation_fin_num. - by rewrite fin_num_adde_defr// expectation_fin_num. -by congr *%E; congr ('E_P[_]); rewrite [RHS]funrposneg. +by rewrite !funrposBneg. Qed. End product_expectation. diff --git a/theories/lebesgue_integral_theory/lebesgue_integrable.v b/theories/lebesgue_integral_theory/lebesgue_integrable.v index fec5bd46e5..7704f24782 100644 --- a/theories/lebesgue_integral_theory/lebesgue_integrable.v +++ b/theories/lebesgue_integral_theory/lebesgue_integrable.v @@ -1,4 +1,4 @@ -(* mathcomp analysis (c) 2025 Inria and AIST. License: CeCILL-C. *) +(* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C. *) From HB Require Import structures. From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint interval finmap. From mathcomp Require Import archimedean. @@ -207,10 +207,9 @@ Proof. by move=> fi gi; exact/(integrableD fi)/integrableN. Qed. Lemma integrable_add_def f : mu_int f -> \int[mu]_(x in D) f^\+ x +? - (\int[mu]_(x in D) f^\- x). Proof. -move=> /integrableP[mf]; rewrite -[fun x => _]/(abse \o f) fune_abse => foo. -rewrite ge0_integralD // in foo; last 2 first. -- exact: measurable_funepos. -- exact: measurable_funeneg. +move=> /integrableP[mf]; rewrite -[fun x => _]/(abse \o f) -funeposDneg => foo. +rewrite ge0_integralD // in foo; [|exact: measurable_funepos + |exact: measurable_funeneg]. apply: ltpinfty_adde_def. - by apply: le_lt_trans foo; rewrite leeDl// integral_ge0. - by rewrite inE (@le_lt_trans _ _ 0)// leeNl oppe0 integral_ge0. @@ -223,7 +222,7 @@ move=> /integrableP[Df foo]; apply/integrableP; split. apply: le_lt_trans foo; apply: ge0_le_integral => //. - by apply/measurableT_comp => //; exact: measurable_funepos. - exact/measurableT_comp. -- by move=> t Dt; rewrite -/((abse \o f) t) fune_abse gee0_abs// leeDl. +- by move=> t Dt; rewrite -/((abse \o f) t) -funeposDneg gee0_abs// leeDl. Qed. Lemma integrable_funeneg f : mu_int f -> mu_int f^\-. @@ -233,7 +232,7 @@ move=> /integrableP[Df foo]; apply/integrableP; split. apply: le_lt_trans foo; apply: ge0_le_integral => //. - by apply/measurableT_comp => //; exact: measurable_funeneg. - exact/measurableT_comp. -- by move=> t Dt; rewrite -/((abse \o f) t) fune_abse gee0_abs// leeDr. +- by move=> t Dt; rewrite -/((abse \o f) t) -funeposDneg gee0_abs// leeDr. Qed. Lemma integral_funeneg_lt_pinfty f : mu_int f -> \int[mu]_(x in D) f^\- x < +oo. @@ -241,9 +240,8 @@ Proof. move=> /integrableP[mf]; apply: le_lt_trans; apply: ge0_le_integral => //. - exact: measurable_funeneg. - exact: measurableT_comp. -- move=> x Dx; have [fx0|/ltW fx0] := leP (f x) 0. - rewrite lee0_abs// funenegE. - by move: fx0; rewrite -{1}oppe0 -leeNr => /max_idPl ->. +- move=> x Dx; have /orP[fx0|fx0] := le_total (f x) 0. + by rewrite lee0_abs// funenegE ge_max lexx leeNr oppe0 fx0. rewrite gee0_abs// funenegE. by move: (fx0); rewrite -{1}oppe0 -leeNl => /max_idPr ->. Qed. @@ -268,7 +266,7 @@ rewrite fin_numElt; apply/andP; split. case: fi => mf; apply: le_lt_trans; apply: ge0_le_integral => //. - exact/measurable_funeneg. - exact/measurableT_comp. -- by move=> x Dx; rewrite -/((abse \o f) x) (fune_abse f) leeDr. +- by move=> x Dx; rewrite -/((abse \o f) x) -funeposDneg leeDr. Qed. Lemma integrable_pos_fin_num f : @@ -280,7 +278,7 @@ rewrite fin_numElt; apply/andP; split. case: fi => mf; apply: le_lt_trans; apply: ge0_le_integral => //. - exact/measurable_funepos. - exact/measurableT_comp. -- by move=> x Dx; rewrite -/((abse \o f) x) (fune_abse f) leeDl. +- by move=> x Dx; rewrite -/((abse \o f) x) -funeposDneg leeDl. Qed. Lemma integrableMr (h : T -> R) g : @@ -593,8 +591,8 @@ have : (g1 \+ g2)^\+ \+ g1^\- \+ g2^\- = (g1 \+ g2)^\- \+ g1^\+ \+ g2^\+. by rewrite !funeposE -!fine_max. by rewrite funeposE !funenegE -!fine_max. apply/eqP. - rewrite -[LHS]/((g1^\+ \+ g2^\+ \- (g1^\- \+ g2^\-)) x) -funeD_posD. - by rewrite -[RHS]/((_ \- _) x) -funeD_Dpos. + rewrite -[LHS]/((g1^\+ \+ g2^\+ \- (g1^\- \+ g2^\-)) x) funeDB. + by rewrite -[RHS]/((_ \- _) x) funeposBneg. move/(congr1 (fun y => \int[mu]_(x in D) (y x) )). rewrite (ge0_integralD mu mD); last 4 first. - by move=> x _; rewrite adde_ge0. @@ -741,7 +739,7 @@ Local Open Scope ereal_scope. Lemma integrable_lty (f : T -> \bar R) : mu.-integrable D f -> \int[mu]_(x in D) f x < +oo. Proof. -move=> intf; rewrite (funeposneg f) integralB//; +move=> intf; rewrite -(funeposBneg f) integralB//; [|exact: integrable_funepos|exact: integrable_funeneg]. rewrite lte_add_pinfty ?integral_funepos_lt_pinfty// lteNl ltNye_eq. by rewrite integrable_neg_fin_num. @@ -799,7 +797,7 @@ rewrite -[X in _ = _ - X]ge0_integral_pushforward//; last first. rewrite -integralB//=; last first. - by apply: integrable_funeneg => //=; exact: integrable_pushforward. - by apply: integrable_funepos => //=; exact: integrable_pushforward. -- by apply/eq_integral=> // x _; rewrite /= [in LHS](funeposneg f). +- by apply/eq_integral=> // x _; rewrite -[in LHS](funeposBneg f). Qed. End transfer. @@ -813,7 +811,7 @@ Lemma negligible_integral (D N : set T) (f : T -> \bar R) : measurable N -> measurable D -> mu.-integrable D f -> mu N = 0 -> \int[mu]_(x in D) f x = \int[mu]_(x in D `\` N) f x. Proof. -move=> mN mD mf muN0; rewrite [f]funeposneg ?integralB //; first last. +move=> mN mD mf muN0; rewrite -[f]funeposBneg ?integralB//; first last. - exact: integrable_funeneg. - exact: integrable_funepos. - apply: (integrableS mD) => //; first exact: measurableD. @@ -859,7 +857,7 @@ Lemma integral_measure_add : \int[measure_add m1 m2]_(x in D) f x = Proof. transitivity (\int[m1]_(x in D) (f^\+ \- f^\-) x + \int[m2]_(x in D) (f^\+ \- f^\-) x); last first. - by congr +%E; apply: eq_integral => x _; rewrite [in RHS](funeposneg f). + by congr +%E; apply: eq_integral => x _; rewrite -[in RHS](funeposBneg f). rewrite integralB//; [|exact: integrable_funepos|exact: integrable_funeneg]. rewrite integralB//; [|exact: integrable_funepos|exact: integrable_funeneg]. rewrite addeACA -ge0_integral_measure_add//; last first. @@ -908,7 +906,7 @@ have ? : \int[mu]_(x in \bigcup_i F i) g x \is a fin_num. transitivity (\int[mu]_(x in \bigcup_i F i) g^\+ x - \int[mu]_(x in \bigcup_i F i) g^\- x)%E. rewrite -integralB. - - by apply: eq_integral => t Ft; rewrite [in LHS](funeposneg g). + - by apply: eq_integral => t Ft; rewrite -[in LHS](funeposBneg g). - exact: bigcupT_measurable. - by apply: integrable_funepos => //; exact: bigcupT_measurable. - by apply: integrable_funeneg => //; exact: bigcupT_measurable. diff --git a/theories/lebesgue_integral_theory/lebesgue_integral_dominated_convergence.v b/theories/lebesgue_integral_theory/lebesgue_integral_dominated_convergence.v index 3622ce6a1e..1c5525ebfc 100644 --- a/theories/lebesgue_integral_theory/lebesgue_integral_dominated_convergence.v +++ b/theories/lebesgue_integral_theory/lebesgue_integral_dominated_convergence.v @@ -1,4 +1,4 @@ -(* mathcomp analysis (c) 2025 Inria and AIST. License: CeCILL-C. *) +(* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C. *) From HB Require Import structures. From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint interval finmap. From mathcomp Require Import archimedean. @@ -297,11 +297,11 @@ exists (fun n => p_ n - n_ n)%R; split. - move=> n; rewrite /comp; under eq_fun => ? do rewrite sfunB /= EFinB. by apply: integrableB => //; [exact: intp | exact: intn]. - move=> ? ?; rewrite /comp; under eq_fun => ? do rewrite sfunB /= EFinB. - rewrite [f]funeposneg; apply: cvgeB => //;[|exact: pf|exact:nf]. + rewrite -[f]funeposBneg; apply: cvgeB => //;[|exact: pf|exact:nf]. exact: add_def_funeposneg. have fpn z n : f z - ((p_ n - n_ n) z)%:E = (f^\+ z - (p_ n z)%:E) - (f^\- z - (n_ n z)%:E). - rewrite sfunB EFinB fin_num_oppeB // {1}[f]funeposneg -addeACA. + rewrite sfunB EFinB fin_num_oppeB // -{1}[f]funeposBneg -addeACA. by congr (_ _); rewrite fin_num_oppeB. case/integrableP: (intf) => mf _. have mfpn n : mu.-integrable E (fun z => f z - ((p_ n - n_ n) z)%:E). diff --git a/theories/lebesgue_integral_theory/lebesgue_integral_fubini.v b/theories/lebesgue_integral_theory/lebesgue_integral_fubini.v index 91897623ac..12808fd21e 100644 --- a/theories/lebesgue_integral_theory/lebesgue_integral_fubini.v +++ b/theories/lebesgue_integral_theory/lebesgue_integral_fubini.v @@ -1,4 +1,4 @@ -(* mathcomp analysis (c) 2025 Inria and AIST. License: CeCILL-C. *) +(* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C. *) From HB Require Import structures. From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint interval finmap. From mathcomp Require Import archimedean. @@ -922,7 +922,7 @@ apply: ge0_le_integral; [by []|by []|..]. + apply: measurableT_comp => //. by apply: measurableT_comp => //; exact: measurable_funepos. + by apply: measurableT_comp => //; exact/measurableT_comp. - + by move=> y _; rewrite gee0_abs// -/((abse \o f) (x, y)) fune_abse leeDl. + + by move=> y _; rewrite gee0_abs// -/((abse \o f) _) -funeposDneg leeDl. Qed. Let integrable_Fminus : m1.-integrable setT Fminus. @@ -939,7 +939,7 @@ apply: ge0_le_integral; [by []|by []|..]. + apply: measurableT_comp => //; apply: measurableT_comp => //. exact: measurable_funeneg. + by apply: measurableT_comp => //; exact: measurableT_comp. - + by move=> y _; rewrite gee0_abs// -/((abse \o f) (x, y)) fune_abse leeDr. + + by move=> y _; rewrite gee0_abs// -/((abse \o f) _) -funeposDneg leeDr. Qed. Lemma integrable_fubini_F : m1.-integrable setT F. @@ -982,7 +982,7 @@ apply: ge0_le_integral; [by []|by []|exact: measurableT_comp|..]. + apply: measurableT_comp => //. by apply: measurableT_comp => //; exact: measurable_funepos. + by apply: measurableT_comp => //; exact: measurableT_comp. - + by move=> x _; rewrite gee0_abs// -/((abse \o f) (x, y)) fune_abse leeDl. + + by move=> x _; rewrite gee0_abs// -/((abse \o f) _) -funeposDneg leeDl. Qed. Let integrable_Gminus : m2.-integrable setT Gminus. @@ -997,7 +997,7 @@ apply: ge0_le_integral; [by []|by []|exact: measurableT_comp|..]. + apply: measurableT_comp => //. by apply: measurableT_comp => //; exact: measurable_funeneg. + by apply: measurableT_comp => //; exact: measurableT_comp. - + by move=> x _; rewrite gee0_abs// -/((abse \o f) (x, y)) fune_abse leeDr. + + by move=> x _; rewrite gee0_abs// -/((abse \o f) _) -funeposDneg leeDr. Qed. Lemma integral12_prod_meas1 : \int[m1]_x F x = \int[m1 \x m2]_z f z. diff --git a/theories/lebesgue_integral_theory/lebesgue_integral_nonneg.v b/theories/lebesgue_integral_theory/lebesgue_integral_nonneg.v index 087a36bd8c..91592f830c 100644 --- a/theories/lebesgue_integral_theory/lebesgue_integral_nonneg.v +++ b/theories/lebesgue_integral_theory/lebesgue_integral_nonneg.v @@ -1,4 +1,4 @@ -(* mathcomp analysis (c) 2025 Inria and AIST. License: CeCILL-C. *) +(* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C. *) From HB Require Import structures. From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint interval finmap. From mathcomp Require Import archimedean. @@ -605,7 +605,7 @@ Proof. have [/[!inE] aD|aD] := boolP (a \in D). rewrite integralE ge0_integral_dirac//; last exact/measurable_funepos. rewrite ge0_integral_dirac//; last exact/measurable_funeneg. - by rewrite [in RHS](funeposneg f) diracE mem_set// mul1e. + by rewrite -[in RHS](funeposBneg f) diracE mem_set// mul1e. rewrite diracE (negbTE aD) mul0e -(integral_measure_zero D f)//. apply: eq_measure_integral => //= S mS DS; rewrite /dirac indicE memNset//. by move=> /DS/mem_set; exact/negP. @@ -613,8 +613,8 @@ Qed. End integral_dirac. -Lemma summable_integral_dirac {R : realType} (a : nat -> \bar R) : summable setT a -> - (\sum_(n (\sum_(n sa. apply: (@le_lt_trans _ _ (\sum_(i \int[measure_add (msum m_ N) (m_ N)]_(x in D) (f_ n x)%:E)). rewrite -monotone_convergence//; last first. by move=> t Dt a b ab; rewrite lee_fin; exact/lefP/nd_nnsfun_approx. - by apply: eq_integral => t /[!inE] Dt; apply/esym/cvg_lim => //; exact: cvg_nnsfun_approx. + apply: eq_integral => t /[!inE] Dt; apply/esym/cvg_lim => //. + exact: cvg_nnsfun_approx. transitivity (limn (fun n => \int[msum m_ N]_(x in D) (f_ n x)%:E + \int[m_ N]_(x in D) (f_ n x)%:E)). by congr (limn _); apply/funext => n; by rewrite integral_measure_add_nnsfun. @@ -1111,14 +1112,14 @@ End ge0_cvgn_integral. Lemma le_abse_integral d (T : measurableType d) (R : realType) (mu : {measure set T -> \bar R}) (D : set T) (f : T -> \bar R) (mD : measurable D) : measurable_fun D f -> - (`| \int[mu]_(x in D) (f x) | <= \int[mu]_(x in D) `|f x|)%E. + (`| \int[mu]_(x in D) f x | <= \int[mu]_(x in D) `|f x|)%E. Proof. move=> mf. rewrite integralE (le_trans (lee_abs_sub _ _))// gee0_abs; last first. exact: integral_ge0. rewrite gee0_abs; last exact: integral_ge0. -by rewrite -ge0_integralD // -?fune_abse//; - [exact: measurable_funepos | exact: measurable_funeneg]. +rewrite -ge0_integralD//; [|exact: measurable_funepos|exact: measurable_funeneg]. +by under [in leRHS]eq_integral do rewrite -/((abse \o f) _) -funeposDneg. Qed. Lemma abse_integralP d (T : measurableType d) (R : realType) @@ -1128,7 +1129,7 @@ Lemma abse_integralP d (T : measurableType d) (R : realType) Proof. move=> mD mf; split => [|] foo; last first. exact: (le_lt_trans (le_abse_integral mu mD mf) foo). -under eq_integral do rewrite -/((abse \o f) _) fune_abse. +under eq_integral do rewrite -/((abse \o f) _) -funeposDneg. rewrite ge0_integralD//;[|exact/measurable_funepos|exact/measurable_funeneg]. move: foo; rewrite integralE/= -fin_num_abs fin_numB => /andP[fpoo fnoo]. by rewrite lte_add_pinfty// ltey_eq ?fpoo ?fnoo. diff --git a/theories/lebesgue_integral_theory/measurable_fun_approximation.v b/theories/lebesgue_integral_theory/measurable_fun_approximation.v index 88af112a6a..e67b078f4b 100644 --- a/theories/lebesgue_integral_theory/measurable_fun_approximation.v +++ b/theories/lebesgue_integral_theory/measurable_fun_approximation.v @@ -1,4 +1,4 @@ -(* mathcomp analysis (c) 2025 Inria and AIST. License: CeCILL-C. *) +(* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C. *) From HB Require Import structures. From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint interval finmap. From mathcomp Require Import archimedean. @@ -404,7 +404,7 @@ exists (fun n => fp_ n \+ cst (-1) \* fn_ n) => x /=. rewrite [X in X @ \oo --> _](_ : _ = EFin \o fp_^~ x \+ (-%E \o EFin \o fn_^~ x))%E; last first. by apply/funext => n/=; rewrite EFinD mulN1r. -by move=> Dx; rewrite (funeposneg f); apply: cvgeD; +by move=> Dx; rewrite -(funeposBneg f); apply: cvgeD; [exact: add_def_funeposneg|apply: cvg_nnsfun_approx|apply:cvgeN; apply: cvg_nnsfun_approx]. Qed. diff --git a/theories/measurable_realfun.v b/theories/measurable_realfun.v index fcd121560e..997feedb79 100644 --- a/theories/measurable_realfun.v +++ b/theories/measurable_realfun.v @@ -1,4 +1,4 @@ -(* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C. *) +(* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C. *) From HB Require Import structures. From mathcomp Require Import all_ssreflect finmap ssralg ssrnum ssrint interval. From mathcomp Require Import archimedean rat. @@ -1089,6 +1089,19 @@ Qed. End measurable_fun_realType. +Section funrposneg_measurable. +Context {d} {aT : measurableType d} {rT : realType}. + +HB.instance Definition _ (f : {mfun aT >-> rT}) := + @isMeasurableFun.Build d _ _ _ f^\+ + (measurable_funrpos (@measurable_funPT _ _ _ _ f)). + +HB.instance Definition _ (f : {mfun aT >-> rT}) := + @isMeasurableFun.Build d _ _ _ f^\- + (measurable_funrneg (@measurable_funPT _ _ _ _ f)). + +End funrposneg_measurable. + Section mono_measurable. Context {R : realType}. diff --git a/theories/measure_theory/measure_negligible.v b/theories/measure_theory/measure_negligible.v index 05c563edc8..e9efb02f82 100644 --- a/theories/measure_theory/measure_negligible.v +++ b/theories/measure_theory/measure_negligible.v @@ -1,4 +1,4 @@ -(* mathcomp analysis (c) 2025 Inria and AIST. License: CeCILL-C. *) +(* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C. *) From HB Require Import structures. From mathcomp Require Import all_ssreflect all_algebra. From mathcomp Require Import boolp classical_sets functions cardinality reals. @@ -273,7 +273,8 @@ Lemma ae_eq_funeposneg (f g : T -> \bar R) : Proof. split=> [fg|[pfg nfg]]. by split; near=> x => Dx; rewrite !(funeposE,funenegE) (near fg). -by near=> x => Dx; rewrite (funeposneg f) (funeposneg g) ?(near pfg, near nfg). +near=> x => Dx. +by rewrite -(funeposBneg f) -(funeposBneg g) ?(near pfg, near nfg). Unshelve. all: by end_near. Qed. Local Close Scope ereal_scope. @@ -283,7 +284,8 @@ Proof. by symmetry. Qed. Lemma ae_eq_trans U (f g h : T -> U) : ae_eq f g -> ae_eq g h -> ae_eq f h. Proof. by apply transitivity. Qed. -Lemma ae_eq_sub W (f g h i : T -> W) : ae_eq f g -> ae_eq h i -> ae_eq (f \- h) (g \- i). +Lemma ae_eq_sub W (f g h i : T -> W) : ae_eq f g -> ae_eq h i -> + ae_eq (f \- h) (g \- i). Proof. by apply: filterS2 => x + + Dx => /= /(_ Dx) -> /(_ Dx) ->. Qed. Lemma ae_eq_mul2r W (f g h : T -> W) : ae_eq f g -> ae_eq (f \* h) (g \* h). @@ -295,7 +297,8 @@ Proof. by move=>/(ae_eq_comp2 (fun x y => h x * y)). Qed. Lemma ae_eq_mul1l W (f g : T -> W) : ae_eq f (cst 1) -> ae_eq g (g \* f). Proof. by apply: filterS => x /= /[apply] ->; rewrite mulr1. Qed. -Lemma ae_eq_abse (f g : T -> \bar R) : ae_eq f g -> ae_eq (abse \o f) (abse \o g). +Lemma ae_eq_abse (f g : T -> \bar R) : ae_eq f g -> + ae_eq (abse \o f) (abse \o g). Proof. by apply: filterS => x /[apply] /= ->. Qed. Lemma ae_foralln (P : nat -> T -> Prop) : @@ -306,8 +309,8 @@ have seqDUAmeas := seqDU_measurable Ameas. exists (\bigcup_n A n); split => //. - exact/bigcup_measurable. - rewrite seqDU_bigcup_eq measure_bigcup// eseries0// => i _ _. - by rewrite (@subset_measure0 _ _ _ _ _ (A i))//=; apply: subset_seqDU. -- by move=> x /=; rewrite -existsNP => -[n NPnx]; exists n => //; apply: NPA. + by rewrite (@subset_measure0 _ _ _ _ _ (A i))//=; exact: subset_seqDU. +- by move=> x /=; rewrite -existsNP => -[n NPnx]; exists n => //; exact: NPA. Qed. End ae_eq. diff --git a/theories/numfun.v b/theories/numfun.v index cd037679ae..c8b549d6e0 100644 --- a/theories/numfun.v +++ b/theories/numfun.v @@ -1,4 +1,4 @@ -(* mathcomp analysis (c) 2025 Inria and AIST. License: CeCILL-C. *) +(* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C. *) From HB Require Import structures. From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint interval finmap. From mathcomp Require Import mathcomp_extra boolp classical_sets fsbigop. @@ -764,9 +764,9 @@ move=> r0; rewrite -[in LHS](opprK r); under eq_fun do rewrite mulNr. by rewrite funrnegN ge0_funrposM ?oppr_ge0. Qed. -Lemma funr_normr f : Num.norm \o f = f^\+ \+ f^\-. +Lemma funrposDneg f : f^\+ + f^\- = Num.norm \o f. Proof. -rewrite funeqE => x /=; have [fx0|/ltW fx0] := leP (f x) 0. +rewrite funeqE => x /=; rewrite !fctE/=; have [fx0|/ltW fx0] := leP (f x) 0. - rewrite ler0_norm// /funrpos /funrneg. move/max_idPr : (fx0) => ->; rewrite add0r. by move: fx0; rewrite -{1}oppr0 lerNr => /max_idPl ->. @@ -774,32 +774,16 @@ rewrite funeqE => x /=; have [fx0|/ltW fx0] := leP (f x) 0. by move: fx0; rewrite -{1}oppr0 lerNl => /max_idPr ->; rewrite addr0. Qed. -Lemma funrposneg f : f = (fun x => f^\+ x - f^\- x). +Lemma funrposBneg f : f^\+ - f^\- = f. Proof. -rewrite funeqE => x; rewrite /funrpos /funrneg; have [|/ltW] := leP (f x) 0. +apply/funext => x. +rewrite /funrpos /funrneg/= !fctE; have [|/ltW] := leP (f x) 0. by rewrite -{1}oppr0 -lerNr => /max_idPl ->; rewrite opprK add0r. by rewrite -{1}oppr0 -lerNl => /max_idPr ->; rewrite subr0. Qed. -Lemma funrD_Dpos f g : f \+ g = (f \+ g)^\+ \- (f \+ g)^\-. -Proof. -apply/funext => x; rewrite /funrpos /funrneg/=; have [|/ltW] := lerP 0 (f x + g x). -- by rewrite -{1}oppr0 -lerNl => /max_idPr ->; rewrite subr0. -- by rewrite -{1}oppr0 -lerNr => /max_idPl ->; rewrite opprK add0r. -Qed. - -Lemma funrD_posD f g : f \+ g = (f^\+ \+ g^\+) \- (f^\- \+ g^\-). -Proof. -apply/funext => x; rewrite /funrpos /funrneg/=. -have [|fx0] := lerP 0 (f x); last rewrite add0r. -- rewrite -{1}oppr0 lerNl => /max_idPr ->; have [|/ltW] := lerP 0 (g x). - by rewrite -{1}oppr0 lerNl => /max_idPr ->; rewrite addr0 subr0. - by rewrite -{1}oppr0 -lerNr => /max_idPl ->; rewrite addr0 sub0r opprK. -- move/ltW : (fx0); rewrite -{1}oppr0 lerNr => /max_idPl ->. - have [|]/= := lerP 0 (g x); last rewrite add0r. - by rewrite -{1}oppr0 lerNl => /max_idPr ->; rewrite addr0 opprK addrC. - by rewrite -oppr0 ltrNr -{1}oppr0 => /ltW/max_idPl ->; rewrite opprD !opprK. -Qed. +Lemma funrDB f g : (f^\+ + g^\+) - (f^\- + g^\-) = f + g. +Proof. by rewrite addBrfctE !funrposBneg. Qed. Lemma funrpos_le f g : {in D, forall x, f x <= g x} -> {in D, forall x, f^\+ x <= g^\+ x}. @@ -920,9 +904,9 @@ move=> r0; rewrite -[in LHS](opprK r); under eq_fun do rewrite EFinN mulNe. by rewrite funenegN ge0_funeposM ?oppr_ge0. Qed. -Lemma fune_abse f : abse \o f = f^\+ \+ f^\-. +Lemma funeposDneg f : f^\+ + f^\- = abse \o f. Proof. -rewrite funeqE => x /=; have [fx0|/ltW fx0] := leP (f x) 0. +rewrite funeqE => x /=; rewrite !fctE/=; have /orP[fx0|fx0] := le_total (f x) 0. - rewrite lee0_abs// funeposE funenegE. move/max_idPr : (fx0) => ->; rewrite add0e. by move: fx0; rewrite -{1}oppe0 leeNr => /max_idPl ->. @@ -930,7 +914,7 @@ rewrite funeqE => x /=; have [fx0|/ltW fx0] := leP (f x) 0. by move: fx0; rewrite -{1}oppe0 leeNl => /max_idPr ->; rewrite adde0. Qed. -Lemma funeposneg f : f = (fun x => f^\+ x - f^\- x). +Lemma funeposBneg f : f^\+ \- f^\- = f. Proof. rewrite funeqE => x; rewrite funeposE funenegE; have [|/ltW] := leP (f x) 0. by rewrite -{1}oppe0 -leeNr => /max_idPl ->; rewrite oppeK add0e. @@ -943,27 +927,13 @@ by rewrite funenegE funeposE; case: (f x) => [r| |]; [rewrite -fine_max/=|rewrite /maxe /= ltNyr|rewrite /maxe /= ltNyr]. Qed. -Lemma funeD_Dpos f g : f \+ g = (f \+ g)^\+ \- (f \+ g)^\-. -Proof. -apply/funext => x; rewrite funeposE funenegE; have [|/ltW] := leP 0 (f x + g x). -- by rewrite -{1}oppe0 -leeNl => /max_idPr ->; rewrite sube0. -- by rewrite -{1}oppe0 -leeNr => /max_idPl ->; rewrite oppeK add0e. -Qed. +#[deprecated(since="mathcomp-analysis 1.15.0", note="use `funeposBneg` instead")] +Lemma funeD_Dpos f g : (f + g)^\+ \- (f + g)^\- = f + g. +Proof. by rewrite funeposBneg. Qed. -Lemma funeD_posD f g : f \+ g = (f^\+ \+ g^\+) \- (f^\- \+ g^\-). +Lemma funeDB f g : (f^\+ + g^\+) \- (f^\- + g^\-) = f + g. Proof. -apply/funext => x; rewrite !funeposE !funenegE. -have [|fx0] := leP 0 (f x); last rewrite add0e. -- rewrite -{1}oppe0 leeNl => /max_idPr ->; have [|/ltW] := leP 0 (g x). - by rewrite -{1}oppe0 leeNl => /max_idPr ->; rewrite adde0 sube0. - by rewrite -{1}oppe0 -leeNr => /max_idPl ->; rewrite adde0 sub0e oppeK. -- move/ltW : (fx0); rewrite -{1}oppe0 leeNr => /max_idPl ->. - have [|] := leP 0 (g x); last rewrite add0e. - by rewrite -{1}oppe0 leeNl => /max_idPr ->; rewrite adde0 oppeK addeC. - move gg' : (g x) => g'; move: g' gg' => [g' gg' g'0|//|goo _]. - + move/ltW : (g'0); rewrite -{1}oppe0 -leeNr => /max_idPl => ->. - by rewrite fin_num_oppeD// 2!oppeK. - + by rewrite /maxe /=; case: (f x) fx0. +by rewrite ge0_addBefctE ?funeposBneg//; by move=> x; rewrite funeneg_ge0. Qed. Lemma funepos_le f g : @@ -985,6 +955,9 @@ move=> fg x Dx; rewrite !funenegE /maxe; case: ifPn => gx; case: ifPn => fx //. Qed. End funposneg_lemmas. +#[deprecated(since="mathcomp-analysis 1.15.0", note="use `-funeDB` instead")] +Notation funeD_posD := funeDB (only parsing). + #[global] Hint Extern 0 (is_true (0%R <= _ ^\+ _)%E) => solve [apply: funepos_ge0] : core. #[global] diff --git a/theories/probability.v b/theories/probability.v index ca1f83d4e5..060dbce25c 100644 --- a/theories/probability.v +++ b/theories/probability.v @@ -1,4 +1,4 @@ -(* mathcomp analysis (c) 2025 Inria and AIST. License: CeCILL-C. *) +(* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C. *) From HB Require Import structures. From mathcomp Require Import all_ssreflect ssralg. From mathcomp Require Import poly ssrnum ssrint interval archimedean finmap. @@ -842,24 +842,6 @@ Definition mmt_gen_fun d (T : measurableType d) (R : realType) (P : probability T R) (X : T -> R) (t : R) := ('E_P[expR \o t \o* X])%E. Notation "'M_ P X" := (@mmt_gen_fun _ _ _ P X). -(* TODO: move earlier *) -Section mfun_measurable_realType. -Context {d} {aT : measurableType d} {rT : realType}. - -HB.instance Definition _ (f : {mfun aT >-> rT}) := - @isMeasurableFun.Build d _ _ _ f^\+ - (measurable_funrpos (@measurable_funPT _ _ _ _ f)). - -HB.instance Definition _ (f : {mfun aT >-> rT}) := - @isMeasurableFun.Build d _ _ _ f^\- - (measurable_funrneg (@measurable_funPT _ _ _ _ f)). - -HB.instance Definition _ (f : {mfun aT >-> rT}) := - @isMeasurableFun.Build d _ _ _ (@normr _ _ \o f) - (measurableT_comp (@normr_measurable _ _) (@measurable_funPT _ _ _ _ f)). - -End mfun_measurable_realType. - Section markov_chebyshev_cantelli. Local Open Scope ereal_scope. Context d (T : measurableType d) (R : realType) (P : probability T R).