Library Lebesgue.Bochner.BInt_Bif

This file is part of the Coq Numerical Analysis library
Copyright (C) Boldo, Clément, Leclerc
This library is free software; you can redistribute it and/or modify it under the terms of the GNU Lesser General Public License as published by the Free Software Foundation; either version 3 of the License, or (at your option) any later version.
This library is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the COPYING file for more details.

Brief description

Support for the integral of Bochner integrable functions to a Banach space.

Usage

This module may be used through the import of Lebesgue.Bochner.Bochner, or Lebesgue.Bochner.Bochner_wDep, where it is exported.

From Requisite Require Import stdlib_wR.
From Coq Require Import ssreflect Utf8.

From Coquelicot Require Import Coquelicot.

From Lebesgue Require Import Lebesgue_p.

Require Import
    series
    hierarchy_notations
    simpl_fun
    CUS_Lim_seq
    BInt_sf
    Bsf_Lsf
    Bi_fun
.

Section BInt_def.

    Context {X : Set}.
    Context {E : CompleteNormedModule R_AbsRing}.
    Context {gen : (X Prop) Prop}.
    Context {μ : measure gen}.

    Definition BInt {f : X E} (bf : Bif μ f) :=
        lim_seq (fun nBInt_sf μ (seq bf n)).

    Theorem is_lim_seq_BInt {f : X E} (bf : Bif μ f) :
        is_lim_seq (fun nBInt_sf μ (seq bf n)) (BInt bf).
    Proof.
        case: bfs ι isf Hspw Hsl1.
        apply NM_Cauchy_seq_lim_seq_correct.
        apply Cauchy_seq_approx with f ⇒ //.
    Qed.

End BInt_def.

Notation "'∫B' bf" := (BInt bf)
        (only printing, at level 45, format "'[ ' '∫B' bf ']'") : Bif_scope.

Section BInt_prop.

    Context {X : Set}.
    Context {E : CompleteNormedModule R_AbsRing}.
    Context {gen : (X Prop) Prop}.
    Context {μ : measure gen}.

    Open Scope Bif_scope.

    Lemma BInt_ext {f f' : X E} :
         bf : Bif μ f, bf' : Bif μ f', ( x : X, f x = f' x)
            BInt bf = BInt bf'.
    Proof.
        movebf bf' Ext;
            case_eq bfs ints Hspw Hsl1 Eqπ;
            case_eq bf's' ints' Hs'pw Hs'l1 Eqπ';
            unfold BInt ⇒ /=.
        pose I := lim_seq (λ n : nat, BInt_sf μ (s n));
        pose I' := lim_seq (λ n : nat, BInt_sf μ (s' n)).
        pose HI := is_lim_seq_BInt bf;
            rewrite Eqπ in HI; simpl in HI;
            clearbody HI; fold I in HI.
        pose HI' := is_lim_seq_BInt bf';
            rewrite Eqπ' in HI'; simpl in HI';
            clearbody HI'; fold I' in HI'.
        move: HI' ⇒ /lim_seq_oppHI'.
        assert (is_lim_seq (λ n : nat, BInt_sf μ (s n) + opp (BInt_sf μ (s' n)))%hy (I + opp I')%hy) as limdif
            by apply: lim_seq_plus ⇒ //.
        clear HI HI'.
        move: limdif ⇒ /(lim_seq_ext _ (λ n : nat, BInt_sf μ (s n - s' n)%sf) _ _) ⇒ limdif.
        assert ( n : nat, (BInt_sf μ (s n) + opp (BInt_sf μ (s' n)))%hy = BInt_sf μ (s n - s' n)%sf).
            moven; rewrite BInt_sf_plus.
            rewrite BInt_sf_scal.
            rewrite scal_opp_one ⇒ //.
            apply ints.
            apply integrable_sf_scal, ints'.
        pose limdif' := limdif H; clearbody limdif';
            clear H; clear limdif.
        assert (is_lim_seq (λ n : nat, BInt_sf μ (s n - s' n)%sf) (I + opp I')%hy)
            as limdif by unfold is_lim_seq ⇒ //; clear limdif'.
        fold I I'.

        suff: (is_lim_seq (λ n : nat, BInt_sf μ (s n - s' n)%sf) zero).
        movelimdif'.
        assert (I + opp I' = zero)%hy.
        apply NM_is_lim_seq_unique with (λ n : nat, BInt_sf μ (s n - s' n)%sf) ⇒ //.
        apply (plus_reg_r (opp I'));
            rewrite H;
            rewrite plus_opp_r ⇒ //.
        clear I I' limdif.

        apply lim_seq_norm_zero.
        suff: (Lim_seq.is_lim_seq (‖(λ n : nat, BInt_sf μ (s n - s' n)%sf)‖)%fn 0%R).
            unfold Lim_seq.is_lim_seq;
            unfold Rbar_locally.
            unfold is_lim_seq ⇒ //.
        suff: (is_LimSup_seq_Rbar ( λ n : nat, BInt_sf μ (s n - s' n)%sf )%fn 0).
            moveHLS.
            simpl in HLS.
            apply is_lim_seq_spec; unfold is_lim_seq'.
            movesigɛ.
            case: (HLS sigɛ) ⇒ _ {}HLS;
                case: HLSN HLS.
             Nn Hn.
            pose HLSn := (HLS n Hn);
                clearbody HLSn;
                clear HLS Hn.
                unfold Rminus; rewrite RIneq.Ropp_0.
                rewrite Raxioms.Rplus_0_l in HLSn.
                rewrite (proj1 (RIneq.Rplus_ne _)).
                rewrite Rabs_pos_eq ⇒ //.
                unfold fun_norm; apply norm_ge_0.

        unfold fun_norm.

        unfold is_LimSup_seq_Rbar ⇒ ɛ; split; swap 1 2.
        simpl; rewrite Raxioms.Rplus_0_l.

        2 : moveN0.
        2 : N0; split ⇒ //.
        2 : simpl; unfold Rminus; rewrite Raxioms.Rplus_0_l.
        2 : apply RIneq.Rlt_le_trans with 0.
        2 : case: ɛ ⇒ ɛ Hɛ ⇒ /=.
        2 : apply RIneq.Ropp_lt_gt_0_contravar ⇒ //.
        2 : apply norm_ge_0.

        case: ɛ ⇒ ɛ Hɛ.

        pose sighalfɛ := RIneq.mkposreal× /2) (R_compl.Rmult_lt_pos_pos_pos _ _ (RIneq.Rgt_lt _ _ Hɛ) RIneq.pos_half_prf).
        case: (Hsl1 sighalfɛ) ⇒ [HsMaj {}Hs].
        case: (Hs'l1 sighalfɛ) ⇒ [Hs'Maj {}Hs'].
        case: HsN HsN.
        case: Hs'N' Hs'N'.
         (max N N').
        moven Hn ⇒ /=.
        unfold minus.
        apply RIneq.Rle_lt_trans with (BInt_sf μ ((s n) - (s' n))%sf).
            apply norm_Bint_sf_le.
        rewrite (BInt_sf_LInt_SF).
        rewrite <-LInt_p_SFp_eq.
            all : swap 1 2.
            unfold sum_Rbar_nonneg.nonnegx /=.
            rewrite fun_sf_norm.
            apply norm_ge_0.
        assert ( x : X, Rbar_le (( s n - s' n )%fn x) ((( f - s n ) + ( f - s' n ))%fn x)).
            movex; simpl.
            unfold fun_norm, fun_plus, fun_scal.
            replace (s n x) with ((s n x) + zero)%hy at 1.
                2 : rewrite plus_zero_r ⇒ //.
            replace zero with (opp (f x) + f x)%hy at 1.
                2 : apply: plus_opp_l.
            rewrite plus_assoc.
            setoid_rewrite plus_comm at 3.
            setoid_rewrite <-norm_opp at 2.
            rewrite opp_plus; setoid_rewrite scal_opp_one at 2.
            rewrite opp_opp; rewrite <-plus_assoc.
            apply norm_triangle.

        pose Ineq := (LInt_p_monotone μ ( s n - s' n )%fn (( f - s n ) + ( f - s' n ))%fn H);
            clearbody Ineq.
        replace ɛ with (real ɛ).
            2 : easy.
        rewrite <-Rbar_lt_finite_eq_rlt.
            3 : easy.
        rewrite (LInt_p_ext _ _ (λ x : X, ( s n - s' n )%fn x)).
            2 : unfold fun_norm.
            2 : setoid_rewrite fun_sf_norm.
            2 : setoid_rewrite fun_sf_plus ⇒ //.
        apply (Rbar_le_lt_trans _ _ (Finite ɛ) Ineq).
        unfold fun_plus at 1.
        rewrite (LInt_p_ext _ _ (λ x : X, Rbar_plus (( f - s n )%fn x) (( f - s' n )%fn x)%hy)).
            2 : by [].
        rewrite LInt_p_plus.
            2, 3 : split.
            2, 4 : unfold sum_Rbar_nonneg.nonnegx.
            2, 3 : unfold fun_norm; apply norm_ge_0.
        replace ɛ with (real (Rbar_plus×/2) (ɛ×/2))).
        clear H Ineq.
        simpl in HsN, Hs'N'.
        rewrite Raxioms.Rplus_0_l in Hs'N'.
        rewrite Raxioms.Rplus_0_l in HsN.
        apply (Rbar_plus_lt_compat (LInt_p μ (λ x : X, ( f - s n )%fn x)) (ɛ×/2)
                                    (LInt_p μ (λ x : X, ( f - s' n )%fn x)) (ɛ×/2)).
            apply HsN; apply Nat.max_lub_l with N' ⇒ //.
            rewrite (LInt_p_ext _ _ (λ x : X, ( f' - s' n )%fn x)).
            apply Hs'N'; apply Nat.max_lub_r with N ⇒ //.
            movex; unfold fun_norm, fun_plus.
            rewrite Ext ⇒ //.
            simpl; rewrite Rlimit.eps2 ⇒ //.
        all : swap 1 3.
        movex; rewrite fun_sf_scal.
            rewrite scal_opp_one; unfold fun_plus, fun_scal.
            rewrite scal_opp_one ⇒ //.
        all : swap 1 3.
        pose Lint_p_Bint_sf :=
            @Finite_BInt_sf_LInt_SF _ _ μ ( s n - s' n )%sf.
            rewrite <-LInt_p_SFp_eq in Lint_p_Bint_sf.
            2 : unfold sum_Rbar_nonneg.nonnegx.
            2 : simpl; rewrite fun_sf_norm.
            2 : apply norm_ge_0.
            rewrite <-Lint_p_Bint_sf ⇒ //.

        all : swap 1 3.
        assert
            ( x : X, is_lim_seq (fun k ⇒ ( s k - s' n )%fn x) (( f - s' n )%fn x)) as Limseqnorm.
            movex; unfold fun_norm.
            apply lim_seq_norm.
            apply lim_seq_plus.
            apply Hspw.
            apply lim_seq_cte.
        apply measurable_fun_ext with (fun x : X ⇒ (Lim_seq_Rbar (λ k : nat, ( s k - s' n )%fn x))).
            movex; rewrite <-Lim_seq_eq.
            apply is_lim_seq_unique.
            unfold Lim_seq.is_lim_seq.
            unfold Rbar_locally ⇒ /=.
            apply: Limseqnorm.
        apply measurable_fun_Lim_seq_Rbar.
        movek; split.
        unfold sum_Rbar_nonneg.nonnegx; apply norm_ge_0.
        apply measurable_fun_R_Rbar.

        apply: (measurable_fun_composition _ open).
        apply measurable_fun_ext with (s k - s' n)%sf.
            movex.
            rewrite fun_sf_plus fun_sf_scal ⇒ //.
        apply (measurable_fun_sf (s k - s' n)%sf).
        moveP; move /sigma_algebra_R_Rbar.measurable_R_equiv_oo.
        apply measurable_fun_continuous.
        apply filterlim_norm.

        assert
            ( x : X, is_lim_seq (fun k ⇒ ( s k - s n )%fn x) (( f - s n )%fn x)) as Limseqnorm.
            movex; unfold fun_norm.
            apply lim_seq_norm.
            apply lim_seq_plus.
            apply Hspw.
            apply lim_seq_cte.
        apply measurable_fun_ext with (fun x : X ⇒ (Lim_seq_Rbar (λ k : nat, ( s k - s n )%fn x))).
            movex; rewrite <-Lim_seq_eq.
            apply is_lim_seq_unique.
            unfold Lim_seq.is_lim_seq.
            unfold Rbar_locally ⇒ /=.
            apply: Limseqnorm.
        apply measurable_fun_Lim_seq_Rbar.
        movek; split.
        unfold sum_Rbar_nonneg.nonnegx; apply norm_ge_0.
        apply measurable_fun_R_Rbar.

        apply: (measurable_fun_composition _ open).
        apply measurable_fun_ext with (s k - s n)%sf.
            movex.
            rewrite fun_sf_plus fun_sf_scal ⇒ //.
        apply (measurable_fun_sf (s k - s n)%sf).
        moveP; move /sigma_algebra_R_Rbar.measurable_R_equiv_oo.
        apply measurable_fun_continuous.
        apply filterlim_norm.

        1, 2 : apply integrable_sf_norm, integrable_sf_plus.
        2, 4 : apply integrable_sf_scal.
        1, 4 : apply ints.
        1, 2 : apply ints'.
    Qed.

    Lemma BInt_BInt_sf {s : simpl_fun E gen} :
         π : integrable_sf μ s,
        BInt_sf μ s = BInt (Bif_integrable_sf π).
    Proof.
        move ⇒ π; unfold BInt; simpl.
        symmetry; apply: lim_seq_eq.
        apply lim_seq_cte.
    Qed.

End BInt_prop.

Section BInt_indic.

    Context {X : Set}.
    Context {E : CompleteNormedModule R_AbsRing}.
    Context {gen : (X Prop) Prop}.
    Context {μ : measure gen}.

    Lemma BInt_indic :
         P : X Prop, π : measurable gen P, π' : is_finite (μ P),
            BInt (Bif_integrable_sf (integrable_sf_indic π π')) = μ P.
    Proof.
        moveP π π'.
        rewrite <-BInt_BInt_sf.
        apply BInt_sf_indic.
    Qed.

End BInt_indic.

Section BInt_op.

    Context {X : Set}.
    Context {E : CompleteNormedModule R_AbsRing}.
    Context {gen : (X Prop) Prop}.
    Context {μ : measure gen}.

    Open Scope hy_scope.
    Open Scope Bif_scope.

    Lemma BInt_plus {f g : X E} :
         (bf : Bif μ f) (bg : Bif μ g),
            BInt (Bif_plus bf bg) = ((BInt bf) + (BInt bg))%hy.
    Proof.
        movebf bg;
        case_eq bfsf isf Hfpw Hfl1 eqbf;
        case_eq bgsg isg Hgpw Hgl1 eqbg;
        rewrite <-eqbf, <-eqbg.
        unfold BInt.
        apply lim_seq_eq.
        apply (lim_seq_ext (fun n : natBInt_sf μ (sf n) + BInt_sf μ (sg n))%hy).
            moven.
            rewrite eqbf eqbg ⇒ /=.
            rewrite BInt_sf_plus ⇒ //.
            apply: lim_seq_plus.
            pose H := is_lim_seq_BInt (mk_Bif f sf isf Hfpw Hfl1);
                clearbody H; simpl in H; rewrite <-eqbf in H.
            assumption.
            pose H := is_lim_seq_BInt (mk_Bif g sg isg Hgpw Hgl1);
                clearbody H; simpl in H; rewrite <-eqbg in H.
            assumption.
    Qed.

    Lemma BInt_scal {f : X E} :
         (bf : Bif μ f), (a : R_AbsRing),
            BInt (Bif_scal a bf) = (a (BInt bf))%hy.
    Proof.
        movebf a.
        case: bfsf isf Hfpw Hfl1.
        apply lim_seq_eq.
        apply (lim_seq_ext (fun n : nata (BInt_sf μ (sf n)))%hy).
            moven; rewrite BInt_sf_scal ⇒ //.
            apply: lim_seq_scal_r.
            pose H := is_lim_seq_BInt (mk_Bif f sf isf Hfpw Hfl1);
                clearbody H; simpl in H.
            assumption.
    Qed.

    Lemma norm_BInt_le {f : X E} :
         (bf : Bif μ f),
             BInt bf %hy BInt (bf)%Bif.
    Proof.
        movebf.
        case: bfsf isf Hfpw Hfl1.
        suff: (Rbar_le ( lim_seq (λ n : nat, BInt_sf μ (sf n)) )%hy (lim_seq (λ n : nat, BInt_sf μ ( sf n )%sf)))
            by simpl ⇒ //.
        apply is_lim_seq_le with (λ n : nat, BInt_sf μ (sf n) )%hy (λ n : nat, BInt_sf μ ( sf n %sf)).
            moven; apply norm_Bint_sf_le.
            apply lim_seq_norm.
            pose H := is_lim_seq_BInt (mk_Bif f sf isf Hfpw Hfl1);
                clearbody H; simpl in H.
            assumption.
            pose H := is_lim_seq_BInt (Bif_norm (mk_Bif f sf isf Hfpw Hfl1));
                clearbody H; simpl in H.
            assumption.
    Qed.

End BInt_op.

Section BInt_linearity.

    Context {X : Set}.
    Context {E : CompleteNormedModule R_AbsRing}.
    Context {gen : (X Prop) Prop}.
    Context {μ : measure gen}.

    Open Scope hy_scope.
    Open Scope Bif_scope.

    Lemma BInt_linearity {f g : X E} :
         (bf : Bif μ f) (bg : Bif μ g), a b : R,
            BInt (a bf + b bg)
            = (a (BInt bf) + (b (BInt bg)))%hy.
    Proof.
        movebf bg a b.
        rewrite BInt_plus.
        do 2 rewrite BInt_scal ⇒ //.
    Qed.

    Lemma BInt_zero {f : X E} :
         (bf : Bif μ f),
            ( x : X, bf x = zero) BInt bf = zero.
    Proof.
        movebf Hbf.
        rewrite (BInt_ext bf (Bif_zero)).
        unfold Bif_zero.
        rewrite <-BInt_BInt_sf.
        unfold BInt_sf ⇒ /=.
        rewrite sum_O.
        rewrite scal_zero_r ⇒ //.
        unfold fun_Bif in Hbf.
        movex; rewrite Hbf ⇒ //.
    Qed.

    Lemma BInt_minus {f g : X E} :
         bf : Bif μ f, bg : Bif μ g,
            BInt (bf - bg)%Bif = ((BInt bf) - (BInt bg))%hy.
    Proof.
        movebf bg.
        rewrite BInt_plus BInt_scal.
        rewrite scal_opp_one ⇒ //.
    Qed.

    Lemma BInt_opp {f : X E} :
         bf : Bif μ f,
            (BInt (- bf)) = (- (BInt bf))%hy.
    Proof.
        movebf.
        rewrite BInt_scal scal_opp_one ⇒ //.
    Qed.

End BInt_linearity.