changelog

Author: affeldt-aist

CHANGELOG_UNRELEASED.md

@@ -57,11 +57,7 @@
   + `measure_extension.v`
   + `measurable_function.v`
   + `measure.v`
-- in `lebesgue_integral_theory/lebesgue_integral_nonneg.v`:
-  + lemmas `ge0_nondecreasing_set_nondecreasing_integral`,
-           `ge0_nondecreasing_set_cvg_integral`,
-           `le0_nondecreasing_set_nonincreasing_integral`,
-	   `le0_nondecreasing_set_cvg_integral`
+
 - in `pseudometric_normed_Zmodule.v`:
   + lemma `continuous_comp_cvg`
 
@@ -71,6 +67,41 @@
 - 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`:
@@ -318,19 +349,6 @@
 
 ### Renamed
 
-- in `measure.v`
-  + definition `ess_sup` moved to `ess_sup_inf.v`
-
-- in `convex.v`
-  + lemma `conv_gt0` to `convR_gt0`
-- in `tvs.v`
-  + HB class `TopologicalNmodule` moved to `PreTopologicalNmodule`
-  + HB class `TopologicalZmodule` moved to `PreTopologicalZmodule`
-  + HB class `TopologicalLmodule` moved to `PreTopologicalLmodule`
-  + structure `topologicalLmodule` moved to `preTopologicalLmodule`
-  + HB class `UniformNmodule` moved to `PreUniformNmodule`
-  + HB class `UniformZmodule` moved to `PreUniformZmodule`
-  + HB class `UniformLmodule` moved to `PreUniformLmodule`
 
 - in `probability.v`:
   + `bernoulli` -> `bernoulli_prob`

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.