Module mathcomp.analysis.measure_theory.measurable_function

From HB Require Import structures.
From mathcomp Require Import boot order.
#[warning="-warn-library-file-internal-analysis"]
From mathcomp Require Import unstable.
From mathcomp Require Import boolp classical_sets functions.
From mathcomp Require Import measurable_structure.

# Measurable Functions ``` measurable_fun D f == the function f with domain D is measurable {mfun aT >-> rT} == type of measurable functions aT and rT are sigmaRingType's. f \in mfun == holds for f : {mfun _ >-> _} ```

Reserved Notation "{ 'mfun' aT >-> T }"
  (at level 0, format "{ 'mfun' aT >-> T }").
Reserved Notation "[ 'mfun' 'of' f ]"
  (at level 0, format "[ 'mfun' 'of' f ]").

Unset SsrOldRewriteGoalsOrder.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Import ProperNotations.

Local Open Scope classical_set_scope.
Local Open Scope ring_scope.

Definition ( : sigmaRingType d) ( : sigmaRingType d')
    ( : set T) ( : T -> U) :=
  measurable D -> forall , measurable Y -> measurable (D `&` f @^-1` Y).

. ( d) (rT : sigmaRingType d')
    (f : aT -> rT) := {
  measurable_funPT : measurable_fun [set: aT] f
}.

.
  { of @isMeasurableFun d d' aT rT f}.
Arguments measurable_funPT {d d' aT rT} s.

Notation := (@MeasurableFun.type _ _ aT T) : form_scope.
Notation := [the {mfun _ >-> _} of f] : form_scope.
#[global] Hint Extern 0 (measurable_fun [set: _] _) =>
  solve [apply: measurable_funPT] : core.

Lemma { : measure_display}
  { : measurableType d} { : sigmaRingType d'}
  ( : set aT) ( : {mfun aT >-> rT}) : measurable_fun D s.

Proof.

move=> mD Y mY; apply: measurableI => //.
by rewrite -(setTI (_ @^-1` _)); exact: measurable_funPT.
Qed.

Arguments measurable_funP {d d' aT rT D} s.

Lemma { } { : measurableType d} { : measurableType d'}
( : {mfun aT >-> rT}) ( : set rT) : measurable Y -> measurable (f @^-1` Y).

Proof.

by move=> mY; rewrite -[f @^-1` _]setTI; exact: measurable_funP. Qed.

#[deprecated(since="mathcomp-analysis 1.13.0", note="renamed to `measurable_funPTI`")]
Notation := measurable_funPTI (only parsing).

Section mfun_pred.
Context { } { : sigmaRingType d} { : sigmaRingType d'}.
Definition : {pred aT -> rT} := mem [set | measurable_fun setT f].
Definition : pred_key mfun

Proof.

exact. Qed.

Canonical := KeyedPred mfun_key.
End mfun_pred.

Section measurable_fun.
Context ( : sigmaRingType d1) ( : sigmaRingType d2)
( : sigmaRingType d3).
Implicit Type D E : set T1.

Lemma : measurable_fun D id.

Proof.

by move=> mD A mA; apply: measurableI. Qed.

Lemma ( : T2 -> T3) ( : T1 -> T2) :
measurable F -> g @` E `<=` F ->
measurable_fun F f -> measurable_fun E g -> measurable_fun E (f \o g).

Proof.

move=> mF FgE mf mg /= mE A mA.
rewrite comp_preimage.
rewrite (_ : _ `&` _ = E `&` g @^-1` (F `&` f @^-1` A)).
apply/seteqP; split=> [|? [?] []//].
by move=> x/= [Ex Afgx]; split => //; split => //; exact: FgE.
by apply/mg => //; exact: mf.
Qed.

Lemma ( : T1 -> T2) :
{in D, f =1 g} -> measurable_fun D f -> measurable_fun D g.

Proof.

by move=> fg mf mD A mA; rewrite [X in measurable X](_ : _ = D `&` f @^-1` A);
[exact/esym/eq_preimage|exact: mf].
Qed.

Lemma ( : T1 -> T2) :
{in D, f =1 g} -> measurable_fun D f <-> measurable_fun D g.

Proof.

by move=> eq_fg; split; apply/eq_measurable_fun => // ? ?; rewrite eq_fg.
Qed.

Lemma ( : T2) : measurable_fun D (cst r : T1 -> _).

Proof.

by move=> mD /= Y mY; rewrite preimage_cst; case: ifPn; rewrite ?setIT ?setI0.
Qed.

Lemma ( : (set T1)^nat) ( : T1 -> T2) :
(forall , measurable (E i)) ->
measurable_fun (\bigcup_ E i) f <-> (forall , measurable_fun (E i) f).

Proof.

move=> mE; split => [|mf /= _ A mA]; last first.
by rewrite setI_bigcupl; apply: bigcup_measurable => i _; exact: mf.
move=> mf i _ A /mf => /(_ (bigcup_measurable (fun _ => mE k))).
move=> /(measurableI (E i))-/(_ (mE i)).
by rewrite setICA setIA (@setIidr _ _ (E i))//; exact: bigcup_sup.
Qed.

Lemma ( : T1 -> T2) : measurable D -> measurable E ->
measurable_fun (D `|` E) f <-> measurable_fun D f /\ measurable_fun E f.

Proof.

Lemma ( : T1 -> T2) :
measurable E -> D `<=` E -> measurable_fun E f ->
measurable_fun D f.

Proof.

move=> mE DE mf mD; have mC : measurable (E `\` D) by exact: measurableD.
move: (mD).
have := measurable_funU f mD mC.
suff -> : D `|` (E `\` D) = E by move=> [[]] //.
by rewrite setDUK.
Qed.

Lemma ( : T1 -> T2) ( : measurable D)
    ( : T1 -> bool) ( : measurable_fun D f) :
  measurable_fun (D `&` (f @^-1` [set true])) g ->
  measurable_fun (D `&` (f @^-1` [set false])) h ->
  measurable_fun D (fun => if f t then g t else h t).

Proof.

move=> mx my /= _ B mB; rewrite (_ : _ @^-1` B =
    ((f @^-1` [set true]) `&` (g @^-1` B)) `|`
    ((f @^-1` [set false]) `&` (h @^-1` B))).
  apply/seteqP; split=> [t /=| t /= [] [] ->//].
  by case: ifPn => ft; [left|right].
rewrite setIUr; apply: measurableU.
- by rewrite setIA; apply: mx => //; exact: mf.
- by rewrite setIA; apply: my => //; exact: mf.
Qed.

Lemma ( : T1 -> T2) : measurable_fun set0 f.

Proof.

by move=> A B _; rewrite set0I. Qed.

Lemma ( : T1 -> T2) : measurable_fun [set a] f.

Proof.

by move=> ? ? ?; rewrite set1I; case: ifP. Qed.

End measurable_fun.
#[global] Hint Extern 0 (measurable_fun _ (fun=> _)) =>
  solve [apply: measurable_cst] : core.
#[global] Hint Extern 0 (measurable_fun _ (cst _)) =>
  solve [apply: measurable_cst] : core.
#[global] Hint Extern 0 (measurable_fun _ id) =>
  solve [apply: measurable_id] : core.
Arguments eq_measurable_fun {d1 d2 T1 T2 D} f {g}.
Arguments measurable_fun_eqP {d1 d2 T1 T2 D} f {g}.
Arguments measurable_funS {d1 d2 T1 T2} E {D f}.

Section mfun.
Context { } { : sigmaRingType d} { : sigmaRingType d'}.
Notation := {mfun aT >-> rT}.
Notation := (@mfun _ _ aT rT).

Section Sub.
Context ( : aT -> rT) ( : f \in mfun).
Definition := @isMeasurableFun.Build d _ aT rT f (set_mem fP).
..
Definition := [mfun of f].
End Sub.

Lemma ( : T -> Type) :
  (forall ( : f \in mfun), K (mfun_Sub Pf)) -> forall : T, K u.

Proof.

move=> Ksub [f [[Pf]]]/=.
by suff -> : Pf = (set_mem (@mem_set _ [set | _] f Pf)) by apply: Ksub.
Qed.

Lemma ( : f \in mfun) : mfun_Sub Pf = f :> (_ -> _).

Proof.

by []. Qed.

..Build _ _ T mfun_rect mfun_valP.

Lemma ( : {mfun aT >-> rT}) : f = g <-> f =1 g.

Proof.

by split=> [->//|fg]; apply/val_inj/funext. Qed.

. of {mfun aT >-> rT} by <:].

..Build d _ aT rT (cst x)
  (@measurable_cst _ _ aT rT setT x).

End mfun.

Section measurable_fun_restrict.
Context ( : measurableType d1) ( : pmeasurableType d2)
  ( : measurableType d3).
Implicit Type D E : set T1.

Lemma ( : T1 -> T2) : measurable D -> measurable E ->
  measurable_fun (E `&` D) f <-> measurable_fun E (f \_ D).

Proof.

move=> mD mE; split => mf _ /= Y mY.
- rewrite preimage_restrict; case: ifPn => ptX; last first.
    by rewrite set0U setIA; apply: mf => //; exact: measurableI.
  rewrite setIUr; apply: measurableU.
    by apply: measurableI => //; exact: measurableC.
  by rewrite setIA; apply: mf => //; exact: measurableI.
- have := mf mE _ mY; rewrite preimage_restrict; case: ifP => ptY; last first.
    by rewrite set0U setIA.
  rewrite setUIr setvU setTI setIUr => /(measurableI _ _ mD).
  by rewrite setIUr setIA setIAC setICr set0I set0U setICA setIA.
Qed.

Lemma ( : T1 -> T2) : measurable D ->
measurable_fun D f <-> measurable_fun [set: T1] (f \_ D).

Proof.

by move=> mD; have := measurable_restrict f mD measurableT; rewrite setTI.
Qed.

End measurable_fun_restrict.

Section measurable_fun_measurableType.
Context ( : measurableType d1) ( : measurableType d2)
( : measurableType d3).
Implicit Type D E : set T1.

Lemma ( : T2 -> T3) ( : T1 -> T2) :
measurable_fun [set: T2] f -> measurable_fun E g -> measurable_fun E (f \o g).

Proof.

exact: measurable_comp. Qed.

Lemma ( : T1 -> T2) :
measurable_fun [set: T1] f -> measurable_fun D f.

Proof.

exact: measurable_funS. Qed.

Lemma ( : T1 -> T2) ( : T1 -> bool)
    ( : measurable_fun [set: T1] f) :
  measurable_fun [set: T1] g -> measurable_fun [set: T1] h ->
  measurable_fun [set: T1] (fun => if f t then g t else h t).

Proof.

by move=> mx my; apply: measurable_fun_if => //;
[exact: measurable_funS mx|exact: measurable_funS my].
Qed.

Section measurable_fun_bool.
Implicit Types f g : T1 -> bool.

Let :
  measurable (D `&` f @^-1` [set true]) ->
  measurable (D `&` f @^-1` [set false]) ->
  measurable_fun D f.

Proof.

move=> mT mF mD /= Y mY.
have := @subsetT _ Y; rewrite setT_bool => YT.
move: mY; have [-> _|-> _|-> _ |-> _] := subset_set2 YT.
- by rewrite preimage0 ?setI0.
- exact: mT.
- exact: mF.
- by rewrite -setT_bool preimage_setT setIT.
Qed.

Lemma :
measurable (D `&` f @^-1` [set b]) -> measurable_fun D f.

Proof.

move=> mb mD; have mDb : measurable (D `&` f @^-1` [set ~~ b]).
  rewrite (_ : [set ~~ b] = [set~ b]).
    by apply/seteqP; split=> -[] /=; case: b {mb}.
  by rewrite -preimage_setC; exact: measurableID.
by case: b => /= in mb mDb *; exact: measurable_fun_TF.
Qed.

#[global] Arguments measurable_fun_bool {D f} _.

Lemma : measurable_fun D f -> measurable_fun D g ->
measurable_fun D (fun => f x && g x).

Proof.

move=> mf mg mD; apply: (measurable_fun_bool true) => //.
rewrite [X in measurable X](_ : _ = D `&` f @^-1` [set true] `&`
(D `&` g @^-1` [set true])).
by rewrite setIACA setIid; congr (_ `&` _); apply/seteqP; split => x /andP.
by apply: measurableI; [exact: mf|exact: mg].
Qed.

Lemma :
measurable_fun D f -> measurable_fun D (fun => ~~ f x).

Proof.

move=> mf mD; apply: (measurable_fun_bool true) => //.
rewrite [X in measurable X](_ : _ = (D `&` f @^-1` [set false])).
by apply/seteqP; split => [x [Dx/= /negbTE]|x [Dx/= ->]].
exact: mf.
Qed.

Lemma : measurable_fun D f -> measurable_fun D g ->
measurable_fun D (fun => f x || g x).

Proof.

move=> mf mg.
rewrite [X in measurable_fun _ X](_ : _ = (fun => ~~ (~~ f x && ~~ g x))).
by apply/funext=> x; rewrite -negb_or negbK.
by apply: measurable_neg; apply: measurable_and; exact: measurable_neg.
Qed.

End measurable_fun_bool.

End measurable_fun_measurableType.
#[global] Hint Extern 0 (measurable_fun _ (fun=> _)) =>
  solve [apply: measurable_cst] : core.
#[global] Hint Extern 0 (measurable_fun _ (cst _)) =>
  solve [apply: measurable_cst] : core.
#[global] Hint Extern 0 (measurable_fun _ id) =>
  solve [apply: measurable_id] : core.
Arguments eq_measurable_fun {d1 d2 T1 T2 D} f {g}.
Arguments measurable_fun_bool {d1 T1 D f} b.

Section mfun_measurableType.
Context {} { : measurableType d1} {} { : measurableType d2}
  {} { : measurableType d3} ( : {mfun T2 >-> T3}) ( : {mfun T1 >-> T2}).

Let : measurable_fun setT (f \o g).

Proof.

exact: measurableT_comp. Qed.

..Build _ _ _ _ (f \o g)
  measurableT_comp_subproof.

End mfun_measurableType.

Lemma ( : Type)
     ( : measurableType d) ( : sigmaRingType d')
    ( : rT -> T) ( : aT -> rT) ( : set aT) :
  measurable_fun setT g ->
  preimage_set_system D (g \o f) measurable `<=`
    preimage_set_system D f measurable.

Proof.

move=> mg A; rewrite /preimage_set_system => -[B GB]; exists (g @^-1` B) => //.
by rewrite -[X in measurable X]setTI; exact: mg.
Qed.

Section g_sigma_algebra_preimage_comp.
Context {} { : measurableType d} {} { : measurableType d1}
  {} { : measurableType d2}.

Lemma ( : {mfun T >-> T1}) ( : T1 -> T2) :
  measurable_fun [set: T1] f ->
  g_sigma_algebra_preimage (f \o X) `<=` g_sigma_algebra_preimage X.

Proof.

exact: preimage_set_system_compS. Qed.

End g_sigma_algebra_preimage_comp.
Arguments g_sigma_algebra_preimage_comp {d T d1 T1 d2 T2 X} f.

Section measurability.

Lemma {} { : choiceType}
    { : measurableType d} ( : set aT) ( : aT -> rT) :
  measurable_fun
    (D : set (g_sigma_algebraType (preimage_set_system D f measurable))) f.

Proof.

by move=> mD A mA; apply: sub_sigma_algebra; exists A. Qed.

The converse hols when `D` is measurable

Lemma { } { : measurableType d}
    { : measurableType d'} ( : set aT) ( : aT -> rT) :
  preimage_set_system D f (@measurable _ rT) `<=` @measurable _ aT ->
  measurable_fun D f.

Proof.

by move=> + mD Y mY; apply; exists Y. Qed.

Lemma { } { : measurableType d} { : measurableType d'}
    ( : set aT) ( : aT -> rT) ( : set_system rT) :
  @measurable _ rT = <<s G >> ->
  preimage_set_system D f G `<=` @measurable _ aT ->
  measurable_fun D f.

Proof.

move=> sG_rT fG_aT /[dup] mD; apply: preimage_measurability.
rewrite sG_rT -g_sigma_preimageE smallest_sub_iff//.
exact: sigma_algebra_measurable.
Qed.

End measurability.
Arguments measurability {d d' aT rT D f} _.

Section prod_measurable_fun.
Context { } { : measurableType d} { : measurableType d1}
{ : measurableType d2}.

Lemma ( : T -> T1 * T2) : measurable_fun setT h <->
measurable_fun setT (fst \o h) /\ measurable_fun setT (snd \o h).

Proof.

apply: (@iff_trans _ (g_sigma_preimageU (fst \o h) (snd \o h) `<=` measurable)).
- rewrite g_sigma_preimageU_comp; split=> [mf A [C HC <-]|f12]; first exact: mf.
  by move=> _ A mA; apply: f12; exists A.
- split => [h12|[mf1 mf2]].
    split => _ A mA; apply: h12; apply: sub_sigma_algebra;
    by [left; exists A|right; exists A].
  apply: smallest_sub; first exact: sigma_algebra_measurable.
  by rewrite subUset; split=> [|] A [C mC <-]; [exact: mf1|exact: mf2].
Qed.

Lemma ( : T -> T1) ( : T -> T2) :
measurable_fun setT f -> measurable_fun setT g ->
measurable_fun setT (fun => (f x, g x)).

Proof.

by move=> mf mg; exact/measurable_fun_pairP. Qed.

End prod_measurable_fun.

Section prod_measurable_proj.
Context { } { : measurableType d1} { : measurableType d2}.

Lemma : measurable_fun [set: T1 * T2] fst.

Proof.

by have /measurable_fun_pairP[] := @measurable_id _ (T1 * T2)%type setT.
Qed.

#[local] Hint Resolve measurable_fst : core.

Lemma : measurable_fun [set: T1 * T2] snd.

Proof.

by have /measurable_fun_pairP[] := @measurable_id _ (T1 * T2)%type setT.
Qed.

#[local] Hint Resolve measurable_snd : core.

Lemma : measurable_fun [set: _] (@swap T1 T2).

Proof.

exact: measurable_fun_pair. Qed.

End prod_measurable_proj.
Arguments measurable_fst {d1 d2 T1 T2}.
Arguments measurable_snd {d1 d2 T1 T2}.
#[global] Hint Extern 0 (measurable_fun _ fst) =>
  solve [apply: measurable_fst] : core.
#[global] Hint Extern 0 (measurable_fun _ snd) =>
  solve [apply: measurable_snd] : core.

Lemma ( : sigmaRingType d) ( : 'I_n) :
  measurable_fun [set: n.-tuple T] (@tnth _ T ^~ i).

Proof.

move=> _ Y mY; rewrite setTI; apply: sub_sigma_algebra => /=.
rewrite -bigcup_seq/=; exists i => /=; first by rewrite mem_index_enum.
by exists Y => //; rewrite setTI.
Qed.

Section measurable_cons.
Context ( : measurableType d1) ( : measurableType d2).

Lemma ( : T1 -> n.-tuple T2) :
measurable_fun [set: T1] f <->
forall , measurable_fun [set: T1] (@tnth n T2 ^~ i \o f).

Proof.

apply: (@iff_trans _ (g_sigma_preimage
    (fun => @tnth n T2 ^~ i \o f) `<=` measurable)).
  rewrite g_sigma_preimage_comp; split=> [mf A [/= C preC <-]|prefS].
    exact: mf.
  by move=> _ A mA; apply: prefS; exists A.
split=> [tnthfS i|mf].
- move=> _ A mA.
  apply: tnthfS; apply: sub_sigma_algebra.
  case: n i => [[] []//|n i] in f *.
  rewrite -bigcup_mkord_ord.
  exists i; first exact: ltn_ord.
  by exists A => //; rewrite inord_val.
- apply: smallest_sub; first exact: sigma_algebra_measurable.
  case: n => [|n] in f mf *; first by rewrite big_ord0.
  rewrite -bigcup_mkord_ord; apply: bigcup_sub => i Ii.
  by move=> A [B mB <-]; exact: mf.
Qed.

Lemma ( : T1 -> T2) ( : T1 -> n.-tuple T2) :
measurable_fun [set: T1] f -> measurable_fun [set: T1] g ->
measurable_fun [set: T1] (fun => [the n.+1.-tuple T2 of f x :: g x]).

Proof.

move=> mf mg; apply/measurable_fun_tnthP => /= i.
have [->//|i0] := eqVneq i ord0.
have i1n : (i.-1 < n)%N by rewrite prednK ?lt0n// -ltnS.
pose j := Ordinal i1n.
rewrite (_ : _ \o _ = fun => tnth (g x) j)//; last first.
apply: (@measurableT_comp _ _ _ _ _ _ (fun => tnth x j)) => //=.
exact: measurable_tnth.
apply/funext => x /=.
rewrite (_ : i = lift ord0 j) ?tnthS//.
by apply/val_inj => /=; rewrite /bump/= add1n prednK// lt0n.
Qed.

End measurable_cons.

Lemma ( : measurableType d) :
measurable_fun [set: n.+1.-tuple T] (fun => [tuple of behead x]).

Proof.

move=> _ Y mY; rewrite setTI.
set f := fun : (n.+1).-tuple T => [tuple of behead x] : n.-tuple T.
move: mY; rewrite /measurable/= => + F [] sF.
pose F' := image_set_system setT f F.
move=> /(_ F') /=.
have -> : F' Y = F (f @^-1` Y) by rewrite /F' /image_set_system /= setTI.
move=> /[swap] bigF; apply; split; first exact: sigma_algebra_image.
move=> A; rewrite /= {}/F' /image_set_system /= setTI.
set bign := (X in X A -> _) => bignA.
apply: bigF; rewrite big_ord_recl /=; right.
set bign1 := (X in X (_ @^-1` _)).
have -> : bign1 = preimage_set_system [set: n.+1.-tuple T] f bign.
  rewrite (big_morph _ (preimage_set_systemU _ _) (preimage_set_system0 _ _)).
  apply: eq_bigr => i _; rewrite -preimage_set_system_comp.
  congr preimage_set_system.
  by apply: funext=> t/=; rewrite [in LHS](tuple_eta t) tnthS.
by exists A => //; rewrite setTI.
Qed.

Lemma ( : measurableType d)
    ( : measurableType d') ( : X -> Y) :
  measurable_fun setT x -> measurable_fun setT y ->
  measurable_fun setT (fun => if tb.2 then x tb.1 else y tb.1).

Proof.

by move=> mx my; apply: measurable_fun_ifT => //=; exact: measurableT_comp.
Qed.

Section pair_measurable_fun.
Context {} {} {} { : measurableType d} { : measurableType d1}
{ : measurableType d2} ( : T1 * T2 -> T).

Lemma ( : T1) : measurable_fun [set: T2] (pair x).

Proof.

have m1pairx : measurable_fun [set: T2] (fst \o pair x) by exact/measurable_cst.
have m2pairx : measurable_fun [set: T2] (snd \o pair x) by exact/measurable_id.
exact/measurable_fun_pairP.
Qed.

Lemma ( : T2) : measurable_fun [set: T1] (pair^~ y).

Proof.

have m1pairy : measurable_fun [set: T1] (fst \o pair^~y) by exact/measurable_id.
have m2pairy : measurable_fun [set: T1] (snd \o pair^~y) by exact/measurable_cst.
exact/measurable_fun_pairP.
Qed.

End pair_measurable_fun.
#[global] Hint Extern 0 (measurable_fun _ (pair _)) =>
  solve [apply: pair1_measurable] : core.
#[global] Hint Extern 0 (measurable_fun _ (pair^~ _)) =>
  solve [apply: pair2_measurable] : core.

Section measurable_section.
Context ( : measurableType d1) ( : measurableType d2)
  ( : measurableType d3).

Lemma ( : set (T1 * T2)) ( : T1) :
  measurable A -> measurable (xsection A x).

Proof.

move=> mA; pose i ( : T2) := (x, y).
have mi : measurable_fun setT i by exact: pair1_measurable.
by rewrite xsectionE -[X in measurable X]setTI; exact: mi.
Qed.

Lemma ( : set (T1 * T2)) ( : T2) :
measurable A -> measurable (ysection A y).

Proof.

move=> mA; pose i ( : T1) := (x, y).
have mi : measurable_fun setT i by exact: pair2_measurable.
by rewrite ysectionE -[X in measurable X]setTI; exact: mi.
Qed.

Lemma ( : T1 * T2 -> T3) ( : T2) :
measurable_fun setT f -> measurable_fun setT (fun => f (x, y)).

Proof.

by move=> mf; exact: measurableT_comp. Qed.

Lemma ( : T1 * T2 -> T3) ( : T1) :
measurable_fun setT f -> measurable_fun setT (fun => f (x, y)).

Proof.

by move=> mf; exact: measurableT_comp. Qed.

End measurable_section.

Files

Module mathcomp.analysis.measure_theory.measurable_function