From ef176a0cc8c2a46090e9048d69e8f17d41d5e381 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Fri, 5 Jun 2026 14:53:11 +0900 Subject: [PATCH 1/4] wip --- theories/lebesgue_measure.v | 4 +-- theories/lebesgue_stieltjes_measure.v | 38 +++++++++++++++++---------- 2 files changed, 26 insertions(+), 16 deletions(-) diff --git a/theories/lebesgue_measure.v b/theories/lebesgue_measure.v index 327961a2ff..52acd297f5 100644 --- a/theories/lebesgue_measure.v +++ b/theories/lebesgue_measure.v @@ -336,9 +336,9 @@ End hlength_extension. End LebesgueMeasure. -Definition lebesgue_measure {R : realType} : - set (measurableTypeR R) -> \bar R := +Definition lebesgue_measure {R : realType} : set R -> \bar R := lebesgue_stieltjes_measure idfun. +Check fun R : realType => lebesgue_stieltjes_measure idfun : Measure.type _ _. HB.instance Definition _ (R : realType) := Measure.on (@lebesgue_measure R). HB.instance Definition _ (R : realType) := SigmaFiniteMeasure.on (@lebesgue_measure R). diff --git a/theories/lebesgue_stieltjes_measure.v b/theories/lebesgue_stieltjes_measure.v index cd14543440..d8b5f4ff41 100644 --- a/theories/lebesgue_stieltjes_measure.v +++ b/theories/lebesgue_stieltjes_measure.v @@ -513,14 +513,34 @@ Definition measurableTypeR (R : realType) := Section lebesgue_stieltjes_measure. Context {R : realType}. -Variable f : cumulative R R. + +Definition lebesgue_display : measure_display := + (R.-ocitv.-measurable).-sigma. +Definition measurableR : set (set R) := + (R.-ocitv.-measurable).-sigma.-measurable. + +HB.instance Definition _ := Pointed.on R. +HB.instance Definition _ := Choice.on (measurableTypeR R). +HB.instance Definition _ := + @isMeasurable.Build lebesgue_display (measurableTypeR R) measurableR + measurable0 (@measurableC _ _) (@bigcupT_measurable _ _). +HB.instance Definition _ := Measurable.copy R (measurableTypeR R). +(*HB.instance (Real.sort R) R_isMeasurable.*) + +Lemma measurableTypeRE : R = g_sigma_algebraType (R.-ocitv.-measurable) + :> measurableType lebesgue_display. +Proof. Admitted. Lemma lebesgue_stieltjes_measure_unique - (mu : {measure set (measurableTypeR R) -> \bar R}) : + (f : cumulative R R) (mu : {measure set R -> \bar R}) : (forall X, ocitv X -> lebesgue_stieltjes_measure f X = mu X) -> - forall A, measurable A -> lebesgue_stieltjes_measure f A = mu A. + forall A : set R, measurable A -> lebesgue_stieltjes_measure f A = mu A. Proof. -move=> muE A mA; apply: measure_extension_unique => //=. +move=> muE A mA. +have @mu' : {measure set (g_sigma_algebraType R.-ocitv.-measurable) -> \bar R}. + rewrite {muE A mA f} -measurableTypeRE. +have := @measure_extension_unique _ _ _ _ _ mu. + apply: measure_extension_unique => //=. exact: wlength_sigma_finite. by move=> X mX; rewrite -muE// -measurable_mu_extE. Qed. @@ -551,16 +571,6 @@ Arguments completed_lebesgue_stieltjes_measure {R}. Section salgebra_R_ssets. Variable R : realType. -Definition measurableR : set (set R) := - (R.-ocitv.-measurable).-sigma.-measurable. - -HB.instance Definition _ := Pointed.on R. -HB.instance Definition R_isMeasurable : - isMeasurable default_measure_display R := - @isMeasurable.Build _ (measurableTypeR R) measurableR - measurable0 (@measurableC _ _) (@bigcupT_measurable _ _). -(*HB.instance (Real.sort R) R_isMeasurable.*) - Lemma measurable_set1 (r : R) : measurable [set r]. Proof. rewrite set1_bigcap_oc; apply: bigcap_measurable => // k _. From 7a7a1c57e8b5e32b5c1c8224d09528936a290d72 Mon Sep 17 00:00:00 2001 From: Cyril Cohen Date: Fri, 5 Jun 2026 17:53:21 +0900 Subject: [PATCH 2/4] Keeping definitionally identical display on R --- theories/ftc.v | 6 ++---- .../lebesgue_integral_differentiation.v | 10 ++++----- theories/lebesgue_measure.v | 4 ++-- theories/lebesgue_stieltjes_measure.v | 21 ++++++------------- theories/measurable_realfun.v | 2 +- 5 files changed, 16 insertions(+), 27 deletions(-) diff --git a/theories/ftc.v b/theories/ftc.v index 59fdcaa715..f71ec3f11f 100644 --- a/theories/ftc.v +++ b/theories/ftc.v @@ -281,8 +281,7 @@ Corollary FTC1 f a : {ae mu, forall x, a < BRight x -> derivable F x 1 /\ F^`() x = f x}. Proof. move=> intf locf F; move: (locf) => /lebesgue_differentiation. -apply: filterS; first exact: (ae_filter_ringOfSetsType mu). -move=> i fi ai. +apply: filterS => i fi ai. by apply: (@FTC1_lebesgue_pt _ _ _ (i + 1)%R) => //; rewrite ltrDl. Qed. @@ -292,8 +291,7 @@ Corollary FTC1Ny f : let F x := (\int[mu]_(t in [set` `]-oo, x]]) (f t))%R in {ae mu, forall x, derivable F x 1 /\ F^`() x = f x}. Proof. -move=> intf locf F; have := FTC1 intf locf. -apply: filterS; first exact: (ae_filter_ringOfSetsType mu). +move=> intf locf F; have := FTC1 intf locf; apply: filterS. by move=> r /=; apply; rewrite ltNyr. Qed. diff --git a/theories/lebesgue_integral_theory/lebesgue_integral_differentiation.v b/theories/lebesgue_integral_theory/lebesgue_integral_differentiation.v index 4536324d23..233538111b 100644 --- a/theories/lebesgue_integral_theory/lebesgue_integral_differentiation.v +++ b/theories/lebesgue_integral_theory/lebesgue_integral_differentiation.v @@ -1016,14 +1016,14 @@ have incl n : Ee `<=` B k `&` (HLf_g_Be n `|` f_g_Be n) by move=> ?; apply. near \oo => n. rewrite (@le_trans _ _ (mu (B k `&` (HLf_g_Be n `|` f_g_Be n))))//. rewrite le_measure// inE//; apply: measurableI; first exact: measurable_ball. - by apply: measurableU => //; [exact: mEHL|exact: mfge]. + by apply: measurableU => //; exact: mfge. rewrite (@le_trans _ _ ((4 / (e / 2))%:E * n.+1%:R^-1%:E))//. rewrite (@le_trans _ _ (mu (HLf_g_Be n `|` f_g_Be n)))//. rewrite le_measure// inE//. apply: measurableI => //. - by apply: measurableU => //; [exact: mEHL|exact: mfge]. - by apply: measurableU => //; [exact: mEHL|exact: mfge]. - rewrite (le_trans (measureU2 _ _ _))//=; [exact: mEHL|exact: mfge|]. + by apply: measurableU => //; exact: mfge. + by apply: measurableU => //; exact: mfge. + rewrite (le_trans (measureU2 _ _ _))//=. apply: le_trans; first by apply: leeD; [exact: HL_null|exact: fgn_null]. rewrite -muleDl// lee_pmul2r// -EFinD lee_fin -{2}(mul1r (_^-1)%R). by rewrite -mulrDl natr1. @@ -1109,7 +1109,7 @@ Lemma lebesgue_density (A : set R) : measurable A -> @[r --> 0^'+] --> (\1_A x)%:E}. Proof. move=> mA; have := lebesgue_differentiation (locally_integrable_indic openT mA). -apply: filter_app; first exact: (ae_filter_ringOfSetsType mu). +apply: filter_app. apply: aeW => /= x Ax. apply: (sube_cvg0 _ _).1 => //. move: Ax; rewrite /lebesgue_pt /davg /= -/mu => Ax. diff --git a/theories/lebesgue_measure.v b/theories/lebesgue_measure.v index 52acd297f5..92c0fe2910 100644 --- a/theories/lebesgue_measure.v +++ b/theories/lebesgue_measure.v @@ -989,7 +989,7 @@ have : mu \o Dn @ \oo --> mu (\bigcup_n Dn n). rewrite -setI_bigcupr; rewrite bigcup_itvT setIT. have finDn n : mu (Dn n) \is a fin_num. rewrite ge0_fin_numE// (le_lt_trans _ Dfin)//. - by rewrite le_measure// ?inE//=; [exact: mDn|exact: subIsetl]. + by rewrite le_measure// ?inE//=; exact: subIsetl. have finD : mu D \is a fin_num by rewrite fin_num_abs gee0_abs. rewrite -[mu D]fineK// => /fine_cvg/(_ (interior (ball (fine (mu D)) eps)))[]. exact/nbhs_interior/nbhsx_ballx. @@ -1001,7 +1001,7 @@ have finDDn : mu D - mu (Dn n) \is a fin_num by rewrite ?fin_numB ?finD /= ?(finDn n). rewrite -fine_abse // gee0_abs ?sube_ge0 ?finD ?(finDn _) //; last first. by rewrite -[_ - _]fineK // lte_fin fine. -by rewrite le_measure// ?inE//; [exact: measurableI |exact: subIsetl]. +by rewrite le_measure// ?inE//; exact: subIsetl. Qed. Lemma lebesgue_regularity_inner (D : set R) (eps : R) : diff --git a/theories/lebesgue_stieltjes_measure.v b/theories/lebesgue_stieltjes_measure.v index d8b5f4ff41..be715f4337 100644 --- a/theories/lebesgue_stieltjes_measure.v +++ b/theories/lebesgue_stieltjes_measure.v @@ -519,28 +519,19 @@ Definition lebesgue_display : measure_display := Definition measurableR : set (set R) := (R.-ocitv.-measurable).-sigma.-measurable. -HB.instance Definition _ := Pointed.on R. -HB.instance Definition _ := Choice.on (measurableTypeR R). -HB.instance Definition _ := - @isMeasurable.Build lebesgue_display (measurableTypeR R) measurableR - measurable0 (@measurableC _ _) (@bigcupT_measurable _ _). +HB.instance Definition _ : Measurable lebesgue_display (measurableTypeR R) := + Measurable.on (measurableTypeR R). +(* Presumably it is safe to use NFI here because morally R is unique + and nothing else can be used here*) +#[non_forgetful_inheritance] HB.instance Definition _ := Measurable.copy R (measurableTypeR R). -(*HB.instance (Real.sort R) R_isMeasurable.*) - -Lemma measurableTypeRE : R = g_sigma_algebraType (R.-ocitv.-measurable) - :> measurableType lebesgue_display. -Proof. Admitted. Lemma lebesgue_stieltjes_measure_unique (f : cumulative R R) (mu : {measure set R -> \bar R}) : (forall X, ocitv X -> lebesgue_stieltjes_measure f X = mu X) -> forall A : set R, measurable A -> lebesgue_stieltjes_measure f A = mu A. Proof. -move=> muE A mA. -have @mu' : {measure set (g_sigma_algebraType R.-ocitv.-measurable) -> \bar R}. - rewrite {muE A mA f} -measurableTypeRE. -have := @measure_extension_unique _ _ _ _ _ mu. - apply: measure_extension_unique => //=. +move=> muE A mA; apply: measure_extension_unique => //=. exact: wlength_sigma_finite. by move=> X mX; rewrite -muE// -measurable_mu_extE. Qed. diff --git a/theories/measurable_realfun.v b/theories/measurable_realfun.v index 75565ec051..28095e43ed 100644 --- a/theories/measurable_realfun.v +++ b/theories/measurable_realfun.v @@ -1088,7 +1088,7 @@ split=> [|f g|f g]; rewrite !inE/=. - exact: measurable_funM. Qed. HB.instance Definition _ := GRing.isSubringClosed.Build _ - (@mfun d default_measure_display aT rT) mfun_subring_closed. + (@mfun d lebesgue_display aT rT) mfun_subring_closed. HB.instance Definition _ := [SubChoice_isSubComPzRing of {mfun aT >-> rT} by <:]. From be508d275c4056fffa3f1f8695d4c141a9760d31 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Mon, 8 Jun 2026 14:51:02 +0900 Subject: [PATCH 3/4] test file --- theories/probability_theory/test.v | 353 +++++++++++++++++++++++++++++ 1 file changed, 353 insertions(+) create mode 100644 theories/probability_theory/test.v diff --git a/theories/probability_theory/test.v b/theories/probability_theory/test.v new file mode 100644 index 0000000000..7f5b16a8ea --- /dev/null +++ b/theories/probability_theory/test.v @@ -0,0 +1,353 @@ +(**md**************************************************************************) +(* # Gaussian-Gaussian conjugate prior *) +(* *) +(* Stated against mathcomp-analysis' [normal_prob m s] (mean [m], standard *) +(* deviation [s]) from [probability_theory/normal_distribution.v]. *) +(* *) +(* For prior [theta ~ normal_prob mu0 sigma0] and Gaussian likelihood *) +(* [X | theta ~ normal_prob theta sigma], the posterior of [theta] given *) +(* [X = x] is itself Gaussian, [normal_prob (mu_post ..) (sigma_post ..)]. *) +(* *) +(* ``` *) +(* sigma_post sigma0 sigma *) +(* := Num.sqrt (sigma0^+2 * sigma^+2 / (sigma0^+2 + sigma^+2)) *) +(* mu_post mu0 sigma0 x sigma *) +(* := (sigma^+2 * mu0 + sigma0^+2 * x) / (sigma0^+2 + sigma^+2) *) +(* *) +(* normal_pdf_conjugate == *) +(* sigma0 != 0 -> sigma != 0 -> *) +(* normal_pdf theta sigma x * normal_pdf mu0 sigma0 theta *) +(* = normal_pdf mu0 (Num.sqrt (sigma0^+2 + sigma^+2)) x *) +(* * normal_pdf (mu_post ..) (sigma_post ..) theta. *) +(* normal_prob_conjugate == *) +(* \int[normal_prob mu0 sigma0]_(theta in V) normal_pdf theta sigma x *) +(* / \int[normal_prob mu0 sigma0]_theta normal_pdf theta sigma x *) +(* = normal_prob (mu_post ..) (sigma_post ..) V. *) +(* ``` *) +(* *) +(* The main theorem is Bayes' rule integrated over [V]: the prior is the *) +(* integration measure, the likelihood [p(x | theta)] is the integrand, and *) +(* the marginal evidence [p(x)] in the denominator is computed as the total *) +(* integral of the likelihood against the prior (no closed-form Gaussian *) +(* density appears in the statement). The marginal factor cancels in the *) +(* quotient, so its explicit value (a Gaussian by [normal_probD] from *) +(* mathcomp/analysis PR #1955) plays no role -- the load-bearing step is the *) +(* pointwise "complete the square" identity [normal_pdf_conjugate]. *) +(******************************************************************************) + +From HB Require Import structures. +From mathcomp Require Import all_boot all_order ssralg ssrnum ssrint interval. +From mathcomp Require Import archimedean finmap interval_inference. +From mathcomp Require Import boolp classical_sets functions cardinality fsbigop. +From mathcomp Require Import reals ereal topology normedtype sequences derive. +From mathcomp Require Import measure exp trigo numfun realfun. +From mathcomp Require Import measurable_realfun lebesgue_measure. +From mathcomp Require Import lebesgue_integral ftc gauss_integral. +From mathcomp Require Import probability_theory.random_variable. +From mathcomp Require Import probability_theory.normal_distribution. +From mathcomp Require Import ring lra. + +Set Implicit Arguments. +Unset Strict Implicit. +Unset Printing Implicit Defensive. + +Import Order.TTheory GRing.Theory Num.Def Num.Theory. +Import numFieldTopology.Exports. + +Reserved Notation "'\Pr_' mu '[' V '|' lik ']'" + (at level 0, V at level 0, lik at level 0, mu at level 0, + format "'\Pr_' mu [ V | lik ]"). + +Local Open Scope classical_set_scope. +Local Open Scope ring_scope. + +(** ** Vendored from mathcomp/analysis PR #1955 + + [integral_normal_prob] is the Radon-Nikodym change-of-variables for + [normal_prob], copied (statement only) from + [theories/probability_theory/normal_distribution.v] on branch + [normal_20260426] of [affeldt-aist/analysis]. Delete this section + when PR #1955 lands. *) +Section vendored_pr1955. +Context {R : realType}. +Local Open Scope ereal_scope. + +Lemma integral_normal_prob (m s : R) (f : R -> \bar R) (U : set R) : + measurable U -> + (normal_prob m s).-integrable U f -> + \int[normal_prob m s]_(x in U) f x + = \int[lebesgue_measure]_(x in U) (f x * (normal_pdf m s x)%:E). +Proof. Admitted. + +End vendored_pr1955. + +(** ** Bayes posterior probability + + Generic measure-theoretic formulation of Bayes' rule. Given a prior + measure [mu] on the parameter space and a likelihood [lik : R -> R] + -- the density of the observation, viewed as a function of the + parameter (i.e., [lik theta = p(observation | theta)]) -- the + posterior probability of a measurable set [V] of parameters is + [(integral over V of lik against mu) / (total integral of lik + against mu)]. Independent of the conjugate-prior application + below; suitable for placement in [probability_theory/]. *) +Section bayes_posterior. +Context {d : measure_display} {T : measurableType d} {R : realType}. +Local Open Scope ereal_scope. + +Definition bayes_posterior + (mu : {measure set T -> \bar R}) (lik : T -> R) (V : set T) : \bar R := + (\int[mu]_(theta in V) (lik theta)%:E) + / (\int[mu]_theta (lik theta)%:E). + +End bayes_posterior. + +Notation "'\Pr_' mu '[' V '|' lik ']'" := (bayes_posterior mu lik V) + : ereal_scope. + +Section gaussian_conjugate. +Context {R : realType}. +Implicit Types (sigma x theta : R) (V : set R). + +(** Posterior standard deviation; squared: + [sigma0^2 * sigma^2 / (sigma0^2 + sigma^2)]. *) +Definition sigma_post (sigma0 sigma : R) : R := + Num.sqrt (sigma0 ^+ 2 * sigma ^+ 2 / (sigma0 ^+ 2 + sigma ^+ 2)). + +(** Posterior mean given observation [x]. *) +Definition mu_post (mu0 sigma0 x sigma : R) : R := + (sigma ^+ 2 * mu0 + sigma0 ^+ 2 * x) / (sigma0 ^+ 2 + sigma ^+ 2). + +(** "Complete the square": the joint density [p(x | theta) * p(theta)] + factors as [K(x) * p_posterior(theta | x)] for some [theta]-independent + factor [K(x)]. Pure [R]-side algebraic identity, established by: + rewriting both [normal_pdf] calls on each side via [normal_pdfE] into + a [normal_peak] match (closed by [sqrtrM] / [invfM] + [field] under + positivity) and a [normal_fun] match (the exponents combine via + [expRD]; equating them is the actual "complete the square" polynomial + identity in [theta], discharged by [field] under the sign + hypotheses). Concretely, [K(x) = normal_pdf mu0 (Num.sqrt + (sigma0^+2 + sigma^+2)) x], but the value is irrelevant to the main + theorem since it cancels in the Bayes quotient. *) +Lemma normal_pdf_conjugate mu0 sigma0 sigma x theta : + sigma0 != 0 -> sigma != 0 -> + normal_pdf theta sigma x * normal_pdf mu0 sigma0 theta + = normal_pdf mu0 (Num.sqrt (sigma0 ^+ 2 + sigma ^+ 2)) x + * normal_pdf (mu_post mu0 sigma0 x sigma) + (sigma_post sigma0 sigma) theta. +Proof. +move=> sigma0_neq0 sigma_neq0. +have sigma0_2pos : 0 < sigma0 ^+ 2 by rewrite exprn_even_gt0. +have sigma_2pos : 0 < sigma ^+ 2 by rewrite exprn_even_gt0. +have sumpos : 0 < sigma0 ^+ 2 + sigma ^+ 2 by apply: addr_gt0. +have sum_neq0 : sigma0 ^+ 2 + sigma ^+ 2 != 0 by rewrite lt0r_neq0. +have sqrt_sum_neq0 : Num.sqrt (sigma0 ^+ 2 + sigma ^+ 2) != 0 + by rewrite sqrtr_eq0 -ltNge. +have sigma_post_pos : 0 < sigma_post sigma0 sigma. + rewrite /sigma_post sqrtr_gt0; apply: divr_gt0 => //. + by apply: mulr_gt0. +have sigma_post_neq0 : sigma_post sigma0 sigma != 0 by rewrite lt0r_neq0. +rewrite !normal_pdfE // mulrACA [RHS]mulrACA. +congr (_ * _); first last. + rewrite /normal_fun -2!expRD; congr (expR _). + rewrite sqr_sqrtr; last exact: ltW sumpos. + rewrite /sigma_post sqr_sqrtr; first last. + apply: divr_ge0; first by apply: mulr_ge0; exact: ltW. + exact: ltW. + rewrite /mu_post; field. + by apply/and3P; split. +have sigmapi2_ge0 : 0 <= sigma ^+ 2 * pi *+ 2 + by apply: mulrn_wge0; apply: mulr_ge0; + [exact: ltW sigma_2pos | exact: pi_ge0]. +have sigma0pi2_ge0 : 0 <= sigma0 ^+ 2 * pi *+ 2 + by apply: mulrn_wge0; apply: mulr_ge0; + [exact: ltW sigma0_2pos | exact: pi_ge0]. +have sumpi2_ge0 : 0 <= (sigma0 ^+ 2 + sigma ^+ 2) * pi *+ 2 + by apply: mulrn_wge0; apply: mulr_ge0; + [exact: ltW sumpos | exact: pi_ge0]. +have sqsum_eq : + Num.sqrt (sigma0 ^+ 2 + sigma ^+ 2) ^+ 2 = sigma0 ^+ 2 + sigma ^+ 2 + by rewrite sqr_sqrtr // ltW. +have sqpost_eq : sigma_post sigma0 sigma ^+ 2 + = sigma0 ^+ 2 * sigma ^+ 2 / (sigma0 ^+ 2 + sigma ^+ 2). + rewrite /sigma_post sqr_sqrtr //. + apply: divr_ge0; first by apply: mulr_ge0; exact: ltW. + exact: ltW. +rewrite /normal_peak sqsum_eq sqpost_eq -invfM -[RHS]invfM -!sqrtrM //. +congr GRing.inv; congr Num.sqrt; field. +exact: sum_neq0. +Qed. + +(** Integrability of the likelihood-as-function-of-theta against the + prior. Pdf values are in [[0, normal_peak sigma]], so the integrand + is bounded, and [normal_prob] is a probability measure, hence + finite. Local because used only in [normal_prob_conjugate]. *) +Local Lemma integrable_normal_pdf_likelihood mu0 sigma0 sigma x V : + sigma != 0 -> measurable V -> + (normal_prob mu0 sigma0).-integrable V + (fun theta => (normal_pdf theta sigma x)%:E). +Proof. +move=> sigma_neq0 mV. +have pdf_sym theta : normal_pdf theta sigma x = normal_pdf x sigma theta. + rewrite !normal_pdfE //; congr (_ * _). + by rewrite /normal_fun -[in LHS](opprB theta x) sqrrN. +have -> : + (fun theta : R => (normal_pdf theta sigma x)%:E) + = (fun theta : R => (normal_pdf x sigma theta)%:E) + by apply/funext => theta; rewrite pdf_sym. +change ((normal_prob mu0 sigma0).-integrable V (EFin \o normal_pdf x sigma)). +apply: (measurable_bounded_integrable + (mu := normal_prob mu0 sigma0) + (f := normal_pdf x sigma) mV). +- apply: le_lt_trans; first exact: probability_le1. + by rewrite ltey. +- by apply: measurable_funTS; exact: measurable_normal_pdf. +- exists (normal_peak sigma); split; first by rewrite num_real. + move=> y ynp theta _. + rewrite /= ger0_norm; last exact: normal_pdf_ge0. + exact: le_trans (normal_pdf_ub _ _ sigma_neq0) (ltW ynp). +Qed. + +(** ** Main theorem *) + +(** Gaussian-Gaussian conjugate prior: the posterior of [theta] given + [X = x] is a single Gaussian [normal_prob (mu_post ..) (sigma_post ..)]. + + Reading the equation. The LHS is Bayes' rule [p(theta | x) = + p(x | theta) p(theta) / p(x)] integrated over [V]: + - [normal_prob mu0 sigma0] (integration measure) is the *prior*; + - [normal_pdf theta sigma x] (integrand) is the *likelihood* + density [p(x | theta)]; + - the *marginal* evidence [p(x)] in the denominator is computed as + the total integral of the likelihood against the prior -- no + closed-form Gaussian density appears in the statement. *) +Lemma normal_prob_conjugate mu0 sigma0 sigma x V : + sigma0 != 0 -> sigma != 0 -> measurable V -> + (\Pr_(normal_prob mu0 sigma0) + [V | fun theta => normal_pdf theta sigma x] + = normal_prob (mu_post mu0 sigma0 x sigma) + (sigma_post sigma0 sigma) V)%E. +Proof. +move=> sigma0_neq0 sigma_neq0 mV. +set tmp : {measure set (measurableTypeR R) -> \bar R} := normal_prob _ _. +rewrite /bayes_posterior /=. +pose K := normal_pdf mu0 (Num.sqrt (sigma0 ^+ 2 + sigma ^+ 2)) x. +pose P := normal_prob (mu_post mu0 sigma0 x sigma) + (sigma_post sigma0 sigma) V. +have sigma0sigma_neq0 : Num.sqrt (sigma0 ^+ 2 + sigma ^+ 2) != 0. + rewrite sqrtr_eq0 -ltNge; apply: addr_gt0; rewrite exprn_even_gt0 //=. +have Kpos : 0 < K. + rewrite /K normal_pdfE //; apply: mulr_gt0. + by rewrite normal_peak_gt0. + by rewrite /normal_fun expR_gt0. +have KEneq0 : (K%:E != 0)%E by rewrite eqe; apply: lt0r_neq0. +have num_eq : + (\int[normal_prob mu0 sigma0]_(theta in V) (normal_pdf theta sigma x)%:E + = K%:E * P)%E. + rewrite integral_normal_prob //; + last exact: integrable_normal_pdf_likelihood. + under eq_integral => theta _ do + rewrite -EFinM + (normal_pdf_conjugate mu0 x theta sigma0_neq0 sigma_neq0) + EFinM. + rewrite -/K ge0_integralZl_EFin //=; first last. + - exact: ltW. + - apply/measurable_EFinP/measurable_funTS; exact: measurable_normal_pdf. + - by move=> theta _; rewrite lee_fin; exact: normal_pdf_ge0. +have denom_eq : + (\int[normal_prob mu0 sigma0]_theta (normal_pdf theta sigma x)%:E + = K%:E)%E. + rewrite integral_normal_prob //; + last exact: integrable_normal_pdf_likelihood. + under eq_integral => theta _ do + rewrite -EFinM + (normal_pdf_conjugate mu0 x theta sigma0_neq0 sigma_neq0) + EFinM. + rewrite -/K ge0_integralZl_EFin //=; first last. + - exact: ltW. + - apply/measurable_EFinP/measurable_funTS; exact: measurable_normal_pdf. + - by move=> theta _; rewrite lee_fin; exact: normal_pdf_ge0. + by rewrite integral_normal_pdf // mule1. +by rewrite num_eq denom_eq muleAC divee // mul1e. +Qed. + +End gaussian_conjugate. + +(** ** Random-variable-style restatement + + Sugar over the measure-theoretic statement above. Given a random + variable [X] on a probability space [P] with [X \~ N(mu0, sigma0)] + and a likelihood family [lik t y = p(Y = y | X = t)] (the Gaussian + case is [lik = normal_pdf ^~ sigma]), the conditional distribution + [\Pr[X | lik = y]] -- computed via Bayes' rule -- is the Gaussian + posterior. + + [\Pr[X | lik = y] \~ D] is shorthand for "the Bayes posterior under + prior [distribution P X] and likelihood [lik^~ y] agrees with [D] + on all measurable sets". The proof of the RV-style statement is + just one [rewrite] using the [X \~ _] hypothesis followed by the + underlying [normal_prob_conjugate]. *) + +Section gaussian_conjugate_RV. +Context {d : measure_display} {T : measurableType d} {R : realType}. +Variable P : pprobability T R. + +Local Notation "X '\~' D" := (distribution P X = D) + (at level 70). + +Local Notation "'\Pr[' X '|' F 'at' y ']' '\~' D" := + (forall V, measurable V -> + (bayes_posterior (distribution P X) (F^~ y) V = D V)%E) + (at level 70, X at next level, F at next level, y at next level). + +(** **Note: canonical-structure obstacle.** + + The proof below should be one line: + [move=> _ _ HX HL V mV; rewrite HX HL; exact: normal_prob_conjugate.] + After [rewrite HX HL], the goal is *syntactically* the conclusion + of [normal_prob_conjugate]. But [exact:] still fails because + [{RV P >-> R}] in [distribution P X] picks the *default* canonical + measurable structure on [R] ([Real_sort__canonical__measurable_ + structure_Measurable]), while [normal_prob] integrates over [R] + viewed with the *ocitv* canonical structure ([lebesgue_stieltjes_ + measure_ocitv_type__canonical__measurable_structure_Measurable]). + These two canonical instances are propositionally the same Borel + sigma-algebra on [R] but Coq does not unify them. Resolving this + is an upstream issue in mathcomp-analysis (unify R's canonical + measurable structure, or add a transfer lemma between the two). *) +Theorem normal_prob_conjugate_RV + (X : {RV P >-> R}) (mu0 sigma0 sigma y : R) : + sigma0 != 0%R -> sigma != 0%R -> + X \~ normal_prob mu0 sigma0 -> + \Pr[X | (fun x => normal_pdf x sigma) at y] + \~ normal_prob (mu_post mu0 sigma0 y sigma) (sigma_post sigma0 sigma). +Proof. +move=> S00 S0 HX V mV. +rewrite /bayes_posterior/=. +rewrite -normal_prob_conjugate//. +rewrite /bayes_posterior. +rewrite -HX. +congr (_ / _)%E => //. + simpl. + rewrite HX//. + rewrite /bayes_posterior. + set tmp := normal_prob _ _. +(*Set Printing All.*) + rewrite /Real_sort__canonical__measurable_structure_Measurable/=. + rewrite /reverse_coercion/=. + set A := (X in @integral _ X). + set B := (X in _ = @integral _ X _ _ _ _). + have : A = B := erefl. + set f := (X in integral tmp V X = _). + set g := (X in _ = integral tmp V X). + have := (@eq_integral _ (measurableTypeR R) _ tmp V f g). + +have := (@normal_prob_conjugate R mu0 sigma0 sig]ma y V S00 S0 mV). + + + + + Qed. + Admitted. + +End gaussian_conjugate_RV. From 3fe91de48d9cec69b10246c11f2cc83b8fdc70b4 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Mon, 8 Jun 2026 17:01:48 +0900 Subject: [PATCH 4/4] doc & changelog --- .nix/config.nix | 28 +- CHANGELOG_UNRELEASED.md | 3 + theories/lebesgue_measure.v | 1 - theories/lebesgue_stieltjes_measure.v | 6 +- theories/probability_theory/test.v | 353 -------------------------- 5 files changed, 20 insertions(+), 371 deletions(-) delete mode 100644 theories/probability_theory/test.v diff --git a/.nix/config.nix b/.nix/config.nix index 50f6625c3d..da755af3bf 100644 --- a/.nix/config.nix +++ b/.nix/config.nix @@ -42,36 +42,34 @@ in { ## select an entry to build in the following `bundles` set ## defaults to "default" - default-bundle = "9.1"; + default-bundle = "9.1-master"; ## write one `bundles.name` attribute set per ## alternative configuration ## When generating GitHub Action CI, one workflow file ## will be created per bundle - bundles."9.0-2.5.0" = { - rocqPackages = { - rocq-core.override.version = "9.0"; - mathcomp.override.version = "2.5.0"; - }; - coqPackages = common-bundle // { - coq.override.version = "9.0"; - mathcomp.override.version = "2.5.0"; - }; - }; - - bundles."9.0" = { + bundles."9.0-master" = { rocqPackages = { rocq-core.override.version = "9.0"; + mathcomp.override.version = "master"; + mathcomp-bigenough.override.version = "master"; + mathcomp-finmap.override.version = "master"; + micromega-plugin.override.version = "master"; }; coqPackages = common-bundle // { coq.override.version = "9.0"; + ssprove.job = false; # not yet available for 9.1 }; }; - bundles."9.1" = { + bundles."9.1-master" = { rocqPackages = { rocq-core.override.version = "9.1"; + mathcomp.override.version = "master"; + mathcomp-bigenough.override.version = "master"; + mathcomp-finmap.override.version = "master"; + micromega-plugin.override.version = "master"; }; coqPackages = common-bundle // { coq.override.version = "9.1"; @@ -85,8 +83,6 @@ in { stdlib.override.version = "master"; rocq-elpi.override.version = "master"; hierarchy-builder.override.version = "master"; - micromega-plugin.override.version = "master"; - micromega-plugin.job = false; mathcomp.override.version = "master"; mathcomp-bigenough.override.version = "master"; mathcomp-finmap.override.version = "master"; diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 0e61ee4fbc..02742f12da 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -96,6 +96,9 @@ - in `reals.v`: + lemmas `sup_ge0`, `has_sup_wpZl`, `gt0_has_supZl`, `has_sup_Mn`, `sup_Mn` +- in `lebesgue_stieltjes_measure.v`: + + definition `lebesgue_display` + ### Changed - moved from `measurable_structure.v` to `classical_sets.v`: diff --git a/theories/lebesgue_measure.v b/theories/lebesgue_measure.v index 92c0fe2910..9f2e38769d 100644 --- a/theories/lebesgue_measure.v +++ b/theories/lebesgue_measure.v @@ -338,7 +338,6 @@ End LebesgueMeasure. Definition lebesgue_measure {R : realType} : set R -> \bar R := lebesgue_stieltjes_measure idfun. -Check fun R : realType => lebesgue_stieltjes_measure idfun : Measure.type _ _. HB.instance Definition _ (R : realType) := Measure.on (@lebesgue_measure R). HB.instance Definition _ (R : realType) := SigmaFiniteMeasure.on (@lebesgue_measure R). diff --git a/theories/lebesgue_stieltjes_measure.v b/theories/lebesgue_stieltjes_measure.v index be715f4337..0a28d88291 100644 --- a/theories/lebesgue_stieltjes_measure.v +++ b/theories/lebesgue_stieltjes_measure.v @@ -33,6 +33,10 @@ From mathcomp Require Import realfun. (* R.-ocitv.-measurable == semiring of sets of open-closed intervals *) (* wlength f A := f b - f a with the hull of the set of real *) (* numbers A being delimited by a and b *) +(* @measurableTypeR R == measurableType generated by R.-ocitv *) +(* @lebesgue_display R == (measure_)display for the sigma-algebra *) +(* generated by R.-ocitv *) +(* @measurableR R == measurable sets generated by R.-ocitv *) (* lebesgue_stieltjes_measure f == Lebesgue-Stieltjes measure for f *) (* f is a cumulative function. *) (* completed_lebesgue_stieltjes_measure f == the completed Lebesgue-Stieltjes *) @@ -522,7 +526,7 @@ Definition measurableR : set (set R) := HB.instance Definition _ : Measurable lebesgue_display (measurableTypeR R) := Measurable.on (measurableTypeR R). (* Presumably it is safe to use NFI here because morally R is unique - and nothing else can be used here*) + and nothing else can be used here *) #[non_forgetful_inheritance] HB.instance Definition _ := Measurable.copy R (measurableTypeR R). diff --git a/theories/probability_theory/test.v b/theories/probability_theory/test.v deleted file mode 100644 index 7f5b16a8ea..0000000000 --- a/theories/probability_theory/test.v +++ /dev/null @@ -1,353 +0,0 @@ -(**md**************************************************************************) -(* # Gaussian-Gaussian conjugate prior *) -(* *) -(* Stated against mathcomp-analysis' [normal_prob m s] (mean [m], standard *) -(* deviation [s]) from [probability_theory/normal_distribution.v]. *) -(* *) -(* For prior [theta ~ normal_prob mu0 sigma0] and Gaussian likelihood *) -(* [X | theta ~ normal_prob theta sigma], the posterior of [theta] given *) -(* [X = x] is itself Gaussian, [normal_prob (mu_post ..) (sigma_post ..)]. *) -(* *) -(* ``` *) -(* sigma_post sigma0 sigma *) -(* := Num.sqrt (sigma0^+2 * sigma^+2 / (sigma0^+2 + sigma^+2)) *) -(* mu_post mu0 sigma0 x sigma *) -(* := (sigma^+2 * mu0 + sigma0^+2 * x) / (sigma0^+2 + sigma^+2) *) -(* *) -(* normal_pdf_conjugate == *) -(* sigma0 != 0 -> sigma != 0 -> *) -(* normal_pdf theta sigma x * normal_pdf mu0 sigma0 theta *) -(* = normal_pdf mu0 (Num.sqrt (sigma0^+2 + sigma^+2)) x *) -(* * normal_pdf (mu_post ..) (sigma_post ..) theta. *) -(* normal_prob_conjugate == *) -(* \int[normal_prob mu0 sigma0]_(theta in V) normal_pdf theta sigma x *) -(* / \int[normal_prob mu0 sigma0]_theta normal_pdf theta sigma x *) -(* = normal_prob (mu_post ..) (sigma_post ..) V. *) -(* ``` *) -(* *) -(* The main theorem is Bayes' rule integrated over [V]: the prior is the *) -(* integration measure, the likelihood [p(x | theta)] is the integrand, and *) -(* the marginal evidence [p(x)] in the denominator is computed as the total *) -(* integral of the likelihood against the prior (no closed-form Gaussian *) -(* density appears in the statement). The marginal factor cancels in the *) -(* quotient, so its explicit value (a Gaussian by [normal_probD] from *) -(* mathcomp/analysis PR #1955) plays no role -- the load-bearing step is the *) -(* pointwise "complete the square" identity [normal_pdf_conjugate]. *) -(******************************************************************************) - -From HB Require Import structures. -From mathcomp Require Import all_boot all_order ssralg ssrnum ssrint interval. -From mathcomp Require Import archimedean finmap interval_inference. -From mathcomp Require Import boolp classical_sets functions cardinality fsbigop. -From mathcomp Require Import reals ereal topology normedtype sequences derive. -From mathcomp Require Import measure exp trigo numfun realfun. -From mathcomp Require Import measurable_realfun lebesgue_measure. -From mathcomp Require Import lebesgue_integral ftc gauss_integral. -From mathcomp Require Import probability_theory.random_variable. -From mathcomp Require Import probability_theory.normal_distribution. -From mathcomp Require Import ring lra. - -Set Implicit Arguments. -Unset Strict Implicit. -Unset Printing Implicit Defensive. - -Import Order.TTheory GRing.Theory Num.Def Num.Theory. -Import numFieldTopology.Exports. - -Reserved Notation "'\Pr_' mu '[' V '|' lik ']'" - (at level 0, V at level 0, lik at level 0, mu at level 0, - format "'\Pr_' mu [ V | lik ]"). - -Local Open Scope classical_set_scope. -Local Open Scope ring_scope. - -(** ** Vendored from mathcomp/analysis PR #1955 - - [integral_normal_prob] is the Radon-Nikodym change-of-variables for - [normal_prob], copied (statement only) from - [theories/probability_theory/normal_distribution.v] on branch - [normal_20260426] of [affeldt-aist/analysis]. Delete this section - when PR #1955 lands. *) -Section vendored_pr1955. -Context {R : realType}. -Local Open Scope ereal_scope. - -Lemma integral_normal_prob (m s : R) (f : R -> \bar R) (U : set R) : - measurable U -> - (normal_prob m s).-integrable U f -> - \int[normal_prob m s]_(x in U) f x - = \int[lebesgue_measure]_(x in U) (f x * (normal_pdf m s x)%:E). -Proof. Admitted. - -End vendored_pr1955. - -(** ** Bayes posterior probability - - Generic measure-theoretic formulation of Bayes' rule. Given a prior - measure [mu] on the parameter space and a likelihood [lik : R -> R] - -- the density of the observation, viewed as a function of the - parameter (i.e., [lik theta = p(observation | theta)]) -- the - posterior probability of a measurable set [V] of parameters is - [(integral over V of lik against mu) / (total integral of lik - against mu)]. Independent of the conjugate-prior application - below; suitable for placement in [probability_theory/]. *) -Section bayes_posterior. -Context {d : measure_display} {T : measurableType d} {R : realType}. -Local Open Scope ereal_scope. - -Definition bayes_posterior - (mu : {measure set T -> \bar R}) (lik : T -> R) (V : set T) : \bar R := - (\int[mu]_(theta in V) (lik theta)%:E) - / (\int[mu]_theta (lik theta)%:E). - -End bayes_posterior. - -Notation "'\Pr_' mu '[' V '|' lik ']'" := (bayes_posterior mu lik V) - : ereal_scope. - -Section gaussian_conjugate. -Context {R : realType}. -Implicit Types (sigma x theta : R) (V : set R). - -(** Posterior standard deviation; squared: - [sigma0^2 * sigma^2 / (sigma0^2 + sigma^2)]. *) -Definition sigma_post (sigma0 sigma : R) : R := - Num.sqrt (sigma0 ^+ 2 * sigma ^+ 2 / (sigma0 ^+ 2 + sigma ^+ 2)). - -(** Posterior mean given observation [x]. *) -Definition mu_post (mu0 sigma0 x sigma : R) : R := - (sigma ^+ 2 * mu0 + sigma0 ^+ 2 * x) / (sigma0 ^+ 2 + sigma ^+ 2). - -(** "Complete the square": the joint density [p(x | theta) * p(theta)] - factors as [K(x) * p_posterior(theta | x)] for some [theta]-independent - factor [K(x)]. Pure [R]-side algebraic identity, established by: - rewriting both [normal_pdf] calls on each side via [normal_pdfE] into - a [normal_peak] match (closed by [sqrtrM] / [invfM] + [field] under - positivity) and a [normal_fun] match (the exponents combine via - [expRD]; equating them is the actual "complete the square" polynomial - identity in [theta], discharged by [field] under the sign - hypotheses). Concretely, [K(x) = normal_pdf mu0 (Num.sqrt - (sigma0^+2 + sigma^+2)) x], but the value is irrelevant to the main - theorem since it cancels in the Bayes quotient. *) -Lemma normal_pdf_conjugate mu0 sigma0 sigma x theta : - sigma0 != 0 -> sigma != 0 -> - normal_pdf theta sigma x * normal_pdf mu0 sigma0 theta - = normal_pdf mu0 (Num.sqrt (sigma0 ^+ 2 + sigma ^+ 2)) x - * normal_pdf (mu_post mu0 sigma0 x sigma) - (sigma_post sigma0 sigma) theta. -Proof. -move=> sigma0_neq0 sigma_neq0. -have sigma0_2pos : 0 < sigma0 ^+ 2 by rewrite exprn_even_gt0. -have sigma_2pos : 0 < sigma ^+ 2 by rewrite exprn_even_gt0. -have sumpos : 0 < sigma0 ^+ 2 + sigma ^+ 2 by apply: addr_gt0. -have sum_neq0 : sigma0 ^+ 2 + sigma ^+ 2 != 0 by rewrite lt0r_neq0. -have sqrt_sum_neq0 : Num.sqrt (sigma0 ^+ 2 + sigma ^+ 2) != 0 - by rewrite sqrtr_eq0 -ltNge. -have sigma_post_pos : 0 < sigma_post sigma0 sigma. - rewrite /sigma_post sqrtr_gt0; apply: divr_gt0 => //. - by apply: mulr_gt0. -have sigma_post_neq0 : sigma_post sigma0 sigma != 0 by rewrite lt0r_neq0. -rewrite !normal_pdfE // mulrACA [RHS]mulrACA. -congr (_ * _); first last. - rewrite /normal_fun -2!expRD; congr (expR _). - rewrite sqr_sqrtr; last exact: ltW sumpos. - rewrite /sigma_post sqr_sqrtr; first last. - apply: divr_ge0; first by apply: mulr_ge0; exact: ltW. - exact: ltW. - rewrite /mu_post; field. - by apply/and3P; split. -have sigmapi2_ge0 : 0 <= sigma ^+ 2 * pi *+ 2 - by apply: mulrn_wge0; apply: mulr_ge0; - [exact: ltW sigma_2pos | exact: pi_ge0]. -have sigma0pi2_ge0 : 0 <= sigma0 ^+ 2 * pi *+ 2 - by apply: mulrn_wge0; apply: mulr_ge0; - [exact: ltW sigma0_2pos | exact: pi_ge0]. -have sumpi2_ge0 : 0 <= (sigma0 ^+ 2 + sigma ^+ 2) * pi *+ 2 - by apply: mulrn_wge0; apply: mulr_ge0; - [exact: ltW sumpos | exact: pi_ge0]. -have sqsum_eq : - Num.sqrt (sigma0 ^+ 2 + sigma ^+ 2) ^+ 2 = sigma0 ^+ 2 + sigma ^+ 2 - by rewrite sqr_sqrtr // ltW. -have sqpost_eq : sigma_post sigma0 sigma ^+ 2 - = sigma0 ^+ 2 * sigma ^+ 2 / (sigma0 ^+ 2 + sigma ^+ 2). - rewrite /sigma_post sqr_sqrtr //. - apply: divr_ge0; first by apply: mulr_ge0; exact: ltW. - exact: ltW. -rewrite /normal_peak sqsum_eq sqpost_eq -invfM -[RHS]invfM -!sqrtrM //. -congr GRing.inv; congr Num.sqrt; field. -exact: sum_neq0. -Qed. - -(** Integrability of the likelihood-as-function-of-theta against the - prior. Pdf values are in [[0, normal_peak sigma]], so the integrand - is bounded, and [normal_prob] is a probability measure, hence - finite. Local because used only in [normal_prob_conjugate]. *) -Local Lemma integrable_normal_pdf_likelihood mu0 sigma0 sigma x V : - sigma != 0 -> measurable V -> - (normal_prob mu0 sigma0).-integrable V - (fun theta => (normal_pdf theta sigma x)%:E). -Proof. -move=> sigma_neq0 mV. -have pdf_sym theta : normal_pdf theta sigma x = normal_pdf x sigma theta. - rewrite !normal_pdfE //; congr (_ * _). - by rewrite /normal_fun -[in LHS](opprB theta x) sqrrN. -have -> : - (fun theta : R => (normal_pdf theta sigma x)%:E) - = (fun theta : R => (normal_pdf x sigma theta)%:E) - by apply/funext => theta; rewrite pdf_sym. -change ((normal_prob mu0 sigma0).-integrable V (EFin \o normal_pdf x sigma)). -apply: (measurable_bounded_integrable - (mu := normal_prob mu0 sigma0) - (f := normal_pdf x sigma) mV). -- apply: le_lt_trans; first exact: probability_le1. - by rewrite ltey. -- by apply: measurable_funTS; exact: measurable_normal_pdf. -- exists (normal_peak sigma); split; first by rewrite num_real. - move=> y ynp theta _. - rewrite /= ger0_norm; last exact: normal_pdf_ge0. - exact: le_trans (normal_pdf_ub _ _ sigma_neq0) (ltW ynp). -Qed. - -(** ** Main theorem *) - -(** Gaussian-Gaussian conjugate prior: the posterior of [theta] given - [X = x] is a single Gaussian [normal_prob (mu_post ..) (sigma_post ..)]. - - Reading the equation. The LHS is Bayes' rule [p(theta | x) = - p(x | theta) p(theta) / p(x)] integrated over [V]: - - [normal_prob mu0 sigma0] (integration measure) is the *prior*; - - [normal_pdf theta sigma x] (integrand) is the *likelihood* - density [p(x | theta)]; - - the *marginal* evidence [p(x)] in the denominator is computed as - the total integral of the likelihood against the prior -- no - closed-form Gaussian density appears in the statement. *) -Lemma normal_prob_conjugate mu0 sigma0 sigma x V : - sigma0 != 0 -> sigma != 0 -> measurable V -> - (\Pr_(normal_prob mu0 sigma0) - [V | fun theta => normal_pdf theta sigma x] - = normal_prob (mu_post mu0 sigma0 x sigma) - (sigma_post sigma0 sigma) V)%E. -Proof. -move=> sigma0_neq0 sigma_neq0 mV. -set tmp : {measure set (measurableTypeR R) -> \bar R} := normal_prob _ _. -rewrite /bayes_posterior /=. -pose K := normal_pdf mu0 (Num.sqrt (sigma0 ^+ 2 + sigma ^+ 2)) x. -pose P := normal_prob (mu_post mu0 sigma0 x sigma) - (sigma_post sigma0 sigma) V. -have sigma0sigma_neq0 : Num.sqrt (sigma0 ^+ 2 + sigma ^+ 2) != 0. - rewrite sqrtr_eq0 -ltNge; apply: addr_gt0; rewrite exprn_even_gt0 //=. -have Kpos : 0 < K. - rewrite /K normal_pdfE //; apply: mulr_gt0. - by rewrite normal_peak_gt0. - by rewrite /normal_fun expR_gt0. -have KEneq0 : (K%:E != 0)%E by rewrite eqe; apply: lt0r_neq0. -have num_eq : - (\int[normal_prob mu0 sigma0]_(theta in V) (normal_pdf theta sigma x)%:E - = K%:E * P)%E. - rewrite integral_normal_prob //; - last exact: integrable_normal_pdf_likelihood. - under eq_integral => theta _ do - rewrite -EFinM - (normal_pdf_conjugate mu0 x theta sigma0_neq0 sigma_neq0) - EFinM. - rewrite -/K ge0_integralZl_EFin //=; first last. - - exact: ltW. - - apply/measurable_EFinP/measurable_funTS; exact: measurable_normal_pdf. - - by move=> theta _; rewrite lee_fin; exact: normal_pdf_ge0. -have denom_eq : - (\int[normal_prob mu0 sigma0]_theta (normal_pdf theta sigma x)%:E - = K%:E)%E. - rewrite integral_normal_prob //; - last exact: integrable_normal_pdf_likelihood. - under eq_integral => theta _ do - rewrite -EFinM - (normal_pdf_conjugate mu0 x theta sigma0_neq0 sigma_neq0) - EFinM. - rewrite -/K ge0_integralZl_EFin //=; first last. - - exact: ltW. - - apply/measurable_EFinP/measurable_funTS; exact: measurable_normal_pdf. - - by move=> theta _; rewrite lee_fin; exact: normal_pdf_ge0. - by rewrite integral_normal_pdf // mule1. -by rewrite num_eq denom_eq muleAC divee // mul1e. -Qed. - -End gaussian_conjugate. - -(** ** Random-variable-style restatement - - Sugar over the measure-theoretic statement above. Given a random - variable [X] on a probability space [P] with [X \~ N(mu0, sigma0)] - and a likelihood family [lik t y = p(Y = y | X = t)] (the Gaussian - case is [lik = normal_pdf ^~ sigma]), the conditional distribution - [\Pr[X | lik = y]] -- computed via Bayes' rule -- is the Gaussian - posterior. - - [\Pr[X | lik = y] \~ D] is shorthand for "the Bayes posterior under - prior [distribution P X] and likelihood [lik^~ y] agrees with [D] - on all measurable sets". The proof of the RV-style statement is - just one [rewrite] using the [X \~ _] hypothesis followed by the - underlying [normal_prob_conjugate]. *) - -Section gaussian_conjugate_RV. -Context {d : measure_display} {T : measurableType d} {R : realType}. -Variable P : pprobability T R. - -Local Notation "X '\~' D" := (distribution P X = D) - (at level 70). - -Local Notation "'\Pr[' X '|' F 'at' y ']' '\~' D" := - (forall V, measurable V -> - (bayes_posterior (distribution P X) (F^~ y) V = D V)%E) - (at level 70, X at next level, F at next level, y at next level). - -(** **Note: canonical-structure obstacle.** - - The proof below should be one line: - [move=> _ _ HX HL V mV; rewrite HX HL; exact: normal_prob_conjugate.] - After [rewrite HX HL], the goal is *syntactically* the conclusion - of [normal_prob_conjugate]. But [exact:] still fails because - [{RV P >-> R}] in [distribution P X] picks the *default* canonical - measurable structure on [R] ([Real_sort__canonical__measurable_ - structure_Measurable]), while [normal_prob] integrates over [R] - viewed with the *ocitv* canonical structure ([lebesgue_stieltjes_ - measure_ocitv_type__canonical__measurable_structure_Measurable]). - These two canonical instances are propositionally the same Borel - sigma-algebra on [R] but Coq does not unify them. Resolving this - is an upstream issue in mathcomp-analysis (unify R's canonical - measurable structure, or add a transfer lemma between the two). *) -Theorem normal_prob_conjugate_RV - (X : {RV P >-> R}) (mu0 sigma0 sigma y : R) : - sigma0 != 0%R -> sigma != 0%R -> - X \~ normal_prob mu0 sigma0 -> - \Pr[X | (fun x => normal_pdf x sigma) at y] - \~ normal_prob (mu_post mu0 sigma0 y sigma) (sigma_post sigma0 sigma). -Proof. -move=> S00 S0 HX V mV. -rewrite /bayes_posterior/=. -rewrite -normal_prob_conjugate//. -rewrite /bayes_posterior. -rewrite -HX. -congr (_ / _)%E => //. - simpl. - rewrite HX//. - rewrite /bayes_posterior. - set tmp := normal_prob _ _. -(*Set Printing All.*) - rewrite /Real_sort__canonical__measurable_structure_Measurable/=. - rewrite /reverse_coercion/=. - set A := (X in @integral _ X). - set B := (X in _ = @integral _ X _ _ _ _). - have : A = B := erefl. - set f := (X in integral tmp V X = _). - set g := (X in _ = integral tmp V X). - have := (@eq_integral _ (measurableTypeR R) _ tmp V f g). - -have := (@normal_prob_conjugate R mu0 sigma0 sig]ma y V S00 S0 mV). - - - - - Qed. - Admitted. - -End gaussian_conjugate_RV.