Skip to content

Commit 1213fbd

Browse files
bmtragerbmtrager
committed
cleanup
1 parent 87be513 commit 1213fbd

1 file changed

Lines changed: 3 additions & 252 deletions

File tree

‎coq/QLearn/Tsitsiklis.v‎

Lines changed: 3 additions & 252 deletions
Original file line numberDiff line numberDiff line change
@@ -9202,255 +9202,6 @@ Qed.
92029202
Next Obligation.
92039203
apply fin_finite.
92049204
Qed.
9205-
9206-
Lemma Finite_conditional_variance_bound1_fun (x c : Ts -> R)
9207-
{dom2 : SigmaAlgebra Ts}
9208-
(sub : sa_sub dom2 dom)
9209-
{rv : RandomVariable dom borel_sa x}
9210-
{rv2 : RandomVariable dom2 borel_sa c}
9211-
{isfe : IsFiniteExpectation prts x}
9212-
{isfe2 : IsFiniteExpectation prts c}
9213-
{isfe0 : IsFiniteExpectation prts (rvsqr x)} :
9214-
almostR2 prts Rle (rvsqr x) (c) ->
9215-
almostR2 (prob_space_sa_sub prts sub) Rle (rvminus (FiniteConditionalExpectation prts sub (rvsqr x))
9216-
(rvsqr (FiniteConditionalExpectation prts sub x)))
9217-
(c).
9218-
Proof.
9219-
intros.
9220-
assert (rv3: RandomVariable dom borel_sa c).
9221-
{
9222-
now apply (RandomVariable_sa_sub sub).
9223-
}
9224-
generalize (FiniteCondexp_ale
9225-
prts sub (rvsqr x) (c)); intros.
9226-
cut_to H0; try easy.
9227-
revert H0; apply almost_impl.
9228-
apply all_almost; intros ??.
9229-
rewrite FiniteCondexp_id with (f := c) in H0; trivial.
9230-
rv_unfold.
9231-
eapply Rle_trans.
9232-
shelve.
9233-
apply H0.
9234-
Unshelve.
9235-
assert (0 <= (FiniteConditionalExpectation prts sub x x0)²).
9236-
{
9237-
apply Rle_0_sqr.
9238-
}
9239-
lra.
9240-
Qed.
9241-
9242-
Ltac rewrite_condexp_pf_irrel H
9243-
:= match type of H with
9244-
| @NonNegCondexp ?Ts ?dom ?prts ?dom2 ?sub ?f ?rv1 ?nnf1 ?x = _ =>
9245-
match goal with
9246-
[|- context [@NonNegCondexp ?Ts ?dom ?prts ?dom2 ?sub ?g ?rv2 ?nnf2 ?x]] =>
9247-
rewrite <- (fun pf => @NonNegCondexp_ext
9248-
Ts dom prts dom2 sub f g rv1 rv2 nnf1 nnf2 pf x); [rewrite H | reflexivity]
9249-
end
9250-
| @ConditionalExpectation ?Ts ?dom ?prts ?dom2 ?sub ?f ?rv1 ?x = _ =>
9251-
match goal with
9252-
[|- context [@ConditionalExpectation ?Ts ?dom ?prts ?dom2 ?sub ?g ?rv2 ?x]] =>
9253-
rewrite <- (fun pf => @ConditionalExpectation_ext
9254-
Ts dom prts dom2 sub f g rv1 rv2 pf x); [rewrite H | reflexivity]
9255-
end
9256-
| @FiniteConditionalExpectation ?Ts ?dom ?prts ?dom2 ?sub ?f ?rv1 ?nnf1 ?x = _ =>
9257-
match goal with
9258-
[|- context [@FiniteConditionalExpectation ?Ts ?dom ?prts ?dom2 ?sub ?f ?rv2 ?nnf2 ?x]] =>
9259-
rewrite <- (fun pf => @FiniteConditionalExpectation_ext
9260-
Ts dom prts dom2 sub f f rv1 rv2 nnf1 nnf2 pf x); [rewrite H | reflexivity]
9261-
end
9262-
end.
9263-
9264-
Lemma Finite_conditional_variance_alt (x : Ts -> R)
9265-
{dom2 : SigmaAlgebra Ts}
9266-
(sub : sa_sub dom2 dom)
9267-
{rv : RandomVariable dom borel_sa x}
9268-
{isfe1 : IsFiniteExpectation prts x}
9269-
{isfe2 : IsFiniteExpectation prts (rvsqr x)}
9270-
{rv2 : RandomVariable
9271-
dom borel_sa
9272-
(rvsqr (rvminus x (FiniteConditionalExpectation prts sub x)))}
9273-
{isfe3 : IsFiniteExpectation
9274-
prts
9275-
(rvsqr (rvminus x (FiniteConditionalExpectation prts sub x)))}
9276-
{isfe4 : IsFiniteExpectation
9277-
prts
9278-
(rvsqr (FiniteConditionalExpectation prts sub x))}
9279-
{isfe5 : IsFiniteExpectation prts (rvmult (FiniteConditionalExpectation prts sub x) x)} :
9280-
almostR2 (prob_space_sa_sub prts sub) eq
9281-
(FiniteConditionalExpectation
9282-
prts sub
9283-
(rvsqr (rvminus x (FiniteConditionalExpectation prts sub x))))
9284-
(rvminus (FiniteConditionalExpectation prts sub (rvsqr x))
9285-
(rvsqr (FiniteConditionalExpectation prts sub x))).
9286-
Proof.
9287-
assert (rv3: RandomVariable dom2 borel_sa (FiniteConditionalExpectation prts sub x)).
9288-
{
9289-
apply FiniteCondexp_rv.
9290-
}
9291-
assert (rv4: RandomVariable dom borel_sa (FiniteConditionalExpectation prts sub x)).
9292-
{
9293-
apply FiniteCondexp_rv'.
9294-
}
9295-
assert (rv5: RandomVariable dom borel_sa (rvsqr (FiniteConditionalExpectation prts sub x))).
9296-
{
9297-
typeclasses eauto.
9298-
}
9299-
assert (rv6: RandomVariable dom borel_sa (rvmult (FiniteConditionalExpectation prts sub x) x)).
9300-
{
9301-
typeclasses eauto.
9302-
}
9303-
assert (rv7: RandomVariable dom borel_sa
9304-
(rvplus (rvscale (-2) (rvmult (FiniteConditionalExpectation prts sub x) x))
9305-
(rvsqr (FiniteConditionalExpectation prts sub x)))).
9306-
{
9307-
typeclasses eauto.
9308-
}
9309-
assert (rv8: RandomVariable
9310-
dom borel_sa
9311-
(rvplus (rvsqr x)
9312-
(rvplus (rvscale (-2) (rvmult (FiniteConditionalExpectation prts sub x) x))
9313-
(rvsqr (FiniteConditionalExpectation prts sub x))))).
9314-
{
9315-
typeclasses eauto.
9316-
}
9317-
9318-
assert (isfe6: IsFiniteExpectation prts (FiniteConditionalExpectation prts sub x)).
9319-
{
9320-
apply FiniteCondexp_isfe.
9321-
}
9322-
9323-
assert (isfe7: IsFiniteExpectation prts
9324-
(rvplus (rvscale (-2) (rvmult (FiniteConditionalExpectation prts sub x) x))
9325-
(rvsqr (FiniteConditionalExpectation prts sub x)))).
9326-
{
9327-
apply IsFiniteExpectation_plus; try typeclasses eauto.
9328-
}
9329-
9330-
assert (isfe8: IsFiniteExpectation
9331-
prts
9332-
(rvplus (rvsqr x)
9333-
(rvplus (rvscale (-2) (rvmult (FiniteConditionalExpectation prts sub x) x))
9334-
(rvsqr (FiniteConditionalExpectation prts sub x))))).
9335-
{
9336-
apply IsFiniteExpectation_plus; try typeclasses eauto.
9337-
}
9338-
assert (almostR2 (prob_space_sa_sub prts sub) eq
9339-
(FiniteConditionalExpectation
9340-
prts sub
9341-
(rvsqr (rvminus x (FiniteConditionalExpectation prts sub x))))
9342-
(FiniteConditionalExpectation
9343-
prts sub
9344-
(rvplus (rvsqr x)
9345-
(rvplus
9346-
(rvscale (- 2)
9347-
(rvmult (FiniteConditionalExpectation prts sub x) x))
9348-
(rvsqr (FiniteConditionalExpectation prts sub x)))))).
9349-
{
9350-
apply FiniteCondexp_proper.
9351-
apply all_almost; intros ?.
9352-
rv_unfold.
9353-
unfold Rsqr.
9354-
lra.
9355-
}
9356-
generalize (FiniteCondexp_plus
9357-
prts sub (rvsqr x)
9358-
(rvplus (rvscale (-2)
9359-
(rvmult (FiniteConditionalExpectation prts sub x) x))
9360-
(rvsqr (FiniteConditionalExpectation prts sub x))) ); intros.
9361-
generalize (FiniteCondexp_plus
9362-
prts sub
9363-
(rvscale (-2)
9364-
(rvmult (FiniteConditionalExpectation prts sub x) x))
9365-
(rvsqr (FiniteConditionalExpectation prts sub x))) ; intros.
9366-
9367-
generalize (FiniteCondexp_scale
9368-
prts sub (-2)
9369-
(rvmult (FiniteConditionalExpectation prts sub x) x)); intros.
9370-
generalize (FiniteCondexp_factor_out_l prts sub x (FiniteConditionalExpectation prts sub x)); intros.
9371-
9372-
revert H3; apply almost_impl.
9373-
revert H2; apply almost_impl.
9374-
revert H1; apply almost_impl.
9375-
revert H0; apply almost_impl.
9376-
revert H; apply almost_impl.
9377-
apply all_almost; intros ??????.
9378-
rewrite H.
9379-
rewrite_condexp_pf_irrel H0.
9380-
unfold rvplus at 1.
9381-
rewrite_condexp_pf_irrel H1.
9382-
unfold rvplus at 1.
9383-
rewrite H2.
9384-
unfold rvscale.
9385-
rewrite H3.
9386-
rv_unfold.
9387-
unfold Rsqr.
9388-
9389-
rewrite (FiniteCondexp_id _ _ (fun omega : Ts =>
9390-
FiniteConditionalExpectation prts sub x omega * FiniteConditionalExpectation prts sub x omega)).
9391-
lra.
9392-
Qed.
9393-
9394-
Instance Finite_conditional_variance_L2_alt_rv (x : Ts -> R)
9395-
{dom2 : SigmaAlgebra Ts}
9396-
(sub : sa_sub dom2 dom)
9397-
{rv : RandomVariable dom borel_sa x}
9398-
{isl2: IsLp prts 2 x} :
9399-
RandomVariable
9400-
dom borel_sa
9401-
(rvsqr (rvminus x (FiniteConditionalExpectation prts sub x))).
9402-
Proof.
9403-
apply (isfe_L2_variance prts sub x).
9404-
Qed.
9405-
9406-
Instance Finite_conditional_variance_L2_alt_isfe (x : Ts -> R)
9407-
{dom2 : SigmaAlgebra Ts}
9408-
(sub : sa_sub dom2 dom)
9409-
{rv : RandomVariable dom borel_sa x}
9410-
{isl2: IsLp prts 2 x} :
9411-
IsFiniteExpectation
9412-
prts
9413-
(rvsqr (rvminus x (FiniteConditionalExpectation prts sub x))).
9414-
Proof.
9415-
apply (isfe_L2_variance prts sub x).
9416-
Qed.
9417-
9418-
9419-
Lemma Finite_conditional_variance_L2_alt (x : Ts -> R)
9420-
{dom2 : SigmaAlgebra Ts}
9421-
(sub : sa_sub dom2 dom)
9422-
{rv : RandomVariable dom borel_sa x}
9423-
{isl2: IsLp prts 2 x} :
9424-
almostR2 (prob_space_sa_sub prts sub) eq
9425-
(FiniteConditionalExpectation
9426-
prts sub
9427-
(rvsqr (rvminus x (FiniteConditionalExpectation prts sub x))))
9428-
(rvminus (FiniteConditionalExpectation prts sub (rvsqr x))
9429-
(rvsqr (FiniteConditionalExpectation prts sub x))).
9430-
Proof.
9431-
apply Finite_conditional_variance_alt; apply (isfe_L2_variance prts sub x).
9432-
Qed.
9433-
9434-
Lemma Finite_conditional_variance_bound_L2_fun (x c : Ts -> R)
9435-
{dom2 : SigmaAlgebra Ts}
9436-
(sub : sa_sub dom2 dom)
9437-
{rv : RandomVariable dom borel_sa x}
9438-
{rv2 : RandomVariable dom2 borel_sa c}
9439-
{isfe2 : IsFiniteExpectation prts c}
9440-
{isl2: IsLp prts 2 x} :
9441-
almostR2 prts Rle (rvsqr x) (c) ->
9442-
almostR2 (prob_space_sa_sub prts sub) Rle (FiniteConditionalExpectation prts sub (rvsqr (rvminus x (FiniteConditionalExpectation prts sub x))))
9443-
(c).
9444-
Proof.
9445-
intros.
9446-
generalize (Finite_conditional_variance_L2_alt x sub); intros.
9447-
generalize (Finite_conditional_variance_bound1_fun x c sub H); intros.
9448-
revert H1; apply almost_impl.
9449-
revert H0; apply almost_impl.
9450-
apply all_almost; intros ???.
9451-
rewrite H0.
9452-
apply H1.
9453-
Qed.
94549205

94559206
End Stochastic_convergence.
94569207

@@ -11284,7 +11035,7 @@ End FixedPoint_contract.
1128411035
{
1128511036
intros.
1128611037

11287-
generalize (Finite_conditional_variance_L2_alt_isfe (Xmin k sa) (filt_sub k)); intros.
11038+
generalize (FiniteConditionalVariance_exp_from_L2 prts (filt_sub k) (Xmin k sa) ); intros.
1128811039
revert H7.
1128911040
apply IsFiniteExpectation_proper.
1129011041
intros ?.
@@ -11314,9 +11065,9 @@ End FixedPoint_contract.
1131411065
apply isfe_Rmax_all; intros; typeclasses eauto.
1131511066
}
1131611067
generalize (Finite_conditional_variance_bound_L2_fun
11317-
(Xmin k sa)
11068+
prts (filt_sub k) (Xmin k sa)
1131811069
(fun ω => (Rmax_all (fun sa => Rsqr (qlearn_Q k ω sa))))
11319-
(filt_sub k)); intros.
11070+
); intros.
1132011071
cut_to H11.
1132111072
- apply almost_prob_space_sa_sub_lift in H11.
1132211073
revert H11.

0 commit comments

Comments
 (0)