beta distribution

CHANGELOG_UNRELEASED.md

@@ -58,6 +58,50 @@
   + `measurable_function.v`
   + `measure.v`
 
+- 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_fun1S`, `beta_fun11`, `beta_funSSS`, `beta_funSS`, `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`
+  + lemma `invr_nonneg_proof`, definition `invr_nonneg`
+  + 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_prod2`, `leq_fact2`, `normr_onem`
+
 ### Changed
 
 - in `lebesgue_stieltjes_measure.v` specialized from `numFieldType` to `realFieldType`:
@@ -305,6 +349,14 @@
 
 ### Renamed
 
+
+- 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`
+
 ### Generalized
 
 - in `pseudometric_normed_Zmodule.v`:

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_prod2 (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_prod2.
+Qed.
+
 Section max_min.
 Variable R : realFieldType.
 
@@ -280,6 +309,14 @@ Qed.
 End onem.
 Notation "`1- r" := (onem r) : ring_scope.
 
+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).
@@ -1332,13 +1338,26 @@ rewrite scalerA -scalerDl mulrCA -[f x * _]exprS.
 by rewrite [in LHS]mulr_natl exprfctE -mulrSr mulr_natl.
 Qed.
 
+(*Global Instance is_deriveX f n x v (df : R) :
+  is_derive x v f df -> is_derive x v (f ^+ n.+1) ((n.+1%:R * f x ^+n) *: df).
+Proof.
+move=> dfx; elim: n => [|n ihn]; first by rewrite expr1 expr0 mulr1 scale1r.
+rewrite exprS; apply: is_derive_eq.
+rewrite scalerA -scalerDl mulrCA -[f x * _]exprS.
+by rewrite [in LHS]mulr_natl exprfctE -mulrSr mulr_natl.
+Qed.*)
+
 Lemma derivableX f n x v : derivable f x v -> derivable (f ^+ n) x v.
 Proof. by case: n => [_|n /derivableP]; [rewrite expr0|]. Qed.
 
 Lemma deriveX f n x v : derivable f x v ->
   'D_v (f ^+ n) x = (n%:R * f x ^+ n.-1) *: 'D_v f x.
 Proof. by move=> /derivableP df; rewrite derive_val. Qed.
 
+(*Lemma deriveX f n x v : derivable f x v ->
+  'D_v (f ^+ n.+1) x = (n.+1%:R * f x ^+ n) *: 'D_v f x.
+Proof. by move=> /derivableP df; rewrite derive_val. Qed.*)
+
 Fact der_inv f x v : f x != 0 -> derivable f x v ->
   (fun h => h^-1 *: (((fun y => (f y)^-1) \o shift x) (h *: v) - (f x)^-1)) @
   0^' --> - (f x) ^-2 *: 'D_v f x.

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)%R, 1%R]) (G (1 - x))%:E).
+Proof.
+move=> r01 cG.
+have := @integration_by_substitution_decreasing R (fun x => 1 - x)%R G (1 - r) 1.
+rewrite subKr subrr => -> //.
+- 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 subKr.
+    apply: (@continuous_comp_cvg _ R^o R^o _ (fun x => 1 - x)%R)=> //=.
+      by move=> x; apply: (@continuousB _ R^o)  => //; exact: cvg_cst.
+    by under eq_fun do rewrite subKr; exact: cvg_id.
+  + by apply: cvg_at_left_filter; apply: (@cvgB _ R^o) => //; 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, r]) (G x) =
+  \int[mu]_(x in `[(1 - r)%R, 1%R]) (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.