Library Lebesgue.Bochner.BInt_sf

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 Bochner integral of simple 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_wDep.

Require Import
    square_bij
    hierarchy_notations
    simpl_fun
.

Open Scope hy_scope.

Section BInt_for_sf.

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

    Open Scope R_scope.

    Definition BInt_sf (μ : measure gen) (sf : simpl_fun _ gen) : E :=
        sum_n
            (fun nscal (real (μ (nth_carrier sf n))) (sf.(val) n))
            (sf.(max_which)).

End BInt_for_sf.

Notation "'∫B_sf' sf 'd' μ" := (BInt_sf μ sf)
        (only printing, at level 45, format "'[ ' '∫B_sf' sf 'd' μ ']'") : sf_scope.

Section BInt_sf_indic.

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

    Open Scope R_scope.
    Open Scope fun_scope.

    Lemma BInt_sf_indic (P : X Prop) (π_meas : measurable gen P)
        : BInt_sf μ (sf_indic gen P π_meas) = real (μ P).
    Proof.
        unfold BInt_sf.
        replace (max_which (sf_indic gen P π_meas)) with 1%nat at 1
            by unfold sf_indic ⇒ //.
        rewrite sum_Sn sum_O.
        case_eq (sf_indic gen P π_meas) ⇒ wP vP maxP axP1 axP2 axP3 EqP;
            unfold nth_carrier; rewrite <-EqP ⇒ /=.
        rewrite (measure_ext gen μ _ P).
            all : swap 1 2.
            movex; case: (in_dec P x) ⇒ //.
        rewrite scal_zero_r plus_zero_r.
        unfold scal ⇒ /=.
        unfold mult ⇒ /=.
        rewrite RIneq.Rmult_1_r ⇒ //.
    Qed.

End BInt_sf_indic.

Open Scope nat_scope.

Lemma sum_n_m_scal_r {A : Ring} {E : ModuleSpace A} :
     a : nat A, u : E, n m : nat,
        sum_n_m (fun k : natscal (a k) u) n m = scal (sum_n_m (fun k : nat ⇒ (a k)) n m) u.
Proof.
    movea u n.
    induction nm.
        induction m.
        do 2 rewrite sum_n_n ⇒ //.
        rewrite sum_n_Sm. 2 : lia.
        rewrite sum_n_Sm. 2 : lia.
        rewrite scal_distr_r.
        rewrite IHm ⇒ //.
    case_eq (n <=? m).
        move /Nat.leb_leHnm.
        pose IHnm := IHn m; clearbody IHnm.
        rewrite sum_Sn_m in IHnm. 2 : lia.
        rewrite [in RHS]sum_Sn_m in IHnm. 2 : lia.
        rewrite scal_distr_r in IHnm.
        apply (plus_reg_l (scal (a n) u)) ⇒ //.
        move /Nat.leb_gtHmn.
        rewrite sum_n_m_zero. 2 : lia.
        rewrite sum_n_m_zero. 2 : lia.
        rewrite scal_zero_l ⇒ //.
Qed.

Lemma sum_n_scal_r {A : Ring} {E : ModuleSpace A} :
     a : nat A, u : E, n m : nat,
        sum_n (fun k : natscal (a k) u) n = scal (sum_n (fun k : nat ⇒ (a k)) n) u.
Proof.
    unfold sum_na u n m.
    apply sum_n_m_scal_r.
Qed.

Lemma sum_n_sum_Rbar :
     u : nat Rbar, n : nat, ( k : nat, k n is_finite (u k))
     sum_n (fun kreal (u k)) n = real (sum_Rbar n u).
Proof.
    induction n.
        rewrite sum_O.
        unfold sum_Rbar ⇒ //.
        moveHu.
        rewrite sum_Sn.
        rewrite IHn.
            all : swap 1 2.
            movek Hkn.
            assert (k S n) by lia.
        apply Hu ⇒ //; clear Hu.
        assert (S n S n) by lia.
        pose Le0uSn := Hu (S n) H; clearbody Le0uSn; clear H.
        assert ( k : nat, k n is_finite (u k)).
            movek Hk.
            assert (k S n) by lia.
            apply Hu ⇒ //.
        pose Le0sum := finite_sum_Rbar u n H; clearbody Le0sum; clear H.
        simpl; rewrite Rbar_plus_comm.
        unfold Rbar_plus, Rbar_plus'.
        unfold is_finite in Le0sum, Le0uSn.
        rewrite <-Le0uSn, <-Le0sum ⇒ //.
Qed.

Section BInt_sf_plus.

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

    Open Scope R_scope.
    Open Scope nat_scope.
    Open Scope sf_scope.

    Lemma BInt_sf_plus {sf_f sf_g : simpl_fun E gen} :
        integrable_sf μ sf_f integrable_sf μ sf_g
            BInt_sf μ (sf_f + sf_g) = ((BInt_sf μ sf_f) + (BInt_sf μ sf_g))%hy.
    Proof.
        unfold integrable_sfaxf4 axg4.
        case_eq sf_fwf vf maxf axf1 axf2 axf3 Eqf.
        case_eq sf_gwg vg maxg axg1 axg2 axg3 Eqg.
        rewrite Eqf Eqg in axf4 axg4; simpl in axf4, axg4.
        rewrite <-Eqf, <- Eqg.
        unfold BInt_sf.
        replace (max_which sf_f) with maxf by rewrite Eqf ⇒ //.
        replace (max_which sf_g) with maxg by rewrite Eqg ⇒ //.
        replace (max_which (sf_f + sf_g)) with ((S maxf) × (S maxg) - 1)%nat.
            2 : rewrite Eqf Eqg ⇒ //.
        unfold nth_carrier.
        rewrite square_bij_sum.
        pose valfg := val (sf_f + sf_g).
            fold valfg.
            assert (valfg = simpl_fun.val (sf_f + sf_g))
                as Eqval by unfold valfg ⇒ //.
            clearbody valfg; rewrite Eqf Eqg in Eqval; simpl in Eqval.
            rewrite Eqval; clear Eqval valfg.
        pose whichfg := which (sf_f + sf_g).
            fold whichfg.
            assert (whichfg = which (sf_f + sf_g))
                as Eqwhich by unfold whichfg ⇒ //.
            clearbody whichfg; rewrite Eqf Eqg in Eqwhich; simpl in Eqwhich.
            rewrite Eqwhich; clear Eqwhich whichfg.
        assert
            ( k1 k2 : nat, k2 maxg
                (μ
                    (λ x : X,
                        square_bij (S maxg) (wf x, wg x) =
                        square_bij (S maxg) (k1, k2))
                ) =
                (μ
                    (λ x : X,
                        wf x = k1 wg x = k2
                    )
                )
            ) as Eqμ.
            movek1 k2 Hk2.
            apply measure_extx; split.
                moveEqwfk.
                assert
                    (square_bij_inv (S maxg)
                        (square_bij (S maxg) (wf x, wg x))
                    =
                    square_bij_inv (S maxg)
                        (square_bij (S maxg) (k1, k2))
                    ) as Eqaux by congruence.
                rewrite is_bij_square in Eqaux.
                    2 : apply axg2.
                rewrite is_bij_square in Eqaux.
                    2 : assumption.
                split; congruence.
                case ⇒ → → //.
        assert
            ( k1 k2 : nat, k2 maxg
                (let (nf, ng) :=
                    square_bij_inv (S maxg) (square_bij (S maxg) (k1, k2)) in
                    plus (vf nf) (vg ng))
                = plus (vf k1) (vg k2)
            ) as Eqsum.
            movek1 k2 Hk2.
            rewrite is_bij_square.
                2 : assumption.
            reflexivity.
        assert
            ( k1 k2 : nat, k2 maxg
                scal
                    (real (μ
                    (λ x : X,
                        square_bij (S maxg) (wf x, wg x) =
                        square_bij (S maxg) (k1, k2))))
                    (let (nf, ng) :=
                    square_bij_inv (S maxg) (square_bij (S maxg) (k1, k2)) in
                    plus (vf nf) (vg ng))
                =
                scal
                    (real (μ (λ x : X, wf x = k1 wg x = k2)))
                    (plus (vf k1) (vg k2))
            ) as Eqsum1.
            movek1 k2 Hk2.
            rewrite Eqsum. 2 : assumption.
            rewrite Eqμ. 2 : assumption.
            reflexivity.
        clear Eqsum Eqμ.
        assert
            ( k1 : nat,
                sum_n
                    (λ k2 : nat,
                        scal
                            (real (μ
                            (λ x : X,
                                square_bij (S maxg) (wf x, wg x) =
                                square_bij (S maxg) (k1, k2))))
                            (let (nf, ng) :=
                            square_bij_inv (S maxg) (square_bij (S maxg) (k1, k2)) in
                            plus (vf nf) (vg ng))
                    ) maxg
                =
                sum_n
                    (λ k2 : nat,
                        scal
                            (real (μ (λ x : X, wf x = k1 wg x = k2)))
                            (plus (vf k1) (vg k2))
                    ) maxg
            ) as Eqsum.
            movek1.
            apply sum_n_ext_lock2 Hk2.
            apply Eqsum1 ⇒ //.
        assert
            (sum_n
            (λ k1 : nat,
                sum_n
                    (λ k2 : nat,
                        scal
                        (real (μ
                            (λ x : X,
                            square_bij (S maxg) (wf x, wg x) =
                            square_bij (S maxg) (k1, k2))))
                        (let (nf, ng) :=
                            square_bij_inv (S maxg) (square_bij (S maxg) (k1, k2)) in
                            plus (vf nf) (vg ng))
                    ) maxg
                ) maxf
            =
            sum_n
            (λ k1 : nat,
                sum_n
                    (λ k2 : nat,
                        scal
                        (real (μ (λ x : X, wf x = k1 wg x = k2)))
                        (plus (vf k1) (vg k2))
                    ) maxg
                ) maxf
            ) as Rwrt
            by apply sum_n_ext ⇒ //.
        rewrite Rwrt; clear Rwrt Eqsum Eqsum1.
        assert
            ( k1 : nat,
                sum_n
                    (λ k2 : nat,
                        scal
                        (real (μ (λ x : X, wf x = k1 wg x = k2)))
                        (plus (vf k1) (vg k2))
                ) maxg
                =
                sum_n
                    (λ k2 : nat,
                        plus
                            (scal
                            (real (μ (λ x : X, wf x = k1 wg x = k2)))
                            (vf k1))
                            (scal
                            (real (μ (λ x : X, wf x = k1 wg x = k2)))
                            (vg k2))
                ) maxg
            ) as Eqsum.
            movek1.
            apply sum_n_ext_lock2 Hk2.
            rewrite scal_distr_l ⇒ //.
        assert
            (sum_n
                (λ k1 : nat,
                sum_n
                    (λ k2 : nat,
                        scal
                        (real (μ (λ x : X, wf x = k1 wg x = k2)))
                        (plus (vf k1) (vg k2))
                ) maxg
            ) maxf
            =
            sum_n
                (λ k1 : nat,
                sum_n
                    (λ k2 : nat,
                        plus
                            (scal
                            (real (μ (λ x : X, wf x = k1 wg x = k2)))
                            (vf k1))
                            (scal
                            (real (μ (λ x : X, wf x = k1 wg x = k2)))
                            (vg k2))
                ) maxg
            ) maxf
            ) as Rwrt
            by apply sum_n_ext ⇒ //.
        rewrite Rwrt; clear Rwrt Eqsum.
        assert
            ( k1 : nat,
                sum_n
                    (λ k2 : nat,
                        plus
                            (scal
                            (real (μ (λ x : X, wf x = k1 wg x = k2)))
                            (vf k1))
                            (scal
                            (real (μ (λ x : X, wf x = k1 wg x = k2)))
                            (vg k2))
                ) maxg
                =
                plus
                    (sum_n
                        (λ k2 : nat,
                            scal
                            (real (μ (λ x : X, wf x = k1 wg x = k2)))
                            (vf k1)
                    ) maxg)
                    (sum_n
                        (λ k2 : nat,
                            scal
                            (real (μ (λ x : X, wf x = k1 wg x = k2)))
                            (vg k2)
                    ) maxg)
            ) as Eqsum.
            movek1.
            apply sum_n_plus.
        assert
            (sum_n
                (λ k1 : nat,
                sum_n
                    (λ k2 : nat,
                        plus
                            (scal
                            (real (μ (λ x : X, wf x = k1 wg x = k2)))
                            (vf k1))
                            (scal
                            (real (μ (λ x : X, wf x = k1 wg x = k2)))
                            (vg k2))
                ) maxg
            ) maxf
            =
            plus
                (sum_n
                    (λ k1 : nat,
                    sum_n
                        (λ k2 : nat,
                            scal
                            (real (μ (λ x : X, wf x = k1 wg x = k2)))
                            (vf k1)
                    ) maxg
                ) maxf)
                (sum_n
                    (λ k1 : nat,
                    sum_n
                        (λ k2 : nat,
                            scal
                            (real (μ (λ x : X, wf x = k1 wg x = k2)))
                            (vg k2)
                    ) maxg
                ) maxf)
            ) as Rwrt.
            rewrite <-sum_n_plus.
            apply sum_n_ext_lock1 //.
        rewrite Rwrt.
        clear Rwrt Eqsum.
        setoid_rewrite sum_n_switch at 2.
        assert
            (sum_n
                (λ j : nat,
                sum_n (λ i : nat, scal (real (μ (λ x : X, wf x = i wg x = j))) (vg j))
            maxf) maxg
            =
            sum_n
                (λ k2 : nat,
                scal
                    (sum_n (λ k1 : nat, (real (μ (λ x : X, wf x = k1 wg x = k2))))
                    maxf)
                    (vg k2)
            ) maxg
            ) as Eqsum.
            apply sum_n_extn.
            rewrite sum_n_scal_r ⇒ //.
        rewrite Eqsum; clear Eqsum.
        assert
            (sum_n
                (λ k1 : nat,
                sum_n (λ k2 : nat, scal (real (μ (λ x : X, wf x = k1 wg x = k2))) (vf k1))
            maxg) maxf
            =
            sum_n
                (λ k1 : nat,
                scal
                    (sum_n (λ k2 : nat, (real (μ (λ x : X, wf x = k1 wg x = k2))))
                    maxg)
                    (vf k1)
            ) maxf
            ) as Eqsum.
            apply sum_n_extn.
            rewrite sum_n_scal_r ⇒ //.
        rewrite Eqsum; clear Eqsum.
        assert
            ( k1 k2 : nat, k1 maxf k2 maxg
                measurable gen (λ x : X, wf x = k1 wg x = k2)
            ) as measurable_inter_fg.
                movek1 k2 Hk1 Hk2.
                apply measurable_inter.
                1, 2 : apply [axf3, axg3] ⇒ //.
        congr plus; apply sum_n_ext_loc.
            replace (val sf_f) with vf by rewrite Eqf ⇒ //.
            movek1 Hk1.
            case (ifflr (Nat.lt_eq_cases k1 maxf)) ⇒ //.
                moveHk1'.
                replace (which sf_f) with wf by rewrite Eqf ⇒ //.
                rewrite sum_n_sum_Rbar.
                    all : swap 1 2.
                    movek2 Hk2.
                    assert
                        (Rbar_le
                            (μ (λ x : X, wf x = k1 wg x = k2))
                            (μ (λ x : X, wf x = k1))
                        ) as inter_le_f.
                        apply measure_le.
                        apply measurable_inter_fg ⇒ //.
                        apply axf3 ⇒ //.
                        easy.
                    pose fin_μ_f := axf4 k1 Hk1'; clearbody fin_μ_f.
                    unfold is_finite in fin_μ_f; rewrite <-fin_μ_f in inter_le_f.
                    unfold real in inter_le_f.
                    unfold is_finite, real.
                    case_eq (μ (λ x : X, wf x = k1 wg x = k2)) ⇒ //.
                        moveAbs_μ; apply False_ind.
                        rewrite Abs_μ in inter_le_f ⇒ //.
                        moveAbs_μ; apply False_ind.
                        pose Ge0μ := meas_nonneg gen μ (λ x : X, wf x = k1 wg x = k2); clearbody Ge0μ.
                        rewrite Abs_μ in Ge0μ ⇒ //.
                    rewrite (measure_decomp_finite gen μ (fun (x : X) ⇒ wf x = k1) maxg (fun k2 ⇒ (fun (x : X) ⇒ wg x = k2))) ⇒ //.
                        apply axf3 ⇒ //.
                        movex; (wg x); split ⇒ //.
                        moven p x _ _ → //.
                move ⇒ →.
                rewrite axf1; do 2 rewrite scal_zero_r ⇒ //.
            replace (val sf_g) with vg by rewrite Eqg ⇒ //.
            movek2 Hk2.
            case (ifflr (Nat.lt_eq_cases k2 maxg)) ⇒ //.
                moveHk2'.
                replace (which sf_g) with wg by rewrite Eqg ⇒ //.
                rewrite sum_n_sum_Rbar.
                    all : swap 1 2.
                    movek1 Hk1.
                    assert
                        (Rbar_le
                            (μ (λ x : X, wf x = k1 wg x = k2))
                            (μ (λ x : X, wg x = k2))
                        ) as inter_le_g.
                        apply measure_le.
                        apply measurable_inter_fg ⇒ //.
                        apply axg3 ⇒ //.
                        easy.
                    pose fin_μ_g := axg4 k2 Hk2'; clearbody fin_μ_g.
                    unfold is_finite in fin_μ_g; rewrite <-fin_μ_g in inter_le_g.
                    unfold real in inter_le_g.
                    unfold is_finite, real.
                    case_eq (μ (λ x : X, wf x = k1 wg x = k2)) ⇒ //.
                        moveAbs_μ; apply False_ind.
                        rewrite Abs_μ in inter_le_g ⇒ //.
                        moveAbs_μ; apply False_ind.
                        pose Ge0μ := meas_nonneg gen μ (λ x : X, wf x = k1 wg x = k2); clearbody Ge0μ.
                        rewrite Abs_μ in Ge0μ ⇒ //.
                    rewrite (measure_decomp_finite gen μ (fun (x : X) ⇒ wg x = k2) maxf (fun k1 ⇒ (fun (x : X) ⇒ wf x = k1))) ⇒ //.
                        rewrite (sum_Rbar_ext maxf (λ n : nat, μ (λ x : X, wg x = k2 wf x = n)) (λ k : nat, μ (λ x : X, wf x = k wg x = k2))).
                        all : swap 1 2.
                        movei Hi.
                        apply measure_extx.
                        split; case ⇒ //.
                        reflexivity.
                        apply axg3 ⇒ //.
                        movex; (wf x); split ⇒ //.
                        moven p x _ _ → //.
                move ⇒ →.
                rewrite axg1; do 2 rewrite scal_zero_r ⇒ //.
    Qed.

End BInt_sf_plus.

Section BInt_sf_scal.

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

    Open Scope R_scope.
    Open Scope nat_scope.
    Open Scope sf_scope.

    Lemma BInt_sf_scal :
         a : R_AbsRing, sf : simpl_fun E gen,
            BInt_sf μ (a sf) = (a (BInt_sf μ sf))%hy.
    Proof.
        movea sf.
        unfold BInt_sf.
        case_eq sfwf vf maxf axf1 axf2 axf3 Eqsf; rewrite <-Eqsf.
        rewrite <-sum_n_scal_l.
        replace (max_which (a sf)) with (max_which sf)
            by rewrite Eqsf ⇒ //.
        apply sum_n_extk.
        unfold nth_carrier.
        replace (which (a sf)) with (which sf)
            by rewrite Eqsf ⇒ //.
        replace (val (a sf) k) with (scal a (val sf k))
            by rewrite Eqsf ⇒ //.
        do 2 rewrite scal_assoc.
        replace mult with Rmult by easy.
        rewrite Raxioms.Rmult_comm.
        replace (@mult R_AbsRing) with Rmult by easy.
        reflexivity.
    Qed.

End BInt_sf_scal.

Section BInt_sf_linearity.

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

    Open Scope R_scope.
    Open Scope nat_scope.
    Open Scope sf_scope.

    Lemma BInt_sf_lin {sf sg : simpl_fun E gen} :
         a b : R_AbsRing, integrable_sf μ sf integrable_sf μ sg
            BInt_sf μ (a sf + b sg)
            = ((a (BInt_sf μ sf)) + (b (BInt_sf μ sg)))%hy.
    Proof.
        movea b isf isg.
        do 2 rewrite <-BInt_sf_scal.
        rewrite BInt_sf_plus ⇒ //.
        1, 2 : apply integrable_sf_scal ⇒ //.
    Qed.

End BInt_sf_linearity.

Lemma norm_scal_eq {E : NormedModule R_AbsRing} :
     r : R, x : E, r x = | r | x .
Proof.
    movea x.
    apply RIneq.Rle_antisym.
        unfold scal at 2 ⇒ /=.
        exact (norm_scal a x).
        case (RIneq.Req_dec a 0).
            move ⇒ →.
            rewrite abs_zero; do 2 rewrite scal_zero_l; rewrite norm_zero.
            apply RIneq.Rle_refl.
        moveaNeq0.
        apply RIneq.Rmult_le_reg_l with (|/a|)%R.
        apply Rabs_pos_lt.
        apply RIneq.Rinv_neq_0_compat ⇒ //.
        replace ((| / a |) × ((| a |) ( x )))%R
            with ((| / a |) ((| a |) ( x )))%hy
            by unfold scal at 1 ⇒ //.
        rewrite scal_assoc.
        unfold abs at 1 2 ⇒ /=.
        rewrite <-Rabs_mult.
        rewrite <-RIneq.Rinv_l_sym.
        unfold scal at 1 ⇒ /=.
        unfold mult ⇒ /=.
        rewrite (Rabs_right _ (RIneq.Rle_ge _ _ RIneq.Rle_0_1)).
        rewrite Raxioms.Rmult_1_l.
        replace x with (/a (a x)) at 1.
            3 : assumption.
            2 : rewrite scal_assoc.
            2 : rewrite <-RIneq.Rinv_l_sym ⇒ //.
            2 : rewrite scal_one ⇒ //.
        apply (norm_scal (/a) (ax)).
Qed.

Section BInt_sf_norm.

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

    Open Scope R_scope.
    Open Scope nat_scope.
    Open Scope sf_scope.

    Lemma norm_Bint_sf_le :
         sf : simpl_fun E gen,
            ( BInt_sf μ sf %hy BInt_sf μ ( sf ))%R.
    Proof.
        movesf;
            case_eq sfvf wf maxf axf1 axf2 axf3 Eqf;
            rewrite <-Eqf.
        unfold BInt_sf.
        replace (max_which sf) with maxf by rewrite Eqf ⇒ //.
        replace (max_which ( sf )) with maxf at 1 by rewrite Eqf ⇒ //.
        rewrite (sum_n_ext_loc _ ((λ n : nat, | real (μ (nth_carrier sf n)) | ( val sf n )%hy)))%hy.
            all : swap 1 2.
            rewrite Eqf ⇒ /=.
            unfold abs ⇒ /= n Hn.
            case: (ifflr (Nat.lt_eq_cases n maxf)) ⇒ // Hn'; clear Hn.
            rewrite Rabs_pos_eq ⇒ //.
            unfold nth_carrier ⇒ /=.
            pose Le0μn := meas_nonneg _ μ (λ x : X, vf x = n); clearbody Le0μn.
            case_eq (μ (λ x : X, vf x = n)).
                mover Eqr; rewrite Eqr in Le0μn ⇒ //.
                move_; simpl; apply RIneq.Rle_refl.
                moveAbs; rewrite Abs in Le0μn ⇒ //.
            setoid_rewrite Hn' at 2 4.
            replace (wf maxf) with (@zero E) at 2 3.
            rewrite norm_zero; do 2 rewrite scal_zero_r ⇒ //.
        rewrite (sum_n_ext _ (λ n : nat, (real (μ (nth_carrier sf n))) (val sf n) )%hy).
            all : swap 1 2.
            moven.
            rewrite norm_scal_eq ⇒ //.
        apply: norm_sum_n_m.
    Qed.

End BInt_sf_norm.

Section BInt_well_defined.

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

    Lemma BInt_sf_zero :
         sf : simpl_fun E gen,
            ( x : X, fun_sf sf x = zero)
             BInt_sf μ sf = zero.
    Proof.
        movesf.
        case_eq sfwf vf maxf axf1 axf2 axf3 Eqf; rewrite <-Eqf.
        unfold fun_sfHf.
        unfold BInt_sf.
        rewrite (sum_n_ext_loc _ (fun (n : nat) ⇒ zero)).
            induction max_which.
                rewrite sum_O ⇒ //.
                rewrite sum_Sn plus_zero_r; apply IHn.
        moven Hn.
        unfold nth_carrier.
        replace (which sf) with wf by rewrite Eqf ⇒ //.
        replace (max_which sf) with maxf in Hn
            by rewrite Eqf ⇒ //.
        case: (ifflr (Nat.lt_eq_cases n maxf)) ⇒ // Hn'.
            pose Le0μn := meas_nonneg _ μ (λ x : X, wf x = n); clearbody Le0μn.
            case: (Rbar_le_cases _ Le0μn).
                move ⇒ →.
                rewrite scal_zero_l ⇒ //.
                case.
                    caser [Lt0r Eqr].
                    assert (Rbar_lt 0%R (μ (λ x : X, wf x = n))) as Lt0μn.
                        rewrite Eqr.
                        unfold Rbar_lt ⇒ //.
                    case: (measure_gt_0_exists _ _ _ Lt0μn) ⇒ x <-.
                    replace (which sf) with wf in Hf by rewrite Eqf ⇒ //.
                    rewrite Hf scal_zero_r ⇒ //.
                    move ⇒ → /=; rewrite scal_zero_l ⇒ //.
            replace (val sf) with vf by rewrite Eqf ⇒ //.
            rewrite Hn'.
            rewrite axf1 scal_zero_r ⇒ //.
    Qed.

    Lemma BInt_sf_ext {sf sf' : simpl_fun E gen} :
        integrable_sf μ sf integrable_sf μ sf'
            ( x : X, fun_sf sf x = fun_sf sf' x)
            BInt_sf μ sf = BInt_sf μ sf'.
    Proof.
        moveisf isf' Hsfsf'.
        pose δ := (sf + (opp one) sf')%sf.
        assert ( x : X, fun_sf δ x = zero) as δNul.
            movex; unfold δ.
            rewrite fun_sf_plus fun_sf_scal.
            rewrite scal_opp_l scal_one.
            rewrite <-Hsfsf'; rewrite plus_opp_r ⇒ //.
            assert ((BInt_sf μ sf) + (opp one) (BInt_sf μ sf') = (BInt_sf μ sf') + (opp one) (BInt_sf μ sf'))%hy as Subgoal.
                rewrite <-BInt_sf_scal at 1.
                rewrite <-BInt_sf_plus at 1.
                fold δ; rewrite BInt_sf_zero.
                rewrite scal_opp_l scal_one plus_opp_r ⇒ //.
                assumption.
            3 : apply plus_reg_r with ((opp one) (BInt_sf μ sf'))%hy ⇒ //.
            2 : apply integrable_sf_scal.
            1, 2 : assumption.
    Qed.

End BInt_well_defined.