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.

Brief description

Support for sigma-algebras of subsets.

Description

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.

Used logic axioms

  • classic, the weak form of excluded middle.

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.

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 xA1 x A2 x).
Proof.
intros A1 A2 H1 H2.
pose (A := fun nmatch n with OA1 | _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 xA 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 xA1 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 xB 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 XgenE 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 calScalS = 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 XAE (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 xf (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 XAE (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.