beta distribution (#1640)

* beta distribution

Author: affeldt-aist

CHANGELOG_UNRELEASED.md

@@ -72,6 +72,49 @@
            `derivable_Nyo_continuousWoo`,
            `derivable_Nyo_continuousW`
 
+- in `pseudometric_normed_Zmodule.v`:
+  + lemma `continuous_comp_cvg`
+
+- in `derive.v`:
+  + lemma `derive1_onem`
+
+- in `ftc.v`:
+  + lemmas `integration_by_substitution_onem`, `Rintegration_by_substitution_onem`
+
+- in `probability.v`:
+  + lemmas `continuous_onemXn`, `onemXn_derivable`,
+    `derivable_oo_continuous_bnd_onemXnMr`, `derive_onemXn`,
+    `Rintegral_onemXn`
+  + definition `XMonemX`
+  + lemmas `XMonemX_ge0`, `XMonemX_le1`, `XMonemX0n`, `XMonemXn0`,
+    `XMonemX00`, `XMonemXC`, `XMonemXM`
+  + lemmas `continuous_XMonemX`, `within_continuous_XMonemX`,
+    `measurable_XMonemX`, `bounded_XMonemX`, `integrable_XMonemX`,
+    `integrable_XMonemX_restrict`, `integral_XMonemX_restrict`
+  + definition `beta_fun`
+  + lemmas `EFin_beta_fun`, `beta_fun_sym`, `beta_fun0n`, `beta_fun00`,
+    `beta_fun1Sn`, `beta_fun11`, `beta_funSSnSm`, `beta_funSnSm`, `beta_fun_fact`
+  + lemmas `beta_funE`, `beta_fun_gt0`, `beta_fun_ge0`
+  + definition `beta_pdf`
+  + lemmas `measurable_beta_pdf`, `beta_pdf_ge0`, `beta_pdf_le_beta_funV`,
+    `integrable_beta_pdf`, `bounded_beta_pdf_01`
+  + definition `beta_prob`
+  + lemmas `integral_beta_pdf`, `beta_prob01`, `beta_prob_fin_num`,
+    `beta_prob_dom`, `beta_prob_uniform`,
+    `integral_beta_prob_bernoulli_prob_lty`,
+    `integral_beta_prob_bernoulli_prob_onemX_lty`,
+    `integral_beta_prob_bernoulli_prob_onem_lty`, `beta_prob_integrable`,
+    `beta_prob_integrable_onem`, `beta_prob_integrable_dirac`,
+    `beta_prob_integrable_onem_dirac`, `integral_beta_prob`
+  + definition `div_beta_fun`
+  + lemmas `div_beta_fun_ge0`, `div_beta_fun_le1`
+  + definition `beta_prob_bernoulli_prob`
+  + lemma `beta_prob_bernoulli_probE`
+
+
+- in `unstable.v`:
+  + lemmas `leq_Mprod_prodD`, `leq_fact2`, `normr_onem`
+
 - in `num_normedtype.v`:
   + lemmas `bigcup_ointsub_sup`, `bigcup_ointsub_mem`
 
@@ -354,6 +397,13 @@
   + `lb_ereal_inf` -> `le_ereal_inf_tmp`
   + `ereal_sup_ge` -> `le_ereal_sup_tmp`
 
+- in `probability.v`:
+  + `bernoulli` -> `bernoulli_prob`
+  + `bernoulli_probE` -> `bernoulliE`
+  + `integral_bernoulli_prob` -> `integral_bernoulli_prob`
+  + `measurable_bernoulli` -> `measurable_bernoulli_prob`
+  + `measurable_bernoulli2` -> `measurable_bernoulli_prob2`
+
 - in `sequences.v`:
   + `adjacent` -> `adjacent_seq`
 

classical/unstable.v

@@ -76,6 +76,35 @@ elim: r => [|a l]; first by rewrite !big_nil exp1n.
 by rewrite !big_cons; case: ifPn => // Pa <-; rewrite expnMn.
 Qed.
 
+Lemma leq_Mprod_prodD (x y n m : nat) : (n <= x)%N -> (m <= y)%N ->
+  (\prod_(m <= i < y) i * \prod_(n <= i < x) i <= \prod_(n + m <= i < x + y) i)%N.
+Proof.
+move=> nx my; rewrite big_addn -addnBA//.
+rewrite [in leqRHS]/index_iota -addnBAC// iotaD big_cat/=.
+rewrite mulnC leq_mul//.
+  by apply: leq_prod; move=> i _; rewrite leq_addr.
+rewrite subnKC//.
+rewrite -[in leqLHS](add0n m) big_addn.
+rewrite [in leqRHS](_ : y - m = ((y - m + x) - x))%N; last first.
+  by rewrite -addnBA// subnn addn0.
+rewrite -[X in iota X _](add0n x) big_addn -addnBA// subnn addn0.
+by apply: leq_prod => i _; rewrite leq_add2r leq_addr.
+Qed.
+
+Lemma leq_fact2 (x y n m : nat) : (n <= x) %N -> (m <= y)%N ->
+  (x`! * y`! * ((n + m).+1)`! <= n`! * m`! * ((x + y).+1)`!)%N.
+Proof.
+move=> nx my.
+rewrite (fact_split nx) -!mulnA leq_mul2l; apply/orP; right.
+rewrite (fact_split my) mulnCA -!mulnA leq_mul2l; apply/orP; right.
+rewrite [leqRHS](_ : _ =
+    (n + m).+1`! * \prod_((n + m).+2 <= i < (x + y).+2) i)%N; last first.
+  by rewrite -fact_split// ltnS leq_add.
+rewrite mulnA mulnC leq_mul2l; apply/orP; right.
+do 2 rewrite -addSn -addnS.
+exact: leq_Mprod_prodD.
+Qed.
+
 Section max_min.
 Variable R : realFieldType.
 
@@ -284,6 +313,14 @@ Proof. by move=> ?; rewrite onem_lt1// exprn_gt0. Qed.
 
 End onem_order.
 
+Lemma normr_onem {R : realDomainType} (x : R) :
+  (0 <= x <= 1 -> `| `1-x | <= 1)%R.
+Proof.
+move=> /andP[x0 x1]; rewrite ler_norml; apply/andP; split.
+  by rewrite lerBrDl lerBlDr (le_trans x1)// lerDl.
+by rewrite lerBlDr lerDl.
+Qed.
+
 Lemma onemV (F : numFieldType) (x : F) : x != 0 -> `1-(x^-1) = (x - 1) / x.
 Proof. by move=> ?; rewrite mulrDl divff// mulN1r. Qed.
 

theories/derive.v

@@ -1267,6 +1267,12 @@ Proof. by have /derivableP := @derivable_id x v; rewrite derive_val. Qed.
 
 End derive_id.
 
+Lemma derive1_onem {R : numFieldType} :
+  (fun x => `1-x : R^o)^`()%classic = cst (-1).
+Proof.
+by apply/funext => x; rewrite derive1E deriveB// derive_id derive_cst sub0r.
+Qed.
+
 Section Derive_lemmasVR.
 Variables (R : numFieldType) (V : normedModType R).
 Implicit Types (f g : V -> R) (x v : V).

theories/ftc.v

@@ -1793,6 +1793,46 @@ Qed.
 
 End integration_by_substitution.
 
+Section integration_by_substitution_onem.
+Context {R : realType}.
+Let mu := (@lebesgue_measure R).
+Local Open Scope ereal_scope.
+
+Lemma integration_by_substitution_onem (G : R -> R) (r : R) :
+  (0 < r <= 1)%R ->
+  {within `[0%R, r], continuous G} ->
+  \int[mu]_(x in `[0%R, r]) (G x)%:E =
+  \int[mu]_(x in `[`1-r, 1%R]) (G `1-x)%:E.
+Proof.
+move=> r01 cG.
+have := @integration_by_substitution_decreasing R onem G `1-r 1.
+rewrite onemK onem1 => -> //.
+- by apply: eq_integral => x xr; rewrite !fctE derive1_onem opprK mulr1.
+- by rewrite ltrBlDl ltrDr; case/andP : r01.
+- by move=> x y _ _ xy; rewrite ler_ltB.
+- by rewrite derive1_onem; move=> ? ?; exact: cvg_cst.
+- by rewrite derive1_onem; exact: is_cvg_cst.
+- by rewrite derive1_onem; exact: is_cvg_cst.
+- split => /=.
+  + by move=> x xr1; exact: derivableB.
+  + apply: cvg_at_right_filter; rewrite onemK.
+    apply: (@continuous_comp_cvg _ _ _ _ onem)=> //=.
+      by move=> x; apply: continuousB => //; exact: cvg_cst.
+    by under eq_fun do rewrite -/(onem _) onemK; exact: cvg_id.
+  + by apply: cvg_at_left_filter; apply: cvgB => //; exact: cvg_cst.
+Qed.
+
+Lemma Rintegration_by_substitution_onem (G : R -> R) (r : R) :
+  (0 < r <= 1)%R ->
+  {within `[0%R, r], continuous G} ->
+  (\int[mu]_(x in `[0, r]) (G x) =
+  \int[mu]_(x in `[`1-r, 1]) (G `1-x))%R.
+Proof.
+by move=> r01 cG; rewrite [in LHS]/Rintegral integration_by_substitution_onem.
+Qed.
+
+End integration_by_substitution_onem.
+
 Section ge0_integralT_even.
 Context {R : realType}.
 Let mu := @lebesgue_measure R.

theories/normedtype_theory/pseudometric_normed_Zmodule.v

@@ -817,6 +817,20 @@ Arguments cvgr_neq0 {R V T F FF f}.
 #[global] Hint Extern 0 (ProperFilter _^'+) =>
   (apply: at_right_proper_filter) : typeclass_instances.
 
+Lemma continuous_comp_cvg {R : numFieldType} (U V : pseudoMetricNormedZmodType R)
+  (f : U -> V) (g : R -> U) (r : R) (l : V) : continuous f ->
+  (f \o g) x @[x --> r] --> l -> f x @[x --> g r] --> l.
+Proof.
+move=> cf fgl; apply/(@cvgrPdist_le _ V) => /= e e0.
+have e20 : 0 < e / 2 by rewrite divr_gt0.
+move/(@cvgrPdist_le _ V) : fgl => /(_ _ e20) fgl.
+have /(@cvgrPdist_le _ V) /(_ _ e20) fgf := cf (g r).
+rewrite !near_simpl/=; near=> t.
+rewrite -(@subrK _ (f (g r)) l) -(addrA (_ + _)) (le_trans (ler_normD _ _))//.
+rewrite (splitr e) lerD//; last by near: t.
+by case: fgl => d /= d0; apply; rewrite /ball_/= subrr normr0.
+Unshelve. all: by end_near. Qed.
+
 Section closure_left_right_open.
 Variable R : realFieldType.
 Implicit Types z : R.