Library QBS.qbs_quotient
From HB Require Import structures.
From mathcomp Require Import all_boot all_algebra reals classical_sets boolp
ereal measurable_structure measurable_function probability_measure
lebesgue_stieltjes_measure lebesgue_integral.
From QBS Require Import quasi_borel probability_qbs.
Import GRing.Theory Num.Def Num.Theory.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Local Open Scope classical_set_scope.
Section qbs_quotient.
Variable R : realType.
Local Notation mR := (measurableTypeR R).
Implicit Types (X Y Z : qbsType R).
From mathcomp Require Import all_boot all_algebra reals classical_sets boolp
ereal measurable_structure measurable_function probability_measure
lebesgue_stieltjes_measure lebesgue_integral.
From QBS Require Import quasi_borel probability_qbs.
Import GRing.Theory Num.Def Num.Theory.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Local Open Scope classical_set_scope.
Section qbs_quotient.
Variable R : realType.
Local Notation mR := (measurableTypeR R).
Implicit Types (X Y Z : qbsType R).
Boolean version of qbs_prob_equiv via classical decidability.
Definition qbs_equiv_op : rel (qbs_prob X) :=
fun p1 p2 ⇒ `[< qbs_prob_equiv X p1 p2 >].
Let qbs_equiv_op_refl : reflexive qbs_equiv_op.
Proof. by move⇒ p; apply/asboolP/qbs_prob_equivxx. Qed.
Let qbs_equiv_op_sym : symmetric qbs_equiv_op.
Proof.
move⇒ p q; apply/idP/idP ⇒ /asboolP h; apply/asboolP/qbs_prob_equivC ⇒ //.
Qed.
Let qbs_equiv_op_trans : transitive qbs_equiv_op.
Proof.
move⇒ q p r /asboolP hpq /asboolP hqr.
by apply/asboolP; exact: (qbs_prob_equiv_trans hpq hqr).
Qed.
fun p1 p2 ⇒ `[< qbs_prob_equiv X p1 p2 >].
Let qbs_equiv_op_refl : reflexive qbs_equiv_op.
Proof. by move⇒ p; apply/asboolP/qbs_prob_equivxx. Qed.
Let qbs_equiv_op_sym : symmetric qbs_equiv_op.
Proof.
move⇒ p q; apply/idP/idP ⇒ /asboolP h; apply/asboolP/qbs_prob_equivC ⇒ //.
Qed.
Let qbs_equiv_op_trans : transitive qbs_equiv_op.
Proof.
move⇒ q p r /asboolP hpq /asboolP hqr.
by apply/asboolP; exact: (qbs_prob_equiv_trans hpq hqr).
Qed.
Canonical equiv_rel structure for generic_quotient.
Canonical qbs_prob_equivRel :=
EquivRel qbs_equiv_op qbs_equiv_op_refl qbs_equiv_op_sym qbs_equiv_op_trans.
EquivRel qbs_equiv_op qbs_equiv_op_refl qbs_equiv_op_sym qbs_equiv_op_trans.
Classical eqType and choiceType instances on qbs_prob X.
These are required by generic_quotient's {eq_quot} construction.
HB.instance Definition _ := gen_eqMixin (qbs_prob X).
HB.instance Definition _ := gen_choiceMixin (qbs_prob X).
End equiv_instances.
HB.instance Definition _ := gen_choiceMixin (qbs_prob X).
End equiv_instances.
The quotient type: qbs_prob X quotiented by pushforward-measure
equality. Elements of qbs_quot X are equivalence classes of
probability triples. Equality in qbs_quot X is decidable
(classically) and corresponds exactly to qbs_prob_equiv.
Recover standard HB instances on the quotient type.
Reflection between Prop-valued qbs_prob_equiv and equality in the
quotient. This is the fundamental bridge: two probability triples
are equivalent iff their images under \pi are equal.
Lemma qbs_equivP (p1 p2 : qbs_prob X) :
reflect (qbs_prob_equiv X p1 p2)
(@pi_subdef _ qbs_quot p1 == @pi_subdef _ qbs_quot p2).
Proof.
suff → : (@pi_subdef _ qbs_quot p1 == @pi_subdef _ qbs_quot p2) =
`[< qbs_prob_equiv X p1 p2 >] by exact: asboolP.
have → : pi_subdef qbs_quot = (\pi : _ → qbs_quot)
by rewrite /pi_subdef unlock.
by rewrite eqquotE.
Qed.
reflect (qbs_prob_equiv X p1 p2)
(@pi_subdef _ qbs_quot p1 == @pi_subdef _ qbs_quot p2).
Proof.
suff → : (@pi_subdef _ qbs_quot p1 == @pi_subdef _ qbs_quot p2) =
`[< qbs_prob_equiv X p1 p2 >] by exact: asboolP.
have → : pi_subdef qbs_quot = (\pi : _ → qbs_quot)
by rewrite /pi_subdef unlock.
by rewrite eqquotE.
Qed.
Equivalent: iff version for rewriting.
Lemma qbs_equivE (p1 p2 : qbs_prob X) :
(@pi_subdef _ qbs_quot p1 == @pi_subdef _ qbs_quot p2) =
`[< qbs_prob_equiv X p1 p2 >].
Proof.
have → : pi_subdef qbs_quot = (\pi : _ → qbs_quot)
by rewrite /pi_subdef unlock.
by rewrite eqquotE.
Qed.
(@pi_subdef _ qbs_quot p1 == @pi_subdef _ qbs_quot p2) =
`[< qbs_prob_equiv X p1 p2 >].
Proof.
have → : pi_subdef qbs_quot = (\pi : _ → qbs_quot)
by rewrite /pi_subdef unlock.
by rewrite eqquotE.
Qed.
repr always picks a representative in the same equivalence class.
Lemma repr_equiv (q : qbs_quot) :
qbs_prob_equiv X (repr q) (repr q).
Proof. exact: qbs_prob_equivxx. Qed.
qbs_prob_equiv X (repr q) (repr q).
Proof. exact: qbs_prob_equivxx. Qed.
\pi composed with repr is the identity (from generic_quotient).
Lemma quot_reprK : cancel (repr : qbs_quot → qbs_prob X)
(\pi : qbs_prob X → qbs_quot).
Proof. exact: reprK. Qed.
End quotient_def.
(\pi : qbs_prob X → qbs_quot).
Proof. exact: reprK. Qed.
End quotient_def.
Local notation for the canonical surjection.
Local Notation piX := (@pi_subdef (qbs_prob X) (qbs_quot X)).
Local Notation piY := (@pi_subdef (qbs_prob Y) (qbs_quot Y)).
Local Notation piY := (@pi_subdef (qbs_prob Y) (qbs_quot Y)).
Return lifted to the quotient.
Integration on the quotient, defined via representative.
Map lifted to the quotient: given a morphism f : X -> Y, push
forward the probability. This uses repr on the input and \pi
on the output.
Definition quot_map (f : X → Y) (hf : qbs_morphism f)
(q : qbs_quot X) : qbs_quot Y :=
piY (monadP_map X Y f hf (repr q)).
(q : qbs_quot X) : qbs_quot Y :=
piY (monadP_map X Y f hf (repr q)).
Bind lifted to the quotient (strong morphism version).
The strong morphism condition ensures diagonal randomness
without an explicit proof. On the quotient, this is the key
improvement: we operate on repr and project back via \pi.
Definition quot_bind_strong
(f : X → qbs_prob Y) (hf : qbs_morphism_strong X Y f)
(q : qbs_quot X) : qbs_quot Y :=
piY (qbs_bind_strong X Y (repr q) f hf).
End lifted_ops.
(f : X → qbs_prob Y) (hf : qbs_morphism_strong X Y f)
(q : qbs_quot X) : qbs_quot Y :=
piY (qbs_bind_strong X Y (repr q) f hf).
End lifted_ops.
Section well_defined.
Variables (X Y : qbsType R).
Local Notation piX := (@pi_subdef (qbs_prob X) (qbs_quot X)).
Local Notation piY := (@pi_subdef (qbs_prob Y) (qbs_quot Y)).
Return: all returns at the same point are identified in the quotient.
Lemma quot_return_equiv (x : X) (mu1 mu2 : probability mR R) :
quot_return x mu1 = quot_return x mu2 :> qbs_quot X.
Proof.
apply/eqP/qbs_equivP.
exact: qbs_return_equiv.
Qed.
quot_return x mu1 = quot_return x mu2 :> qbs_quot X.
Proof.
apply/eqP/qbs_equivP.
exact: qbs_return_equiv.
Qed.
Map respects the quotient.
Lemma quot_map_proper (f : X → Y) (hf : qbs_morphism f)
(p1 p2 : qbs_prob X) :
qbs_prob_equiv X p1 p2 →
piY (monadP_map X Y f hf p1) = piY (monadP_map X Y f hf p2) :> qbs_quot Y.
Proof.
move⇒ hequiv; apply/eqP/qbs_equivP ⇒ U hU /=.
have hpreimg : ∀ (p : qbs_prob X),
(f \o qbs_prob_alpha p) @^-1` U = qbs_prob_alpha p @^-1` (f @^-1` U).
by move⇒ p.
by rewrite !hpreimg; apply: hequiv; move⇒ alpha halpha; apply: hU; apply: hf.
Qed.
(p1 p2 : qbs_prob X) :
qbs_prob_equiv X p1 p2 →
piY (monadP_map X Y f hf p1) = piY (monadP_map X Y f hf p2) :> qbs_quot Y.
Proof.
move⇒ hequiv; apply/eqP/qbs_equivP ⇒ U hU /=.
have hpreimg : ∀ (p : qbs_prob X),
(f \o qbs_prob_alpha p) @^-1` U = qbs_prob_alpha p @^-1` (f @^-1` U).
by move⇒ p.
by rewrite !hpreimg; apply: hequiv; move⇒ alpha halpha; apply: hU; apply: hf.
Qed.
Bind (strong) respects the quotient in its probability argument,
given a factoring morphism. This is the quotient-level version
of qbs_bind_strong_equiv_l.
Lemma quot_bind_strong_proper
(f : X → qbs_prob Y)
(g : X → Y) (hg : qbs_morphism g)
(hf : qbs_morphism_strong X Y f)
(hfact : ∀ (p : qbs_prob X) r,
qbs_prob_alpha (f (qbs_prob_alpha p r)) r = g (qbs_prob_alpha p r))
(p1 p2 : qbs_prob X)
(hequiv : qbs_prob_equiv X p1 p2) :
piY (qbs_bind_strong X Y p1 f hf) =
piY (qbs_bind_strong X Y p2 f hf) :> qbs_quot Y.
Proof.
apply/eqP/qbs_equivP.
exact: (qbs_bind_strong_equiv_l hg hf (hfact p1) (hfact p2) hequiv).
Qed.
(f : X → qbs_prob Y)
(g : X → Y) (hg : qbs_morphism g)
(hf : qbs_morphism_strong X Y f)
(hfact : ∀ (p : qbs_prob X) r,
qbs_prob_alpha (f (qbs_prob_alpha p r)) r = g (qbs_prob_alpha p r))
(p1 p2 : qbs_prob X)
(hequiv : qbs_prob_equiv X p1 p2) :
piY (qbs_bind_strong X Y p1 f hf) =
piY (qbs_bind_strong X Y p2 f hf) :> qbs_quot Y.
Proof.
apply/eqP/qbs_equivP.
exact: (qbs_bind_strong_equiv_l hg hf (hfact p1) (hfact p2) hequiv).
Qed.
Integration respects the quotient for qbs-measurable integrands.
Lemma quot_integral_proper (p1 p2 : qbs_prob X)
(h : X → \bar R)
(hm : qbs_measurable X h)
(hint1 : (qbs_prob_mu p1).-integrable setT
(h \o qbs_prob_alpha p1))
(hint2 : (qbs_prob_mu p2).-integrable setT
(h \o qbs_prob_alpha p2)) :
qbs_prob_equiv X p1 p2 →
qbs_integral X p1 h = qbs_integral X p2 h.
Proof. exact: qbs_integral_equiv. Qed.
End well_defined.
(h : X → \bar R)
(hm : qbs_measurable X h)
(hint1 : (qbs_prob_mu p1).-integrable setT
(h \o qbs_prob_alpha p1))
(hint2 : (qbs_prob_mu p2).-integrable setT
(h \o qbs_prob_alpha p2)) :
qbs_prob_equiv X p1 p2 →
qbs_integral X p1 h = qbs_integral X p2 h.
Proof. exact: qbs_integral_equiv. Qed.
End well_defined.
Section monad_laws_quot.
Variables (X Y Z : qbsType R).
Local Notation piX := (@pi_subdef (qbs_prob X) (qbs_quot X)).
Local Notation piY := (@pi_subdef (qbs_prob Y) (qbs_quot Y)).
Left unit: bind (return x) f ~ f x, as an equality in the quotient.
We state this at the level of piY applied to qbs_bind_strong, not
through quot_bind_strong (which goes via repr, losing the definitional
structure of the return).
Lemma quot_bind_returnl (x : X)
(f : X → qbs_prob Y)
(hf_morph : qbs_morphism f)
(hf_strong : qbs_morphism_strong X Y f) :
piY (qbs_bind_strong X Y (qbs_return X x (qbs_prob_mu (f x))) f hf_strong) =
piY (f x) :> qbs_quot Y.
Proof.
apply/eqP/qbs_equivP.
exact: qbs_bind_returnl.
Qed.
(f : X → qbs_prob Y)
(hf_morph : qbs_morphism f)
(hf_strong : qbs_morphism_strong X Y f) :
piY (qbs_bind_strong X Y (qbs_return X x (qbs_prob_mu (f x))) f hf_strong) =
piY (f x) :> qbs_quot Y.
Proof.
apply/eqP/qbs_equivP.
exact: qbs_bind_returnl.
Qed.
Right unit: bind m return ~ m, as an equality in the quotient.
Lemma quot_bind_returnr (m : qbs_prob X) (mu : probability mR R) :
@pi_subdef _ (qbs_quot X)
(qbs_bind X X m (qbs_return X ^~ mu)
(qbs_bind_alpha_random_return m mu)) =
@pi_subdef _ (qbs_quot X) m.
Proof.
apply/eqP/qbs_equivP.
exact: qbs_bind_returnr.
Qed.
End monad_laws_quot.
@pi_subdef _ (qbs_quot X)
(qbs_bind X X m (qbs_return X ^~ mu)
(qbs_bind_alpha_random_return m mu)) =
@pi_subdef _ (qbs_quot X) m.
Proof.
apply/eqP/qbs_equivP.
exact: qbs_bind_returnr.
Qed.
End monad_laws_quot.
End qbs_quotient.
Arguments qbs_equiv_op {R X}.
Arguments qbs_prob_equivRel {R}.
Arguments qbs_quot {R}.
Arguments qbs_equivP {R X}.
Arguments qbs_equivE {R X}.
Arguments quot_return {R X}.
Arguments quot_integral {R X}.
Arguments quot_map {R X Y}.
Arguments quot_bind_strong {R X Y}.
Arguments quot_return_equiv {R X}.
Arguments quot_bind_returnl {R X Y}.