Skip to content

Commit

Permalink
fix
Browse files Browse the repository at this point in the history
  • Loading branch information
affeldt-aist committed Dec 2, 2024
1 parent 6db6439 commit 639b4dd
Show file tree
Hide file tree
Showing 3 changed files with 35 additions and 40 deletions.
55 changes: 25 additions & 30 deletions theories/lang_syntax.v
Original file line number Diff line number Diff line change
Expand Up @@ -144,7 +144,7 @@ exists 0%R.
rewrite not_implyE; split; first by rewrite boundl_in_itv/= bnd_simp.
move/left_right_continuousP.
apply/not_andP; left.
move/cvgrPdist_le.
move/(@cvgrPdist_le _ R^o).
apply/existsNP.
exists (2%:R^-1).
rewrite not_implyE; split; first by rewrite invr_gt0.
Expand All @@ -171,7 +171,7 @@ rewrite invf_lt1//.
rewrite {1}(_:1%R = 1%:R)//; apply: ltr_nat.
Qed.

Let dintuni : derivable_oo_continuous_bnd (@id R) 0 1.
Let dintuni : derivable_oo_continuous_bnd (@id R^o) 0 1.
Proof.
split.
- move=> x _.
Expand All @@ -180,7 +180,7 @@ split.
- exact: cvg_at_left_filter.
Qed.

Let intuni'uni : {in `]0%R, 1%R[, (@id R)^`() =1 uni}.
Let intuni'uni : {in `]0%R, 1%R[, (@id R^o)^`() =1 uni}.
Proof.
move=> x x01.
rewrite derive1E derive_id.
Expand Down Expand Up @@ -258,7 +258,7 @@ move=> ab cf.
move/continuous_within_itvP : cf => /(_ ab) [cf _ _].
rewrite (_ : f = (f \o -%R) \o -%R); last first.
by apply/funext => y; rewrite /= opprK.
apply: continuous_comp; first exact: opp_continuous.
apply: continuous_comp; first exact: (@opp_continuous _ R^o).
by apply: cf; rewrite -oppr_itvoo opprK.
+ move/continuous_within_itvP : cf => /(_ ab) [_ _ cf].
apply/cvg_at_rightNP.
Expand All @@ -274,7 +274,7 @@ Lemma oppr_change (f : R -> R) a b : (a < b)%R ->
\int[mu]_(x in `[-%R b, -%R a]) ((f \o -%R) x)%:E.
Proof.
move=> ab cf.
have dN : ((-%R : R -> R)^`() = cst (-1) :> (R -> R))%R. (* TODO: lemma? *)
have dN : ((-%R : R -> R^o)^`() = cst (-1) :> (R -> R))%R. (* TODO: lemma? *)
by apply/funext => x/=; rewrite derive1E deriveN// derive_id.
rewrite integration_by_substitution_decreasing//.
- by apply: eq_integral => /= x _; rewrite dN/= opprK mulr1 -compA/= opprK.
Expand Down Expand Up @@ -302,7 +302,7 @@ move=> x y x01 y01.
by rewrite le_eqVlt => /predU1P[->//|/dF] => /(_ x01 y01)/ltW.
Qed.

Lemma derive1_onem {R: realType} : (fun x0 : R => (1 - x0)%R)^`() = (cst (-1)%R).
Lemma derive1_onem {R: realType} : (fun x0 : R^o => (1 - x0)%R)^`() = (cst (-1)%R).
Proof.
apply/funext => x.
by rewrite derive1E deriveB// derive_id derive_cst sub0r.
Expand All @@ -315,11 +315,11 @@ Lemma cvg_comp_filter {R : realType} (f g : R -> R) (r l : R) :
f x @[x --> g r] --> l.
Proof.
move=> cf fgrl.
apply/cvgrPdist_le => /= e e0.
apply/(@cvgrPdist_le _ R^o) => /= e e0.
have e20 : 0 < e / 2 by rewrite divr_gt0.
move/cvgrPdist_le : fgrl => /(_ _ e20) fgrl.
move/(@cvgrPdist_le _ R^o) : fgrl => /(_ _ e20) fgrl.
have := cf (g r).
move=> /cvgrPdist_le => /(_ _ e20)[x x0]H.
move=> /(@cvgrPdist_le _ R^o) => /(_ _ e20)[x x0]H.
exists (minr x (e/2)).
by rewrite lt_min x0.
move=> z.
Expand Down Expand Up @@ -366,12 +366,12 @@ move=> ->//.
rewrite opprB addrCA addrA addrK.
apply: (@cvg_comp_filter _ _ (fun x => 1 - x)%R)=> //=.
move=> x.
apply: continuousB => //.
apply: (@continuousB _ R^o) => //.
exact: cvg_cst.
under eq_fun do rewrite opprD addrA subrr add0r opprK.
apply: cvg_id.
apply: cvg_at_left_filter.
apply: cvgB => //.
apply: (@cvgB _ R^o) => //.
exact: cvg_cst.
Qed.

Expand Down Expand Up @@ -436,7 +436,7 @@ exact: leq_prod2.
Qed.

Lemma bounded_norm_expn_onem {R : realType} (a b : nat) :
[bounded `|x ^+ a * (1 - x) ^+ b|%R : R | x in (`[0%R, 1%R]%classic : set R)].
[bounded `|x ^+ a * (1 - x) ^+ b|%R : R^o | x in (`[0%R, 1%R]%classic : set R)].
Proof.
exists 1%R; split; [by rewrite num_real|move=> x x1 /= y].
rewrite in_itv/= => /andP[y0 y1].
Expand Down Expand Up @@ -536,22 +536,17 @@ by apply: eq_integral => /= x _; rewrite patchE mem_setE in_itv/=; case: ifPn.
Qed.*)

Lemma onemXn_derivable {R : realType} n (x : R) :
derivable (fun y : R => `1-y ^+ n)%R x 1.
derivable (fun y : R^o => `1-y ^+ n : R^o)%R x 1.
Proof.
have := @derivableX R R (@onem R) n x 1%R.
have := @derivableX R R^o (@onem R) n x 1%R.
rewrite fctE.
apply.
exact: derivableB.
Qed.

Lemma deriveX_idfun {R : realType} n x :
'D_1 (@GRing.exp R ^~ n.+1) x = n.+1%:R *: (x ^+ n)%R.
Proof.
rewrite exp_derive.
rewrite -scalerA.
congr (_ *: _).
by rewrite [LHS]mulr1.
Qed.
'D_1 (@GRing.exp R^o ^~ n.+1) x = n.+1%:R *: (x ^+ n)%R.
Proof. by rewrite exp_derive /GRing.scale/= mulr1. Qed.

Lemma derive1Mr [R : realFieldType] [f : R^o -> R^o] [x r : R^o] :
derivable f x 1 -> ((fun x => f x * r)^`() x = (r * f^`() x)%R :> R)%R.
Expand All @@ -578,7 +573,7 @@ Lemma continuous_onemXn {R : realType} (n : nat) x :
{for x, continuous (fun y : R => `1-y ^+ n)%R}.
Proof.
apply: (@continuous_comp _ _ _ (@onem R) (fun x => GRing.exp x n)).
by apply: cvgB; [exact: cvg_cst|exact: cvg_id].
by apply: (@cvgB _ R^o); [exact: cvg_cst|exact: cvg_id].
exact: exprn_continuous.
Qed.

Expand Down Expand Up @@ -625,7 +620,7 @@ by apply: continuous_in_subspaceT => x _; exact: continuous_XMonemX.
Qed.

Lemma bounded_XMonemX {R : realType} (a b : nat) :
[bounded XMonemX a b x : R | x in (`[0, 1]%classic : set R)].
[bounded XMonemX a b x : R^o | x in (`[0, 1]%classic : set R)].
Proof.
exists 1%R; split; [by rewrite num_real|move=> x x1 /= y y01].
rewrite ger0_norm//; last by rewrite XMonemX_ge0.
Expand All @@ -648,7 +643,7 @@ Local Open Scope ereal_scope.
Lemma integral_exprn {R : realType} (n : nat) :
fine (\int[lebesgue_measure]_(x in `[0%R, 1%R]) (x ^+ n)%:E) = n.+1%:R^-1 :> R.
Proof.
pose F (x : R) := (n.+1%:R^-1 * x ^+ n.+1)%R.
pose F (x : R) : R^o := (n.+1%:R^-1 * x ^+ n.+1)%R.
have cX m : {in `[0%R, 1%R], continuous (fun x : R => x ^+ m)%R}.
by move=> x x01; exact: exprn_continuous.
have cF0 : {for 0%R, continuous F}.
Expand All @@ -664,7 +659,7 @@ have dcF : derivable_oo_continuous_bnd F 0 1.
by apply/cvg_at_right_filter/cX; rewrite in_itv/= lexx ler01.
- apply: continuous_cvg; first exact: mulrl_continuous.
by apply/cvg_at_left_filter/cX; rewrite in_itv/= lexx ler01.
have dFE : {in `]0%R, 1%R[, F^`() =1 (fun x : R => x ^+ n)%R}.
have dFE : {in `]0%R, 1%R[, F^`() =1 (fun x : R => x ^+ n : R)%R}.
move=> x x01.
rewrite derive1Ml; last exact: exprn_derivable.
by rewrite derive1E deriveX_idfun mulrA mulVf// mul1r.
Expand All @@ -674,24 +669,24 @@ by apply: continuous_subspaceT; exact: exprn_continuous.
Qed.

Lemma derivable_oo_continuous_bnd_onemXnMr {R : realType} (n : nat) (r : R) :
derivable_oo_continuous_bnd (fun x : R => `1-x ^+ n.+1 * r)%R 0 1.
derivable_oo_continuous_bnd (fun x : R => `1-x ^+ n.+1 * r : R^o)%R 0 1.
Proof.
split.
- by move=> x x01; apply: derivableM => //=; exact: onemXn_derivable.
- apply: cvgM; last exact: cvg_cst.
apply: cvg_at_right_filter.
apply: (@cvg_comp _ _ _ (fun x => 1 - x)%R (fun x => GRing.exp x n.+1)%R).
by apply: cvgB; [exact: cvg_cst|exact: cvg_id].
by apply: (@cvgB _ R^o); [exact: cvg_cst|exact: cvg_id].
exact: exprn_continuous.
- apply: cvg_at_left_filter.
apply: cvgM; last exact: cvg_cst.
apply: (@cvg_comp _ _ _ (fun x => 1 - x)%R (fun x => GRing.exp x n.+1)%R).
by apply: cvgB; [exact: cvg_cst|exact: cvg_id].
by apply: (@cvgB _ R^o); [exact: cvg_cst|exact: cvg_id].
exact: exprn_continuous.
Qed.

Lemma derive_onemXn {R : realType} (n : nat) x :
((fun y : R => `1-y ^+ n.+1)^`() x = - n.+1%:R * `1-x ^+ n)%R.
((fun y : R => `1-y ^+ n.+1 : R^o)^`() x = - n.+1%:R * `1-x ^+ n)%R.
Proof.
rewrite (@derive1_comp _ (@onem R) (fun x => GRing.exp x n.+1))//; last first.
exact: exprn_derivable.
Expand Down Expand Up @@ -1071,7 +1066,7 @@ Qed.

Local Open Scope ring_scope.
Lemma bounded_beta_pdf_01 :
[bounded beta_pdf x | x in `[0%R, 1%R]%classic : set R].
[bounded beta_pdf x : R^o | x in `[0%R, 1%R]%classic : set R].
Proof.
exists (betafun a b)^-1; split; first by rewrite num_real.
move=> // y y1.
Expand Down
16 changes: 8 additions & 8 deletions theories/lang_syntax_table_game.v
Original file line number Diff line number Diff line change
Expand Up @@ -77,7 +77,7 @@ Local Open Scope lang_scope.
Local Open Scope ereal_scope.
Context {R : realType}.

Lemma bounded_id_01 : [bounded x0 | x0 in `[0%R, 1%R]%classic : set R].
Lemma bounded_id_01 : [bounded x0 | x0 in `[0%R, 1%R]%classic : set R^o].
Proof.
exists 1%R; split => // y y1.
near=> M => /=.
Expand All @@ -88,7 +88,7 @@ rewrite in_itv/= => /andP[M0 M1].
by rewrite ler_norml M1 andbT (le_trans _ M0).
Unshelve. all: by end_near. Qed.

Lemma bounded_onem_01 : [bounded (`1- x : R) | x in `[0%R, 1%R]%classic : set R].
Lemma bounded_onem_01 : [bounded (`1- x : R^o) | x in `[0%R, 1%R]%classic : set R].
Proof.
exists 1%R; split => // y y1.
near=> M => /=.
Expand All @@ -101,7 +101,7 @@ rewrite ler_norml (@le_trans _ _ 0%R)//=.
by rewrite onem_ge0.
Unshelve. all: by end_near. Qed.

Lemma bounded_cst_01 (x : R) : [bounded x | _ in `[0%R, 1%R]%classic : set R].
Lemma bounded_cst_01 (x : R^o) : [bounded x | _ in `[0%R, 1%R]%classic : set R].
Proof.
exists `|x|%R; split.
by rewrite num_real.
Expand All @@ -111,8 +111,8 @@ by rewrite (le_trans _ (ltW y1)).
Qed.

Lemma bounded_norm (f : R -> R) :
[bounded f x | x in (`[0%R, 1%R]%classic : set R)] <->
[bounded normr (f x) | x in (`[0%R, 1%R]%classic : set R)].
[bounded f x : R^o | x in (`[0%R, 1%R]%classic : set R)] <->
[bounded normr (f x) : R^o | x in (`[0%R, 1%R]%classic : set R)].
Proof.
split.
move=> [M [Mreal HM]].
Expand All @@ -127,8 +127,8 @@ by rewrite (le_lt_trans _ Mr)// ler_norm.
Qed.

Lemma boundedMl k (f : R -> R) :
[bounded f x | x in (`[0%R, 1%R]%classic : set R)] ->
[bounded (k * f x)%R | x in (`[0%R, 1%R]%classic : set R)].
[bounded f x : R^o | x in (`[0%R, 1%R]%classic : set R)] ->
[bounded (k * f x)%R : R^o | x in (`[0%R, 1%R]%classic : set R)].
Proof.
move=> [M [Mreal HM]].
exists `|k * M|%R; split; first by rewrite normr_real.
Expand Down Expand Up @@ -394,7 +394,7 @@ by apply: measurable_funX; exact: measurable_funB.
Qed.

Lemma bounded_norm_XnonemXn {R : realType} :
[bounded normr (56 * XMonemX 5 3 x)%R : R | x in `[0%R, 1%R] : set R].
[bounded normr (56 * XMonemX 5 3 x)%R : R^o | x in `[0%R, 1%R] : set R].
Proof. exact/(bounded_norm _).1/boundedMl/bounded_XMonemX. Qed.

Lemma integrable_bernoulli_XMonemX {R : realType} U :
Expand Down
4 changes: 2 additions & 2 deletions theories/prob_lang_wip.v
Original file line number Diff line number Diff line change
Expand Up @@ -65,10 +65,10 @@ Proof.
apply: continuousM => //=; first exact: cvg_cst.
apply: continuous_comp => /=; last exact: continuous_expR.
apply: continuousM => //=; last exact: cvg_cst.
apply: continuous_comp => //=; last exact: continuousN.
apply: continuous_comp => //=; last exact: (@continuousN _ R^o).
apply: (@continuous_comp _ _ _ _ (fun x : R => x ^+ 2)%R); last exact: exprn_continuous.
apply: continuousM => //=; last exact: cvg_cst.
by apply: continuousD => //=; exact: cvg_cst.
by apply: (@continuousD _ R^o) => //=; exact: cvg_cst.
Qed.

End gauss_pdf.
Expand Down

0 comments on commit 639b4dd

Please sign in to comment.