Module mathcomp.analysis.lebesgue_integral_theory.simple_functions

From HB Require Import structures.
From mathcomp Require Import boot order ssralg ssrnum ssrint interval.
From mathcomp Require Import interval_inference archimedean finmap.
From mathcomp Require Import boolp classical_sets functions cardinality fsbigop.
From mathcomp Require Import reals real_interval topology ereal.
From mathcomp Require Import normedtype sequences esum measure.
From mathcomp Require Import real_measure numfun realfun.

# Simple functions This file contains a formalization of simple functions and with basic properties (addition, etc.). About the use of simple functions: Because of a limitation of HB <= 1.8.0, we need some care to be able to use simple functions. The structure SimpleFun (resp. NonNegSimpleFun) is located inside the module HBSimple (resp. HBNNSimple). As a consequence, we need to import HBSimple (resp. HBNNSimple) to use the coercion from simple functions (resp. non-negative simple functions) to Rocq functions. Also, assume that f (e.g., cst, indic) is equipped with the structure of MeasurableFun. For f to be equipped with the structure of SimpleFun (resp. NonNegSimpleFun), one need locally to import HBSimple (resp. HBNNSimple) and to instantiate FiniteImage (resp. NonNegFun) locally. Detailed contents: ```` {sfun T >-> R} == type of simple functions They form a (potentially zero) ring. {nnsfun T >-> R} == type of non-negative simple functions indic_sfun mD := mindic _ mD cst_sfun r == constant simple function cst_nnsfun r == constant simple function nnsfun0 := cst_nnsfun 0 add_nnsfun f g := f \+ g mul_nnsfun f g := f \* g max_nnsfun f g := f \max g proj_nssfun f mA == projection of the function f to the set A mA is a proof that A is measurable scale_nnsfun k f == scales f by the non-negative real number k sum_nnsfun f n := \big[add_nnsfun/nnsfun0]_(i < n) f i bigmax_nnsfun f n := \big[max_nnsfun/nnsfun0]_(i < n) f i ````

Reserved Notation "{ 'nnfun' aT >-> T }"
  (at level 0, format "{ 'nnfun' aT >-> T }").
Reserved Notation "[ 'nnfun' 'of' f ]"
  (at level 0, format "[ 'nnfun' 'of' 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 ]").
Reserved Notation "{ 'sfun' aT >-> T }"
  (at level 0, format "{ 'sfun' aT >-> T }").
Reserved Notation "[ 'sfun' 'of' f ]"
  (at level 0, format "[ 'sfun' 'of' f ]").

Unset SsrOldRewriteGoalsOrder.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Import Order.TTheory GRing.Theory Num.Def Num.Theory.
Import numFieldNormedType.Exports.

Local Open Scope classical_set_scope.
Local Open Scope ring_scope.

Module .
Import MeasurableR.

. ( d) (rT : realType) :=
  { of @isMeasurableFun d _ aT rT f & @FiniteImage aT rT f}.

End HBSimple.

Notation := (@HBSimple.SimpleFun.type _ aT T) : form_scope.
Notation := [the {sfun _ >-> _} of f] : form_scope.

Module .
Import HBSimple.

.
     ( d) (rT : realType) :=
  { of @SimpleFun d _ _ f & @NonNegFun aT rT f}.

End HBNNSimple.

Notation := (@HBNNSimple.NonNegSimpleFun.type _ aT%type T) : form_scope.
Notation := [the {nnsfun _ >-> _} of f] : form_scope.

Section sfun_pred.
Context {} { : sigmaRingType d} { : realType}.
Import MeasurableR.
Definition : {pred _ -> _} := [predI @mfun _ _ aT rT & fimfun].
Definition : pred_key sfun

Proof.

exact. Qed.

Canonical := KeyedPred sfun_key.
Lemma : {subset sfun <= mfun}

Proof.

by move=> x /andP[]. Qed.

Lemma : {subset sfun <= fimfun}

Proof.

by move=> x /andP[]. Qed.

End sfun_pred.

Section sfun.
Context {} { : measurableType d} { : realType}.
Notation := {sfun aT >-> rT}.
Notation := (@sfun _ aT rT).
Section Sub.
Context ( : aT -> rT) ( : f \in sfun).
Import MeasurableR.
Definition :=
  @isMeasurableFun.Build d _ aT rT f (set_mem (sub_sfun_mfun fP)).
..
Definition :=
  @FiniteImage.Build aT rT f (set_mem (sub_sfun_fimfun fP)).

Import HBSimple.

..
Definition := [sfun of f].
End Sub.

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

Proof.

move=> Ksub [f [[Pf1] [Pf2]]]; have Pf : f \in sfun by apply/andP; rewrite ?inE.
have -> : Pf1 = set_mem (sub_sfun_mfun Pf) by [].
have -> : Pf2 = set_mem (sub_sfun_fimfun Pf) by [].
exact: Ksub.
Qed.

Import HBSimple.

Lemma ( : f \in sfun) : sfun_Sub Pf = f :> (_ -> _).

Proof.

by []. Qed.

..Build _ _ T sfun_rect sfun_valP.

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

Proof.

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

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

Import MeasurableR.

. aT rT (cst x) := FImFun.on (cst x).

Definition : {sfun aT >-> rT} := cst x.

Lemma : @cst_sfun x =1 cst x

Proof.

by []. Qed.

End sfun.

Lemma ( : Type) ( : pzRingType) ( : T -> K) : f + g = f \+ g.

Proof.

by []. Qed.

Lemma ( : Type) ( : pzRingType) ( : T -> K) : - f = \- f.

Proof.

by []. Qed.

Lemma ( : Type) ( : pzRingType) ( : T -> K) : f * g = f \* g.

Proof.

by []. Qed.

Lemma ( : Type) ( : pzRingType) ( : lmodType K) ( : T -> L) :
k *: f = k \*: f.

Proof.

by []. Qed.

Arguments cst _ _ _ _ /.
Definition := (fctD, fctN, fctM, fctZ).

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

Lemma : subring_closed (@sfun d aT rT).

Proof.

by split=> [|f g|f g]; rewrite ?inE/= ?rpred1//;
move=> /andP[/= mf ff] /andP[/= mg fg]; rewrite !(rpredB, rpredM).
Qed.

..isSubringClosed.Build _ sfun
sfun_subring_closed.
. of {sfun aT >-> rT} by <:].

Implicit Types (f g : {sfun aT >-> rT}).

Import HBSimple.

Lemma : (0 : {sfun aT >-> rT}) =1 cst 0

Proof.

by []. Qed.

Lemma : (1 : {sfun aT >-> rT}) =1 cst 1

Proof.

by []. Qed.

Lemma : - f =1 \- f

Proof.

by []. Qed.

Lemma : f + g =1 f \+ g

Proof.

by []. Qed.

Lemma : f - g =1 f \- g

Proof.

by []. Qed.

Lemma : f * g =1 f \* g

Proof.

by []. Qed.

Lemma ( : {pred I}) ( : I -> {sfun aT >-> rT}) ( : aT) :
(\sum_( <- r | P i) f i) x = \sum_( <- r | P i) f i x.

Proof.

by elim/big_rec2: _ => //= i y ? Pi <-. Qed.

Lemma ( : {pred I}) ( : I -> {sfun aT >-> rT}) ( : aT) :
(\sum_( <- r | P i) f i) x = \sum_( <- r | P i) f i x.

Proof.

by elim/big_rec2: _ => //= i y ? Pi <-. Qed.

Lemma : f ^+ n =1 (fun => f x ^+ n).

Proof.

by move=> x; elim: n => [|n IHn]//; rewrite !exprS sfunM/= IHn. Qed.

Import MeasurableR.

..copy (f \+ g) (f + g).
..copy (\- f) (- f).
..copy (f \- g) (f - g).
..copy (f \* g) (f * g).

Import HBSimple.

. ( aT) (mD : measurable D) :
   @FImFun aT rT (mindic _ mD) := FImFun.on (mindic _ mD).
Definition ( : set aT) ( : measurable D) : {sfun aT >-> rT} :=
  mindic rT mD.

..copy (k \o* f) (f * cst_sfun k).
Definition : {sfun aT >-> rT} := k \o* f.

End ring.
Arguments indic_sfun {d aT rT} _.

Lemma ( : realDomainType) ( : {nnfun T >-> R}) :
  t < 0 -> f @^-1` [set t] = set0.

Proof.

move=> t0.
by apply/preimage10 => -[x _]; apply: contraPnot t0 => <-; rewrite le_gtF.
Qed.

Lemma ( : realFieldType) ( : R) ( : T -> R) :
x != 0 -> (cst x \* f) @^-1` [set y] = f @^-1` [set y / x].

Proof.

move=> x0; apply/seteqP.
by split=> [z/= <-|z/= ->]; rewrite [x * _]mulrC (mulfK, divfK).
Qed.

Section simple_bounded.
Context {} { : sigmaRingType d} { : realType}.

Import HBSimple.

Lemma ( : {sfun T >-> R}) : bounded_fun f.

Proof.

have /finite_seqP[r fr] := fimfunP f.
exists (fine (\big[maxe/-oo%E]_( <- r) `|i|%:E)).
split; rewrite ?num_real// => x mx z _; apply/ltW/(le_lt_trans _ mx).
have ? : f z \in r by have := imageT f z; rewrite fr.
rewrite -[leLHS]/(fine `|f z|%:E) fine_le//.
  rewrite -(big_map (EFin \o normr) xpredT idfun)/= bigmaxe_fin_num//.
    rewrite -size_eq0 -lt0n -has_predT; apply/hasP.
    by exists `|f z|%:E => //=; apply/mapP; exists (f z).
  by move=> /= y /mapP[s sr/= ->]; rewrite leNye.
exact: (bigmax_sup_seq _ _ _ _ _ _ _ (lexx _)).
Qed.

End simple_bounded.

Section nnsfun_functions.
Context ( : measurableType d) ( : realType).

Import HBNNSimple.
Import MeasurableR.

Lemma ( : {nonneg R}) : forall : T, 0 <= cst x%:num t.

Proof.

by move=> /=. Qed.

..Build T R (cst x%:num)
(cst_nnfun_subproof x).

Definition ( : {nonneg R}) : {nnsfun T >-> R} := cst r%:num.

Definition : {nnsfun T >-> R} := cst_nnsfun 0%:nng.

Lemma ( : set T) : forall , 0 <= (\1_D) x :> R.

Proof.

by []. Qed.

..Build T R \1_D
(indic_nnfun_subproof D).

. ( D) :
@NonNegFun T R (mindic R mD) := NonNegFun.on (mindic R mD).

End nnsfun_functions.
Arguments nnsfun0 {d T R}.

Section nnfun_bin.
Variables ( : Type) ( : numDomainType) ( : {nnfun T >-> R}).

Lemma : @isNonNegFun T R (f \+ g).

Proof.

by split => x; rewrite addr_ge0//; apply/fun_ge0. Qed.

..

Lemma : @isNonNegFun T R (f \* g).

Proof.

by split => x; rewrite mulr_ge0//; apply/fun_ge0. Qed.

..

Lemma : @isNonNegFun T R (f \max g).

Proof.

by split => x /=; rewrite /maxr; case: ifPn => _; apply: fun_ge0. Qed.

..

End nnfun_bin.

Section nnsfun_bin.
Context ( : measurableType d) ( : realType).
Variables : {nnsfun T >-> R}.

Import HBNNSimple.
Import MeasurableR.

..on (f \+ g).
Definition : {nnsfun T >-> R} := f \+ g.

..on (f \* g).
Definition : {nnsfun T >-> R} := f \* g.

..on (f \max g).
Definition : {nnsfun T >-> R} := f \max g.

Definition ( : measurable A) : {nnsfun T >-> R} := mindic R mA.

End nnsfun_bin.
Arguments add_nnsfun {d T R} _ _.
Arguments mul_nnsfun {d T R} _ _.
Arguments max_nnsfun {d T R} _ _.

Definition ( : measurableType d) ( : realType)
    ( : {nnsfun T >-> R}) ( : R) ( : 0 <= k) :=
  mul_nnsfun (cst_nnsfun T (NngNum k0)) f.

Definition ( : measurableType d) ( : realType)
    ( : {nnsfun T >-> R}) ( : set T) ( : measurable A) :=
  mul_nnsfun f (indic_nnsfun R mA).

Section mrestrict.
Import HBNNSimple.

Lemma ( : measurableType d) ( : realType) ( : {nnsfun T >-> R})
   ( : measurable A) : f \_ A = proj_nnsfun f mA.

Proof.

apply/funext => x /=; rewrite /patch mindicE.
by case: ifP; rewrite (mulr0, mulr1).
Qed.

End mrestrict.

Section nnsfun_iter.
Context ( : measurableType d) ( : realType) ( : set T).
Variable : {nnsfun T >-> R}^nat.

Definition := \big[add_nnsfun/nnsfun0]_( < n) f i.

Import HBNNSimple.

Lemma : sum_nnsfun n t = \sum_( < n) (f i t).

Proof.

by rewrite /sum_nnsfun; elim/big_ind2 : _ => [|x g y h <- <-|]. Qed.

Definition := \big[max_nnsfun/nnsfun0]_( < n) f i.

Lemma : bigmax_nnsfun n t = \big[maxr/0]_( < n) (f i t).

Proof.

by rewrite /bigmax_nnsfun; elim/big_ind2 : _ => [|x g y h <- <-|]. Qed.

End nnsfun_iter.

Section nnsfun_cover.
Local Open Scope ereal_scope.
Context ( : measurableType d) ( : realType).
Variable : {nnsfun T >-> R}.

Import HBNNSimple.

Lemma : \big[setU/set0]_( \in range f) (f @^-1` [set i]) = setT.

Proof.

by rewrite fsbig_setU//= -subTset => x _; exists (f x). Qed.

Lemma : \big[setU/set0]_( \in [set: R]) f @^-1` [set i] = setT.

Proof.

by rewrite -(fsbig_widen (range f)) ?nnsfun_cover//= => x [_ /preimage10].
Qed.

End nnsfun_cover.

Section measure_fsbig.
Local Open Scope ereal_scope.
Context ( : measurableType d) ( : realType).
Variable : {measure set T -> \bar R}.

Lemma ( : choiceType) ( : set I) ( : I -> set T) :
  finite_set A ->
  (forall , A i -> measurable (F i)) -> trivIset A F ->
  m (\big[setU/set0]_( \in A) F i) = \sum_( \in A) m (F i).

Proof.

move=> Afin Fm Ft.
by rewrite fsbig_finite// -measure_fin_bigcup// -bigsetU_fset_set.
Qed.

Import HBNNSimple.
Import MeasurableR.

Lemma ( : {nnsfun T >-> R}) :
\sum_( \in range g) m (f @^-1` [set x] `&` (g @^-1` [set i])) =
m (f @^-1` [set x] `&` \big[setU/set0]_( \in range g) (g @^-1` [set i])).

Proof.

rewrite -?measure_fsbig//.
- by move=> i Ai; apply: measurableI.
- exact/trivIset_setIl/trivIset_preimage1.
- by rewrite !fsbig_finite//= big_distrr.
Qed.

Lemma ( : {nnsfun T >-> R}) :
\sum_( \in range g) m (g @^-1` [set i] `&` (f @^-1` [set x])) =
m (\big[setU/set0]_( \in range g) (g @^-1` [set i]) `&` f @^-1` [set x]).

Proof.

by under eq_fsbigr do rewrite setIC; rewrite setIC additive_nnsfunr. Qed.

End measure_fsbig.

Section mulem_ge0.
Local Open Scope ereal_scope.

Let ( : realDomainType) ( : R -> \bar R) :
0 <= f x -> ((x < 0)%R -> f x = 0) -> 0 <= x%:E * f x.

Proof.

case: (ltP x 0%R) => [x_lt0 ? ->|x_ge0 fx_ge0 _] //; last exact: mule_ge0.
by rewrite mule0.
Qed.

Lemma ( : sigmaRingType d) ( : realDomainType)
( : {nnfun T >-> R}) : 0 <= r%:E * (\1_(f @^-1` [set r]) z)%:E.

Proof.

apply: (@mulef_ge0 _ _ (fun => (\1_(f @^-1` [set r]) z)%:E)).
by rewrite lee_fin// indicE.
by move=> r0; rewrite preimage_nnfun0// indic0.
Qed.

Lemma ( : sigmaRingType d) ( : realType)
( : {measure set T -> \bar R}) ( : R -> set T) :
((x < 0)%R -> A x = set0) -> 0 <= x%:E * mu (A x).

Proof.

by move=> xA; rewrite (@mulef_ge0 _ _ (mu \o _))//= => /xA ->; rewrite measure0.
Qed.

Global Arguments mulemu_ge0 {d T R mu x} A.

Import HBNNSimple.

Lemma ( : sigmaRingType d) ( : realType)
( : {measure set T -> \bar R}) ( : {nnsfun T >-> R}) :
0 <= x%:E * mu (f @^-1` [set x]).

Proof.

by apply: (mulemu_ge0 (fun => f @^-1` [set x])); exact: preimage_nnfun0.
Qed.

End mulem_ge0.

Files

Module mathcomp.analysis.lebesgue_integral_theory.simple_functions