Files

  • mathcomp

    • Top

    Module mathcomp.analysis.probability_theory.uniform_distribution

    From HB Require Import structures.
    From mathcomp Require Import all_ssreflect_compat ssralg ssrnum ssrint interval.
    From mathcomp Require Import interval_inference archimedean finmap.
    From mathcomp Require Import boolp classical_sets functions cardinality fsbigop.
    From mathcomp Require Import reals ereal topology normedtype.
    From mathcomp Require Import sequences measure measurable_realfun numfun.
    From mathcomp Require Import lebesgue_measure lebesgue_integral.

    # Uniform distribution ``` uniform_pdf a b == uniform pdf over the interval [a,b] uniform_prob a b ab == uniform probability over the interval [a,b] where ab0 a proof that 0 < b - a ```

    Set SsrOldRewriteGoalsOrder.
    Set Implicit Arguments.
    Unset Strict Implicit.
    Unset Printing Implicit Defensive.

    Import Order.TTheory GRing.Theory Num.Def Num.Theory.
    Import numFieldTopology.Exports.

    Local Open Scope classical_set_scope.
    Local Open Scope ring_scope.

    Section uniform_probability.
    Local Open Scope ring_scope.
    Context (R : realType) (a b : R).

    Definition
    uniform_pdf

    uniform_pdf : forall [R : realType], R -> R -> R -> R uniform_pdf is not universe polymorphic Arguments uniform_pdf [R] (a b)%_ring_scope x uniform_pdf is transparent Expands to: Constant mathcomp.analysis.probability_theory.uniform_distribution.uniform_pdf Declared in library mathcomp.analysis.probability_theory.uniform_distribution, line 36, characters 11-22

    x := if a <= x <= b then (b - a)^-1 else 0.

    Lemma uniform_pdf_ge0 x : a < b -> 0 <= uniform_pdf x.
    Proof.
    move=> ab; rewrite /uniform_pdf; case: ifPn => // axb.
    by rewrite invr_ge0// ltW// subr_gt0.
    Qed.

    Lemma measurable_uniform_pdf : measurable_fun setT uniform_pdf.
    Proof.
    rewrite /uniform_pdf /=; apply: measurable_fun_if => //=.
    by apply: measurable_and => //; exact: measurable_fun_ler.
    Qed.

    Local Notation mu := lebesgue_measure.

    Lemma integral_uniform_pdf U :
      (\int[mu]_(x in U) (uniform_pdf x)%:E =
       \int[mu]_(x in U `&` `[a, b]) (uniform_pdf x)%:E)%E.
    Proof.
    rewrite [RHS]integral_mkcondr/=; apply: eq_integral => x xU.
    rewrite patchE; case: ifPn => //.
    rewrite notin_setE/= in_itv/= => /negP/negbTE xab.
    by rewrite /uniform_pdf xab.
    Qed.

    Lemma integral_uniform_pdf1 A (ab : a < b) : `[a, b] `<=` A ->
      (\int[mu]_(x in A) (uniform_pdf x)%:E = 1)%E.
    Proof.
    move=> abA; rewrite integral_uniform_pdf setIidr//.
    rewrite (eq_integral (fun=> (b - a)^-1%:E)); last first.
      by move=> x; rewrite inE/= in_itv/= /uniform_pdf => ->.
    rewrite integral_cst//= lebesgue_measure_itv/= lte_fin.
    by rewrite ab -EFinD -EFinM mulVf// gt_eqF// subr_gt0.
    Qed.

    Definition
    uniform_prob

    uniform_prob : forall [R : realType] [a b : R], (a < b)%R -> set (measurable_structure_g_sigma_algebraType__canonical__measurable_structure_Measurable (T:=lebesgue_stieltjes_measure_ocitv_type__canonical__classical_sets_Pointed R) (R.-ocitv).-measurable) -> \bar R uniform_prob is not universe polymorphic Arguments uniform_prob [R] [a b]%_ring_scope ab _%_classical_set_scope uniform_prob is transparent Expands to: Constant mathcomp.analysis.probability_theory.uniform_distribution.uniform_prob Declared in library mathcomp.analysis.probability_theory.uniform_distribution, line 72, characters 11-23

    (ab : a < b) : set _ -> \bar R :=
      fun U => (\int[mu]_(x in U) (uniform_pdf x)%:E)%E.

    Hypothesis ab : (a < b)%R.

    Let uniform0 : uniform_prob ab set0 = 0.
    Proof.
    by rewrite /uniform_prob integral_set0. Qed.

    Let uniform_ge0 U : (0 <= uniform_prob ab U)%E.
    Proof.
    by apply: integral_ge0 => /= x Ux; rewrite lee_fin uniform_pdf_ge0.
    Qed.

    Lemma integrable_uniform_pdf :
      mu.-integrable setT (fun x => (uniform_pdf x)%:E).
    Proof.
    apply/integrableP; split.
      by apply: measurableT_comp => //; exact: measurable_uniform_pdf.
    under eq_integral.
      move=> x _; rewrite gee0_abs//; last by rewrite lee_fin uniform_pdf_ge0.
      over.
    by rewrite /= integral_uniform_pdf1 ?ltry// -subr_gt0.
    Qed.

    Let uniform_sigma_additive : semi_sigma_additive (uniform_prob ab).
    Proof.
    move=> /= F mF tF mUF; rewrite /uniform_prob; apply: cvg_toP.
      apply: ereal_nondecreasing_is_cvgn => m n mn.
      apply: lee_sum_nneg_natr => // k _ _.
      by apply: integral_ge0 => /= x Fkx; rewrite lee_fin uniform_pdf_ge0.
    rewrite ge0_integral_bigcup//=.
    - apply: measurable_funTS; apply: measurableT_comp => //.
      exact: measurable_uniform_pdf.
    - by move=> x _; rewrite lee_fin uniform_pdf_ge0.
    Qed.

    HB.instance Definition _ := isMeasure.Build _ _ _ (uniform_prob ab)
      uniform0 uniform_ge0 uniform_sigma_additive.

    Let uniform_setT : uniform_prob ab [set: _] = 1%:E.
    Proof.
    by rewrite /uniform_prob /mscale/= integral_uniform_pdf1. Qed.

    HB.instance Definition _ := @Measure_isProbability.Build _ _ R
      (uniform_prob ab) uniform_setT.

    Lemma dominates_uniform_prob : uniform_prob ab `<< mu.
    Proof.
    apply/null_content_dominatesP.
    move=> A mA muA0; rewrite /uniform_prob integral_uniform_pdf.
    apply/eqP; rewrite eq_le; apply/andP; split; last first.
      apply: integral_ge0 => x [Ax /=]; rewrite in_itv /= => xab.
      by rewrite lee_fin uniform_pdf_ge0.
    apply: (@le_trans _ _
        (\int[mu]_(x in A `&` `[a, b]%classic) (b - a)^-1%:E))%E; last first.
      rewrite integral_cst//= ?mul1e//.
        by rewrite pmule_rle0 ?lte_fin ?invr_gt0// ?subr_gt0// -muA0 measureIl.
      exact: measurableI.
    apply: ge0_le_integral => //=.
    - exact: measurableI.
    - by move=> x [Ax]; rewrite /= in_itv/= => axb; rewrite lee_fin uniform_pdf_ge0.
    - by apply/measurable_EFinP/measurable_funTS; exact: measurable_uniform_pdf.
    - by move=> x [Ax]; rewrite in_itv/= /uniform_pdf => ->.
    Qed.

    Let integral_uniform_indic E : measurable E ->
      (\int[uniform_prob ab]_x (\1_E x)%:E =
       (b - a)^-1%:E * \int[mu]_(x in `[a, b]) (\1_E x)%:E)%E.
    Proof.
    move=> mE; rewrite integral_indic//= /uniform_prob setIT -ge0_integralZl//=.
    - rewrite [LHS]integral_mkcond/= [RHS]integral_mkcond/=.
      apply: eq_integral => x _; rewrite !patchE; case: ifPn => xE.
        case: ifPn.
          rewrite inE/= in_itv/= => xab.
          by rewrite /uniform_pdf xab indicE xE mule1.
        by rewrite notin_setE/= in_itv/= => /negP/negbTE; rewrite /uniform_pdf => ->.
      case: ifPn => //.
      by rewrite inE/= in_itv/= => axb; rewrite indicE (negbTE xE) mule0.
    - exact/measurable_EFinP/measurable_indic.
    - by rewrite lee_fin invr_ge0// ltW// subr_gt0.
    Qed.

    Import HBNNSimple.

    Let integral_uniform_nnsfun (f : {nnsfun _ >-> R}) :
      (\int[uniform_prob ab]_x (f x)%:E =
       (b - a)^-1%:E * \int[mu]_(x in `[a, b]) (f x)%:E)%E.
    Proof.
    under [LHS]eq_integral do rewrite fimfunE -fsumEFin//.
    rewrite [LHS]ge0_integral_fsum//; last 2 first.
      - by move=> r; exact/measurable_EFinP/measurableT_comp.
      - by move=> n x _; rewrite EFinM nnfun_muleindic_ge0.
    rewrite -[RHS]ge0_integralZl//; last 3 first.
      - exact/measurable_EFinP/measurable_funTS.
      - by move=> x _; rewrite lee_fin.
      - by rewrite lee_fin invr_ge0// ltW// subr_gt0.
    under [RHS]eq_integral.
      move=> x xD; rewrite fimfunE -fsumEFin// ge0_mule_fsumr; last first.
        by move=> r; rewrite EFinM nnfun_muleindic_ge0.
      over.
    rewrite [RHS]ge0_integral_fsum//; last 2 first.
      - by move=> r; apply/measurable_EFinP; do 2 apply/measurableT_comp => //.
      - move=> n x _; rewrite EFinM mule_ge0//; last by rewrite nnfun_muleindic_ge0.
        by rewrite lee_fin invr_ge0// ltW// subr_gt0.
    apply: eq_fsbigr => r _; rewrite ge0_integralZl//.
    - by rewrite !integralZl_indic_nnsfun//= integral_uniform_indic// muleCA.
    - exact/measurable_EFinP/measurableT_comp.
    - by move=> t _; rewrite nnfun_muleindic_ge0.
    - by rewrite lee_fin invr_ge0// ltW// subr_gt0.
    Qed.

    Lemma integral_uniform (f : _ -> \bar R) :
      measurable_fun setT f -> (forall x, 0 <= f x)%E ->
      (\int[uniform_prob ab]_x f x = (b - a)^-1%:E * \int[mu]_(x in `[a, b]) f x)%E.
    Proof.
    move=> mf f0.
    pose f_ := nnsfun_approx measurableT mf.
    transitivity (lim (\int[uniform_prob ab]_x (f_ n x)%:E @[n --> \oo])%E).
      rewrite -monotone_convergence//=.
      - apply: eq_integral => ? /[!inE] xD; apply/esym/cvg_lim => //=.
        exact: cvg_nnsfun_approx.
      - by move=> n; exact/measurable_EFinP/measurable_funTS.
      - by move=> n ? _; rewrite lee_fin.
      - by move=> ? _ ? ? mn; rewrite lee_fin; exact/lefP/nd_nnsfun_approx.
    rewrite [X in _ = (_ * X)%E](_ : _ = lim
        (\int[mu]_(x in `[a, b]) (f_ n x)%:E @[n --> \oo])%E); last first.
      rewrite -monotone_convergence//=.
      - apply: eq_integral => ? /[!inE] xD; apply/esym/cvg_lim => //.
        exact: cvg_nnsfun_approx.
      - by move=> n; exact/measurable_EFinP/measurable_funTS.
      - by move=> n ? _; rewrite lee_fin.
      - by move=> ? _ ? ? ?; rewrite lee_fin; exact/lefP/nd_nnsfun_approx.
    rewrite -limeMl//.
      by apply: congr_lim; apply/funext => n /=; exact: integral_uniform_nnsfun.
    apply/ereal_nondecreasing_is_cvgn => x y xy; apply: ge0_le_integral => //=.
    - by move=> ? _; rewrite lee_fin.
    - exact/measurable_EFinP/measurable_funTS.
    - exact/measurable_EFinP/measurable_funTS.
    - by move=> ? _; rewrite lee_fin; exact/lefP/nd_nnsfun_approx.
    Qed.

    End uniform_probability.
    Generated by rocqnavi