Library Lebesgue.Bochner.simpl_fun

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 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
    Rmax_n
    topology_compl
.

Declare Scope sf_scope.
Delimit Scope sf_scope with sf.

Declare Scope fun_scope.
Delimit Scope fun_scope with fn.

Open Scope hy_scope.
Open Scope fun_scope.
Open Scope sf_scope.

Section simpl_fun_def.

    Context {X : Set}.
    Context {A : AbsRing}.
    Context {E : ModuleSpace A}.

    Definition indic (P : X Prop) : X A :=
        fun x
            match (in_dec P x) return A with
                | left _one
                | right _zero
            end.

    Open Scope core_scope.
    Open Scope type_scope.
    Open Scope nat_scope.

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

    Record simpl_fun := mk_simpl_fun {
        which : X nat;
        val : nat E;
        max_which : nat;

        ax_val_max_which :
            val max_which = zero;
        ax_which_max_which :
             x : X, which x max_which;
        ax_measurable :
             n : nat, n max_which
                measurable gen (fun xwhich x = n);
    }.

    Definition integrable_sf (sf : simpl_fun) :=
         n : nat, n < max_which sf
            is_finite (μ (fun xwhich sf x = n)).

    Definition nth_carrier (sf : simpl_fun) (n : nat) : (X Prop) :=
        (fun xsf.(which) x = n).

    Definition fun_sf (sf : simpl_fun) : X E :=
        fun xsf.(val) (sf.(which) x).

    Coercion fun_sf : simpl_fun >-> Funclass.

    Definition is_simpl (f : X E) :=
         sf : simpl_fun, x : X, sf x = f x.

End simpl_fun_def.

Arguments simpl_fun {X A} E gen.
Arguments is_simpl {X A} [E] gen f.
Arguments integrable_sf {X A} [E] {gen} μ sf.

Notation "'χ(' P ')'" := (indic P) (at level 0) : fun_scope.

Section simpl_fun_indic.

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

    Open Scope nat_scope.
    Open Scope R_scope.

    Definition sf_indic (P : X Prop) :
        measurable gen P simpl_fun R_ModuleSpace gen.
        movePmeas.
        pose w := fun x
            match (in_dec P x) return nat with
                | left _O
                | right _ ⇒ (S O)
            end.
        pose v := fun n
            match n return R with
                | O ⇒ 1
                | _ ⇒ 0
            end.
        pose max_w := (S O).
        apply (mk_simpl_fun w v max_w).
            unfold max_w ⇒ //.
            movex; unfold w, max_w.
            case: (in_dec P x); lia.
            unfold max_w; case.
                move_.
                apply measurable_ext with P.
                unfold wx.
                case: (in_dec P x) ⇒ //.
                exact Pmeas.
            moven Hn.
            assert (S n = 1%nat) by lia.
            rewrite H; clear Hn H; clear n.
            apply measurable_ext with (fun x¬ P x).
            unfold wx.
            case: (in_dec P x) ⇒ //.
            apply measurable_compl.
            apply measurable_ext with (fun xP x).
            movex; split; case: (in_dec P x).
                move_; auto.
                auto.
                auto.
                moveNPx NNPx; apply False_ind.
                exact (NNPx NPx).
            exact Pmeas.
    Defined.

    Lemma sf_indic_alt :
         P : X Prop, measurable gen P
             is_simpl gen (χ(P): X R).
    Proof.
        moveP Pmeas.
         (sf_indic P Pmeas) ⇒ x.
        unfold fun_sf, "χ( _ )" ⇒ /=.
        case: (in_dec P x) ⇒ //.
    Qed.

    Context (μ : measure gen).

    Lemma integrable_sf_indic (P : X Prop) (π : measurable gen P) :
        is_finite (μ P) integrable_sf μ (sf_indic P π).
    Proof.
        movePfin n Hn; simpl in ×.
            assert (n = O) by lia.
            rewrite H; clear H Hn; clear n.
            rewrite <-(measure_ext gen _ P).
            exact Pfin.
            movex.
            case (in_dec P x) ⇒ //.
    Qed.

End simpl_fun_indic.

Arguments integrable_sf_indic {X gen μ P} π.

Section sf_zero_fun.

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

    Context {A : AbsRing}.
    Context {E : NormedModule A}.

    Definition sf_zero : simpl_fun E gen.
        pose whichz := fun _ : XO.
        pose valz := fun _ : natzero : E.
        apply (mk_simpl_fun whichz valz 0).
        unfold valz ⇒ //.
        unfold whichz ⇒ //.
        moven /(Nat.le_0_r) →.
        unfold whichz; apply measurable_Prop.
    Defined.

    Lemma sf_zero_zero : x : X, sf_zero x = zero.
    Proof.
       by [].
    Qed.

    Context (μ : measure gen).

    Lemma integrable_sf_zero :
        integrable_sf μ sf_zero.
    Proof.
        unfold integrable_sf ⇒ /=.
        lia.
    Qed.

End sf_zero_fun.

Section simpl_fun_norm.

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

    Open Scope R_scope.
    Open Scope nat_scope.

    Definition fun_norm (f : X E) :=
        fun xnorm (f x).

    Notation "‖ f ‖" := (fun_norm f) (at level 100) : fun_scope.

    Definition sf_norm (sf : simpl_fun E gen) : simpl_fun R_ModuleSpace gen.
        case: sfwhich val max_which ax1 ax2 ax3.
        pose nval :=
            fun nnorm (val n).
        apply (mk_simpl_fun which nval max_which).
            unfold nval; rewrite ax1.
            apply norm_zero; assumption.
            exact ax2.
            exact ax3.
    Defined.

    Context {μ : measure gen}.

    Lemma integrable_sf_norm {sf : simpl_fun E gen} (isf : integrable_sf μ sf) :
        integrable_sf μ (sf_norm sf).
    Proof.
        unfold integrable_sf in ×.
        case_eq sfwf vf mawf axf1 axf2 axf3 Eqf ⇒ /=.
        rewrite Eqf in isf; simpl in isf ⇒ //.
    Qed.

    Notation "‖ sf ‖" := (sf_norm sf) (at level 100) : sf_scope.

    Lemma sf_norm_alt :
         f : X E, is_simpl gen f
            is_simpl gen (fun_norm f).
    Proof.
        movef.
        casesf. case_eq sfwhich val max_which ax1 ax2 ax3 Eqsf Eqf.
         (sf_norm sf).
        rewrite Eqsf.
        movex; unfold fun_sf, sf_norm ⇒ /=.
        simpl in Eqf.
        rewrite Eqf ⇒ //.
    Qed.

    Lemma fun_sf_norm :
         sf : simpl_fun E gen,
            (∀ x : X, fun_sf (sf) x = ( fun_sf sf x )%hy).
    Proof.
        movesf.
        case_eq sfwf vf maxf axf1 axf2 axf3 Eqf; rewrite <-Eqf ⇒ /=.
        unfold fun_sf.
        rewrite Eqf ⇒ //.
    Qed.

End simpl_fun_norm.

Notation "‖ f ‖" := (fun_norm f) (at level 100) : fun_scope.
Notation "‖ sf ‖" := (sf_norm sf) (at level 100) : sf_scope.

Section simpl_fun_power.

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

    Definition fun_power (f : X R_NormedModule) (p : posreal) :=
        (fun xRpow (f x) p.(pos)).

    Definition sf_power (sf : simpl_fun R_NormedModule gen) (p : RIneq.posreal) : simpl_fun R_NormedModule gen.
    case: sfwhich val max_which ax1 ax2 ax3.
    pose nval :=
        fun nRpow (val n) p.(pos).
    apply (mk_simpl_fun which nval max_which).
        unfold nval; rewrite ax1.
        rewrite Rpow_0_alt ⇒ //.
        case p ⇒ //.
        exact ax2.
        exact ax3.
    Defined.

    Notation "sf ^ p" := (sf_power sf p).

    Lemma fun_sf_power :
         sf : simpl_fun R_NormedModule gen, p : RIneq.posreal,
            (∀ x : X, fun_sf (sf ^ p) x = (Rpow (fun_sf sf x) p)).
    Proof.
        movesf.
        case_eq sfwf vf maxf axf1 axf2 axf3 Eqf; rewrite <-Eqf ⇒ /=.
        unfold fun_sf.
        rewrite Eqf ⇒ //.
    Qed.

    Context {μ : measure gen}.

    Lemma integrable_sf_power {sf : simpl_fun R_NormedModule gen} (p : RIneq.posreal) (isf : integrable_sf μ sf) :
        integrable_sf μ (sf ^ p).
    Proof.
        unfold integrable_sf in ×.
        case_eq sfwf vf mawf axf1 axf2 axf3 Eqf ⇒ /=.
        rewrite Eqf in isf; simpl in isf ⇒ //.
    Qed.

End simpl_fun_power.

Notation "f ^ p" := (fun_power f p) : fun_scope.
Notation "sf '^' p" := (sf_power sf p) : sf_scope.

Section simpl_fun_plus.

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

    Open Scope nat_scope.

    Definition fun_plus (f : X E) (g : X E) :=
        (fun xplus (f x) (g x)).

    Notation "f + g" := (fun_plus f g) (left associativity, at level 50) : fun_scope.

    Definition sf_plus (sf sg : simpl_fun E gen) : simpl_fun E gen.
        case: sfwf vf maxf axf1 axf2 axf3.
        case: sgwg vg maxg axg1 axg2 axg3.
        pose val := fun m
            let (nf, ng) := square_bij_inv (S maxg) m in
            plus (vf nf) (vg ng).
        pose max_which := (S maxf) × (S maxg) - 1.
        pose which := fun (x : X) ⇒
            let nf := wf x in
            let ng := wg x in
            square_bij (S maxg) (nf, ng).
        apply (mk_simpl_fun which val max_which).
            unfold val, max_which.
            rewrite (square_bij_inv_corner maxg maxf).
            rewrite axf1 axg1 plus_zero_r; reflexivity.
            movex; unfold which, max_which.
            apply confined_square.
            split; apply [axf2, axg2].
            assert
                ( n : nat, n max_which
                 c : nat × nat, c = square_bij_inv (S maxg) n
                 nf ng : nat, (nf, ng) = c
                    measurable gen (λ x : X, wf x = nf wg x = ng)
                ) as measurable_inter_fg.
                moven Hn c Eqc nf ng Hnfngc.
                pose Hnfng := confined_square_inv maxg maxf n Hn; clearbody Hnfng ⇒ /=.
                rewrite <-Eqc, <-Hnfngc in Hnfng.
                case: HnfngHnf Hng.
                apply measurable_inter.
                apply axf3 ⇒ //.
                apply axg3 ⇒ //.
            moven Hn; unfold which.
            pose c := square_bij_inv (S maxg) n.
            case_eq c ⇒ [nf ng] Eqc.
            apply measurable_ext with (fun xwf x = nf wg x = ng).
            movex.
            assert (n = square_bij (S maxg) c) as Eqn.
                rewrite is_bij_square_inv ⇒ //.
            rewrite Eqn Eqc.
            split.
                case ⇒ → → //.
                moveEqwn.
                assert (square_bij_inv (S maxg) (square_bij (S maxg) (wf x, wg x)) = square_bij_inv (S maxg) (square_bij (S maxg) (nf, ng)))
                    by congruence.
                rewrite is_bij_square in H.
                    2 : apply axg2.
                rewrite is_bij_square in H.
                    all : swap 1 2.
                    pose Hng := confined_snd_square_inv maxg n.
                    fold c in Hng; clearbody Hng; rewrite Eqc in Hng.
                    exact Hng.
                split; congruence.
                apply measurable_inter_fg with n c ⇒ //.
    Defined.

    Notation "sf + sg" := (sf_plus sf sg) (left associativity, at level 50) : sf_scope.

    Lemma sf_plus_alt :
         f g : X E,
        is_simpl gen f is_simpl gen g
        is_simpl gen (fun_plus f g).
    Proof.
        movef g.
        casesf Eq_sf_f; casesg Eq_sg_g.
         (sf_plus sf sg).
        case_eq sfwf vf maxf axf1 axf2 axf3 Eqf.
        case_eq sgwg vg maxg axg1 axg2 axg3 Eqg.
        unfold fun_sf ⇒ /= x.
        rewrite is_bij_square.
            2 : apply axg2.
        unfold fun_plus.
        congr plus.
            unfold fun_sf in Eq_sf_f.
            rewrite Eqf in Eq_sf_f; simpl in Eq_sf_f.
            rewrite Eq_sf_f ⇒ //.
            unfold fun_sf in Eq_sg_g.
            rewrite Eqg in Eq_sg_g; simpl in Eq_sg_g.
            rewrite Eq_sg_g ⇒ //.
    Qed.

    Lemma fun_sf_plus :
         sf sg : simpl_fun E gen,
            (∀ x : X, fun_sf (sf + sg)%sf x = (fun_sf sf x + fun_sf sg x)%hy).
    Proof.
        movesf sg.
        case_eq sfwf vf maxf axf1 axf2 axf3 Eqf; rewrite <-Eqf ⇒ /=.
        case_eq sgwg vg maxg axg1 axg2 axg3 Eqg; rewrite <-Eqg ⇒ /=.
        unfold fun_sf.
        rewrite Eqf Eqgx /=.
        rewrite is_bij_square ⇒ //.
    Qed.

    Context {μ : measure gen}.

    Lemma integrable_sf_plus {sf sg : simpl_fun E gen} :
        (integrable_sf μ sf) (integrable_sf μ sg) (integrable_sf μ (sf_plus sf sg)).
    Proof.
        unfold integrable_sf.
        moveaxf4 axg4.
        case_eq sfwf vf maxf axf1 axf2 axf3 Eqf.
        case_eq sgwg vg maxg axg1 axg2 axg3 Eqg ⇒ /=.
        rewrite Eqf Eqg in axf4 axg4; simpl in axf4, axg4.
        pose max_which := (S maxf) × (S maxg) - 1.
        assert
            ( n : nat, n max_which
             c : nat × nat, c = square_bij_inv (S maxg) n
             nf ng : nat, (nf, ng) = c
                measurable gen (λ x : X, wf x = nf wg x = ng)
            ) as measurable_inter_fg.
            moven Hn c Eqc nf ng Hnfngc.
            pose Hnfng := confined_square_inv maxg maxf n Hn; clearbody Hnfng ⇒ /=.
            rewrite <-Eqc, <-Hnfngc in Hnfng.
            case: HnfngHnf Hng.
            apply measurable_inter.
            apply axf3 ⇒ //.
            apply axg3 ⇒ //.
    moven Hn; unfold which.
    pose c := square_bij_inv (S maxg) n.
    case_eq c ⇒ [nf ng] Eqc.
    assert (
         x : Rbar, Rbar_le (@zero R_AbelianGroup) x Rbar_lt x p_infty
            is_finite x
    ) as Rbar_pos_lt_finite.
        movex; case: x ⇒ //.
    apply Rbar_pos_lt_finite.
    apply meas_nonneg.
    assert (n = square_bij (S maxg) c).
        unfold c; rewrite is_bij_square_inv ⇒ //.
    rewrite H Eqc.
    replace
        (μ (λ x : X, square_bij (S maxg) (wf x, wg x) = square_bij (S maxg) (nf, ng)))
        with
        (μ (λ x : X, wf x = nf wg x = ng)).
        all : swap 1 2.
        apply measure_extx; split.
            move ⇒ [-> ->] ⇒ //.
            moveEqfg.
            assert
                (square_bij_inv (S maxg) (square_bij (S maxg) (wf x, wg x)) = square_bij_inv (S maxg) (square_bij (S maxg) (nf, ng)))
                as Eqfg2 by congruence.
            rewrite is_bij_square in Eqfg2.
                2 : apply axg2.
            rewrite is_bij_square in Eqfg2.
                all : swap 1 2.
                pose Hng := confined_snd_square_inv maxg n.
                fold c in Hng; clearbody Hng; rewrite Eqc in Hng.
                exact Hng.
            split; congruence.
        assert
            (n max_which)
            as Le_n_mw.
            apply Nat.lt_le_incl ⇒ //.
        pose Hnfng := confined_square_inv maxg maxf n Le_n_mw; clearbody Hnfng.
        fold c in Hnfng; rewrite Eqc in Hnfng; case: HnfngHnf Hng.
        assert
            (Rbar_le
                (μ (λ x : X, wf x = nf wg x = ng))
                (μ (λ x : X, wf x = nf))
            ) as inter_le_f.
            apply measure_le.
            apply measurable_inter_fg with n c ⇒ //.
            apply axf3 ⇒ //.
            easy.
        assert
        (Rbar_le
            (μ (λ x : X, wf x = nf wg x = ng))
            (μ (λ x : X, wg x = ng))
        ) as inter_le_g.
            apply measure_le.
            apply measurable_inter_fg with n c ⇒ //.
            apply axg3 ⇒ //.
            easy.
        case: (le_lt_v_eq nf maxf) ⇒ // Hnf'.
            assert
                (is_finite (μ (λ x : X, wf x = nf)))
                as fin_f.

                apply axf4 ⇒ //.
            assert
                (Rbar_lt (μ (λ x : X, wf x = nf)) p_infty) as fin_f'.
                unfold is_finite, real in fin_f.
                rewrite <-fin_f ⇒ //.
            apply (Rbar_le_lt_trans _ _ _ inter_le_f fin_f').
            assert (ng < maxg).
                apply not_leHng'.
                assert (ng = maxg)
                    as Eqgng by apply Nat.le_antisymm ⇒ //.
                rewrite Hnf' Eqgng in Eqc.
                rewrite Eqc in H; rewrite square_bij_corner in H.
                rewrite H in Hn; unfold max_which in Hn.
                exact (Nat.Private_Tac.lt_irrefl Hn).
            assert
                (is_finite (μ (λ x : X, wg x = ng)))
                as fin_g.
                apply axg4 ⇒ //.
            assert
                (Rbar_lt (μ (λ x : X, wg x = ng)) p_infty) as fin_g'.
                unfold is_finite, real in fin_g.
                rewrite <-fin_g ⇒ //.
            apply (Rbar_le_lt_trans _ _ _ inter_le_g fin_g').
    Qed.

End simpl_fun_plus.

Notation "f + g" := (fun_plus f g) (left associativity, at level 50) : fun_scope.
Notation "sf + sg" := (sf_plus sf sg) (left associativity, at level 50) : sf_scope.

Section simpl_fun_scal.

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

    Open Scope nat_scope.

    Definition fun_scal (a : A) (g : X E) :=
        (fun xscal a (g x)).

    Notation "a ⋅ g" := (fun_scal a g) (left associativity, at level 45) : fun_scope.

    Definition sf_scal (a : A) (sf : simpl_fun E gen) : simpl_fun E gen.
        case: sfwf vf maxf axf1 axf2 axf3.
        pose val := fun kscal a (vf k).
        apply (mk_simpl_fun wf val maxf).
            unfold val; rewrite axf1 scal_zero_r ⇒ //.
            exact axf2.
            exact axf3.
    Defined.

    Notation "a ⋅ sf" := (sf_scal a sf) (left associativity, at level 45) : sf_scope.

    Lemma sf_scal_alt :
         a : A, f : X E,
        is_simpl gen f
        is_simpl gen (fun_scal a f).
    Proof.
        movea f.
        casesf; case_eq sfwf vf maxf axf1 axf2 axf3 Eqsf ⇒ /= Eqf.
         (sf_scal a sf) ⇒ x.
        unfold fun_sf, val, which; rewrite Eqsf ⇒ /=.
        unfold fun_scal; rewrite Eqf ⇒ //.
    Qed.

    Lemma fun_sf_scal :
         a : A, sf : simpl_fun E gen,
            (∀ x : X, fun_sf (a sf) x = (a (fun_sf sf x))%hy).
    Proof.
        movea sf.
        case_eq sfwf vf maxf axf1 axf2 axf3 Eqf; rewrite <-Eqf ⇒ /=.
        unfold fun_sf.
        rewrite Eqf ⇒ //.
    Qed.

    Context {μ : measure gen}.

    Lemma integrable_sf_scal (a : A) {sf : simpl_fun E gen} :
        integrable_sf μ sf integrable_sf μ (sf_scal a sf).
    Proof.
        unfold integrable_sf.
        case: sf ⇒ //.
    Qed.

End simpl_fun_scal.

Notation "a ⋅ g" := (fun_scal a g) (left associativity, at level 45) : fun_scope.
Notation "a ⋅ sf" := (sf_scal a sf) (left associativity, at level 45) : sf_scope.
Notation "- g" := (fun_scal (opp one) g) : fun_scope.
Notation "- sg" := (sf_scal (opp one) sg) : sf_scope.
Notation "f - g" := (fun_plus f (- g))%fn : fun_scope.
Notation "sf - sg" := (sf_plus sf (- sg)) : sf_scope.

Section simpl_fun_bounded.

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

    Open Scope hy_scope.

    Definition sf_bounded :
         sf : simpl_fun E gen, { M : R | ( x : X, fun_sf sf x M) 0 M }.
        movesf.
        apply exist with (Rbasic_fun.Rmax 0 (Rmax_n (fun k val sf k ) (max_which sf))).
        split.
        movex; unfold fun_sf.
        pose Hwx := ax_which_max_which sf x; clearbody Hwx.
        apply Rle_trans with (2:=Rbasic_fun.Rmax_r _ _).
        apply: fo_le_Rmax_n ⇒ //.
        apply Rbasic_fun.Rmax_l.
    Qed.

End simpl_fun_bounded.

Open Scope R_scope.
Open Scope nat_scope.

Lemma finite_sum_Rbar :
     u : nat Rbar, n : nat, ( k : nat, k n is_finite (u k))
     is_finite (sum_Rbar n u).
Proof.
    moveu; induction nHu.
        unfold sum_Rbar.
        assert (0 0) by lia.
        apply Hu ⇒ //.
        simpl.
        assert (S n S n) by lia.
        pose HuSn := (Hu (S n) H); clearbody HuSn.
        assert ( k : nat, k n is_finite (u k)).
            movek Hk.
            assert (k S n) by lia.
            apply Hu ⇒ //.
        pose Hsum := IHn H0; clearbody Hsum; clear H0.
        unfold is_finite in HuSn, Hsum |- ×.
        rewrite <-HuSn, <-Hsum ⇒ //.
Qed.

Section simpl_fun_meas.

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

    Lemma measurable_sf_preim :
         sf : simpl_fun E gen, y : E,
            measurable gen (fun x : Xsf x = y).
    Proof.
        movesf.
        case_eq sfwf vf maxf axf1 axf2 axf3 Eqf; rewrite <-Eqf ⇒ /=.
        movey.
        pose P := fun k ⇒ (λ x : X, vf k = y which sf x = k).
        apply measurable_ext with (λ x : X, k : nat, k maxf P k x).
            movex; split.
                casek; caseHk.
                unfold P; case ⇒ <-; unfold fun_sf ⇒ →.
                rewrite Eqf ⇒ /=; split; auto with arith.
                moveEq_sfx_vfn.
                 (which sf x); split.
                    replace (which sf x) with (wf x) by rewrite Eqf ⇒ //; apply axf2.
                    unfold P; split.
                    unfold fun_sf in Eq_sfx_vfn.
                    replace (vf (which sf x)) with (val sf (which sf x))
                        by rewrite Eqf ⇒ //.
                    rewrite Eq_sfx_vfn ⇒ //.
                    reflexivity.
                apply measurable_union_finitek Hk.
                unfold P; apply measurable_inter.
        apply measurable_Prop.
        replace (which sf) with (wf) by rewrite Eqf ⇒ //.
        apply axf3 ⇒ //.
    Qed.

    Lemma sf_measurable_preim_le :
         sf : simpl_fun E gen, n : nat, n max_which sf
            measurable gen (λ x : X, which sf x n).
    Proof.
        movesf.
        case_eq sfwf vf maxf axf1 axf2 axf3 Eqf; rewrite <-Eqf ⇒ /=.
        moven Hn.
        pose B := fun k ⇒ (λ x : X, which sf x = k).
        apply measurable_ext with (fun x k : nat, k n which sf x = k).
            movex; split.
                casek [Hk Eqk]; lia.
                moveHsfx; (which sf x); auto.
            apply (measurable_union_finite _ ) ⇒ k Hk.
            apply ax_measurable.
            lia.
    Qed.

    Lemma sf_measurable_preim_lt :
         sf : simpl_fun E gen, n : nat, n max_which sf
            measurable gen (λ x : X, which sf x < n).
    Proof.
        movesf.
        case_eq sfwf vf maxf axf1 axf2 axf3 Eqf; rewrite <-Eqf ⇒ /=.
        case.
            move_.
            apply measurable_ext with (fun _False).
            movex; split ⇒ //.
            lia.
            apply measurable_Prop.

            moven' HSn'.
            apply measurable_ext with (fun xwhich sf x n').
            movex; split; lia.
            apply sf_measurable_preim_le; lia.
    Qed.

    Lemma is_finite_sf_preim_lt {sf : simpl_fun E gen} :
        integrable_sf μ sf n : nat, n max_which sf
            is_finite (μ (λ x : X, which sf x < n)).
    Proof.
        unfold integrable_sfaxf4.
        case_eq sfwf vf maxf axf1 axf2 axf3 Eqf; rewrite <-Eqf ⇒ /=.
        rewrite Eqf in axf4; simpl in axf4.
        case.
            move_.
            rewrite (measure_ext _ _ _ (fun _False)).
            rewrite meas_emptyset ⇒ //.
            lia.
        moven Hn.
        rewrite (measure_ext _ _ _ (λ x : X, which sf x n)); swap 1 2.
            lia.
        pose B := fun k ⇒ (λ x : X, which sf x = k).
        rewrite (measure_decomp_finite _ μ _ maxf B).
        assert (n < maxf) as Ltnmaxf.
        rewrite Eqf in Hn; simpl in Hn.
        lia.
        apply finite_sum_Rbark Hk; unfold B.
        case_eq (k <=? n).
            move ⇒ /Nat.leb_le Hk'.
            rewrite (measure_ext _ _ _ (fun xwhich sf x = k)).
            rewrite Eqf ⇒ /=; apply axf4; lia.
            movex; split; [easy | move ⇒ → //].
            move ⇒ /Nat.leb_gt Hk'.
            rewrite (measure_ext _ _ _ (fun _False)).
            rewrite meas_emptyset ⇒ //.
            movex; split ⇒ //.
            lia.
        apply sf_measurable_preim_le; lia.
        movek Hk; unfold B; apply ax_measurable; rewrite Eqf ⇒ //.
        movex; unfold B; (which sf x); split ⇒ //.
        rewrite Eqf ⇒ /=; apply axf2.

        movep q x Hp Hq; unfold B; move ⇒ → //.
    Qed.

    Lemma sf_decomp_preim_which :
         sf : simpl_fun E gen, y : E,
            (μ (fun x : Xsf x = y))
            = sum_Rbar (max_which sf) (fun k ⇒ (μ (fun x : Xval sf k = y which sf x = k))).
    Proof.
        movesf.
        case_eq sfwf vf maxf axf1 axf2 axf3 Eqf; rewrite <-Eqf ⇒ /=.
        movey.
        pose B := fun k ⇒ (λ x : X, which sf x = k).
            rewrite (measure_decomp_finite _ μ (fun xsf x = y) maxf B).
            unfold B; rewrite Eqf ⇒ /=.
            apply sum_Rbar_extk Hk.
            apply measure_extx; split.
                caseEq_sfx_y Eq_wfx_k.
                split; [rewrite <-Eq_wfx_k | rewrite Eq_wfx_k] ⇒ //.
                caseEq_vfk_y Eq_wfx_k.
                split; [rewrite Eq_wfx_k | ] ⇒ //.
            apply measurable_sf_preim.
            movek Hk.
            unfold B; apply ax_measurable; rewrite Eqf ⇒ //.
            movex; unfold B; (which sf x).
            split; [rewrite Eqf ⇒ /=; apply axf2 | reflexivity].
            movep q x Hp Hq; unfold B ⇒ → //.
    Qed.

    Lemma finite_sf_preim_neq_0 {sf : simpl_fun E gen} :
        integrable_sf μ sf y : E, y zero
            is_finite (μ (fun x : Xsf x = y)).
    Proof.
        unfold integrable_sfaxf4.
        case_eq sfwf vf maxf axf1 axf2 axf3 Eqf; rewrite <-Eqf ⇒ /=.
        rewrite Eqf in axf4; simpl in axf4.
        movey Hy.
        rewrite sf_decomp_preim_which.
        apply finite_sum_Rbark Hk.
        case: (ifflr (Nat.lt_eq_cases k (max_which sf)) Hk) ⇒ Hkmaxf.
            apply Rbar_bounded_is_finite with (real 0%R) (μ (λ x : X, which sf x = k)).
            apply meas_nonneg.
            apply (measure_le _ μ (λ x : X, val sf k = y which sf x = k) (fun xwhich sf x = k)).
            apply measurable_inter.
            apply measurable_Prop.
            1, 2 : rewrite Eqf ⇒ /=; apply axf3; rewrite Eqf in Hk; simpl in Hk ⇒ //.
            movex; case; auto.
            easy.
            rewrite Eqf ⇒ /=; apply axf4.
            rewrite Eqf in Hkmaxf ⇒ //.

            rewrite (measure_ext _ _ _ (fun _False)).
            rewrite meas_emptyset ⇒ //.
            movex; split ⇒ //.
            case; moveAbs _.
            rewrite Hkmaxf in Abs.
            rewrite <-Abs in Hy.
            rewrite Eqf in Hy; simpl in Hy ⇒ //.
    Qed.

    Lemma measurable_fun_sf_aux :
         sf : simpl_fun E gen,
            (∀ P : E Prop, measurable open P measurable gen (fun x : XP (sf x))).
    Proof.
        movesf.
        case_eq sfwf vf maxf axf1 axf2 axf3 Eqf; rewrite <-Eqf ⇒ /=.

        moveP HP.
        pose B := fun (n : nat) ⇒ (fun x : X(which sf x = n) (P (val sf n))).
        apply measurable_ext with (λ x : X, n : nat, n max_which sf B n x).
        movex; split.
            casen [Hn Bnx]; unfold B in Bnx.
            case: Bnx ⇒ [Eqwsfx Pvsfn]; unfold fun_sf.
            rewrite Eqwsfx ⇒ //.
            movePsfx; (which sf x).
            split;
                [apply ax_which_max_which
                | unfold B; split;
                    [reflexivity | assumption]].
        apply measurable_union_finiten Hn.
        apply measurable_inter.
        apply ax_measurable ⇒ //.
        apply measurable_Prop.
    Qed.

    Lemma measurable_fun_sf :
         sf : simpl_fun E gen,
            measurable_fun gen open sf.
    Proof.
        movesf.
        case_eq sfwf vf maxf axf1 axf2 axf3 Eqf; rewrite <-Eqf ⇒ /=.

        moveP HP; inversion HP.
            clear A0 H0.
            apply measurable_fun_sf_aux ⇒ //.

            clear H HP P.
            constructor 2.

            clear H0 A0.
            apply measurable_fun_sf_aux ⇒ //.

            clear H0 HP.
            constructor 4.
            moven; apply measurable_fun_sf_aux ⇒ //.
    Qed.

    Lemma finite_sf_preim_neq_0_alt {sf : simpl_fun E gen} :
        integrable_sf μ sf
            is_finite (μ (fun x : Xsf x zero)).
    Proof.
        unfold integrable_sfaxf4.
        case_eq sfwf vf maxf axf1 axf2 axf3 Eqf; rewrite <-Eqf ⇒ /=.
        rewrite Eqf in axf4; simpl in axf4.
        apply Rbar_bounded_is_finite with 0%R (μ (fun x n : nat, n < max_which sf which sf x = n)).
        apply meas_nonneg.
        apply measure_le.
        apply (measurable_fun_sf sf (fun x : Ex zero)).
        apply measurable_gen.
        apply NM_open_neq.
        apply measurable_union_finite_altn Hn.
        apply ax_measurable; lia.
        movex Neq0.
         (which sf x); split ⇒ //.
        case: (ifflr (Nat.lt_eq_cases _ _) (ax_which_max_which sf x)) ⇒ //.
        moveAbs.
        unfold fun_sf in Neq0.
        rewrite Abs in Neq0.
        rewrite ax_val_max_which in Neq0 ⇒ //.
        easy.
        rewrite (measure_decomp_finite _ μ _ (max_which sf) (fun nfun xwhich sf x = n)).
        apply finite_sum_Rbark Hk.
        case: (ifflr (Nat.lt_eq_cases _ _) Hk) ⇒ Hk'.
        rewrite (measure_ext _ _ _ (λ x : X, which sf x = k)).
        rewrite Eqf in Hk' |- × ⇒ /=; simpl in Hk'.
        apply axf4 ⇒ //.
        movex; split.
        easy.
        move ⇒ →.
        split.
         k ⇒ //.
        reflexivity.
        rewrite Hk'.
        rewrite (measure_ext _ _ _ (fun _False)).
        rewrite meas_emptyset ⇒ //.
        movex; split ⇒ //.
        case; casen; caseHn1 →.
        lia.
        apply measurable_union_finite_alt.
        moven Hn.
        apply ax_measurable; lia.
        moven Hn.
        apply ax_measurable ⇒ //.
        movex.
         (which sf x); split.
        apply ax_which_max_which.
        reflexivity.
        moven p x Hn Hp Eqwn <- //.
    Qed.

End simpl_fun_meas.

Require Import Lra.

Section simpl_fun_nonzero.

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

    Lemma sf_nonzero_ind (sf : simpl_fun E gen) (n : nat) :
        { sf' : simpl_fun E gen
                | ( x : X, sf x = sf' x)
                 (max_which sf' max_which sf)
                 ((max_which sf - max_which sf') n)
                 ( k : nat, k < n - (max_which sf - max_which sf') k < max_which sf' val sf' k zero)
        }.
    Proof.
        induction n.
         sf; repeat split; lia.
        case: IHnsf'n [Ext [Ineqmax IHn]].
        case_eq (n <? max_which sf); swap 1 2.
        move ⇒ /Nat.ltb_ge n_large.
         sf'n; repeat split ⇒ //.
        lia.
        movek Hk1 Hk2;
            apply IHn; lia.
        move ⇒ /Nat.ltb_lt n_small.
        pose m := (n - (max_which sf - max_which sf'n)).
        case: (Hierarchy.eq_dec (val sf'n m) (zero)); swap 1 2.
            moveNotEq0.
             sf'n; repeat split ⇒ //.
            lia.
            movek.
            move ⇒ /Nat.lt_eq_cases; case.
            moveH1 H2.
            apply IHn.
            1, 2 : lia.
            moveH.
            assert (k = m) as Eqkn by lia; clear H.
            rewrite Eqkn.
            move_.
            assumption.

            moveEq0.
            case_eq sf'nwhichn valn maxn axfn1 axfn2 axfn3 Eqsfn.
            pose valSn :=
            (
                fun (k : nat) ⇒
                    if (k <? m) then (valn k)
                    else valn (S k)
            ).
            pose maxSn := maxn - 1.
            pose whichSn :=
            (
                fun (x : X) ⇒
                    if (whichn x =? m) then maxSn
                    else if (m <? whichn x) then (whichn x - 1)
                    else whichn x
            ).
            assert (m maxn - 1) as Lemmaxn.
            replace maxn with (max_which sf'n)
                by rewrite Eqsfn ⇒ //.
            lia.
            assert (0 < maxn) as Lt0maxn.
            replace maxn with (max_which sf'n)
                by rewrite Eqsfn ⇒ //.
            lia.
            assert (valSn maxSn = zero) as axSn1.
            unfold valSn, maxSn.
            assert (maxn - 1 <? m = false).
            apply Nat.leb_gt.
            lia.
            rewrite H; clear H.
            replace (S (maxn - 1)) with maxn by lia.
            assumption.
            assert ( x : X, whichSn x maxSn) as axSn2.
            movex; unfold whichSn, maxSn.
            case: (whichn x =? m) ⇒ //.
            case_eq (m <? whichn x).
            move_.
            assert (whichn x maxn) by apply axfn2.
            lia.
            move ⇒ /Nat.ltb_ge.
            lia.
            assert (max_which sf - maxSn S n) as Ineq2.
            unfold maxSn.
            replace maxn with (max_which sf'n).
            2 : rewrite Eqsfn ⇒ //.
            lia.
            assert ( k : nat,
                k maxSn
                 measurable gen (λ x : X, whichSn x = k)) as axSn3.
            movek Hk; unfold whichSn.
            case: (ifflr (Nat.lt_eq_cases _ _) Hk); swap 1 2.
            move ⇒ →.
            apply measurable_ext with (fun (x : X) ⇒ whichn x = m whichn x = maxn).
            movex; split.
            case.
            move ⇒ /Nat.eqb_eq → //.
            moveHx.
            assert (m <? whichn x = true).
            apply Nat.ltb_lt; lia.
            rewrite H; clear H.
            assert (whichn x =? m = false).
            apply Nat.eqb_neq; lia.
            rewrite H; clear H.
            unfold maxSn; lia.
            case_eq (whichn x =? m).
            move ⇒ /Nat.eqb_eq ->; left ⇒ //.
            move ⇒ /Nat.eqb_neq Hx0.
            case_eq (m <? whichn x).
            move ⇒ /Nat.ltb_lt Hx1.
            unfold maxSnH.
            right; lia.
            move ⇒ /Nat.ltb_ge Hx1.
            lia.
            apply measurable_union.
            apply axfn3.
            lia.
            apply axfn3 ⇒ //.
            moveLtkmaxSn.
            case: (le_lt_dec m k) ⇒ Hkm.
            apply measurable_ext with (fun x : Xwhichn x = S k).
            movex; split.
            moveHx0.
            assert (whichn x =? m = false).
            apply Nat.eqb_neq; lia.
            rewrite H; clear H.
            assert (m <? whichn x = true).
            apply Nat.ltb_lt; lia.
            rewrite H; clear H.
            lia.
            case_eq (whichn x =? m).
            move ⇒ /Nat.eqb_eq; lia.
            move ⇒ /Nat.eqb_neq Hx0.
            case_eq (m <? whichn x).
            move ⇒ /Nat.ltb_lt; lia.
            move ⇒ /Nat.ltb_ge Hx1; lia.
            apply axfn3; lia.
            apply measurable_ext with (fun x : Xwhichn x = k).
            movex; split.
            moveHx0.
            assert (whichn x =? m = false).
            apply Nat.eqb_neq; lia.
            rewrite H; clear H.
            assert (m <? whichn x = false).
            apply Nat.ltb_ge; lia.
            rewrite H; clear H.
            lia.
            case_eq (whichn x =? m).
            move ⇒ /Nat.eqb_eq; lia.
            move ⇒ /Nat.eqb_neq Hx0.
            case_eq (m <? whichn x).
            move ⇒ /Nat.ltb_lt; lia.
            move ⇒ /Nat.ltb_ge Hx1; lia.
            apply axfn3; lia.
            assert (m = S n - (max_which sf - maxSn)) as Eqm.
            unfold maxSn.
            replace maxn with (max_which sf'n).
            2 : rewrite Eqsfn ⇒ //.
            lia.
             (mk_simpl_fun whichSn valSn maxSn axSn1 axSn2 axSn3) ⇒ /=.
            assert (maxSn max_which sf) as Ineq.
            unfold maxSn.
            assert (maxn max_which sf).
            rewrite Eqsfn in Ineqmax; simpl in Ineqmax.
            assumption.
            lia.
            repeat split.
            movex; unfold valSn, whichSn.
            case: (lt_eq_lt_dec (whichn x) m).
            case.
            moveHxm.
            assert (whichn x =? m = false).
            apply Nat.eqb_neq; lia.
            rewrite H; clear H.
            assert (m <? whichn x = false).
            apply Nat.ltb_ge; lia.
            rewrite H; clear H.
            assert (whichn x <? m = true).
            apply Nat.ltb_lt; lia.
            rewrite H; clear H.
            replace (valn (whichn x)) with (sf'n x).
                2 : unfold fun_sf.
                2 : rewrite Eqsfn ⇒ //.
            apply Ext.
            moveHxm.
            assert (whichn x =? m = true).
            apply Nat.eqb_eq; lia.
            rewrite H; clear H.
            assert (maxSn <? m = false).
            apply Nat.ltb_ge; lia.
            rewrite H; clear H.
            replace (S maxSn) with maxn by lia.
            rewrite Ext.
            unfold fun_sf.
            rewrite Eqsfn ⇒ /=.
            rewrite Hxm.
            rewrite Eqsfn in Eq0; simpl in Eq0.
            rewrite axfn1 Eq0 ⇒ //.
            moveHxm.
            assert (whichn x =? m = false).
            apply Nat.eqb_neq; lia.
            rewrite H; clear H.
            assert (m <? whichn x = true).
            apply Nat.ltb_lt; lia.
            rewrite H; clear H.
            assert (whichn x - 1 <? m = false).
            apply Nat.ltb_ge; lia.
            rewrite H; clear H.
            replace (S (whichn x - 1)) with (whichn x) by lia.
            replace (valn (whichn x)) with (sf'n x).
            2 : unfold fun_sf.
            2 : rewrite Eqsfn ⇒ //.
            apply Ext.
            assumption.
            assumption.
            movek Hk1 Hk2.
            replace (match max_which sf - maxSn with
            | 0 ⇒ S n
            | S ln - l
            end) with ((S n) - (max_which sf - maxSn)) in Hk1.
            2 : case: (max_which sf - maxSn) ⇒ //.
            case: (ifflr (Nat.lt_eq_cases _ _) Hk1).
            moveHkn.
            case: IHnIHn1 IHn2.
            rewrite Eqsfn in IHn2; simpl in IHn2.
            unfold valSn, m.
            rewrite Eqsfn ⇒ /=.
            assert (k < n - (max_which sf - maxn)) by lia.
            assert (k <? n - (max_which sf - maxn) = true).
                apply Nat.ltb_lt ⇒ //.
                rewrite H0; clear H0.
            apply IHn2 ⇒ //.
            lia.
            moveEqk.
            assert (k = n - (max_which sf - maxSn)) by lia.
            unfold valSn.
            assert (k <? m = true).
            apply Nat.ltb_lt.
            unfold m; rewrite Eqsfn ⇒ /=.
            case_eq (S n - (max_which sf - maxSn)).
            lia.
            movel Hl.
            assert (max_which sf - maxSn < S n) by lia.
            unfold maxSn in H0.
            replace (max_which sf - (maxn - 1)) with (S (max_which sf - maxn)) in H0.
            lia.
            lia.
            rewrite H0.
            case: IHn ⇒ [IHn1 IHn2].
            rewrite Eqsfn in IHn2; simpl in IHn2.
            apply IHn2.
            lia.
            lia.
    Qed.

    Lemma sf_remove_zeros (sf : simpl_fun E gen) :
        { sf' : simpl_fun E gen
                | ( x : X, sf x = sf' x)
                 ( k : nat, k < max_which sf' val sf' k zero)
        }.
    Proof.
        case: (sf_nonzero_ind sf (max_which sf)).
        movesf' [Ext [Ineq [_ Hsf']]].
         sf'; split ⇒ //.
        movek Hk.
        apply Hsf' ⇒ //.
        lia.
    Qed.

End simpl_fun_nonzero.