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.
Inductive types for SFplus and Mplus
This module may be used through the import of Lebesgue.Lebesgue_p, or
Lebesgue.Lebesgue_p_wDep, where it is exported.
Brief description
Used logic axioms
- classic, the weak form of excluded middle;
- fun_ext, an alias for functional_extensionality.
Usage
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 x ⇒ a × f x)
| SFp_plus : ∀ (f g : E → R), SFp f → SFp g → SFp (fun x ⇒ f 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 x ⇒ v1 × charac (fun x ⇒ f 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 x ⇒ f x + (v1 - v2) × charac (fun t ⇒ f t = v2) x).
intros Hg; fold g in Hg; destruct Hg as [Hg1 Hg2].
apply SFp_ext with (fun x ⇒ (v2 - v1) × charac (fun t ⇒ f 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 x ⇒ Sup_seq (fun n ⇒ f 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 x ⇒ Sup_seq (fun n ⇒ mk_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 x ⇒ a × f x)
| Mp2_plus : ∀ (f g : E → R), Mp2 f → Mp2 g → Mp2 (fun x ⇒ f x + g x)
| Mp2_sup : ∀ (f : nat → E → R), incr_fun_seq f →
(∀ n, Mp2 (f n)) → Mp2 (fun x ⇒ Sup_seq (fun n ⇒ f 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 x ⇒ Rbar_mult a (f x))
| Mp_plus : ∀ f g, Mp f → Mp g → Mp (fun x ⇒ Rbar_plus (f x) (g x))
| Mp_sup : ∀ f, incr_fun_seq f →
(∀ n, Mp (f n)) → Mp (fun x ⇒ Sup_seq (fun n ⇒ f 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 x ⇒ Rbar_mult a (f x)); now try apply Mp_scal.
apply Mp_ext with (fun x ⇒ Rbar_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.