Skip to content

Commit

Permalink
trying to generalize mfun
Browse files Browse the repository at this point in the history
  • Loading branch information
@affeldt-aist @hoheinzollern
affeldt-aist authored and hoheinzollern committed Jul 4, 2024
1 parent 47d1b22 commit 9ba0002
Showing 1 changed file with 55 additions and 53 deletions.
108 changes: 55 additions & 53 deletions theories/lebesgue_integral.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -100,12 +100,11 @@ Reserved Notation "m1 '\x^' m2" (at level 40, m2 at next level).
#[global]
Hint Extern 0 (measurable [set _]) => solve [apply: measurable_set1] : core.

HB.mixin Record isMeasurableFun d (aT : sigmaRingType d) (rT : realType)
(f : aT -> rT) := {
measurable_funP : measurable_fun [set: aT] f
HB.mixin Record isMeasurableFun d d' (aT : sigmaRingType d) (rT : sigmaRingType d') (f : aT -> rT) := {
measurable_funP : measurable_fun setT f
}.
HB.structure Definition MeasurableFun d aT rT :=
{f of @isMeasurableFun d aT rT f}.
HB.structure Definition MeasurableFun d d' aT rT :=
{f of @isMeasurableFun d d' aT rT f}.

(* HB.mixin Record isMeasurableFun d (aT : measurableType d) (rT : realType) (f : aT -> rT) := { *)
(* measurable_funP : measurable_fun setT f *)
Expand All @@ -117,22 +116,12 @@ Reserved Notation "{ 'mfun' aT >-> T }"
(at level 0, format "{ 'mfun' aT >-> T }").
Reserved Notation "[ 'mfun' 'of' f ]"
(at level 0, format "[ 'mfun' 'of' f ]").
Notation "{ 'mfun' aT >-> T }" := (@MeasurableFun.type _ aT T) : form_scope.
Notation "{ 'mfun' aT >-> T }" := (@MeasurableFun.type _ _ aT T) : form_scope.
Notation "[ 'mfun' 'of' f ]" := [the {mfun _ >-> _} of f] : form_scope.
#[global] Hint Extern 0 (measurable_fun [set: _] _) =>
solve [apply: measurable_funP] : core.

HB.structure Definition SimpleFun d (aT : sigmaRingType d) (rT : realType) :=
(* HB.structure Definition SimpleFun d (aT (*rT*) : measurableType d) (rT : realType) := *)
{f of @isMeasurableFun d aT rT f & @FiniteImage aT rT f}.
Reserved Notation "{ 'sfun' aT >-> T }"
(at level 0, format "{ 'sfun' aT >-> T }").
Reserved Notation "[ 'sfun' 'of' f ]"
(at level 0, format "[ 'sfun' 'of' f ]").
Notation "{ 'sfun' aT >-> T }" := (@SimpleFun.type _ aT T) : form_scope.
Notation "[ 'sfun' 'of' f ]" := [the {sfun _ >-> _} of f] : form_scope.

Lemma measurable_sfunP {d} {aT : measurableType d} {rT : realType}
Lemma measurable_sfunP {d} {aT : measurableType d} {rT : realType} (* to generalize rT -> measurableType *)
(f : {mfun aT >-> rT}) (Y : set rT) : measurable Y -> measurable (f @^-1` Y).
Proof. by move=> mY; rewrite -[f @^-1` _]setTI; exact: measurable_funP. Qed.

Expand All @@ -148,18 +137,6 @@ Notation "{ 'nnfun' aT >-> T }" := (@NonNegFun.type aT T) : form_scope.
Notation "[ 'nnfun' 'of' f ]" := [the {nnfun _ >-> _} of f] : form_scope.
#[global] Hint Extern 0 (is_true (0 <= _)) => solve [apply: fun_ge0] : core.

(* HB.structure Definition NonNegSimpleFun d (aT : measurableType d) (rT : realType) := *)

HB.structure Definition NonNegSimpleFun
d (aT : sigmaRingType d) (rT : realType) :=
{f of @SimpleFun d _ _ f & @NonNegFun aT rT f}.
Reserved Notation "{ 'nnsfun' aT >-> T }"
(at level 0, format "{ 'nnsfun' aT >-> T }").
Reserved Notation "[ 'nnsfun' 'of' f ]"
(at level 0, format "[ 'nnsfun' 'of' f ]").
Notation "{ 'nnsfun' aT >-> T }" := (@NonNegSimpleFun.type _ aT%type T) : form_scope.
Notation "[ 'nnsfun' 'of' f ]" := [the {nnsfun _ >-> _} of f] : form_scope.

Section ring.
Context (aT : pointedType) (rT : ringType).

Expand Down Expand Up @@ -252,19 +229,19 @@ HB.builders Context T R f of @FiniteDecomp T R f.
HB.end.

Section mfun_pred.
Context {d} {aT : sigmaRingType d} {rT : realType}.
Context {d d'} {aT : sigmaRingType d} {rT : sigmaRingType d'}.
Definition mfun : {pred aT -> rT} := mem [set f | measurable_fun setT f].
Definition mfun_key : pred_key mfun. Proof. exact. Qed.
Canonical mfun_keyed := KeyedPred mfun_key.
End mfun_pred.

Section mfun.
Context {d} {aT : measurableType d} {rT : realType}.
Context {d d'} {aT : measurableType d} {rT : measurableType d'}.
Notation T := {mfun aT >-> rT}.
Notation mfun := (@mfun _ aT rT).
Notation mfun := (@mfun _ _ aT rT).
Section Sub.
Context (f : aT -> rT) (fP : f \in mfun).
Definition mfun_Sub_subproof := @isMeasurableFun.Build d aT rT f (set_mem fP).
Definition mfun_Sub_subproof := @isMeasurableFun.Build d d' aT rT f (set_mem fP).
#[local] HB.instance Definition _ := mfun_Sub_subproof.
Definition mfun_Sub := [mfun of f].
End Sub.
Expand All @@ -286,39 +263,43 @@ Proof. by split=> [->//|fg]; apply/val_inj/funext. Qed.

HB.instance Definition _ := [Choice of {mfun aT >-> rT} by <:].

Lemma cst_mfun_subproof x : @isMeasurableFun d aT rT (cst x).
Proof. by split. Qed.
HB.instance Definition _ x := @cst_mfun_subproof x.
Lemma cst_mfun_subproof x : @measurable_fun d d' aT rT setT (cst x). (* measurableTypeR rT *)
Proof. done. Qed.
HB.instance Definition _ x := @isMeasurableFun.Build _ _ _ _ (cst x) (cst_mfun_subproof x).
Definition cst_mfun x := [the {mfun aT >-> rT} of cst x].

Lemma mfun_cst x : @cst_mfun x =1 cst x. Proof. by []. Qed.

HB.instance Definition _ := @isMeasurableFun.Build _ _ rT
(@normr rT rT) (@measurable_normr rT setT).

HB.instance Definition _ :=
isMeasurableFun.Build _ _ _ (@expR rT) (@measurable_expR rT).

Lemma measurableT_comp_subproof (f : {mfun _ >-> rT}) (g : {mfun aT >-> rT}) :
measurable_fun setT (f \o g).
Proof. exact: measurableT_comp. Qed.

HB.instance Definition _ (f : {mfun _ >-> rT}) (g : {mfun aT >-> rT}) :=
isMeasurableFun.Build _ _ _ (f \o g) (measurableT_comp_subproof _ _).
isMeasurableFun.Build _ _ _ _ (f \o g) (measurableT_comp_subproof _ _).

End mfun.

Section mfun_realType.
Context {d} {aT : measurableType d} {rT : realType}.

HB.instance Definition _ := @isMeasurableFun.Build _ _ _ rT
(@normr rT rT) (@measurable_normr rT setT).

HB.instance Definition _ :=
isMeasurableFun.Build _ _ _ _ (@expR rT) (@measurable_expR rT).
End mfun_realType.

Section ring.
Context d (aT : measurableType d) (rT : realType).

Lemma mfun_subring_closed : subring_closed (@mfun _ aT rT).
Lemma mfun_subring_closed : subring_closed (@mfun _ _ aT rT).
Proof.
split=> [|f g|f g]; rewrite !inE/=.
- exact: measurable_cst.
- exact: measurable_funB.
- exact: measurable_funM.
Qed.
HB.instance Definition _ := GRing.isSubringClosed.Build _ mfun
HB.instance Definition _ := GRing.isSubringClosed.Build _ (@mfun _ _ aT rT)
mfun_subring_closed.
HB.instance Definition _ := [SubChoice_isSubComRing of {mfun aT >-> rT} by <:].

Expand Down Expand Up @@ -351,7 +332,7 @@ Proof. by rewrite /mindic funeqE => t; rewrite indicE. Qed.
HB.instance Definition _ (D : set aT) (mD : measurable D) :
@FImFun aT rT (mindic mD) := FImFun.on (mindic mD).
Lemma indic_mfun_subproof (D : set aT) (mD : measurable D) :
@isMeasurableFun d aT rT (mindic mD).
@isMeasurableFun d _ aT rT (mindic mD).
Proof.
split=> mA /= B mB; rewrite preimage_indic.
case: ifPn => B1; case: ifPn => B0 //.
Expand All @@ -368,7 +349,7 @@ Definition indic_mfun (D : set aT) (mD : measurable D) :=
HB.instance Definition _ k f := MeasurableFun.copy (k \o* f) (f * cst_mfun k).
Definition scale_mfun k f := [the {mfun aT >-> rT} of k \o* f].

Lemma max_mfun_subproof f g : @isMeasurableFun d aT rT (f \max g).
Lemma max_mfun_subproof f g : @isMeasurableFun d _ aT rT (f \max g).
Proof. by split; apply: measurable_maxr. Qed.
HB.instance Definition _ f g := max_mfun_subproof f g.
Definition max_mfun f g := [the {mfun aT >-> _} of f \max g].
Expand All @@ -387,9 +368,28 @@ Qed.
#[deprecated(since="mathcomp-analysis 0.6.3", note="use `measurable_indic` instead")]
Notation measurable_fun_indic := measurable_indic (only parsing).

HB.structure Definition SimpleFun d (aT : measurableType d) (rT : realType) :=
{f of @isMeasurableFun d _ aT rT f & @FiniteImage aT rT f}.
Reserved Notation "{ 'sfun' aT >-> T }"
(at level 0, format "{ 'sfun' aT >-> T }").
Reserved Notation "[ 'sfun' 'of' f ]"
(at level 0, format "[ 'sfun' 'of' f ]").
Notation "{ 'sfun' aT >-> T }" := (@SimpleFun.type _ aT T) : form_scope.
Notation "[ 'sfun' 'of' f ]" := [the {sfun _ >-> _} of f] : form_scope.

HB.structure Definition NonNegSimpleFun
d (aT : measurableType d) (rT : realType) :=
{f of @SimpleFun d _ _ f & @NonNegFun aT rT f}.
Reserved Notation "{ 'nnsfun' aT >-> T }"
(at level 0, format "{ 'nnsfun' aT >-> T }").
Reserved Notation "[ 'nnsfun' 'of' f ]"
(at level 0, format "[ 'nnsfun' 'of' f ]").
Notation "{ 'nnsfun' aT >-> T }" := (@NonNegSimpleFun.type _ aT%type T) : form_scope.
Notation "[ 'nnsfun' 'of' f ]" := [the {nnsfun _ >-> _} of f] : form_scope.

Section sfun_pred.
Context {d} {aT : sigmaRingType d} {rT : realType}.
Definition sfun : {pred _ -> _} := [predI @mfun _ aT rT & fimfun].
Definition sfun : {pred _ -> _} := [predI @mfun _ _ aT rT & fimfun].
Definition sfun_key : pred_key sfun. Proof. exact. Qed.
Canonical sfun_keyed := KeyedPred sfun_key.
Lemma sub_sfun_mfun : {subset sfun <= mfun}. Proof. by move=> x /andP[]. Qed.
Expand All @@ -403,7 +403,7 @@ Notation sfun := (@sfun _ aT rT).
Section Sub.
Context (f : aT -> rT) (fP : f \in sfun).
Definition sfun_Sub1_subproof :=
@isMeasurableFun.Build d aT rT f (set_mem (sub_sfun_mfun fP)).
@isMeasurableFun.Build d _ aT rT f (set_mem (sub_sfun_mfun fP)).
#[local] HB.instance Definition _ := sfun_Sub1_subproof.
Definition sfun_Sub2_subproof :=
@FiniteImage.Build aT rT f (set_mem (sub_sfun_fimfun fP)).
Expand All @@ -430,13 +430,15 @@ Proof. by split=> [->//|fg]; apply/val_inj/funext. Qed.

HB.instance Definition _ := [Choice of {sfun aT >-> rT} by <:].

End sfun.

(* TODO: BUG: HB *)
(* HB.instance Definition _ (x : rT) := @cst_mfun_subproof aT rT x. *)
Definition cst_sfun x := [the {sfun aT >-> rT} of cst x].
(* HB.instance Definition _ (x : rT) := @cst_mfun_subproof _ _ aT rT x. *)
HB.instance Definition _ d (rT : measurableType d) (x : rT) := MeasurableFun.on (cst x).

Lemma cst_sfunE x : @cst_sfun x =1 cst x. Proof. by []. Qed.
Definition cst_sfun x := [the @SimpleFun.type _ aT rT (* {sfun aT >-> rT} *) of cst x].

End sfun.
Lemma cst_sfunE x : @cst_sfun x =1 cst x. Proof. by []. Qed.

(* a better way to refactor function stuffs *)
Lemma fctD (T : pointedType) (K : ringType) (f g : T -> K) : f + g = f \+ g.
Expand Down

0 comments on commit 9ba0002

Please sign in to comment.