Library QBS.quasi_borel
From HB Require Import structures.
From mathcomp Require Import all_boot all_algebra reals classical_sets
num_topology measurable_structure measurable_function
lebesgue_stieltjes_measure measurable_realfun.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Import Num.Def Num.Theory.
Import numFieldTopology.Exports.
Local Open Scope classical_set_scope.
Local Open Scope ring_scope.
From mathcomp Require Import all_boot all_algebra reals classical_sets
num_topology measurable_structure measurable_function
lebesgue_stieltjes_measure measurable_realfun.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Import Num.Def Num.Theory.
Import numFieldTopology.Exports.
Local Open Scope classical_set_scope.
Local Open Scope ring_scope.
Mixin: a QBS is a type with a set of random elements.
HB.mixin Record isQBS (R : realType) (T : Type) := {
qbs_Mx : set (measurableTypeR R → T) ;
qbs_Mx_comp : ∀ alpha
(f : {mfun measurableTypeR R >-> measurableTypeR R}),
qbs_Mx alpha → qbs_Mx (alpha \o f) ;
qbs_Mx_const : ∀ x : T, qbs_Mx (fun _ ⇒ x) ;
qbs_Mx_glue : ∀ (P : {mfun measurableTypeR R >-> nat})
(Fi : nat → measurableTypeR R → T),
(∀ i, qbs_Mx (Fi i)) →
qbs_Mx (fun r ⇒ Fi (P r) r) }.
qbs_Mx : set (measurableTypeR R → T) ;
qbs_Mx_comp : ∀ alpha
(f : {mfun measurableTypeR R >-> measurableTypeR R}),
qbs_Mx alpha → qbs_Mx (alpha \o f) ;
qbs_Mx_const : ∀ x : T, qbs_Mx (fun _ ⇒ x) ;
qbs_Mx_glue : ∀ (P : {mfun measurableTypeR R >-> nat})
(Fi : nat → measurableTypeR R → T),
(∀ i, qbs_Mx (Fi i)) →
qbs_Mx (fun r ⇒ Fi (P r) r) }.
Structure: a quasi-Borel space over reals R.
#[short(type="qbsType")]
HB.structure Definition QBSpace (R : realType) := { T of isQBS R T }.
HB.mixin Record isQBSMorphism (R : realType) (X Y : qbsType R)
(f : X → Y) := {
qbs_hom_proof : ∀ alpha, qbs_Mx (s := X) alpha →
qbs_Mx (s := Y) (f \o alpha)
}.
#[short(type="qbsHomType")]
HB.structure Definition QBSHom (R : realType) (X Y : qbsType R) :=
{f of @isQBSMorphism R X Y f}.
Section qbs.
Variable R : realType.
Local Notation mR := (measurableTypeR R).
Implicit Types (X Y Z W : qbsType R).
HB.structure Definition QBSpace (R : realType) := { T of isQBS R T }.
HB.mixin Record isQBSMorphism (R : realType) (X Y : qbsType R)
(f : X → Y) := {
qbs_hom_proof : ∀ alpha, qbs_Mx (s := X) alpha →
qbs_Mx (s := Y) (f \o alpha)
}.
#[short(type="qbsHomType")]
HB.structure Definition QBSHom (R : realType) (X Y : qbsType R) :=
{f of @isQBSMorphism R X Y f}.
Section qbs.
Variable R : realType.
Local Notation mR := (measurableTypeR R).
Implicit Types (X Y Z W : qbsType R).
QBS morphism: preserves random elements.
Definition qbs_morphism (X Y : qbsType R) (f : X → Y) : Prop :=
∀ alpha, qbs_Mx alpha → qbs_Mx (f \o alpha).
Section qbs_id_instance.
Variable X : qbsType R.
Let f : X → X := idfun.
Let hf : qbs_morphism f := fun alpha halpha ⇒ halpha.
HB.instance Definition _ := @isQBSMorphism.Build R X X f hf.
Definition qbs_id : qbsHomType X X := f.
End qbs_id_instance.
Section qbs_comp_instance.
Variables (X Y Z : qbsType R).
Variables (f : qbsHomType X Y) (g : qbsHomType Y Z).
Let gf := (g : Y → Z) \o (f : X → Y).
Let hgf : qbs_morphism gf :=
fun alpha halpha ⇒
qbs_hom_proof _ (qbs_hom_proof _ halpha).
HB.instance Definition _ := @isQBSMorphism.Build R X Z gf hgf.
Definition qbs_comp : qbsHomType X Z := gf.
End qbs_comp_instance.
Section qbs_const_instance.
Variables (X Y : qbsType R) (y : Y).
Let f := fun _ : X ⇒ y.
Let hf : qbs_morphism f :=
fun alpha _ ⇒ qbs_Mx_const y.
HB.instance Definition _ := @isQBSMorphism.Build R X Y f hf.
Definition qbs_const : qbsHomType X Y := f.
End qbs_const_instance.
∀ alpha, qbs_Mx alpha → qbs_Mx (f \o alpha).
Section qbs_id_instance.
Variable X : qbsType R.
Let f : X → X := idfun.
Let hf : qbs_morphism f := fun alpha halpha ⇒ halpha.
HB.instance Definition _ := @isQBSMorphism.Build R X X f hf.
Definition qbs_id : qbsHomType X X := f.
End qbs_id_instance.
Section qbs_comp_instance.
Variables (X Y Z : qbsType R).
Variables (f : qbsHomType X Y) (g : qbsHomType Y Z).
Let gf := (g : Y → Z) \o (f : X → Y).
Let hgf : qbs_morphism gf :=
fun alpha halpha ⇒
qbs_hom_proof _ (qbs_hom_proof _ halpha).
HB.instance Definition _ := @isQBSMorphism.Build R X Z gf hgf.
Definition qbs_comp : qbsHomType X Z := gf.
End qbs_comp_instance.
Section qbs_const_instance.
Variables (X Y : qbsType R) (y : Y).
Let f := fun _ : X ⇒ y.
Let hf : qbs_morphism f :=
fun alpha _ ⇒ qbs_Mx_const y.
HB.instance Definition _ := @isQBSMorphism.Build R X Y f hf.
Definition qbs_const : qbsHomType X Y := f.
End qbs_const_instance.
Convenience wrappers: accept bare measurable_fun setT proofs.
Lemma qbs_Mx_compT (X : qbsType R) (alpha : mR → X) (f : mR → mR) :
qbs_Mx alpha → measurable_fun setT f → qbs_Mx (alpha \o f).
Proof.
by move⇒ ha hf; exact: (qbs_Mx_comp (s := X) alpha (mfun_Sub (mem_set hf)) ha).
Qed.
Lemma qbs_Mx_glueT (X : qbsType R)
(P : mR → nat) (Fi : nat → mR → X) :
measurable_fun setT P →
(∀ i, qbs_Mx (Fi i)) →
qbs_Mx (fun r ⇒ Fi (P r) r).
Proof.
by move⇒ hP hFi; exact: (qbs_Mx_glue (s := X) (mfun_Sub (mem_set hP)) Fi hFi).
Qed.
Lemma measurable_glue d (M : measurableType d)
(P : mR → nat) (Fi : nat → mR → M) :
measurable_fun setT P →
(∀ i, measurable_fun setT (Fi i)) →
measurable_fun setT (fun r ⇒ Fi (P r) r).
Proof.
move⇒ hP hFi _ U mU; rewrite setTI.
have → : (fun r ⇒ Fi (P r) r) @^-1` U =
\bigcup_i (P @^-1` [set i] `&` (Fi i) @^-1` U).
rewrite eqEsubset; split ⇒ [r hUr | r [i _ [hPi hFir]]].
by ∃ (P r).
by rewrite /preimage /=; rewrite /preimage /= in hPi; rewrite hPi.
apply: bigcupT_measurable ⇒ i; apply: measurableI.
by have := hP measurableT [set i] I; rewrite setTI; exact.
by have := hFi i measurableT U mU; rewrite setTI; exact.
Qed.
Section R_qbs_instance.
Context d (M : measurableType d).
Let Mx := [set f : mR → M | measurable_fun setT f].
Let ax1 : ∀ alpha (f : {mfun mR >-> mR}),
Mx alpha → Mx (alpha \o f).
Proof.
move⇒ alpha f ha; rewrite /Mx /=.
exact: measurableT_comp.
Qed.
Let ax2 : ∀ x : M, Mx (fun _ ⇒ x).
Proof. by move⇒ x; rewrite /Mx /=; exact: measurable_cst. Qed.
Let ax3 : ∀ (P : {mfun mR >-> nat}) (Fi : nat → mR → M),
(∀ i, Mx (Fi i)) → Mx (fun r ⇒ Fi (P r) r).
Proof.
move⇒ P Fi hFi; rewrite /Mx /=.
exact: measurable_glue.
Qed.
HB.instance Definition _ := @isQBS.Build R M Mx ax1 ax2 ax3.
R functor: measurableType to qbsType via measurable funs.
Concrete QBS instances for R, nat, bool.
Definition realQ : qbsType R := R_qbs mR.
Definition natQ : qbsType R := R_qbs nat.
Definition boolQ : qbsType R := R_qbs bool.
Local Lemma prodQ_Mx_comp (X Y : qbsType R) :
∀ (alpha : mR → X × Y) (f : {mfun mR >-> mR}),
(qbs_Mx (fun r ⇒ (alpha r).1) ∧
qbs_Mx (fun r ⇒ (alpha r).2)) →
(qbs_Mx (fun r ⇒ ((alpha \o f) r).1) ∧
qbs_Mx (fun r ⇒ ((alpha \o f) r).2)).
Proof.
move⇒ alpha f [h1 h2]; split.
exact: qbs_Mx_comp h1.
exact: qbs_Mx_comp h2.
Qed.
Local Lemma prodQ_Mx_const (X Y : qbsType R) :
∀ xy : X × Y,
qbs_Mx (fun _ : mR ⇒ xy.1) ∧
qbs_Mx (fun _ : mR ⇒ xy.2).
Proof.
by move⇒ [x y]; split; exact: qbs_Mx_const.
Qed.
Local Lemma prodQ_Mx_glue (X Y : qbsType R) :
∀ (P : {mfun mR >-> nat})
(Fi : nat → mR → X × Y),
(∀ i, qbs_Mx (fun r ⇒ (Fi i r).1) ∧
qbs_Mx (fun r ⇒ (Fi i r).2)) →
qbs_Mx (fun r ⇒ (Fi (P r) r).1) ∧
qbs_Mx (fun r ⇒ (Fi (P r) r).2).
Proof.
move⇒ P Fi hFi; split.
apply: (qbs_Mx_glue P (fun i r ⇒ (Fi i r).1)) ⇒ i.
by have [] := hFi i.
apply: (qbs_Mx_glue P (fun i r ⇒ (Fi i r).2)) ⇒ i.
by have [] := hFi i.
Qed.
Section prodQ_instance.
Variables (X Y : qbsType R).
HB.instance Definition _ :=
@isQBS.Build R (X × Y)%type
[set f : mR → X × Y | qbs_Mx (fun r ⇒ (f r).1) ∧
qbs_Mx (fun r ⇒ (f r).2)]
(@prodQ_Mx_comp X Y)
(@prodQ_Mx_const X Y)
(@prodQ_Mx_glue X Y).
Definition natQ : qbsType R := R_qbs nat.
Definition boolQ : qbsType R := R_qbs bool.
Local Lemma prodQ_Mx_comp (X Y : qbsType R) :
∀ (alpha : mR → X × Y) (f : {mfun mR >-> mR}),
(qbs_Mx (fun r ⇒ (alpha r).1) ∧
qbs_Mx (fun r ⇒ (alpha r).2)) →
(qbs_Mx (fun r ⇒ ((alpha \o f) r).1) ∧
qbs_Mx (fun r ⇒ ((alpha \o f) r).2)).
Proof.
move⇒ alpha f [h1 h2]; split.
exact: qbs_Mx_comp h1.
exact: qbs_Mx_comp h2.
Qed.
Local Lemma prodQ_Mx_const (X Y : qbsType R) :
∀ xy : X × Y,
qbs_Mx (fun _ : mR ⇒ xy.1) ∧
qbs_Mx (fun _ : mR ⇒ xy.2).
Proof.
by move⇒ [x y]; split; exact: qbs_Mx_const.
Qed.
Local Lemma prodQ_Mx_glue (X Y : qbsType R) :
∀ (P : {mfun mR >-> nat})
(Fi : nat → mR → X × Y),
(∀ i, qbs_Mx (fun r ⇒ (Fi i r).1) ∧
qbs_Mx (fun r ⇒ (Fi i r).2)) →
qbs_Mx (fun r ⇒ (Fi (P r) r).1) ∧
qbs_Mx (fun r ⇒ (Fi (P r) r).2).
Proof.
move⇒ P Fi hFi; split.
apply: (qbs_Mx_glue P (fun i r ⇒ (Fi i r).1)) ⇒ i.
by have [] := hFi i.
apply: (qbs_Mx_glue P (fun i r ⇒ (Fi i r).2)) ⇒ i.
by have [] := hFi i.
Qed.
Section prodQ_instance.
Variables (X Y : qbsType R).
HB.instance Definition _ :=
@isQBS.Build R (X × Y)%type
[set f : mR → X × Y | qbs_Mx (fun r ⇒ (f r).1) ∧
qbs_Mx (fun r ⇒ (f r).2)]
(@prodQ_Mx_comp X Y)
(@prodQ_Mx_const X Y)
(@prodQ_Mx_glue X Y).
Binary product QBS on (X * Y).
Definition prodQ : qbsType R := (X × Y)%type.
End prodQ_instance.
Arguments prodQ : clear implicits.
Section qbs_fst_instance.
Variables (X Y : qbsType R).
Let f : X × Y → X := fst.
Let hf : qbs_morphism f :=
fun alpha h ⇒ h.1.
HB.instance Definition _ :=
@isQBSMorphism.Build R (prodQ X Y) X f hf.
Definition qbs_fst : qbsHomType (prodQ X Y) X := f.
End qbs_fst_instance.
Section qbs_snd_instance.
Variables (X Y : qbsType R).
Let f : X × Y → Y := snd.
Let hf : qbs_morphism f :=
fun alpha h ⇒ h.2.
HB.instance Definition _ :=
@isQBSMorphism.Build R (prodQ X Y) Y f hf.
Definition qbs_snd : qbsHomType (prodQ X Y) Y := f.
End qbs_snd_instance.
Section qbs_pair_instance.
Variables (W X Y : qbsType R).
Variables (f : qbsHomType W X) (g : qbsHomType W Y).
Let fg := fun w : W ⇒ ((f : W → X) w, (g : W → Y) w).
Let hfg : qbs_morphism fg :=
fun alpha halpha ⇒
conj (qbs_hom_proof _ halpha) (qbs_hom_proof _ halpha).
HB.instance Definition _ :=
@isQBSMorphism.Build R W (prodQ X Y) fg hfg.
Definition qbs_pair : qbsHomType W (prodQ X Y) := fg.
End qbs_pair_instance.
Local Lemma expQ_Mx_comp (X Y : qbsType R) :
∀ alpha (f : {mfun mR >-> mR}),
(qbs_morphism (fun p : realQ × X ⇒ (alpha p.1 : X → Y) p.2)) →
qbs_morphism
(fun p : realQ × X ⇒ ((alpha \o f) p.1 : X → Y) p.2).
Proof.
move⇒ alpha f halpha beta [hb1 hb2].
have → : (fun p : realQ × X ⇒ (alpha \o f) p.1 p.2) \o beta =
(fun p : realQ × X ⇒ alpha p.1 p.2) \o
(fun r ⇒ (f (fst (beta r)), snd (beta r))) by [].
apply: halpha; split ⇒ /=.
exact: measurableT_comp.
exact: hb2.
Qed.
Local Lemma expQ_Mx_const (X Y : qbsType R) :
∀ g : qbsHomType X Y,
qbs_morphism (fun p : realQ × X ⇒ ((fun _ : mR ⇒ g) p.1 : X → Y) p.2).
Proof.
move⇒ g beta [_ hb2].
exact: qbs_hom_proof.
Qed.
Local Lemma expQ_Mx_glue (X Y : qbsType R) :
∀ (P : {mfun mR >-> nat})
(Fi : nat → mR → qbsHomType X Y),
(∀ i, qbs_morphism
(fun p : realQ × X ⇒ (Fi i p.1 : X → Y) p.2)) →
qbs_morphism
(fun p : realQ × X ⇒ ((fun r ⇒ Fi (P r) r) p.1 : X → Y) p.2).
Proof.
move⇒ P Fi hFi beta [hb1 hb2].
set Q := mfun_Sub (mem_set
(measurableT_comp (measurable_funPT P) hb1) :
(fun r ⇒ P (fst (beta r))) \in mfun).
apply: (qbs_Mx_glue Q
(fun i ⇒ (fun p : realQ × X ⇒ Fi i p.1 p.2) \o beta)).
by move⇒ i; exact: hFi i _ (conj hb1 hb2).
Qed.
Section expQ_instance.
Variables (X Y : qbsType R).
HB.instance Definition _ :=
@isQBS.Build R (qbsHomType X Y)
[set g : mR → qbsHomType X Y |
qbs_morphism (fun p : realQ × X ⇒ (g p.1 : X → Y) p.2)]
(@expQ_Mx_comp X Y)
(@expQ_Mx_const X Y)
(@expQ_Mx_glue X Y).
End prodQ_instance.
Arguments prodQ : clear implicits.
Section qbs_fst_instance.
Variables (X Y : qbsType R).
Let f : X × Y → X := fst.
Let hf : qbs_morphism f :=
fun alpha h ⇒ h.1.
HB.instance Definition _ :=
@isQBSMorphism.Build R (prodQ X Y) X f hf.
Definition qbs_fst : qbsHomType (prodQ X Y) X := f.
End qbs_fst_instance.
Section qbs_snd_instance.
Variables (X Y : qbsType R).
Let f : X × Y → Y := snd.
Let hf : qbs_morphism f :=
fun alpha h ⇒ h.2.
HB.instance Definition _ :=
@isQBSMorphism.Build R (prodQ X Y) Y f hf.
Definition qbs_snd : qbsHomType (prodQ X Y) Y := f.
End qbs_snd_instance.
Section qbs_pair_instance.
Variables (W X Y : qbsType R).
Variables (f : qbsHomType W X) (g : qbsHomType W Y).
Let fg := fun w : W ⇒ ((f : W → X) w, (g : W → Y) w).
Let hfg : qbs_morphism fg :=
fun alpha halpha ⇒
conj (qbs_hom_proof _ halpha) (qbs_hom_proof _ halpha).
HB.instance Definition _ :=
@isQBSMorphism.Build R W (prodQ X Y) fg hfg.
Definition qbs_pair : qbsHomType W (prodQ X Y) := fg.
End qbs_pair_instance.
Local Lemma expQ_Mx_comp (X Y : qbsType R) :
∀ alpha (f : {mfun mR >-> mR}),
(qbs_morphism (fun p : realQ × X ⇒ (alpha p.1 : X → Y) p.2)) →
qbs_morphism
(fun p : realQ × X ⇒ ((alpha \o f) p.1 : X → Y) p.2).
Proof.
move⇒ alpha f halpha beta [hb1 hb2].
have → : (fun p : realQ × X ⇒ (alpha \o f) p.1 p.2) \o beta =
(fun p : realQ × X ⇒ alpha p.1 p.2) \o
(fun r ⇒ (f (fst (beta r)), snd (beta r))) by [].
apply: halpha; split ⇒ /=.
exact: measurableT_comp.
exact: hb2.
Qed.
Local Lemma expQ_Mx_const (X Y : qbsType R) :
∀ g : qbsHomType X Y,
qbs_morphism (fun p : realQ × X ⇒ ((fun _ : mR ⇒ g) p.1 : X → Y) p.2).
Proof.
move⇒ g beta [_ hb2].
exact: qbs_hom_proof.
Qed.
Local Lemma expQ_Mx_glue (X Y : qbsType R) :
∀ (P : {mfun mR >-> nat})
(Fi : nat → mR → qbsHomType X Y),
(∀ i, qbs_morphism
(fun p : realQ × X ⇒ (Fi i p.1 : X → Y) p.2)) →
qbs_morphism
(fun p : realQ × X ⇒ ((fun r ⇒ Fi (P r) r) p.1 : X → Y) p.2).
Proof.
move⇒ P Fi hFi beta [hb1 hb2].
set Q := mfun_Sub (mem_set
(measurableT_comp (measurable_funPT P) hb1) :
(fun r ⇒ P (fst (beta r))) \in mfun).
apply: (qbs_Mx_glue Q
(fun i ⇒ (fun p : realQ × X ⇒ Fi i p.1 p.2) \o beta)).
by move⇒ i; exact: hFi i _ (conj hb1 hb2).
Qed.
Section expQ_instance.
Variables (X Y : qbsType R).
HB.instance Definition _ :=
@isQBS.Build R (qbsHomType X Y)
[set g : mR → qbsHomType X Y |
qbs_morphism (fun p : realQ × X ⇒ (g p.1 : X → Y) p.2)]
(@expQ_Mx_comp X Y)
(@expQ_Mx_const X Y)
(@expQ_Mx_glue X Y).
Exponential (function space) QBS.
Definition expQ : qbsType R := qbsHomType X Y.
End expQ_instance.
Arguments expQ : clear implicits.
Section qbs_eval_instance.
Variables (X Y : qbsType R).
Let f := fun p : prodQ (expQ X Y) X ⇒ (p.1 : X → Y) p.2.
Let hf : qbs_morphism f.
Proof.
move⇒ beta [hb1 hb2].
have hmorph : qbs_morphism
(fun p : realQ × X ⇒ ((fst \o beta) p.1 : X → Y) p.2).
exact: hb1.
set gamma := (fun r : mR ⇒ (r, snd (beta r))) : mR → realQ × X.
have hgamma : qbs_Mx gamma.
split ⇒ /=.
exact: measurable_id.
exact: hb2.
by have := hmorph gamma hgamma.
Qed.
HB.instance Definition _ :=
@isQBSMorphism.Build R (prodQ (expQ X Y) X) Y f hf.
End expQ_instance.
Arguments expQ : clear implicits.
Section qbs_eval_instance.
Variables (X Y : qbsType R).
Let f := fun p : prodQ (expQ X Y) X ⇒ (p.1 : X → Y) p.2.
Let hf : qbs_morphism f.
Proof.
move⇒ beta [hb1 hb2].
have hmorph : qbs_morphism
(fun p : realQ × X ⇒ ((fst \o beta) p.1 : X → Y) p.2).
exact: hb1.
set gamma := (fun r : mR ⇒ (r, snd (beta r))) : mR → realQ × X.
have hgamma : qbs_Mx gamma.
split ⇒ /=.
exact: measurable_id.
exact: hb2.
by have := hmorph gamma hgamma.
Qed.
HB.instance Definition _ :=
@isQBSMorphism.Build R (prodQ (expQ X Y) X) Y f hf.
Evaluation: cartesian closed structure (eval).
Definition qbs_eval : qbsHomType (prodQ (expQ X Y) X) Y :=
f.
End qbs_eval_instance.
Lemma prodQ_const_random (X Y : qbsType R) (x : X) (alpha : mR → Y) :
qbs_Mx alpha → qbs_Mx (fun r ⇒ (x, alpha r)).
Proof.
move⇒ halpha; split ⇒ /=.
exact: qbs_Mx_const.
exact: halpha.
Qed.
Section qbs_curry_instance.
Variables (X Y Z : qbsType R).
Variable f : qbsHomType (prodQ X Y) Z.
Variable x : X.
Let curry_fun := fun y ⇒ (f : prodQ X Y → Z) (x, y).
Let curry_proof : ∀ alpha, qbs_Mx alpha →
qbs_Mx (curry_fun \o alpha).
Proof.
by move⇒ alpha halpha; exact: qbs_hom_proof
(prodQ_const_random x halpha).
Qed.
HB.instance Definition _ := @isQBSMorphism.Build R Y Z curry_fun curry_proof.
f.
End qbs_eval_instance.
Lemma prodQ_const_random (X Y : qbsType R) (x : X) (alpha : mR → Y) :
qbs_Mx alpha → qbs_Mx (fun r ⇒ (x, alpha r)).
Proof.
move⇒ halpha; split ⇒ /=.
exact: qbs_Mx_const.
exact: halpha.
Qed.
Section qbs_curry_instance.
Variables (X Y Z : qbsType R).
Variable f : qbsHomType (prodQ X Y) Z.
Variable x : X.
Let curry_fun := fun y ⇒ (f : prodQ X Y → Z) (x, y).
Let curry_proof : ∀ alpha, qbs_Mx alpha →
qbs_Mx (curry_fun \o alpha).
Proof.
by move⇒ alpha halpha; exact: qbs_hom_proof
(prodQ_const_random x halpha).
Qed.
HB.instance Definition _ := @isQBSMorphism.Build R Y Z curry_fun curry_proof.
Curried function as a bundled QBS morphism Y -> Z.
# Universal property of exponentials The following lemmas state that eval and curry form the bijection underlying the cartesian closed structure on QBS. They are stated as pointwise equations and hold by reflexivity.
Beta rule for cartesian closure: evaluating the curried form
recovers the original morphism. The underlying function of
qbs_curry f at x is fun y ⇒ f (x, y), so applying
it at y yields f (x, y).
Here we package the curried function at x as a qbsHomType
directly to let HB resolve its structure; the prodQ_const_random
witness provides the required isQBSMorphism instance.
Lemma qbs_morphism_curry_eval (X Y Z : qbsType R)
(f : qbsHomType (prodQ X Y) Z) (x : X) (y : Y) :
let cf : Y → Z := fun y0 ⇒ (f : prodQ X Y → Z) (x, y0) in
cf y = (f : prodQ X Y → Z) (x, y).
Proof. by []. Qed.
(f : qbsHomType (prodQ X Y) Z) (x : X) (y : Y) :
let cf : Y → Z := fun y0 ⇒ (f : prodQ X Y → Z) (x, y0) in
cf y = (f : prodQ X Y → Z) (x, y).
Proof. by []. Qed.
Eta rule for cartesian closure: the evaluation morphism applied
to a pair (h, y) with h : qbsHomType R Y Z recovers the
pointwise application h y. This shows that eval is a left
inverse of curry at the level of underlying functions.
Lemma qbs_morphism_eval_curry (Y Z : qbsType R)
(h : qbsHomType Y Z) (y : Y) :
(fun p : prodQ (expQ Y Z) Y ⇒ (p.1 : Y → Z) p.2) (h, y) =
(h : Y → Z) y.
Proof. by []. Qed.
Section unitQ_instance.
HB.instance Definition _ :=
@isQBS.Build R unit
[set _ : mR → unit | True]
(fun _ _ _ ⇒ I)
(fun _ ⇒ I)
(fun _ _ _ ⇒ I).
(h : qbsHomType Y Z) (y : Y) :
(fun p : prodQ (expQ Y Z) Y ⇒ (p.1 : Y → Z) p.2) (h, y) =
(h : Y → Z) y.
Proof. by []. Qed.
Section unitQ_instance.
HB.instance Definition _ :=
@isQBS.Build R unit
[set _ : mR → unit | True]
(fun _ _ _ ⇒ I)
(fun _ ⇒ I)
(fun _ _ _ ⇒ I).
Terminal (unit) QBS.
Definition unitQ : qbsType R := unit.
End unitQ_instance.
Section qbs_unit_instance.
Variable X : qbsType R.
Let f := fun _ : X ⇒ tt.
Let hf : qbs_morphism f := fun alpha _ ⇒ I.
HB.instance Definition _ :=
@isQBSMorphism.Build R X unitQ f hf.
Definition qbs_unit : qbsHomType X unitQ := f.
End qbs_unit_instance.
Definition sigma_Mx (X : qbsType R) : set (set X) :=
[set U | ∀ alpha, qbs_Mx alpha →
measurable (alpha @^-1` U)].
Lemma sigma_Mx_setT (X : qbsType R) : sigma_Mx (X := X) setT.
Proof. by move⇒ alpha _; exact: measurableT. Qed.
Lemma sigma_Mx_setC (X : qbsType R) (U : set X) :
sigma_Mx U → sigma_Mx (~` U).
Proof.
move⇒ hU alpha halpha.
rewrite preimage_setC.
exact: measurableC (hU _ halpha).
Qed.
Lemma sigma_Mx_bigcup (X : qbsType R) (F : nat → set X) :
(∀ i, sigma_Mx (F i)) →
sigma_Mx (\bigcup_i F i).
Proof.
move⇒ hF alpha halpha.
rewrite preimage_bigcup.
apply: bigcup_measurable ⇒ i _; exact: hF.
Qed.
Definition qbs_add : qbsHomType (prodQ realQ realQ) realQ :=
@QBSHom.Pack R (prodQ realQ realQ) realQ
(fun p ⇒ (p.1 + p.2))
(QBSHom.Class
(@isQBSMorphism.Build R (prodQ realQ realQ) realQ _
(fun alpha h ⇒ measurable_funD h.1 h.2))).
Definition qbs_mul : qbsHomType (prodQ realQ realQ) realQ :=
@QBSHom.Pack R (prodQ realQ realQ) realQ
(fun p ⇒ (p.1 × p.2))
(QBSHom.Class
(@isQBSMorphism.Build R (prodQ realQ realQ) realQ _
(fun alpha h ⇒ measurable_funM h.1 h.2))).
Section sub_qbs_def.
Variables (X : qbsType R) (P : set X).
Let sub_car := {x : X | P x}.
Let sub_proj : sub_car → X := @proj1_sig _ P.
Let sub_Mx : set (mR → sub_car) :=
[set alpha | qbs_Mx (fun r ⇒ sub_proj (alpha r))].
Local Lemma sub_qbs_Mx_comp : ∀ alpha
(f : {mfun mR >-> mR}),
sub_Mx alpha → sub_Mx (alpha \o f).
Proof.
move⇒ alpha f halpha; rewrite /sub_Mx /=.
exact: qbs_Mx_comp halpha.
Qed.
Local Lemma sub_qbs_Mx_const : ∀ x : sub_car,
sub_Mx (fun _ ⇒ x).
Proof.
move⇒ x; rewrite /sub_Mx /=.
exact: qbs_Mx_const.
Qed.
Local Lemma sub_qbs_Mx_glue : ∀ (Q : {mfun mR >-> nat})
(Fi : nat → mR → sub_car),
(∀ i, sub_Mx (Fi i)) →
sub_Mx (fun r ⇒ Fi (Q r) r).
Proof.
move⇒ Q Fi hFi; rewrite /sub_Mx /=.
exact: (qbs_Mx_glue Q (fun i r ⇒ sub_proj (Fi i r)) hFi).
Qed.
HB.instance Definition _ :=
@isQBS.Build R sub_car sub_Mx
sub_qbs_Mx_comp sub_qbs_Mx_const sub_qbs_Mx_glue.
Definition sub_qbs : qbsType R := sub_car.
End sub_qbs_def.
Inductive generating_Mx (T : Type) (G : set (mR → T))
: (mR → T) → Prop :=
| gen_base : ∀ alpha, G alpha → generating_Mx G alpha
| gen_comp : ∀ alpha (f : {mfun mR >-> mR}),
generating_Mx G alpha →
generating_Mx G (alpha \o f)
| gen_const : ∀ x : T, generating_Mx G (fun _ ⇒ x)
| gen_glue : ∀ (P : {mfun mR >-> nat})
(Fi : nat → mR → T),
(∀ i, generating_Mx G (Fi i)) →
generating_Mx G (fun r ⇒ Fi (P r) r).
Section generating_qbs_instance.
Variables (T : Type) (G : set (mR → T)).
HB.instance Definition _ :=
@isQBS.Build R T (generating_Mx G)
(fun alpha f ha ⇒ gen_comp f ha)
(fun x ⇒ gen_const G x)
(fun P Fi hFi ⇒ gen_glue P hFi).
Definition generating_qbs : qbsType R := T.
End generating_qbs_instance.
Lemma generating_qbs_incl (T : Type) (G : set (mR → T)) :
G `<=` qbs_Mx (s := generating_qbs G).
Proof. by move⇒ alpha halpha; exact: gen_base. Qed.
Local Lemma prodQ_random_const (X Y : qbsType R) (alpha : mR → X) (y : Y) :
qbs_Mx alpha → qbs_Mx (fun r ⇒ (alpha r, y)).
Proof.
move⇒ halpha; split ⇒ /=.
exact: halpha.
exact: qbs_Mx_const.
Qed.
Definition map_qbs (X Y : qbsType R) (f : X → Y)
(hf : qbs_morphism f) : qbsType R :=
generating_qbs [set beta : mR → Y |
∃ alpha, qbs_Mx alpha ∧ beta = f \o alpha].
Lemma map_qbs_random (X Y : qbsType R) (f : X → Y)
(hf : qbs_morphism f) (alpha : mR → X) :
qbs_Mx alpha → qbs_Mx (s := map_qbs hf) (f \o alpha).
Proof.
move⇒ halpha; apply: gen_base; ∃ alpha; split ⇒ //.
Qed.
Lemma map_qbs_sub (X Y : qbsType R) (f : X → Y)
(hf : qbs_morphism f) :
∀ beta, qbs_Mx (s := map_qbs hf) beta → qbs_Mx (s := Y) beta.
Proof.
move⇒ beta; elim⇒ {beta}.
- by move⇒ _ [alpha [halpha ->]]; exact: hf halpha.
- by move⇒ alpha g _ hIH; exact: qbs_Mx_comp hIH.
- by move⇒ x; exact: qbs_Mx_const.
- by move⇒ P Fi hFi IH; exact: qbs_Mx_glue IH.
Qed.
Lemma map_qbs_morphism_out (X Y Z : qbsType R) (f : X → Y) (g : Y → Z)
(hf : qbs_morphism f) (hg : qbs_morphism g) :
qbs_morphism (X := map_qbs hf) (Y := Z) g.
Proof.
by move⇒ beta /map_qbs_sub; exact: hg.
Qed.
Lemma map_qbs_morph_from (X Y : qbsType R) (f : X → Y)
(hf : qbs_morphism f) :
qbs_morphism (X := X) (Y := map_qbs hf) f.
Proof.
by move⇒ alpha halpha; exact: map_qbs_random halpha.
Qed.
Section qbs_order.
Variable T : Type.
Definition qbs_leT (MxX MxY : set (mR → T)) : Prop :=
MxX `<=` MxY.
Lemma qbs_leT_refl (Mx : set (mR → T)) :
qbs_leT Mx Mx.
Proof. by move⇒ alpha. Qed.
Lemma qbs_leT_trans (Mx1 Mx2 Mx3 : set (mR → T)) :
qbs_leT Mx1 Mx2 → qbs_leT Mx2 Mx3 → qbs_leT Mx1 Mx3.
Proof. by move⇒ h12 h23 alpha /h12 /h23. Qed.
Lemma qbs_leT_antisym (Mx1 Mx2 : set (mR → T)) :
qbs_leT Mx1 Mx2 → qbs_leT Mx2 Mx1 → Mx1 = Mx2.
Proof.
move⇒ h12 h21; rewrite eqEsubset; split ⇒ alpha h.
exact: h12.
exact: h21.
Qed.
End qbs_order.
Lemma generating_qbs_least (T : Type) (G : set (mR → T)) (Mx : set (mR → T))
(c1 : ∀ alpha (f : {mfun mR >-> mR}),
Mx alpha → Mx (alpha \o f))
(c2 : ∀ x : T, Mx (fun _ ⇒ x))
(c3 : ∀ (P : {mfun mR >-> nat}) (Fi : nat → mR → T),
(∀ i, Mx (Fi i)) → Mx (fun r ⇒ Fi (P r) r)) :
G `<=` Mx → generating_Mx G `<=` Mx.
Proof.
move⇒ hG beta hbeta; elim: hbeta.
- by move⇒ alpha hGa; exact: hG hGa.
- by move⇒ alpha f _ hIH; exact: c1 hIH.
- by move⇒ x; exact: c2.
- by move⇒ P Fi hFi IH; exact: c3 IH.
Qed.
Definition qbs_supT (T : Type) (MxX MxY : set (mR → T)) : qbsType R :=
generating_qbs [set alpha : mR → T | MxX alpha ∨ MxY alpha].
Lemma qbs_supT_ub_l (T : Type) (MxX MxY : set (mR → T)) :
qbs_leT MxX (qbs_Mx (s := qbs_supT MxX MxY)).
Proof.
by move⇒ alpha halpha; apply: gen_base; left.
Qed.
Lemma qbs_supT_ub_r (T : Type) (MxX MxY : set (mR → T)) :
qbs_leT MxY (qbs_Mx (s := qbs_supT MxX MxY)).
Proof.
by move⇒ alpha halpha; apply: gen_base; right.
Qed.
Lemma qbs_supT_least (T : Type) (MxX MxY MxZ : set (mR → T))
(c1 : ∀ alpha (f : {mfun mR >-> mR}),
MxZ alpha → MxZ (alpha \o f))
(c2 : ∀ x : T, MxZ (fun _ ⇒ x))
(c3 : ∀ (P : {mfun mR >-> nat}) (Fi : nat → mR → T),
(∀ i, MxZ (Fi i)) →
MxZ (fun r ⇒ Fi (P r) r)) :
qbs_leT MxX MxZ →
qbs_leT MxY MxZ →
qbs_leT (qbs_Mx (s := qbs_supT MxX MxY)) MxZ.
Proof.
move⇒ hX hY.
apply: generating_qbs_least c1 c2 c3 _.
by move⇒ alpha /= -[/hX | /hY].
Qed.
End qbs.
End unitQ_instance.
Section qbs_unit_instance.
Variable X : qbsType R.
Let f := fun _ : X ⇒ tt.
Let hf : qbs_morphism f := fun alpha _ ⇒ I.
HB.instance Definition _ :=
@isQBSMorphism.Build R X unitQ f hf.
Definition qbs_unit : qbsHomType X unitQ := f.
End qbs_unit_instance.
Definition sigma_Mx (X : qbsType R) : set (set X) :=
[set U | ∀ alpha, qbs_Mx alpha →
measurable (alpha @^-1` U)].
Lemma sigma_Mx_setT (X : qbsType R) : sigma_Mx (X := X) setT.
Proof. by move⇒ alpha _; exact: measurableT. Qed.
Lemma sigma_Mx_setC (X : qbsType R) (U : set X) :
sigma_Mx U → sigma_Mx (~` U).
Proof.
move⇒ hU alpha halpha.
rewrite preimage_setC.
exact: measurableC (hU _ halpha).
Qed.
Lemma sigma_Mx_bigcup (X : qbsType R) (F : nat → set X) :
(∀ i, sigma_Mx (F i)) →
sigma_Mx (\bigcup_i F i).
Proof.
move⇒ hF alpha halpha.
rewrite preimage_bigcup.
apply: bigcup_measurable ⇒ i _; exact: hF.
Qed.
Definition qbs_add : qbsHomType (prodQ realQ realQ) realQ :=
@QBSHom.Pack R (prodQ realQ realQ) realQ
(fun p ⇒ (p.1 + p.2))
(QBSHom.Class
(@isQBSMorphism.Build R (prodQ realQ realQ) realQ _
(fun alpha h ⇒ measurable_funD h.1 h.2))).
Definition qbs_mul : qbsHomType (prodQ realQ realQ) realQ :=
@QBSHom.Pack R (prodQ realQ realQ) realQ
(fun p ⇒ (p.1 × p.2))
(QBSHom.Class
(@isQBSMorphism.Build R (prodQ realQ realQ) realQ _
(fun alpha h ⇒ measurable_funM h.1 h.2))).
Section sub_qbs_def.
Variables (X : qbsType R) (P : set X).
Let sub_car := {x : X | P x}.
Let sub_proj : sub_car → X := @proj1_sig _ P.
Let sub_Mx : set (mR → sub_car) :=
[set alpha | qbs_Mx (fun r ⇒ sub_proj (alpha r))].
Local Lemma sub_qbs_Mx_comp : ∀ alpha
(f : {mfun mR >-> mR}),
sub_Mx alpha → sub_Mx (alpha \o f).
Proof.
move⇒ alpha f halpha; rewrite /sub_Mx /=.
exact: qbs_Mx_comp halpha.
Qed.
Local Lemma sub_qbs_Mx_const : ∀ x : sub_car,
sub_Mx (fun _ ⇒ x).
Proof.
move⇒ x; rewrite /sub_Mx /=.
exact: qbs_Mx_const.
Qed.
Local Lemma sub_qbs_Mx_glue : ∀ (Q : {mfun mR >-> nat})
(Fi : nat → mR → sub_car),
(∀ i, sub_Mx (Fi i)) →
sub_Mx (fun r ⇒ Fi (Q r) r).
Proof.
move⇒ Q Fi hFi; rewrite /sub_Mx /=.
exact: (qbs_Mx_glue Q (fun i r ⇒ sub_proj (Fi i r)) hFi).
Qed.
HB.instance Definition _ :=
@isQBS.Build R sub_car sub_Mx
sub_qbs_Mx_comp sub_qbs_Mx_const sub_qbs_Mx_glue.
Definition sub_qbs : qbsType R := sub_car.
End sub_qbs_def.
Inductive generating_Mx (T : Type) (G : set (mR → T))
: (mR → T) → Prop :=
| gen_base : ∀ alpha, G alpha → generating_Mx G alpha
| gen_comp : ∀ alpha (f : {mfun mR >-> mR}),
generating_Mx G alpha →
generating_Mx G (alpha \o f)
| gen_const : ∀ x : T, generating_Mx G (fun _ ⇒ x)
| gen_glue : ∀ (P : {mfun mR >-> nat})
(Fi : nat → mR → T),
(∀ i, generating_Mx G (Fi i)) →
generating_Mx G (fun r ⇒ Fi (P r) r).
Section generating_qbs_instance.
Variables (T : Type) (G : set (mR → T)).
HB.instance Definition _ :=
@isQBS.Build R T (generating_Mx G)
(fun alpha f ha ⇒ gen_comp f ha)
(fun x ⇒ gen_const G x)
(fun P Fi hFi ⇒ gen_glue P hFi).
Definition generating_qbs : qbsType R := T.
End generating_qbs_instance.
Lemma generating_qbs_incl (T : Type) (G : set (mR → T)) :
G `<=` qbs_Mx (s := generating_qbs G).
Proof. by move⇒ alpha halpha; exact: gen_base. Qed.
Local Lemma prodQ_random_const (X Y : qbsType R) (alpha : mR → X) (y : Y) :
qbs_Mx alpha → qbs_Mx (fun r ⇒ (alpha r, y)).
Proof.
move⇒ halpha; split ⇒ /=.
exact: halpha.
exact: qbs_Mx_const.
Qed.
Definition map_qbs (X Y : qbsType R) (f : X → Y)
(hf : qbs_morphism f) : qbsType R :=
generating_qbs [set beta : mR → Y |
∃ alpha, qbs_Mx alpha ∧ beta = f \o alpha].
Lemma map_qbs_random (X Y : qbsType R) (f : X → Y)
(hf : qbs_morphism f) (alpha : mR → X) :
qbs_Mx alpha → qbs_Mx (s := map_qbs hf) (f \o alpha).
Proof.
move⇒ halpha; apply: gen_base; ∃ alpha; split ⇒ //.
Qed.
Lemma map_qbs_sub (X Y : qbsType R) (f : X → Y)
(hf : qbs_morphism f) :
∀ beta, qbs_Mx (s := map_qbs hf) beta → qbs_Mx (s := Y) beta.
Proof.
move⇒ beta; elim⇒ {beta}.
- by move⇒ _ [alpha [halpha ->]]; exact: hf halpha.
- by move⇒ alpha g _ hIH; exact: qbs_Mx_comp hIH.
- by move⇒ x; exact: qbs_Mx_const.
- by move⇒ P Fi hFi IH; exact: qbs_Mx_glue IH.
Qed.
Lemma map_qbs_morphism_out (X Y Z : qbsType R) (f : X → Y) (g : Y → Z)
(hf : qbs_morphism f) (hg : qbs_morphism g) :
qbs_morphism (X := map_qbs hf) (Y := Z) g.
Proof.
by move⇒ beta /map_qbs_sub; exact: hg.
Qed.
Lemma map_qbs_morph_from (X Y : qbsType R) (f : X → Y)
(hf : qbs_morphism f) :
qbs_morphism (X := X) (Y := map_qbs hf) f.
Proof.
by move⇒ alpha halpha; exact: map_qbs_random halpha.
Qed.
Section qbs_order.
Variable T : Type.
Definition qbs_leT (MxX MxY : set (mR → T)) : Prop :=
MxX `<=` MxY.
Lemma qbs_leT_refl (Mx : set (mR → T)) :
qbs_leT Mx Mx.
Proof. by move⇒ alpha. Qed.
Lemma qbs_leT_trans (Mx1 Mx2 Mx3 : set (mR → T)) :
qbs_leT Mx1 Mx2 → qbs_leT Mx2 Mx3 → qbs_leT Mx1 Mx3.
Proof. by move⇒ h12 h23 alpha /h12 /h23. Qed.
Lemma qbs_leT_antisym (Mx1 Mx2 : set (mR → T)) :
qbs_leT Mx1 Mx2 → qbs_leT Mx2 Mx1 → Mx1 = Mx2.
Proof.
move⇒ h12 h21; rewrite eqEsubset; split ⇒ alpha h.
exact: h12.
exact: h21.
Qed.
End qbs_order.
Lemma generating_qbs_least (T : Type) (G : set (mR → T)) (Mx : set (mR → T))
(c1 : ∀ alpha (f : {mfun mR >-> mR}),
Mx alpha → Mx (alpha \o f))
(c2 : ∀ x : T, Mx (fun _ ⇒ x))
(c3 : ∀ (P : {mfun mR >-> nat}) (Fi : nat → mR → T),
(∀ i, Mx (Fi i)) → Mx (fun r ⇒ Fi (P r) r)) :
G `<=` Mx → generating_Mx G `<=` Mx.
Proof.
move⇒ hG beta hbeta; elim: hbeta.
- by move⇒ alpha hGa; exact: hG hGa.
- by move⇒ alpha f _ hIH; exact: c1 hIH.
- by move⇒ x; exact: c2.
- by move⇒ P Fi hFi IH; exact: c3 IH.
Qed.
Definition qbs_supT (T : Type) (MxX MxY : set (mR → T)) : qbsType R :=
generating_qbs [set alpha : mR → T | MxX alpha ∨ MxY alpha].
Lemma qbs_supT_ub_l (T : Type) (MxX MxY : set (mR → T)) :
qbs_leT MxX (qbs_Mx (s := qbs_supT MxX MxY)).
Proof.
by move⇒ alpha halpha; apply: gen_base; left.
Qed.
Lemma qbs_supT_ub_r (T : Type) (MxX MxY : set (mR → T)) :
qbs_leT MxY (qbs_Mx (s := qbs_supT MxX MxY)).
Proof.
by move⇒ alpha halpha; apply: gen_base; right.
Qed.
Lemma qbs_supT_least (T : Type) (MxX MxY MxZ : set (mR → T))
(c1 : ∀ alpha (f : {mfun mR >-> mR}),
MxZ alpha → MxZ (alpha \o f))
(c2 : ∀ x : T, MxZ (fun _ ⇒ x))
(c3 : ∀ (P : {mfun mR >-> nat}) (Fi : nat → mR → T),
(∀ i, MxZ (Fi i)) →
MxZ (fun r ⇒ Fi (P r) r)) :
qbs_leT MxX MxZ →
qbs_leT MxY MxZ →
qbs_leT (qbs_Mx (s := qbs_supT MxX MxY)) MxZ.
Proof.
move⇒ hX hY.
apply: generating_qbs_least c1 c2 c3 _.
by move⇒ alpha /= -[/hX | /hY].
Qed.
End qbs.