beta distribution #1640
beta distribution #1640
Conversation
affeldt-aist
force-pushed
the
probability_20250605
branch
from
02ba384 to
c59f7db
Compare
|
ping @hoheinzollern |
affeldt-aist
force-pushed
the
probability_20250605
branch
from
c59f7db to
d687620
Compare
|
@hoheinzollern changelog and doc are complete (hopefully) |
|
ping @hoheinzollern |
| 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. |
There was a problem hiding this comment.
This is a weirdly specific lemma with a generic name, I would fix the naming first.
Also, you might not need the two hypotheses (n <= x)%N and (m <= y)%N.
| 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. |
There was a problem hiding this comment.
Similarly, you might be able to drop the two assumptions. This suggests that the previous lemma is a subproof of leq_fact2
| Lemma derive1_onem {R : numFieldType} : | ||
| (fun x => 1 - x : R^o)^`()%classic = cst (-1). |
There was a problem hiding this comment.
onem typically recalls the syntax ``1-`, why is it not being used here?
| (*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.*) | ||
|
|
There was a problem hiding this comment.
Commented code, either remove or add a human-readable comment for why this is here still.
| (*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.*) | ||
|
|
| by rewrite Rintegral_mkcond. | ||
| Qed. | ||
|
|
||
| Lemma beta_funSS a b : beta_fun a.+1 b.+1 = |
There was a problem hiding this comment.
Similarly, neither this nor the previous lemma name suggests what variable is being incremented. Proposal: SaSb? though I'm not fully satisfied either.
| Let int_beta_pdf01 : (\int[mu]_(x in `[0%R, 1%R]) (beta_pdf x)%:E = | ||
| \int[mu]_x (beta_pdf x)%:E :> \bar R)%E. |
There was a problem hiding this comment.
Similarly, there should be no need for %E
| under eq_integral. | ||
| move=> /= x _. | ||
| rewrite ger0_norm//; last by rewrite beta_pdf_ge0. | ||
| over. |
There was a problem hiding this comment.
| under eq_integral. | |
| move=> /= x _. | |
| rewrite ger0_norm//; last by rewrite beta_pdf_ge0. | |
| over. | |
| under eq_integral=> /= x _ do rewrite ger0_norm ?beta_pdf_ge0//. |
should work?
|
|
||
| End beta_pdf. | ||
|
|
||
| (* TODO: move? *) |
| (\int[beta_prob a b]_(x in U) f x = | ||
| \int[mu]_(x in U) (f x * (beta_pdf a b x)%:E))%E. |
There was a problem hiding this comment.
| (\int[beta_prob a b]_(x in U) f x = | |
| \int[mu]_(x in U) (f x * (beta_pdf a b x)%:E))%E. | |
| \int[beta_prob a b]_(x in U) f x = | |
| \int[mu]_(x in U) (f x * (beta_pdf a b x)%:E). |
2 participants
Motivation for this change
Checklist
CHANGELOG_UNRELEASED.mdReference: How to document
Merge policy
As a rule of thumb:
all compile are preferentially merged into master.
Reminder to reviewers