Library Lebesgue.sigma_algebra
This file is part of the Coq Numerical Analysis library
Copyright (C) Boldo, Clément, Faissole, Martin, Mayero
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.
Support for sigma-algebras of subsets.
References to pen-and-paper statements are from RR-9386-v2,
https://hal.inria.fr/hal-03105815v2/
This file refers to Sections 8.6 (pp. 84-88), 9.1 (pp. 91-92),
and 9.4 (pp. 98-101).
Some proof paths may differ.
This module may be used through the import of Lebesgue.Lebesgue_p, or
Lebesgue.Lebesgue_p_wDep, where it is exported.
Brief description
Description
Used logic axioms
- classic, the weak form of excluded middle.
Usage
From Requisite Require Import stdlib.
From Coquelicot Require Import Coquelicot.
Close Scope R_scope.
From Subsets Require Import Subsets_wDep.
From Lebesgue Require Import subset_compl.
Section Sigma_algebra_def.
Context {E : Type}.
Variable gen : (E → Prop) → Prop.
Inductive measurable : (E → Prop) → Prop :=
| measurable_gen : ∀ A, gen A → measurable A
| measurable_empty : measurable (fun _ ⇒ False)
| measurable_compl : ∀ A, measurable (fun x ⇒ ¬ A x) → measurable A
| measurable_union_countable :
∀ A : nat → E → Prop,
(∀ n, measurable (A n)) →
measurable (fun x ⇒ ∃ n, A n x).
Definition measurable_seq : (nat → E → Prop) → Prop :=
fun A ⇒ ∀ n, measurable (A n).
Lemma measurable_ext :
∀ A1 A2, (∀ x, A1 x ↔ A2 x) → measurable A1 → measurable A2.
Proof.
intros A1 A2 H H'.
replace A2 with A1; try exact H'.
apply subset_ext; easy.
Qed.
Lemma measurable_full : measurable (fun _ ⇒ True).
Proof.
apply measurable_compl.
apply measurable_ext with (fun _ ⇒ False).
2: apply measurable_empty.
intros _; split; try easy.
Qed.
Lemma measurable_Prop : ∀ P, measurable (fun _ ⇒ P).
Proof.
intros P; case (classic P); intros HP.
apply measurable_ext with (2:=measurable_full).
easy.
apply measurable_ext with (2:=measurable_empty).
easy.
Qed.
Lemma measurable_compl_rev :
∀ A, measurable A → measurable (fun x ⇒ ¬ A x).
Proof.
intros A H.
apply measurable_compl.
apply measurable_ext with A; try assumption.
intros x; split.
intros K K'; now apply K'.
apply NNPP.
Qed.
Lemma measurable_inter_countable :
∀ A, measurable_seq A → measurable (fun x ⇒ ∀ n, A n x).
Proof.
intros A H.
apply measurable_compl.
apply measurable_ext with (fun x ⇒ ∃ n, ¬ A n x).
intros x; split.
intros (n,Hn) H1.
apply Hn, H1.
intros K.
now apply not_all_ex_not.
apply measurable_union_countable.
intros n; now apply measurable_compl_rev.
Qed.
Lemma measurable_union :
∀ A1 A2,
measurable A1 → measurable A2 →
measurable (fun x ⇒ A1 x ∨ A2 x).
Proof.
intros A1 A2 H1 H2.
pose (A := fun n ⇒ match n with O ⇒ A1 | _ ⇒ A2 end ).
apply measurable_ext with (fun x ⇒ ∃ n, A n x).
intros x; split.
intros (n,Hn).
destruct n; simpl in Hn.
now left.
now right.
intros H; destruct H.
∃ 0; easy.
∃ 1; easy.
apply measurable_union_countable.
intros n; destruct n; easy.
Qed.
Lemma measurable_union_finite :
∀ (A : nat → E → Prop) N,
(∀ n, n ≤ N → measurable (A n)) →
measurable (fun x ⇒ ∃ n, n ≤ N ∧ A n x).
Proof.
intros A N H.
pose (AA:= fun n (x:E) ⇒ match (le_lt_dec n N) with
| left _ ⇒ A n x
| right _ ⇒ False
end).
assert (K1: ∀ i x, i ≤ N → AA i x = A i x).
intros i x Hi.
unfold AA; case (le_lt_dec _ _); intros T; try easy.
contradict T; auto with arith.
assert (K2: ∀ i x, N < i → AA i x = False).
intros i x Hi.
unfold AA; case (le_lt_dec _ _); intros T; try easy.
contradict T; auto with arith.
apply measurable_ext with (fun x : E ⇒ ∃ n : nat, AA n x).
intros x; split; intros (n,Hn).
case (le_lt_dec n N); intros Hn'.
∃ n; split; try easy.
rewrite <- K1; auto.
contradict Hn.
rewrite K2; auto.
∃ n.
rewrite K1; apply Hn.
apply measurable_union_countable.
intros n; case (le_lt_dec n N).
intros H0; apply measurable_ext with (fun x ⇒ A n x).
intros x; rewrite K1; easy.
apply H; auto.
intros H0; apply measurable_ext with (fun _ ⇒ False).
intros x; rewrite K2; easy.
apply measurable_empty.
Qed.
Lemma measurable_union_finite_alt :
∀ (A : nat → E → Prop) N,
(∀ n, n < N → measurable (A n)) →
measurable (fun x ⇒ ∃ n, n < N ∧ A n x).
Proof.
intros A N.
case N.
intros H; apply measurable_ext with (fun _ ⇒ False).
intros x; split; try easy.
intros (n,(Hn,_)); contradict Hn; auto with arith.
apply measurable_empty.
clear N; intros N H.
apply measurable_ext with (fun x : E ⇒ ∃ n : nat, n ≤ N ∧ A n x).
intros x; split; intros (n,(Hn1,Hn2)); ∃ n; split; auto with arith.
apply measurable_union_finite.
intros n Hn; apply H; auto with arith.
Qed.
Lemma measurable_inter :
∀ A1 A2,
measurable A1 → measurable A2 →
measurable (fun x ⇒ A1 x ∧ A2 x).
Proof.
intros A1 A2 H1 H2.
apply measurable_compl.
apply measurable_ext with (fun x ⇒ (¬A1 x) ∨ ¬A2 x).
intros x; split.
apply or_not_and.
apply not_and_or.
apply measurable_union.
now apply measurable_compl_rev.
now apply measurable_compl_rev.
Qed.
Lemma measurable_set_diff :
∀ (A B : E → Prop),
measurable A → measurable B →
measurable (fun x ⇒ B x ∧ ¬ A x).
Proof.
intros A B HA HB.
apply measurable_inter; try easy.
now apply measurable_compl_rev.
Qed.
Lemma measurable_layers :
∀ A, measurable_seq A → measurable_seq (layers A).
Proof.
intros A HA n; case n.
apply HA.
clear n; intros n; now apply measurable_inter, measurable_compl_rev.
Qed.
End Sigma_algebra_def.
Section SA_bis.
Context {E : Type}.
Variable genE : (E → Prop) → Prop.
Lemma measurable_gen_monotone :
∀ (gen1 gen2 : (E → Prop) → Prop),
(∀ (A : E → Prop), gen1 A → gen2 A) →
∀ (A : E → Prop), measurable gen1 A → measurable gen2 A.
Proof.
intros gen1 gen2 H A HA.
induction HA as [A | | A | A].
apply measurable_gen; now apply (H A).
apply measurable_empty.
now apply measurable_compl.
now apply measurable_union_countable.
Qed.
Lemma measurable_gen_ext :
∀ genE' : (E → Prop) → Prop,
(∀ A, genE A → measurable genE' A) →
(∀ A, genE' A → measurable genE A) →
∀ A, measurable genE A ↔ measurable genE' A.
Proof.
intros genE' H1 H2 A; split; intros H3.
induction H3.
apply H1; easy.
apply measurable_empty.
apply measurable_compl; easy.
apply measurable_union_countable; easy.
induction H3.
apply H2; easy.
apply measurable_empty.
apply measurable_compl; easy.
apply measurable_union_countable; easy.
Qed.
Lemma measurable_gen_remove :
∀ A B,
measurable (fun X ⇒ genE X ∨ X = A) B →
measurable genE A → measurable genE B.
Proof.
intros A B H1 H2.
induction H1.
case H; intros H3.
apply measurable_gen; easy.
rewrite H3; easy.
apply measurable_empty.
apply measurable_compl; easy.
apply measurable_union_countable; easy.
Qed.
Definition is_sigma_algebra : ((E → Prop) → Prop) → Prop :=
fun calS ⇒ calS = measurable calS.
Lemma is_sigma_algebra_correct :
∀ calS,
is_sigma_algebra calS ↔
(calS (fun _ ⇒ False) ∧
(∀ A, calS (fun x ⇒ ¬ A x) → calS A) ∧
(∀ A : nat → E → Prop,
(∀ n, calS (A n)) →
calS (fun x ⇒ ∃ n, A n x))).
Proof.
intros calS; apply iff_sym; split.
intros (H1,(H2,H3)).
apply subset_ext; intros x; split; intros H4.
apply measurable_gen; easy.
induction H4; try easy.
apply H2; easy.
apply H3; easy.
intros H; rewrite H; split; try split.
apply measurable_empty.
apply measurable_compl.
apply measurable_union_countable.
Qed.
Lemma is_sigma_algebra_discrete : is_sigma_algebra (fun _ ⇒ True).
Proof.
apply subset_ext; intros A; split; try easy.
intros _; now apply measurable_gen.
Qed.
Lemma is_sigma_algebra_trivial :
is_sigma_algebra (fun A ⇒ (∀ x, ¬ A x) ∨ (∀ x, A x)).
Proof.
apply subset_ext; intros A; split.
intros [HA | HA].
assert (HA1: A = (fun _ ⇒ False)).
apply subset_ext; intros x; split; try easy; apply HA.
rewrite HA1; apply measurable_empty.
assert (HA1: A = (fun _ ⇒ True)).
apply subset_ext; intros x; split; try easy; apply HA.
rewrite HA1; apply measurable_full.
intros HA; induction HA; try easy.
now left.
destruct IHHA as [IHHA | IHHA]; [right | left]; try easy.
intros x; now apply NNPP.
pose (P := ∃ n, ∀ x, A n x).
case (classic P); intros HP.
right; intros x; destruct HP as [n Hn]; now ∃ n.
left; intros x [n Hn].
destruct (H0 n) as [Hn' | Hn'].
now apply (Hn' x).
apply HP; now ∃ n.
Qed.
Lemma measurable_idem : is_sigma_algebra (measurable genE).
Proof.
apply subset_ext; intros A; apply measurable_gen_ext; try easy.
clear A; intros A HA.
apply measurable_gen; now apply measurable_gen.
Qed.
End SA_bis.
Section SA_ter.
Context {E : Type}.
Lemma measurable_correct :
∀ P : ((E → Prop) → Prop) → Prop,
(∀ calS, is_sigma_algebra calS → P calS) ↔
(∀ gen, P (measurable gen)).
Proof.
intros P; split.
intros HP gen; apply HP, measurable_idem.
intros HP calS HcalS; rewrite HcalS; apply HP.
Qed.
End SA_ter.
Section Borel_sigma_algebra.
Context {E : UniformSpace}.
Definition measurable_Borel := @measurable E open.
Lemma measurable_Borel_closed : ∀ A, closed A → measurable_Borel A.
Proof.
intros A HA.
now apply measurable_compl, measurable_gen, open_not.
Qed.
Lemma measurable_gen_open :
∀ gen : (E → Prop) → Prop,
(∀ A, gen A → open A) →
(∀ A, open A → ∃ (B : nat → E → Prop),
(∀ n, gen (B n)) ∧
(∀ x, A x ↔ ∃ n, B n x)) →
∀ A, measurable gen A ↔ measurable_Borel A.
Proof.
intros gen H1 H2.
apply measurable_gen_ext.
intros A H3.
apply measurable_gen.
apply H1; easy.
intros A H3.
destruct (H2 A H3) as (B, (HB1,HB2)).
apply measurable_ext with (fun x ⇒ ∃ n : nat, B n x).
intros x; split; apply HB2.
apply measurable_union_countable.
intros n; apply measurable_gen, HB1.
Qed.
End Borel_sigma_algebra.
Section Cartesian_product_def.
Context {E F : Type}.
Variable genE : (E → Prop) → Prop.
Variable genF : (F → Prop) → Prop.
Definition Gen_Product : (E × F → Prop) → Prop :=
fun A ⇒ ∃ AE, ∃ AF,
(genE AE ∨ AE = fun _ ⇒ True) ∧
(genF AF ∨ AF = fun _ ⇒ True) ∧
(∀ X, A X ↔ AE (fst X) ∧ AF (snd X)).
End Cartesian_product_def.
Section Cartesian_product.
Context {E F : Type}.
Variable genE : (E → Prop) → Prop.
Variable genF : (F → Prop) → Prop.
Lemma Gen_Product_is_product_measurable :
∀ AE AF,
measurable genE AE →
measurable genF AF →
measurable (Gen_Product genE genF) (fun X ⇒ AE (fst X) ∧ AF (snd X)).
Proof.
intros AE AF H1 H2.
apply measurable_inter.
induction H1.
apply measurable_gen.
∃ A; ∃ (fun _ ⇒ True).
split; try (left;easy).
split; try easy; now right.
apply measurable_empty.
apply measurable_compl; easy.
apply measurable_union_countable; easy.
induction H2.
apply measurable_gen.
∃ (fun _ ⇒ True); ∃ A.
split; try (right; easy).
split; try easy; now left.
apply measurable_empty.
apply measurable_compl; easy.
apply measurable_union_countable; easy.
Qed.
Definition swap : ∀ {T : Type}, (E × F → T) → F × E → T :=
fun T f x ⇒ f (snd x, fst x).
Lemma measurable_swap : ∀ A,
measurable (Gen_Product genE genF) A →
measurable (Gen_Product genF genE) (swap A).
Proof.
intros A HA.
induction HA.
apply measurable_gen.
destruct H as [AE [AF [H1 [H2 H3]]]].
∃ AF; ∃ AE.
split; try easy.
split; try easy.
intros X.
unfold swap; rewrite H3; simpl; easy.
apply measurable_empty.
apply measurable_compl; easy.
apply measurable_union_countable; easy.
Qed.
End Cartesian_product.
Section Cartesian_product_bis.
Context {E F : Type}.
Variable genE genE' : (E → Prop) → Prop.
Variable genF genF' : (F → Prop) → Prop.
Lemma measurable_Gen_Product_equiv_aux1 :
(∀ A, measurable genE A ↔ measurable genE' A) →
(∀ A, measurable genF A ↔ measurable genF' A) →
∀ A, (Gen_Product genE genF) A → measurable (Gen_Product genE' genF') A.
Proof.
intros H1 H2.
intros A (AE,(AF,(K1,(K2,K3)))).
apply measurable_ext with (fun X ⇒ AE (fst X) ∧ AF (snd X)).
intros; split; apply K3.
apply measurable_inter.
assert (L1:measurable genE' AE).
case K1; intros K1'.
apply H1.
apply measurable_gen; easy.
rewrite K1'; apply measurable_full.
clear -L1.
induction L1.
apply measurable_gen.
∃ A; ∃ (fun _ ⇒ True).
split; try easy.
left; easy.
split; try easy.
right; easy.
apply measurable_empty.
apply measurable_compl; easy.
apply measurable_union_countable; easy.
assert (L1:measurable genF' AF).
case K2; intros K2'.
apply H2.
apply measurable_gen; easy.
rewrite K2'; apply measurable_full.
clear -L1.
induction L1.
apply measurable_gen.
∃ (fun _ ⇒ True); ∃ A.
split; try easy.
right; easy.
split; try easy.
left; easy.
apply measurable_empty.
apply measurable_compl; easy.
apply measurable_union_countable; easy.
Qed.
Lemma measurable_Gen_Product_equiv_aux2 :
(∀ A, measurable genE A ↔ measurable genE' A) →
(∀ A, measurable genF A ↔ measurable genF' A) →
∀ A, measurable (Gen_Product genE genF) A → measurable (Gen_Product genE' genF') A.
Proof.
intros H1 H2 A HA.
induction HA.
apply measurable_Gen_Product_equiv_aux1; try easy.
apply measurable_empty.
apply measurable_compl; easy.
apply measurable_union_countable; easy.
Qed.
End Cartesian_product_bis.
Section Cartesian_product_ter.
Context {E F : Type}.
Variable genE genE' : (E → Prop) → Prop.
Variable genF genF' : (F → Prop) → Prop.
Lemma measurable_Gen_Product_equiv :
(∀ A, measurable genE A ↔ measurable genE' A) →
(∀ A, measurable genF A ↔ measurable genF' A) →
∀ A, measurable (Gen_Product genE genF) A ↔ measurable (Gen_Product genE' genF') A.
Proof.
intros; split; now apply measurable_Gen_Product_equiv_aux2.
Qed.
End Cartesian_product_ter.