Skip to content

Commit

Permalink
cleanup
Browse files Browse the repository at this point in the history
  • Loading branch information
@bmtrager
bmtrager committed Jan 27, 2025
1 parent 87be513 commit 1213fbd
Showing 1 changed file with 3 additions and 252 deletions.
255 changes: 3 additions & 252 deletions coq/QLearn/Tsitsiklis.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -9202,255 +9202,6 @@ Qed.
Next Obligation.
apply fin_finite.
Qed.

Lemma Finite_conditional_variance_bound1_fun (x c : Ts -> R)
{dom2 : SigmaAlgebra Ts}
(sub : sa_sub dom2 dom)
{rv : RandomVariable dom borel_sa x}
{rv2 : RandomVariable dom2 borel_sa c}
{isfe : IsFiniteExpectation prts x}
{isfe2 : IsFiniteExpectation prts c}
{isfe0 : IsFiniteExpectation prts (rvsqr x)} :
almostR2 prts Rle (rvsqr x) (c) ->
almostR2 (prob_space_sa_sub prts sub) Rle (rvminus (FiniteConditionalExpectation prts sub (rvsqr x))
(rvsqr (FiniteConditionalExpectation prts sub x)))
(c).
Proof.
intros.
assert (rv3: RandomVariable dom borel_sa c).
{
now apply (RandomVariable_sa_sub sub).
}
generalize (FiniteCondexp_ale
prts sub (rvsqr x) (c)); intros.
cut_to H0; try easy.
revert H0; apply almost_impl.
apply all_almost; intros ??.
rewrite FiniteCondexp_id with (f := c) in H0; trivial.
rv_unfold.
eapply Rle_trans.
shelve.
apply H0.
Unshelve.
assert (0 <= (FiniteConditionalExpectation prts sub x x0)²).
{
apply Rle_0_sqr.
}
lra.
Qed.

Ltac rewrite_condexp_pf_irrel H
:= match type of H with
| @NonNegCondexp ?Ts ?dom ?prts ?dom2 ?sub ?f ?rv1 ?nnf1 ?x = _ =>
match goal with
[|- context [@NonNegCondexp ?Ts ?dom ?prts ?dom2 ?sub ?g ?rv2 ?nnf2 ?x]] =>
rewrite <- (fun pf => @NonNegCondexp_ext
Ts dom prts dom2 sub f g rv1 rv2 nnf1 nnf2 pf x); [rewrite H | reflexivity]
end
| @ConditionalExpectation ?Ts ?dom ?prts ?dom2 ?sub ?f ?rv1 ?x = _ =>
match goal with
[|- context [@ConditionalExpectation ?Ts ?dom ?prts ?dom2 ?sub ?g ?rv2 ?x]] =>
rewrite <- (fun pf => @ConditionalExpectation_ext
Ts dom prts dom2 sub f g rv1 rv2 pf x); [rewrite H | reflexivity]
end
| @FiniteConditionalExpectation ?Ts ?dom ?prts ?dom2 ?sub ?f ?rv1 ?nnf1 ?x = _ =>
match goal with
[|- context [@FiniteConditionalExpectation ?Ts ?dom ?prts ?dom2 ?sub ?f ?rv2 ?nnf2 ?x]] =>
rewrite <- (fun pf => @FiniteConditionalExpectation_ext
Ts dom prts dom2 sub f f rv1 rv2 nnf1 nnf2 pf x); [rewrite H | reflexivity]
end
end.

Lemma Finite_conditional_variance_alt (x : Ts -> R)
{dom2 : SigmaAlgebra Ts}
(sub : sa_sub dom2 dom)
{rv : RandomVariable dom borel_sa x}
{isfe1 : IsFiniteExpectation prts x}
{isfe2 : IsFiniteExpectation prts (rvsqr x)}
{rv2 : RandomVariable
dom borel_sa
(rvsqr (rvminus x (FiniteConditionalExpectation prts sub x)))}
{isfe3 : IsFiniteExpectation
prts
(rvsqr (rvminus x (FiniteConditionalExpectation prts sub x)))}
{isfe4 : IsFiniteExpectation
prts
(rvsqr (FiniteConditionalExpectation prts sub x))}
{isfe5 : IsFiniteExpectation prts (rvmult (FiniteConditionalExpectation prts sub x) x)} :
almostR2 (prob_space_sa_sub prts sub) eq
(FiniteConditionalExpectation
prts sub
(rvsqr (rvminus x (FiniteConditionalExpectation prts sub x))))
(rvminus (FiniteConditionalExpectation prts sub (rvsqr x))
(rvsqr (FiniteConditionalExpectation prts sub x))).
Proof.
assert (rv3: RandomVariable dom2 borel_sa (FiniteConditionalExpectation prts sub x)).
{
apply FiniteCondexp_rv.
}
assert (rv4: RandomVariable dom borel_sa (FiniteConditionalExpectation prts sub x)).
{
apply FiniteCondexp_rv'.
}
assert (rv5: RandomVariable dom borel_sa (rvsqr (FiniteConditionalExpectation prts sub x))).
{
typeclasses eauto.
}
assert (rv6: RandomVariable dom borel_sa (rvmult (FiniteConditionalExpectation prts sub x) x)).
{
typeclasses eauto.
}
assert (rv7: RandomVariable dom borel_sa
(rvplus (rvscale (-2) (rvmult (FiniteConditionalExpectation prts sub x) x))
(rvsqr (FiniteConditionalExpectation prts sub x)))).
{
typeclasses eauto.
}
assert (rv8: RandomVariable
dom borel_sa
(rvplus (rvsqr x)
(rvplus (rvscale (-2) (rvmult (FiniteConditionalExpectation prts sub x) x))
(rvsqr (FiniteConditionalExpectation prts sub x))))).
{
typeclasses eauto.
}

assert (isfe6: IsFiniteExpectation prts (FiniteConditionalExpectation prts sub x)).
{
apply FiniteCondexp_isfe.
}

assert (isfe7: IsFiniteExpectation prts
(rvplus (rvscale (-2) (rvmult (FiniteConditionalExpectation prts sub x) x))
(rvsqr (FiniteConditionalExpectation prts sub x)))).
{
apply IsFiniteExpectation_plus; try typeclasses eauto.
}

assert (isfe8: IsFiniteExpectation
prts
(rvplus (rvsqr x)
(rvplus (rvscale (-2) (rvmult (FiniteConditionalExpectation prts sub x) x))
(rvsqr (FiniteConditionalExpectation prts sub x))))).
{
apply IsFiniteExpectation_plus; try typeclasses eauto.
}
assert (almostR2 (prob_space_sa_sub prts sub) eq
(FiniteConditionalExpectation
prts sub
(rvsqr (rvminus x (FiniteConditionalExpectation prts sub x))))
(FiniteConditionalExpectation
prts sub
(rvplus (rvsqr x)
(rvplus
(rvscale (- 2)
(rvmult (FiniteConditionalExpectation prts sub x) x))
(rvsqr (FiniteConditionalExpectation prts sub x)))))).
{
apply FiniteCondexp_proper.
apply all_almost; intros ?.
rv_unfold.
unfold Rsqr.
lra.
}
generalize (FiniteCondexp_plus
prts sub (rvsqr x)
(rvplus (rvscale (-2)
(rvmult (FiniteConditionalExpectation prts sub x) x))
(rvsqr (FiniteConditionalExpectation prts sub x))) ); intros.
generalize (FiniteCondexp_plus
prts sub
(rvscale (-2)
(rvmult (FiniteConditionalExpectation prts sub x) x))
(rvsqr (FiniteConditionalExpectation prts sub x))) ; intros.

generalize (FiniteCondexp_scale
prts sub (-2)
(rvmult (FiniteConditionalExpectation prts sub x) x)); intros.
generalize (FiniteCondexp_factor_out_l prts sub x (FiniteConditionalExpectation prts sub x)); intros.

revert H3; apply almost_impl.
revert H2; apply almost_impl.
revert H1; apply almost_impl.
revert H0; apply almost_impl.
revert H; apply almost_impl.
apply all_almost; intros ??????.
rewrite H.
rewrite_condexp_pf_irrel H0.
unfold rvplus at 1.
rewrite_condexp_pf_irrel H1.
unfold rvplus at 1.
rewrite H2.
unfold rvscale.
rewrite H3.
rv_unfold.
unfold Rsqr.

rewrite (FiniteCondexp_id _ _ (fun omega : Ts =>
FiniteConditionalExpectation prts sub x omega * FiniteConditionalExpectation prts sub x omega)).
lra.
Qed.

Instance Finite_conditional_variance_L2_alt_rv (x : Ts -> R)
{dom2 : SigmaAlgebra Ts}
(sub : sa_sub dom2 dom)
{rv : RandomVariable dom borel_sa x}
{isl2: IsLp prts 2 x} :
RandomVariable
dom borel_sa
(rvsqr (rvminus x (FiniteConditionalExpectation prts sub x))).
Proof.
apply (isfe_L2_variance prts sub x).
Qed.

Instance Finite_conditional_variance_L2_alt_isfe (x : Ts -> R)
{dom2 : SigmaAlgebra Ts}
(sub : sa_sub dom2 dom)
{rv : RandomVariable dom borel_sa x}
{isl2: IsLp prts 2 x} :
IsFiniteExpectation
prts
(rvsqr (rvminus x (FiniteConditionalExpectation prts sub x))).
Proof.
apply (isfe_L2_variance prts sub x).
Qed.


Lemma Finite_conditional_variance_L2_alt (x : Ts -> R)
{dom2 : SigmaAlgebra Ts}
(sub : sa_sub dom2 dom)
{rv : RandomVariable dom borel_sa x}
{isl2: IsLp prts 2 x} :
almostR2 (prob_space_sa_sub prts sub) eq
(FiniteConditionalExpectation
prts sub
(rvsqr (rvminus x (FiniteConditionalExpectation prts sub x))))
(rvminus (FiniteConditionalExpectation prts sub (rvsqr x))
(rvsqr (FiniteConditionalExpectation prts sub x))).
Proof.
apply Finite_conditional_variance_alt; apply (isfe_L2_variance prts sub x).
Qed.

Lemma Finite_conditional_variance_bound_L2_fun (x c : Ts -> R)
{dom2 : SigmaAlgebra Ts}
(sub : sa_sub dom2 dom)
{rv : RandomVariable dom borel_sa x}
{rv2 : RandomVariable dom2 borel_sa c}
{isfe2 : IsFiniteExpectation prts c}
{isl2: IsLp prts 2 x} :
almostR2 prts Rle (rvsqr x) (c) ->
almostR2 (prob_space_sa_sub prts sub) Rle (FiniteConditionalExpectation prts sub (rvsqr (rvminus x (FiniteConditionalExpectation prts sub x))))
(c).
Proof.
intros.
generalize (Finite_conditional_variance_L2_alt x sub); intros.
generalize (Finite_conditional_variance_bound1_fun x c sub H); intros.
revert H1; apply almost_impl.
revert H0; apply almost_impl.
apply all_almost; intros ???.
rewrite H0.
apply H1.
Qed.

End Stochastic_convergence.

Expand Down Expand Up @@ -11284,7 +11035,7 @@ End FixedPoint_contract.
{
intros.

generalize (Finite_conditional_variance_L2_alt_isfe (Xmin k sa) (filt_sub k)); intros.
generalize (FiniteConditionalVariance_exp_from_L2 prts (filt_sub k) (Xmin k sa) ); intros.
revert H7.
apply IsFiniteExpectation_proper.
intros ?.
Expand Down Expand Up @@ -11314,9 +11065,9 @@ End FixedPoint_contract.
apply isfe_Rmax_all; intros; typeclasses eauto.
}
generalize (Finite_conditional_variance_bound_L2_fun
(Xmin k sa)
prts (filt_sub k) (Xmin k sa)
(fun ω => (Rmax_all (fun sa => Rsqr (qlearn_Q k ω sa))))
(filt_sub k)); intros.
); intros.
cut_to H11.
- apply almost_prob_space_sa_sub_lift in H11.
revert H11.
Expand Down

0 comments on commit 1213fbd

Please sign in to comment.