Library Lebesgue.Bochner.B_spaces

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 Bochner spaces.

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
    hierarchy_notations
    topology_compl
    simpl_fun
    Bi_fun
    BInt_Bif
    BInt_LInt_p
.

Section ae_eq_prop.

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

    Open Scope Bif_scope.

    Lemma BInt_ae_zero {f : X E} {bf : Bif μ f} :
        ae_eq μ bf (fun _zero)
            BInt bf = zero.
    Proof.
        pose NZ := (fun xbf x zero).
        assert (measurable gen NZ) as π.
        apply (measurable_Bif bf (fun xx zero)).
        apply measurable_gen.
        apply NM_open_neq.
        unfold ae_eq, ae_rel.
        moveHae0.
        apply: norm_eq_zero.
        suff: (( BInt bf )%hy 0).
        moveLe.
        apply RIneq.Rle_le_eq.
        split ⇒ //.
        apply norm_ge_0.
        apply RIneq.Rle_trans with (BInt (bf)).
        apply norm_BInt_le.
        assert (μ (λ x : X, bf x zero) = Finite 0%R) as negNZ.
        case Hae0A [Hle [HMA HμA]].
        suff: (Rbar_le (μ (λ x : X, bf x zero)) 0).
            moveHLe.
            apply Rbar_le_antisym ⇒ //.
            apply meas_nonneg.
            apply Rbar_le_trans with (μ A).
            apply measure_le ⇒ //.
            rewrite HμA; apply Rbar_le_refl.
        assert (is_finite (μ (λ x : X, bf x zero))) as π'.
        rewrite negNZ ⇒ //.
        rewrite BInt_LInt_p_eq; swap 1 2.
        movex; rewrite Bif_fn_norm; apply norm_ge_0.
        assert (ae μ (λ x : X, bf x = zero)).
        apply ae_ext with (λ x : X, bf x = zero) ⇒ //.
        movex; rewrite Bif_fn_norm; split.
        move ⇒ ->; rewrite norm_zero ⇒ //.
        move ⇒ /norm_eq_zero//.
        suff: (LInt_p μ (λ x : X, (‖ bf ‖) x) = 0).
        move ->; apply RIneq.Rle_refl.
        apply LInt_p_ae_definite.
        split.
        movex; rewrite Bif_fn_norm; apply norm_ge_0.
        apply measurable_fun_R_Rbar.
        apply measurable_fun_ext with (fun x bf x %hy).
        movex; rewrite Bif_fn_norm //.
        apply measurable_fun_composition with open.
        apply measurable_Bif.
        suff: measurable_fun open open (@norm _ E).
        moveHmeas P /measurable_R_equiv_oo/Hmeas//.
        apply measurable_fun_continuous.
        movex.
        apply filterlim_norm.
        unfold ae_eq, ae_rel.
        unfold zero in H; simpl in H.
        unfold ae, negligible in ×.
        case: HA [HA1 [HA2 HA3]].
         A; repeat split ⇒ //.
        movex Hx.
        apply HA1Abs.
        rewrite Abs in Hx ⇒ //.
    Qed.

End ae_eq_prop.

Section ae_eq_prop2.

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

    Open Scope Bif_scope.

    Lemma BInt_ae_eq {f f' : X E} :
         bf : Bif μ f, bf' : Bif μ f',
        ae_eq μ f f' BInt bf = BInt bf'.
    Proof.
        movebf bf' H.
        suff: (BInt (bf + (opp one) bf') = zero).
        rewrite BInt_plus BInt_scal.
        moveHzero.
        apply plus_reg_r with (opp one (BInt bf'))%hy.
        rewrite Hzero.
        rewrite -BInt_scal -BInt_plus.
        rewrite BInt_zero ⇒ //.
        movex.
        rewrite Bif_fn_plus Bif_fn_scal.
        rewrite scal_opp_one plus_opp_r ⇒ //.
        apply: norm_eq_zero.
        suff: (( BInt (bf + opp one bf')%Bif )%hy 0).
        moveLe.
        assert (0 ( BInt (bf + opp one bf')%Bif )%hy) as Ge.
        apply norm_ge_0.
        apply RIneq.Rle_le_eq ⇒ //.
        apply RIneq.Rle_trans with (BInt ( bf + opp one bf' )%Bif).
        apply norm_BInt_le.
        suff: (BInt ( bf + opp one bf' ) = 0).
        move ⇒ ->; apply RIneq.Rle_refl.
        rewrite BInt_ae_zero ⇒ //.
        unfold ae_eq, ae_rel in ×.
        apply ae_ext with (fun xbf x = bf' x) ⇒ //.
        movex; rewrite Bif_fn_norm Bif_fn_plus Bif_fn_scal scal_opp_one; split.
        move ->; rewrite plus_opp_r norm_zero ⇒ //.
        move ⇒ /norm_eq_zero.
        moveHz; apply plus_reg_r with (- bf' x)%hy.
        rewrite Hz plus_opp_r ⇒ //.
    Qed.

    Lemma BInt_ae_eq_norm1_zero {f : X E} {bf : Bif μ f} :
        ae_eq μ bf (fun _zero)
            BInt (bf) = zero.
    Proof.
        moveH.
        apply BInt_ae_zero.
        unfold ae_eq, ae_rel in ×.
        apply ae_ext with (λ x : X, bf x = zero).
        movex; rewrite Bif_fn_norm; split.
            move ⇒ ->; rewrite norm_zero ⇒ //.
            move ⇒ /norm_eq_zero//.
        assumption.
    Qed.

    Lemma BInt_norm1_zero_ae_eq {f f' : X E} {bf : Bif μ f} {bf' : Bif μ f'} :
        BInt (bf) = 0 ae_eq μ bf (fun _zero).
    Proof.
        pose NZ := (fun xbf x zero).
        assert (measurable gen NZ) as π.
        apply (measurable_Bif bf (fun xx zero)).
        apply measurable_gen.
        apply NM_open_neq.
        unfold ae_eq, ae_rel.
        moveHInt0.
        apply ae_ext with (fun x bf x = 0).
        movex; rewrite Bif_fn_norm; split.
            move ⇒ /norm_eq_zero//.
            move ⇒ ->; rewrite norm_zero //.
        suff: (ae_eq μ (bf) (λ _ : X, 0)).
        unfold ae_eq, ae_rel ⇒ //.
        assert (sum_Rbar_nonneg.nonneg (λ x : X, (‖ bf ‖) x)) as H_0.
            movex; rewrite Bif_fn_norm; apply norm_ge_0.
        assert (measurable_fun_Rbar gen (λ x : X, (‖ bf ‖) x)) as H_1.
        apply measurable_fun_R_Rbar.
        apply measurable_fun_ext with (fun x bf x %hy).
        movex; rewrite Bif_fn_norm //.
        apply measurable_fun_composition with open.
        apply measurable_Bif.
        suff: measurable_fun open open (@norm _ E).
        moveHmeas P /measurable_R_equiv_oo/Hmeas//.
        apply measurable_fun_continuous.
        movex.
        apply filterlim_norm.
        assert (H : Mplus gen (λ x, bf x)).
            split ⇒ //.
        clear H_0 H_1.
        case: (LInt_p_ae_definite μ (bf : X R) H) ⇒ _ HypLInt_p.
        unfold ae_eq, ae_rel in HypLInt_p |- ×.
        move: HInt0.
        rewrite BInt_LInt_p_eq; swap 1 2.
        movex; rewrite Bif_fn_norm; apply norm_ge_0.
        rewrite <-is_finite_LInt_p_Bif in HypLInt_p; swap 1 2.
        movex; rewrite Bif_fn_norm; apply norm_ge_0.
        simplH'.
        assert (@eq Rbar
                (Finite
                (real
                (@LInt_p X gen μ
                (fun x : X
                Finite
                (@fun_Bif X R_NormedModule gen μ
                (@fun_norm X R_AbsRing
                (CompleteNormedModule.NormedModule R_AbsRing E) f)
                (@Bif_norm X E gen μ f bf) x)))))
                (Finite (IZR Z0))) as Hstrange.
        congr Finite ⇒ //.
        move: Hstrange ⇒ /HypLInt_p GoalStrange.
        clear HypLInt_p.
        unfold ae, ae_rel, negligible in ×.
        case: GoalStrangeA [HA1 [HA2 HA3]].
         A; repeat split ⇒ //.
        movex NH.
        apply HA1Abs.
        apply NH.
        suff: Finite ((‖ bf ‖) x) = Finite 0 ⇒ //.
        congruence.
    Qed.

End ae_eq_prop2.

Section B_space_def.

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

    Definition in_B_space (μ : measure gen) (p : posreal) (f : X E) :=
        Datatypes.prod (strongly_measurable gen f) (is_finite (LInt_p μ (f ^ p)%fn) inhabited X).

    Lemma Bif_norm_power (μ : measure gen) (p : posreal) (f : X E)
        : in_B_space μ p f Bif μ (f^p)%fn.
    Proof.
        moveHf.
        apply: strongly_measurable_integrable_Bif.
        assert ( x : X, 0 ( f )%fn x) as normf_pos.
        movex; unfold fun_norm; apply norm_ge_0.
        case: Hf ⇒ /strongly_measurable_norm/(strongly_measurable_power p).
        moveHf _; apply Hf ⇒ //.
        case: Hf_ [Hf _].
        rewrite (LInt_p_ext _ _ (λ x : X, (( f ) ^ p)%fn x)) ⇒ //.
        movex; unfold fun_norm, fun_power.
        unfold norm at 1 ⇒ /=.
        unfold abs at 1 ⇒ /=.
        rewrite Rabs_pos_eq ⇒ //.
        apply R_compl.Rpow_nonneg, norm_ge_0.
    Qed.

    Definition semi_norm_p (μ : measure gen) (p : posreal) {f : X E} (inBf : in_B_space μ p f) :=
        BInt (Bif_norm_power μ p f inBf).


End B_space_def.