Library Lebesgue.Mp

This file is part of the Coq Numerical Analysis library
Copyright (C) Boldo, Clément, Martin, Mayero, Mouhcine
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

Inductive types for SFplus and Mplus

Used logic axioms

Usage

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

From Requisite Require Import stdlib_wR.
From Coq Require Import List.

From Coquelicot Require Import Coquelicot.
Close Scope R_scope.

From Subsets Require Import Subsets_wDep.
From Lebesgue Require Import sum_Rbar_nonneg.
From Lebesgue Require Import sigma_algebra.
From Lebesgue Require Import measurable_fun.
From Lebesgue Require Import simple_fun.

Local Open Scope R_scope.

Section SFp_def.

Inductive type for SFplus.

Context {E : Type}.

Variable gen : (E Prop) Prop.

Inductive SFp : (E R) Prop :=
  | SFp_charac : A, measurable gen A SFp (charac A)
  | SFp_scal : a (f : E R), 0 a SFp f SFp (fun xa × f x)
  | SFp_plus : (f g : E R), SFp f SFp g SFp (fun xf x + g x).


Lemma SFp_ext : f1 f2, ( x, f1 x = f2 x) SFp f1 SFp f2.
Proof.
intros f1 f2 H; apply fun_ext in H; now subst.
Qed.

Lemma SFplus_is_SFp : f : E R, SFplus gen f SFp f.
Proof.
case (classic (inhabited E)); intros Y.
destruct Y as [ x0 ].
intros f [Hf1 [l Hf2]].
generalize l f Hf1 Hf2; clear l f Hf1 Hf2.
intros l; case l.
intros f _ ((_,(_,H)),_) ; contradiction H.
clear l; intros v1 l; generalize v1; clear v1.
induction l as [ | v2 l].
intros v1 f Hf1 Hf2.
generalize (SF_aux_measurable _ _ Hf2); intros Hf4.
destruct Hf2 as [Hf2 Hf3].
generalize (finite_vals_sum_eq _ _ Hf2); intros Hf5.
apply SFp_ext with (fun xv1 × charac (fun xf x = v1) x + 0).
intros x; rewrite <- Rbar_finite_eq, Hf5; unfold sum_Rbar_map; now simpl.
apply SFp_plus.
apply SFp_scal.
apply (In_finite_vals_nonneg f (v1 :: nil)); now try apply in_eq.
apply SFp_charac.
apply Hf3.
apply SFp_ext with (charac emptyset).
intros; now rewrite charac_emptyset.
apply SFp_charac, measurable_empty.
intros v1 f Hf1 Hf2.
generalize (SFplus_cons _ _ _ _ _ Hf1 Hf2).
pose (g := fun xf x + (v1 - v2) × charac (fun tf t = v2) x).
intros Hg; fold g in Hg; destruct Hg as [Hg1 Hg2].
apply SFp_ext with (fun x(v2 - v1) × charac (fun tf t = v2) x + g x).
intros x; unfold g; f_equal; ring.
apply SFp_plus.
apply SFp_scal.
apply Raux.Rle_0_minus, Rlt_le; destruct Hf2 as [[Hf2 _] _]; now inversion Hf2.
apply SFp_charac.
apply Hf2.
now apply IHl with v1.
intros f H.
eapply SFp_ext.
2: apply SFp_charac.
2: apply measurable_empty.
intros x.
contradict Y; easy.
Qed.

Lemma SFp_is_SFplus : f, SFp f SFplus gen f.
Proof.
intros f Hf; induction Hf as
    [A HA | a f Ha Hf1 [Hf2 [l Hl]] | f g Hf1 [Hf2 [lf Hlf]] Hg1 [Hg2 [lg Hlg]]]; split.
apply nonneg_charac.
destruct (SF_charac A HA) as [l Hl]; now l.
now apply nonneg_scal_R.
assert (Hf3 : SF gen f) by now l.
destruct (SF_scal f Hf3 a) as [al Hal]; now al.
now apply nonneg_plus_R.
assert (Hf3 : SF gen f) by now lf.
assert (Hg3 : SF gen g) by now lg.
destruct (SF_plus f Hf3 g Hg3) as [l Hl]; now l.
Qed.

Lemma SFp_correct : f, SFp f SFplus gen f.
Proof.
intros; split; [apply SFp_is_SFplus | apply SFplus_is_SFp].
Qed.

Lemma SFp_is_Mplus : f, SFp f Mplus gen f.
Proof.
intros f Hf; apply SFp_correct in Hf; try easy; destruct Hf as [Hf1 [l Hf2]].
apply SFplus_Mplus; try easy; now l.
Qed.

End SFp_def.

Section Mp1_def.

First inductive type for Mplus based on SFp and real-valued functions.

Context {E : Type}.

Variable gen : (E Prop) Prop.

Inductive Mp1 : (E Rbar) Prop :=
  | Mp1_SFp : f : E R, SFp gen f Mp1 f
  | Mp1_sup : (f : nat E R), incr_fun_seq f
                ( n, Mp1 (f n)) Mp1 (fun xSup_seq (fun nf n x)).


Lemma Mp1_ext : f1 f2, ( x, f1 x = f2 x) Mp1 f1 Mp1 f2.
Proof.
intros f1 f2 H; apply fun_ext in H; now subst.
Qed.

Lemma Mplus_is_Mp1 : f, Mplus gen f Mp1 f.
Proof.
intros f Hf.
apply Mp1_ext with (fun xSup_seq (fun nmk_adapted_seq f n x)).
  intros; now rewrite <- (mk_adapted_seq_Sup _ Hf).
apply Mp1_sup.
apply mk_adapted_seq_incr.
intros n; apply Mp1_SFp.
apply SFp_correct; try easy; split.
apply (mk_adapted_seq_nonneg _ Hf).
destruct (mk_adapted_seq_SF _ Hf n) as [l Hl]; now l.
Qed.

Lemma Mp1_is_Mplus : f, Mp1 f Mplus gen f.
Proof.
intros f Hf; induction Hf as [f Hf | ]. apply SFp_correct in Hf; try easy; destruct Hf as [Hf1 [l Hf2]].
apply SFplus_Mplus; try easy; now l.
now apply Mplus_Sup_seq.
Qed.

Lemma Mp1_correct : f, Mp1 f Mplus gen f.
Proof.
intros; split; [apply Mp1_is_Mplus | apply Mplus_is_Mp1].
Qed.

End Mp1_def.

Section Mp2_def.

Second inductive type for Mplus based on real-valued functions.

Context {E : Type}.

Variable gen : (E Prop) Prop.

Inductive Mp2 : (E Rbar) Prop :=
  | Mp2_charac : A, measurable gen A Mp2 (charac A)
  | Mp2_scal : a (f : E R), 0 a Mp2 f Mp2 (fun xa × f x)
  | Mp2_plus : (f g : E R), Mp2 f Mp2 g Mp2 (fun xf x + g x)
  | Mp2_sup : (f : nat E R), incr_fun_seq f
                ( n, Mp2 (f n)) Mp2 (fun xSup_seq (fun nf n x)).


Lemma Mp2_ext : f1 f2, ( x, f1 x = f2 x) Mp2 f1 Mp2 f2.
Proof.
intros f1 f2 H; apply fun_ext in H; now subst.
Qed.

Lemma SFp_is_Mp2 : f, SFp gen f Mp2 f.
Proof.
intros f Hf; induction Hf.
now apply Mp2_charac.
now apply Mp2_scal.
now apply Mp2_plus.
Qed.

Lemma Mp1_is_Mp2 : f, Mp1 gen f Mp2 f.
Proof.
intros f Hf; induction Hf as [f Hf | ].
now apply SFp_is_Mp2.
now apply Mp2_sup.
Qed.

Lemma Mplus_is_Mp2 : f, Mplus gen f Mp2 f.
Proof.
intros; now apply Mp1_is_Mp2, Mplus_is_Mp1.
Qed.

Lemma Mp2_is_Mplus : f, Mp2 f Mplus gen f.
Proof.
intros f Hf; induction Hf.
now apply Mp1_is_Mplus, Mp1_SFp, SFp_charac.
now apply Mplus_scal_R.
now apply Mplus_plus_R.
apply Mp1_is_Mplus, Mp1_sup; try easy; intros; now apply Mplus_is_Mp1.
Qed.

Lemma Mp2_is_Mp1 : f, Mp2 f Mp1 gen f.
Proof.
intros; now apply Mplus_is_Mp1, Mp2_is_Mplus.
Qed.

Lemma Mp2_correct : f, Mp2 f Mplus gen f.
Proof.
intros; split; [apply Mp2_is_Mplus | apply Mplus_is_Mp2].
Qed.

End Mp2_def.

Section Mp_def.

Third inductive type for Mplus based on extended real-valued functions.

Context {E : Type}.

Variable gen : (E Prop) Prop.

Inductive Mp : (E Rbar) Prop :=
  | Mp_charac : A, measurable gen A Mp (charac A)
  | Mp_scal : a f, 0 a Mp f Mp (fun xRbar_mult a (f x))
  | Mp_plus : f g, Mp f Mp g Mp (fun xRbar_plus (f x) (g x))
  | Mp_sup : f, incr_fun_seq f
               ( n, Mp (f n)) Mp (fun xSup_seq (fun nf n x)).


Lemma Mp_ext : f1 f2, ( x, f1 x = f2 x) Mp f1 Mp f2.
Proof.
intros f1 f2 H; apply fun_ext in H; now subst.
Qed.

Lemma Mp2_is_Mp : f, Mp2 gen f Mp f.
Proof.
intros f Hf; induction Hf as [f Hf | a f | f g | ].
now apply Mp_charac.
apply Mp_ext with (fun xRbar_mult a (f x)); now try apply Mp_scal.
apply Mp_ext with (fun xRbar_plus (f x) (g x)); now try apply Mp_plus.
now apply Mp_sup.
Qed.

Lemma Mplus_is_Mp : f, Mplus gen f Mp f.
Proof.
intros; now apply Mp2_is_Mp, Mplus_is_Mp2.
Qed.

Lemma Mp_is_Mplus : f, Mp f Mplus gen f.
Proof.
intros f Hf; induction Hf.
now apply Mp1_is_Mplus, Mp1_SFp, SFp_charac.
now apply Mplus_scal.
now apply Mplus_plus.
now apply Mplus_Sup_seq.
Qed.

Lemma Mp_is_Mp1 : f, Mp f Mp1 gen f.
Proof.
intros; now apply Mplus_is_Mp1, Mp_is_Mplus.
Qed.

Lemma Mp_correct : f, Mp f Mplus gen f.
Proof.
intros; split; [apply Mp_is_Mplus | apply Mplus_is_Mp].
Qed.

Definition Mp_seq : (nat E Rbar) Prop :=
  fun f n, Mp (f n).

Lemma Mp_seq_correct : f, Mp_seq f Mplus_seq gen f.
Proof.
intros f; split; intros Hf n; now apply Mp_correct.
Qed.

End Mp_def.