Library Lebesgue.sigma_algebra_R_Rbar

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 of (extended) real numbers.

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 Qreals.

From Coquelicot Require Import Coquelicot.
Close Scope R_scope.

From Numbers Require Import countable_sets.
From Subsets Require Import Subsets.
From Lebesgue Require Import R_compl Rbar_compl.
From Lebesgue Require Import UniformSpace_compl topo_bases_R.
From Lebesgue Require Import sigma_algebra.

Local Open Scope R_scope.

Section sigma_algebra_R.

Lemma measurable_R_Borel_eq :
   (x : R), measurable_Borel (fun yy = x).
Proof.
intros x; apply measurable_Borel_closed, closed_eq.
Qed.

Definition gen_R_Qoo : (R Prop) Prop :=
  fun A (a b : Q), x, A x Q2R a < x < Q2R b.

Definition gen_R_oo : (R Prop) Prop :=
  fun A a b, x, A x a < x < b.

Definition gen_R_co : (R Prop) Prop :=
  fun A a b, x, A x a x < b.

Definition gen_R_oc : (R Prop) Prop :=
  fun A a b, x, A x a < x b.

Definition gen_R_cc : (R Prop) Prop :=
  fun A a b, x, A x a x b.

Definition gen_R_lt : (R Prop) Prop :=
  fun A b, x, A x x < b.

Definition gen_R_ge : (R Prop) Prop :=
  fun A a, x, A x a x.

Definition gen_R_le : (R Prop) Prop :=
  fun A b, x, A x x b.

Definition gen_R_gt : (R Prop) Prop :=
  fun A a, x, A x a < x.

Lemma measurable_R_equiv_Qoo :
   A, measurable gen_R_Qoo A measurable_Borel A.
Proof.
apply measurable_gen_open; intros A HA.
destruct HA as [a [b HA]].
apply open_ext with (fun xQ2R a < x < Q2R b).
intros x; now rewrite HA.
apply open_and; [apply open_gt | apply open_lt].
destruct (proj2 R_second_countable A HA) as [P HP].
(fun n xP n topo_basis_R n x); split; try easy.
intros n; case (in_dec P n); intros Hn.
assert (H : (P Q R : Prop), P Q R (P Q R)) by tauto.
eexists; eexists; intros x; unfold topo_basis_R; now apply H.
0%Q; 0%Q; intros x; split.
now intros [Hn' _].
intros [Hx1 Hx2]; now apply Rlt_le, Rle_not_lt in Hx2.
Qed.

Lemma measurable_R_equiv_oo :
   A, measurable gen_R_oo A measurable_Borel A.
Proof.
intros A; rewrite <- measurable_R_equiv_Qoo.
apply measurable_gen_ext; clear A; intros A [a [b HA]].
apply measurable_ext
    with (fun x n1 n2,
            a < Q2R (bij_NQ n1)
            (Q2R (bij_NQ n1) < x x < Q2R (bij_NQ n2))
            Q2R (bij_NQ n2) < b).
intros x; rewrite HA; split.
intros [n1 [n2 H]]; lra.
intros [H1 H2].
destruct (Q_dense a x H1) as [q1 Hq1].
destruct (Q_dense x b H2) as [q2 Hq2].
(bij_QN q1); (bij_QN q2).
repeat rewrite bij_NQN; lra.
apply measurable_union_countable; intros n1;
    apply measurable_union_countable; intros n2.
apply measurable_inter; [ | apply measurable_inter].
1,3: apply measurable_Prop.
apply measurable_gen.
(bij_NQ n1); (bij_NQ n2); intros x; lra.
apply measurable_gen; now eexists; eexists.
Qed.

Lemma measurable_R_equiv_co :
   A, measurable gen_R_co A measurable_Borel A.
Proof.
intros A; rewrite <- measurable_R_equiv_oo.
apply measurable_gen_ext; clear A; intros A [a [b HA]].
all: case (Rlt_le_dec a b); intros H.
2: { apply measurable_ext with (fun _False).
    intros x; rewrite HA; split; try easy; intros [Hx1 Hx2]; lra.
    apply measurable_empty. }
3: { apply measurable_ext with (fun _False).
    intros x; rewrite HA; split; try easy; intros [Hx1 Hx2]; lra.
    apply measurable_empty. }

apply measurable_ext with (fun xx = a (a < x < b)).
intros x; rewrite HA; split; try lra.
apply measurable_union.
rewrite measurable_R_equiv_oo; apply measurable_R_Borel_eq.
apply measurable_gen; now eexists; eexists.
apply measurable_ext with (fun x n, a + / (INR n + 1) x < b).
intros x; now rewrite HA, intoo_intco_ex.
apply measurable_union_countable.
intros n; apply measurable_gen; now eexists; eexists.
Qed.

Lemma measurable_R_equiv_oc :
   A, measurable gen_R_oc A measurable_Borel A.
Proof.
intros A; rewrite <- measurable_R_equiv_oo.
apply measurable_gen_ext; clear A; intros A [a [b HA]].
all: case (Rlt_le_dec a b); intros H.
2: { apply measurable_ext with (fun _False).
    intros x; rewrite HA; split; try easy; intros [Hx1 Hx2]; lra.
    apply measurable_empty. }
3: { apply measurable_ext with (fun _False).
    intros x; rewrite HA; split; try easy; intros [Hx1 Hx2]; lra.
    apply measurable_empty. }

apply measurable_ext with (fun x(a < x < b) x = b).
intros x; rewrite HA; split; try lra.
apply measurable_union.
apply measurable_gen; now eexists; eexists.
rewrite measurable_R_equiv_oo; apply measurable_R_Borel_eq.
apply measurable_ext with (fun x n, a < x b - / (INR n + 1)).
intros x; now rewrite HA, intoo_intoc_ex.
apply measurable_union_countable.
intros n; apply measurable_gen; now eexists; eexists.
Qed.

Lemma measurable_R_equiv_cc :
   A, measurable gen_R_cc A measurable_Borel A.
Proof.
intros A; rewrite <- measurable_R_equiv_oo.
apply measurable_gen_ext; clear A; intros A [a [b HA]].
all: case (Rle_lt_dec a b); intros H.
2: { apply measurable_ext with (fun _False).
    intros x; rewrite HA; split; try easy; intros [Hx1 Hx2]; lra.
    apply measurable_empty. }
3: { apply measurable_ext with (fun _False).
    intros x; rewrite HA; split; try easy; intros [Hx1 Hx2]; lra.
    apply measurable_empty. }

apply measurable_ext with (fun xx = a (a < x < b) x = b).
intros x; rewrite HA; split; try lra.
repeat apply measurable_union.
1,3: rewrite measurable_R_equiv_oo; apply measurable_R_Borel_eq.
apply measurable_gen; now eexists; eexists.
apply measurable_ext
    with (fun x n, a + / (INR n + 1) x b - / (INR n + 1)).
intros x; now rewrite HA, intoo_intcc_ex.
apply measurable_union_countable.
intros n; apply measurable_gen; now eexists; eexists.
Qed.

Lemma measurable_R_equiv_lt :
   A, measurable gen_R_lt A measurable_Borel A.
Proof.
intros A; rewrite <- measurable_R_equiv_co.
apply measurable_gen_ext; clear A; intros A.
intros [b HA]; eapply measurable_ext.
intros x; now rewrite <- HA.
rewrite measurable_R_equiv_co.
apply measurable_gen, open_lt.
intros [a [b HA]].
apply measurable_ext with (fun x¬ x < a x < b).
intros x; rewrite HA; lra.
apply measurable_inter.
apply measurable_compl_rev.
all: apply measurable_gen; now eexists.
Qed.

Lemma measurable_R_equiv_ge :
   A, measurable gen_R_ge A measurable_Borel A.
Proof.
intros A; rewrite <- measurable_R_equiv_co.
apply measurable_gen_ext; clear A; intros A.
intros [a HA]; eapply measurable_ext.
intros x; now rewrite <- HA.
rewrite measurable_R_equiv_co.
apply measurable_Borel_closed, closed_ge.
intros [a [b HA]].
apply measurable_ext with (fun xa x ¬ b x).
intros x; rewrite HA; lra.
apply measurable_inter.
2: apply measurable_compl_rev.
all: apply measurable_gen; now eexists.
Qed.

Lemma measurable_R_equiv_le :
   A, measurable gen_R_le A measurable_Borel A.
Proof.
intros A; rewrite <- measurable_R_equiv_oc.
apply measurable_gen_ext; clear A; intros A.
intros [b HA]; eapply measurable_ext.
intros x; now rewrite <- HA.
rewrite measurable_R_equiv_oc.
apply measurable_Borel_closed, closed_le.
intros [a [b HA]].
apply measurable_ext with (fun x¬ x a x b).
intros x; rewrite HA; lra.
apply measurable_inter.
apply measurable_compl_rev.
all: apply measurable_gen; now eexists.
Qed.

Lemma measurable_R_equiv_gt :
   A, measurable gen_R_gt A measurable_Borel A.
Proof.
intros A; rewrite <- measurable_R_equiv_oc.
apply measurable_gen_ext; clear A; intros A.
intros [a HA]; eapply measurable_ext.
intros x; now rewrite <- HA.
rewrite measurable_R_equiv_oc.
apply measurable_gen, open_gt.
intros [a [b HA]].
apply measurable_ext with (fun xa < x ¬ b < x).
intros x; rewrite HA; lra.
apply measurable_inter.
2: apply measurable_compl_rev.
all: apply measurable_gen; now eexists.
Qed.

Definition gen_R := gen_R_oo.

Definition measurable_R := measurable gen_R.

Lemma measurable_R_eq :
   a, measurable_R (fun xx = a).
Proof.
intros.
rewrite measurable_R_equiv_oo.
apply measurable_R_Borel_eq.
Qed.

Lemma measurable_R_intoo :
   a b, measurable_R (fun xa < x < b).
Proof.
intros.
apply measurable_gen; now eexists; eexists.
Qed.

Lemma measurable_R_intco :
   a b, measurable_R (fun xa x < b).
Proof.
intros.
rewrite measurable_R_equiv_oo, <- measurable_R_equiv_co.
apply measurable_gen; now eexists; eexists.
Qed.

Lemma measurable_R_intoc :
   a b, measurable_R (fun xa < x b).
Proof.
intros.
rewrite measurable_R_equiv_oo, <- measurable_R_equiv_oc.
apply measurable_gen; now eexists; eexists.
Qed.

Lemma measurable_R_intcc :
   a b, measurable_R (fun xa x b).
Proof.
intros.
rewrite measurable_R_equiv_oo, <- measurable_R_equiv_cc.
apply measurable_gen; now eexists; eexists.
Qed.

Lemma measurable_R_lt :
   b, measurable_R (fun xx < b).
Proof.
intros.
rewrite measurable_R_equiv_oo, <- measurable_R_equiv_lt.
apply measurable_gen; now eexists.
Qed.

Lemma measurable_R_ge :
   a, measurable_R (fun xa x).
Proof.
intros.
rewrite measurable_R_equiv_oo, <- measurable_R_equiv_ge.
apply measurable_gen; now eexists.
Qed.

Lemma measurable_R_le :
   b, measurable_R (fun xx b).
Proof.
intros.
rewrite measurable_R_equiv_oo, <- measurable_R_equiv_le.
apply measurable_gen; now eexists.
Qed.

Lemma measurable_R_gt :
   a, measurable_R (fun xa < x).
Proof.
intros.
rewrite measurable_R_equiv_oo, <- measurable_R_equiv_gt.
apply measurable_gen; now eexists.
Qed.

Lemma measurable_scal_R : A l, measurable_R A
   measurable_R (fun xA (Rmult l x)).
Proof.
intros A l H.
rewrite measurable_R_equiv_oo, <- measurable_R_equiv_cc.
rewrite measurable_R_equiv_oo, <- measurable_R_equiv_cc in H.
induction H.
2:apply measurable_empty.
2:now apply measurable_compl.
2:now apply measurable_union_countable.
destruct H as (a,(b,Ha)).
destruct (total_order_T l 0) as [H|H].
destruct H.
  apply measurable_gen.
   (/l×b); (/l×a).
  intros x; split; intros Hx.
  apply Ha in Hx.
  replace x with (/l*(l×x)).
  2: field; auto with real.
  split; apply Rmult_le_compat_neg_l; try apply Hx; auto with real.
  apply Ha.
  replace a with (l*(/l×a)) by (field; auto with real).
  replace b with (l*(/l×b)) by (field; auto with real).
  split; apply Rmult_le_compat_neg_l; try apply Hx; auto with real.
  rewrite e; case (in_dec A 0).
  intros Y; apply measurable_ext with (fun _True).
  intros x; rewrite Rmult_0_l; split; easy.
  apply measurable_full.
  intros Y; apply measurable_ext with (fun _False).
  intros x; rewrite Rmult_0_l; split; easy.
  apply measurable_empty.
  apply measurable_gen.
   (/l×a); (/l×b).
  intros x; split; intros Hx.
  apply Ha in Hx.
  replace x with (/l*(l×x)).
  2: field; auto with real.
  split; apply Rmult_le_compat_l; try apply Hx; auto with real.
  apply Ha.
  replace a with (l*(/l×a)) by (field; auto with real).
  replace b with (l*(/l×b)) by (field; auto with real).
  split; apply Rmult_le_compat_l; try apply Hx; auto with real.
Qed.

End sigma_algebra_R.

Section sigma_algebra_Rbar.

Definition gen_Rbar_lt : (Rbar Prop) Prop :=
  fun A b, x, A x Rbar_lt x b.

Definition gen_Rbar_ge : (Rbar Prop) Prop :=
  fun A a, x, A x Rbar_le a x.

Definition gen_Rbar_le : (Rbar Prop) Prop :=
  fun A b, x, A x Rbar_le x b.

Definition gen_Rbar_gt : (Rbar Prop) Prop :=
  fun A a, x, A x Rbar_lt a x.

Definition gen_Rbar := gen_Rbar_ge.

Definition measurable_Rbar := measurable gen_Rbar.

Lemma measurable_Rbar_lt : a,
   measurable_Rbar (fun xRbar_lt a x).
Proof.
intros a.
destruct a.
pose (A := fun nRbar_le (r+/INR (S n))).
apply measurable_ext with (fun x n, A n x).
intros x; split.
intros (n,Hn); unfold A in Hn.
trans Hn 2.
apply Rle_lt_trans with (r+0);[right; ring|idtac].
apply Rplus_lt_compat_l.
apply Rinv_0_lt_compat.
apply lt_0_INR.
auto with arith.
case x.
clear x; intros x H; simpl in H.
assert (0 < x - r).
now apply Rlt_0_minus.
(Z.abs_nat (up (/(x-r)))).
unfold A; apply Rle_trans with (r+(x-r));[idtac|right; ring].
apply Rplus_le_compat_l.
rewrite <- Rinv_inv.
apply Rinv_le_contravar.
now apply Rinv_0_lt_compat.
apply Rle_trans with (IZR (up (/(x-r)))).
left; apply archimed.
rewrite Zabs2Nat.abs_nat_spec, S_INR, INR_IZR_INZ, Z2Nat.id.
2: apply Zabs_pos.
rewrite Z.abs_eq.
left; apply Rlt_plus_1.
apply le_IZR.
left; apply Rlt_trans with (/ (x-r)).
simpl; now apply Rinv_0_lt_compat.
apply archimed.
intros H; 0%nat.
unfold A; easy.
intros H; contradict H; easy.
apply measurable_union_countable.
intros n; apply measurable_gen.
(r+/INR (S n)); easy.
apply measurable_ext with (fun _False).
intros x; case x; easy.
apply measurable_empty.
pose (A := fun nRbar_le (-INR n)).
apply measurable_ext with (fun x n, A n x).
intros x; split.
intros (n,Hn); unfold A in Hn.
trans Hn 2.
case x.
clear x; intros x H.
case (Rle_or_lt 0 x); intros Hx.
0%nat; unfold A.
simpl; rewrite Ropp_0; easy.
(S (Z.abs_nat (up x))); unfold A.
apply Rle_trans with (IZR (up x)-1).
rewrite Zabs2Nat.abs_nat_spec, S_INR, INR_IZR_INZ, Z2Nat.id.
2: apply Zabs_pos.
rewrite <- Zabs_Zopp, Z.abs_eq.
rewrite opp_IZR; right; ring.
assert (up x < 1)%Z; try auto with zarith.
apply lt_IZR; simpl (IZR 1).
apply Rplus_lt_reg_r with (-x).
apply Rle_lt_trans with 1.
apply archimed.
apply Rplus_lt_reg_l with (-1); ring_simplify.
rewrite <- Ropp_0; now apply Ropp_lt_contravar.
apply Rplus_le_reg_l with (-x+1).
ring_simplify (-x+1+x).
apply Rle_trans with (2:=proj2 (archimed x)).
right; ring.
intros H; 0%nat; easy.
intros H; now contradict H.
apply measurable_union_countable.
intros n; apply measurable_gen.
(-INR n); easy.
Qed.

Lemma measurable_Rbar_interv : a b,
    measurable_Rbar (fun xRbar_le a x Rbar_le x b).
Proof.
intros a b.
apply measurable_inter.
apply measurable_gen.
a; easy.
apply measurable_compl.
apply measurable_ext with (fun xRbar_lt b x).
intros x; split.
apply Rbar_lt_not_le.
apply Rbar_not_le_lt.
apply measurable_Rbar_lt.
Qed.

Lemma measurable_Rbar_eq :
   a, measurable_Rbar (fun xx = a).
Proof.
intros.
apply measurable_ext with (fun xRbar_le a x Rbar_le x a).
2: apply measurable_Rbar_interv.
intros; split.
intros (H1,H2).
now apply Rbar_le_antisym.
intros H; rewrite H; split; apply Rbar_le_refl.
Qed.

Lemma measurable_Rbar_is_finite :
  measurable_Rbar is_finite.
Proof.
apply measurable_ext with (fun xRbar_lt m_infty x
      ¬ (Rbar_le p_infty x)).
intros x; now case x.
apply measurable_inter.
apply measurable_Rbar_lt.
apply measurable_compl_rev, measurable_gen.
now p_infty.
Qed.

Lemma measurable_singl_Rbar: (x:Rbar), measurable_Rbar (fun yy = x).
Proof.
intros x.
apply measurable_ext with (fun yRbar_le x y Rbar_le y x).
2: apply measurable_Rbar_interv.
intros y; split.
intros (H1,H2).
now apply Rbar_le_antisym.
intros H; rewrite H; split; apply Rbar_le_refl.
Qed.

Definition gen_Rbar_alt := gen_Rbar_le.

Lemma measurable_Rbar_alt_le : a,
  measurable gen_Rbar_alt (fun xRbar_le a x).
Proof.
intros a; apply measurable_compl.
apply measurable_ext with (fun xRbar_lt x a).
intros x; split.
apply Rbar_lt_not_le.
apply Rbar_not_le_lt.
destruct a.
pose (A := fun n xRbar_le x (r-/INR (S n))).
apply measurable_ext with (fun x n, A n x).
intros x; split.
intros (n,Hn); unfold A in Hn.
trans.
apply Rlt_le_trans with (r-0);[idtac|right; ring].
apply Rplus_lt_compat_l.
apply Ropp_lt_contravar.
apply Rinv_0_lt_compat.
apply lt_0_INR.
auto with arith.
case x.
clear x; intros x H; simpl in H.
assert (0 < r - x).
now apply Rlt_0_minus.
(Z.abs_nat (up (/(r-x)))).
unfold A; apply Rle_trans with (r-(r-x));[right; ring|idtac].
apply Rplus_le_compat_l.
apply Ropp_le_contravar.
rewrite <- Rinv_inv.
apply Rinv_le_contravar.
now apply Rinv_0_lt_compat.
apply Rle_trans with (IZR (up (/(r-x)))).
left; apply archimed.
rewrite Zabs2Nat.abs_nat_spec, S_INR, INR_IZR_INZ, Z2Nat.id.
2: apply Zabs_pos.
rewrite Z.abs_eq.
left; apply Rlt_plus_1.
apply le_IZR.
left; apply Rlt_trans with (/ (r-x)).
simpl; now apply Rinv_0_lt_compat.
apply archimed.
intros H; contradict H; easy.
intros H; 0%nat.
unfold A; easy.
apply measurable_union_countable.
intros n; apply measurable_gen.
(r-/INR (S n)); easy.
pose (A := fun n xRbar_le x (INR n)).
apply measurable_ext with (fun x n, A n x).
intros x; split.
intros (n,Hn); unfold A in Hn.
trans.
case x.
clear x; intros x H.
case (Rle_or_lt x 0); intros Hx.
0%nat; unfold A.
simpl; easy.
(S (Z.abs_nat (up x))); unfold A.
apply Rle_trans with (IZR (up x)).
left; apply archimed.
rewrite Zabs2Nat.abs_nat_spec, S_INR, INR_IZR_INZ, Z2Nat.id.
2: apply Zabs_pos.
rewrite Z.abs_eq.
auto with real.
apply le_IZR.
apply Rle_trans with x; left; try easy.
apply archimed.
intros H; now contradict H.
intros H; 0%nat; easy.
apply measurable_union_countable.
intros n; apply measurable_gen.
(INR n); easy.
apply measurable_ext with (fun _False).
intros x; case x; easy.
apply measurable_empty.
Qed.

Lemma measurable_Rbar_equiv : A,
   measurable_Rbar A
    measurable gen_Rbar_alt A.
Proof.
apply measurable_gen_ext.
intros A (a,Ha).
apply measurable_ext with (fun xRbar_le a x).
intros x; split; apply Ha.
apply measurable_Rbar_alt_le.
intros A (a,Ha).
apply measurable_compl.
apply measurable_ext with (2:=measurable_Rbar_lt a).
intros x; split; intros H.
intros H1; contradict H; apply Rbar_le_not_lt.
apply Ha; easy.
case (Rbar_lt_le_dec a x); try easy; intros H1.
contradict H; apply Ha; easy.
Qed.

Lemma measurable_Rbar_R : (A:RbarProp),
    measurable_Rbar A
     measurable_R (fun x:RA (Finite x)).
Proof.
intros A H.
induction H.
destruct H as (e,He).
destruct e.
apply measurable_ext with (fun x ⇒ (r x)%R).
intros x; split; intros Hx.
apply He; easy.
assert (Rbar_le r x); try easy.
now apply He.
apply measurable_R_ge.
apply measurable_ext with (fun xFalse).
intros x; split; try easy.
intros H1.
absurd (Rbar_le p_infty x); try easy.
now apply He.
apply measurable_empty.
apply measurable_ext with (fun xTrue).
intros x; split; try easy.
intros _.
apply He; easy.
apply measurable_full.
apply measurable_empty.
apply measurable_compl; easy.
apply measurable_union_countable; easy.
Qed.


Lemma measurable_R_Rbar : (A:RProp), measurable_R A
  measurable_Rbar (fun x:Rbaris_finite x A x)
     measurable_Rbar (fun x(is_finite x A x) x = p_infty)
     measurable_Rbar (fun x(is_finite x A x) x = m_infty)
     measurable_Rbar (fun x(is_finite x A x) x = m_infty x = p_infty).
Proof.
intros A H1.
rewrite measurable_R_equiv_oo, <- measurable_R_equiv_cc in H1.
assert (measurable_Rbar (fun x : Rbaris_finite x A x)).
induction H1.
destruct H as (a,(b,H)).
apply measurable_ext with
   (fun x:RbarRbar_le a x Rbar_le x b).
intros x; case x; simpl.
intros r; split.
intros J; split; try easy; apply H; easy.
intros (J1,J2); apply H; easy.
split; easy.
split; easy.
apply measurable_inter.
apply measurable_gen.
a; easy.
apply measurable_compl.
apply measurable_ext with (fun xRbar_lt b x).
intros x; split.
apply Rbar_lt_not_le.
apply Rbar_not_le_lt.
apply measurable_Rbar_lt.
apply measurable_ext with (fun _False).
intros x; split; easy.
apply measurable_empty.
apply measurable_compl.
apply measurable_ext with (fun x:Rbar
   (is_finite x ¬ A x) x = m_infty x = p_infty).
intros x; case x; simpl; split; try easy.
intros T1 (T2,T3); case T1; try easy.
intros T4; case T4; easy.
intros T; left; split; try easy.
intros T'; apply T; split; easy.
intros T; right; right; easy.
intros T; right; left; easy.
apply measurable_union; try easy.
apply measurable_union; apply measurable_singl_Rbar.
apply measurable_ext with (fun x:Rbar
   ( n : nat, is_finite x A n x)).
intros x; split.
intros (n,(H1,H2)); split; try easy.
now n.
intros (H1,(n,H2)); n; split; easy.
apply measurable_union_countable; easy.
split.
exact H.
split.
apply measurable_union; try easy.
apply measurable_singl_Rbar.
split.
apply measurable_union; try easy.
apply measurable_singl_Rbar.
apply measurable_union; try easy.
apply measurable_union; apply measurable_singl_Rbar.
Qed.

Lemma measurable_opp_Rbar : A, measurable_Rbar A
   measurable_Rbar (fun xA (Rbar_opp x)).
Proof.
intros A H.
induction H.
destruct H as (a,Ha).
apply measurable_compl.
apply measurable_ext with (fun xRbar_lt (Rbar_opp a) x).
2: apply measurable_Rbar_lt.
intros x; split; intros H.
apply Rbar_lt_not_le in H.
intros H1; apply H.
apply Ha in H1.
apply Rbar_opp_le.
now rewrite Rbar_opp_involutive.
apply Rbar_not_le_lt.
intros H1; apply H.
apply Ha.
apply Rbar_opp_le.
now rewrite Rbar_opp_involutive.
apply measurable_empty.
apply measurable_compl.
easy.
apply measurable_union_countable.
easy.
Qed.

Lemma measurable_abs_Rbar :
   A, measurable_Rbar A measurable_Rbar (fun xA (Rbar_abs x)).
Proof.
intros A H; induction H.
destruct H as (a,Ha).
eapply measurable_ext.
intros t; apply iff_sym, Ha.
apply measurable_ext with (fun tRbar_le t (Rbar_opp a) Rbar_le a t).
intros t.
case (Rbar_le_lt_dec 0 t); intros Ht.
rewrite Rbar_abs_pos; try easy.
split; intros T;[idtac|now right].
case T; try easy; intros Ht'.
apply Rbar_le_trans with (2:=Ht).
apply Rbar_opp_le.
apply Rbar_le_trans with (2:=Ht').
simpl (Rbar_opp 0); rewrite Ropp_0; easy.
rewrite Rbar_abs_neg.
2: now apply Rbar_lt_le.
split; intros T.
case T; intros Ht'.
apply Rbar_opp_le.
rewrite Rbar_opp_involutive; easy.
apply Rbar_le_trans with (1:=Ht').
apply Rbar_lt_le, Rbar_lt_le_trans with (1:=Ht).
apply Rbar_opp_le.
rewrite Rbar_opp_involutive.
simpl (Rbar_opp 0); rewrite Ropp_0.
apply Rbar_lt_le; easy.
left; apply Rbar_opp_le.
rewrite Rbar_opp_involutive; easy.
apply measurable_union.
apply measurable_compl.
eapply measurable_ext.
2: apply (measurable_Rbar_lt (Rbar_opp a)).
intros t; split.
apply Rbar_lt_not_le.
apply Rbar_not_le_lt.
apply measurable_gen.
a; easy.
apply measurable_empty.
apply measurable_compl; easy.
apply measurable_union_countable; easy.
Qed.

Definition p_infty_finite (x : R) : Rbar := match (Rle_dec 0 x) with
                | left Hmatch Rle_lt_or_eq_dec _ _ H with
                     | left _p_infty
                     | right _ ⇒ 0 end
                | right _m_infty
end.

Definition p_infty_finite_Rbar (x : Rbar) := match x with
                    | p_inftyp_infty
                    | m_inftym_infty
                    | Finite x'p_infty_finite x'
end.

Definition m_infty_finite (x : R) : Rbar := match (Rle_dec 0 x) with
                | left Hmatch Rle_lt_or_eq_dec _ _ H with
                     | left _m_infty
                     | right _ ⇒ 0 end
                | right _p_infty
end.

Definition m_infty_finite_Rbar (x : Rbar) := match x with
             | p_inftym_infty
             | m_inftyp_infty
             | Finite x'm_infty_finite x'
end.

Lemma measurable_Rbar_gt : a,
  measurable_Rbar (fun xRbar_lt x a).
Proof.
intros a.
apply measurable_compl, measurable_ext
         with (fun xRbar_le a x Rbar_le x p_infty).
intros x; split; intros H.
destruct H as [H1 H2].
intros Hf; now apply Rbar_lt_not_le in H1.
split.
now apply Rbar_not_lt_le.
simpl; now destruct x.
apply measurable_Rbar_interv.
Qed.

Lemma measurable_p_infty_finite_Rbar : a,
      measurable_Rbar (fun x : RbarRbar_le a (p_infty_finite_Rbar x)).
Proof.
intros a.
destruct (Rbar_le_dec a m_infty) as [Hp | Hp].
apply measurable_ext with (fun xTrue).
intros x; split; intros Ho; try easy.
replace a with m_infty.
simpl; easy.
destruct a; [now exfalso | now exfalso | reflexivity].
apply measurable_full.
destruct (Rbar_le_dec a 0).
apply measurable_compl.
apply measurable_ext with (fun xRbar_lt x 0).
intros x; split; intros Ho.
destruct x.
unfold p_infty_finite_Rbar, p_infty_finite in ×.
destruct (Rle_dec 0 r0); try easy; try (simpl in Ho; exfalso; lra).
simpl in Ho; exfalso; lra.
destruct a; easy.
unfold p_infty_finite_Rbar, p_infty_finite in Ho.
destruct x.
destruct (Rle_dec 0 r0); try easy.
destruct (Rle_lt_or_eq_dec 0 r0 r1); try easy.
apply Rbar_not_le_lt in Ho.
simpl in Ho; exfalso; lra.
apply Rbar_not_le_lt; now simpl.
apply Rbar_not_le_lt in Ho.
simpl in Ho; exfalso; easy.
simpl; easy.
apply measurable_Rbar_gt.
apply measurable_ext with (fun xRbar_lt 0 x).
intros x; split; intros Ho.
destruct x.
unfold p_infty_finite_Rbar, p_infty_finite in ×.
destruct (Rle_dec 0 r); try easy.
destruct (Rle_lt_or_eq_dec 0 r r0); try easy.
destruct a; easy.
rewrite <-e in Ho.
exfalso.
now apply Rlt_irrefl in Ho.
exfalso.
apply n0.
apply Rbar_lt_le in Ho.
apply Ho.
destruct a; easy.
simpl in Ho; easy.
destruct x; try easy.
unfold p_infty_finite_Rbar, p_infty_finite in Ho.
destruct (Rle_dec 0 r); try easy.
destruct (Rle_lt_or_eq_dec 0 r r0); try easy.
apply measurable_Rbar_lt.
Qed.

Lemma measurable_m_infty_finite_Rbar : a,
      measurable_Rbar (fun x : RbarRbar_le a (m_infty_finite_Rbar x)).
Proof.
intros a.
destruct (Rbar_le_dec a m_infty) as [Hp | Hp].
apply measurable_ext with (fun xTrue).
intros x; split; intros Ho; try easy.
replace a with m_infty.
simpl; easy.
destruct a; [ now exfalso | now exfalso | reflexivity ].
apply measurable_full.
destruct (Rbar_le_dec a 0).
apply measurable_compl.
apply measurable_ext with (fun xRbar_lt 0 x).
intros x; split; intros Ho.
intros Hf.
destruct x; try easy.
unfold m_infty_finite_Rbar, m_infty_finite in ×.
destruct (Rle_dec 0 r0); unfold Rbar_lt in *; try lra; try easy.
destruct (Rle_lt_or_eq_dec 0 r0 r1); unfold Rbar_lt in *;
try lra; try easy.
destruct x; try easy.
unfold m_infty_finite_Rbar, m_infty_finite in Ho.
destruct (Rle_dec 0 r0); try easy.
destruct (Rle_lt_or_eq_dec 0 r0 r1); try easy.
exfalso; apply Ho.
destruct a; easy.
exfalso; apply Ho.
destruct a; easy.
apply measurable_Rbar_lt.
apply measurable_ext with (fun xRbar_lt x 0).
intros x; split; intros Ho; destruct x; try easy.
unfold m_infty_finite_Rbar, m_infty_finite in ×.
destruct (Rle_dec 0 r); try easy.
destruct (Rle_lt_or_eq_dec 0 r r0).
simpl in Ho.
apply Rlt_not_le in r1.
exfalso.
apply r1.
now apply Rlt_le.
rewrite <-e in Ho.
exfalso.
simpl in Ho.
now apply Rlt_irrefl in Ho.
destruct a; easy.
now destruct a.
unfold m_infty_finite_Rbar, m_infty_finite in Ho.
destruct (Rle_dec 0 r); try easy.
destruct (Rle_lt_or_eq_dec 0 r r0); try easy.
now apply Rbar_not_le_lt.
apply measurable_compl.
apply measurable_ext with (fun xRbar_le 0 x
                  Rbar_le x p_infty).
intros x; split; intros Ho.
destruct Ho as (Ho1,Ho2).
intros Hf.
now apply Rbar_lt_not_le in Ho1.
split; [ now apply Rbar_not_lt_le | now destruct x ].
apply measurable_Rbar_interv.
Qed.

Lemma measurable_scalRpos_Rbar : (a : Rbar) (l : R), 0 < l
          measurable_Rbar (fun x : RbarRbar_le a (Rbar_mult l x)).
Proof.
intros a l Hll.
assert (H : l 0).
lra.
assert (r : 0 l).
lra.
apply measurable_gen.
destruct a as [a | | ].
((1/l)*a).
intros x; split; intros Ho.
destruct x as [x | | ]; try easy.
rewrite Rmult_comm.
replace (a × (1 / l)) with (a / l) by now field.
apply Rle_div_l.
apply Rlt_gt.
destruct (Rlt_dec 0 l); try easy.
now rewrite Rmult_comm.
simpl in Ho; destruct (Rle_dec 0 l); try easy.
destruct (Rle_lt_or_eq_dec 0 l r0); try easy.
now rewrite e in H.
destruct x as [x | | ]; try now simpl in ×.
replace (1 / l × a) with (a / l) in Ho by now field.
apply Rle_div_l in Ho.
now simpl in *; rewrite Rmult_comm.
destruct (Rlt_dec 0 l); try easy.
clear Ho.
simpl.
destruct (Rle_dec 0 l); try now exfalso.
destruct (Rle_lt_or_eq_dec 0 l r0); try easy.
exfalso; now apply H.
p_infty.
intros x; split; intros Ho.
destruct x; try easy.
simpl in *; destruct (Rle_dec 0 l); try easy;
destruct (Rle_lt_or_eq_dec 0 l r0); try easy.
destruct x; simpl in *; try easy.
destruct (Rle_dec 0 l); try easy;
destruct (Rle_lt_or_eq_dec 0 l r0); try easy.
now (rewrite e in H; contradict H).
m_infty.
intros x; split; intros Ho; try easy.
Qed.

Lemma measurable_scalR_Rbar : (a : Rbar) (l : R),
  measurable_Rbar (fun x : RbarRbar_le a (Rbar_mult l x)).
Proof.
intros a l.
destruct (Req_dec l 0) as [H | H];
[ rewrite H in *; clear H| idtac].
destruct (Rbar_lt_dec 0 a).
apply measurable_compl, measurable_ext with (fun x:Rbar
             Rbar_lt (Rbar_mult 0 x) a).
intros x; split; intros Hx.
now apply Rbar_lt_not_le.
now apply Rbar_not_le_lt.
apply measurable_ext with (fun x:RbarRbar_lt 0 a).
destruct x.
simpl; now rewrite Rmult_0_l.
simpl; destruct (Rle_dec 0 0); try easy.
destruct (Rle_lt_or_eq_dec 0 0 r0); try easy.
now apply Rlt_not_le in r1.
case (n (Rle_refl 0)).
simpl; destruct (Rle_dec 0 0); try easy.
destruct (Rle_lt_or_eq_dec 0 0 r0); try easy.
now apply Rlt_not_le in r1.
case (n (Rle_refl 0)).
now (apply measurable_ext with (fun xTrue);
           [ | apply measurable_full]).
apply Rbar_not_lt_le in n.
apply measurable_gen.
m_infty; split; intros Ho;
[easy | destruct x as [x | | ]].
simpl; rewrite Rmult_0_l; easy.
simpl; destruct (Rle_dec 0 0); try easy.
destruct (Rle_lt_or_eq_dec 0 0 r); try easy.
now apply Rlt_not_le in r0.
case (n0 (Rle_refl 0)).
simpl; destruct (Rle_dec 0 0); try easy.
simpl; destruct (Rle_lt_or_eq_dec 0 0 r); try easy.
now apply Rlt_not_le in r0.
case (n0 (Rle_refl 0)).
destruct (Rle_dec 0 l).
apply measurable_scalRpos_Rbar; lra.
apply measurable_compl, measurable_ext with
         (fun xRbar_lt (Rbar_opp a) (Rbar_mult (-l) x)).
intros x; split; intros Hx;
[intros Hf | apply Rbar_not_le_lt].
replace (Finite (-l)) with (Rbar_opp l) in Hx by easy.
apply Rbar_opp_lt in Hx.
rewrite Rbar_opp_involutive, <- Rbar_mult_opp_l,
        Rbar_opp_involutive in Hx.
now apply Rbar_lt_not_le in Hx.
intros Hf; apply Hx.
replace (Finite (-l)) with (Rbar_opp l) in Hf by easy.
rewrite Rbar_mult_opp_l in Hf.
now apply Rbar_opp_le.
apply measurable_ext with
              (fun xRbar_le (Rbar_opp a)
                        (Rbar_mult (-l) x)
                (Rbar_opp a) (Rbar_mult (-l) x)).
intros x; split.
intros (H1,H2).
now apply Rbar_le_lt_or_eq_dec in H1; destruct H1.
split.
now apply Rbar_lt_le.
intros Hf.
rewrite Hf in H0.
apply Rbar_lt_not_eq in H0.
now apply H0.
apply measurable_inter.
apply measurable_scalRpos_Rbar; lra.
destruct a as [ a | | ].
apply measurable_compl, measurable_ext with (fun x : Rbar
                        x = (-a) / -l ).
intros x; split; intros Hx.
intros Hf.
rewrite Hx in Hf.
apply Hf.
simpl; simpl in Hf.
rewrite Rmult_comm.
rewrite Rdiv_opp_l.
replace (- (a / -l)× -l) with (- a × (- l/ -l)).
replace (- l / -l) with 1.
rewrite Rmult_1_r; reflexivity.
now field.
now field.
simpl in Hx.
destruct x.
simpl; simpl in Hx.
destruct (Req_dec (-a) (- l × r)).
rewrite H0.
simpl; rewrite Rmult_comm.
transitivity (r × (-l / -l)).
replace (- l / -l) with 1.
now rewrite Rmult_1_r.
now field_simplify.
repeat rewrite Rdiv_opp_l.
replace (r × - (l / - l)) with (r × (-l / -l)).
replace (- l / -l) with 1.
replace (r × - l / - l) with (r × (-l / -l)).
replace (- l / -l) with 1.
easy.
now field_simplify.
now field.
now field_simplify.
now field.
exfalso; apply Hx.
now apply Rbar_finite_neq.
simpl in Hx.
destruct (Rle_dec 0 (-l)).
destruct (Rle_lt_or_eq_dec 0 (-l) r).
exfalso; apply Hx.
easy.
replace 0 with (-0) in e by ring.
apply Ropp_eq_compat in e.
repeat (rewrite Ropp_involutive in e).
rewrite <- e in H.
exfalso; now apply H.
exfalso.
apply n.
apply Rnot_le_lt, Ropp_gt_lt_0_contravar in n0.
rewrite Ropp_involutive in n0.
apply Rgt_lt in n0.
now apply Rlt_le.
simpl in Hx.
destruct (Rle_dec 0 (-l)).
destruct (Rle_lt_or_eq_dec 0 (-l) r).
exfalso.
now apply Hx.
replace 0 with (-0) in e by ring.
apply Ropp_eq_compat in e.
repeat (rewrite Ropp_involutive in e).
rewrite <- e in H.
exfalso; now apply H.
exfalso; apply n.
apply Rnot_le_lt, Ropp_gt_lt_0_contravar in n0.
rewrite Ropp_involutive in n0.
apply Rgt_lt in n0.
now apply Rlt_le.
apply measurable_singl_Rbar.
apply measurable_compl.
simpl.
apply measurable_ext with (fun xx = m_infty).
intros x; split; intros Hx.
rewrite Hx.
simpl; destruct (Rle_dec 0 (-l)); try easy.
destruct (Rle_lt_or_eq_dec 0 (-l) r); try easy.
replace 0 with (-0) in e by ring.
apply Ropp_eq_compat in e.
repeat (rewrite Ropp_involutive in e).
rewrite <- e in H.
exfalso; now apply H.
exfalso.
apply n.
apply Rnot_le_lt, Ropp_gt_lt_0_contravar in n0.
rewrite Ropp_involutive in n0.
apply Rgt_lt in n0.
now apply Rlt_le.
destruct (Rbar_eq_dec x m_infty); try easy.
destruct x; try easy.
exfalso;now apply Hx.
simpl in Hx; destruct (Rle_dec 0 (-l)); try easy.
destruct (Rle_lt_or_eq_dec 0 (-l)); exfalso; apply Hx; easy.
exfalso.
apply n.
apply Rnot_le_lt in n1.
apply Ropp_gt_lt_0_contravar in n1.
rewrite Ropp_involutive in n1.
apply Rgt_lt in n1.
now apply Rlt_le.
apply measurable_singl_Rbar.
apply measurable_compl.
apply measurable_ext with (fun xx = p_infty).
intros x; split; intros Hx.
rewrite Hx.
simpl; destruct (Rle_dec 0 (-l)); try easy.
destruct (Rle_lt_or_eq_dec 0 (-l) r); try easy.
replace 0 with (-0) in e by ring.
apply Ropp_eq_compat in e.
repeat (rewrite Ropp_involutive in e).
rewrite <- e in H.
exfalso; now apply H.
exfalso.
apply n.
apply Rnot_le_lt, Ropp_gt_lt_0_contravar in n0.
rewrite Ropp_involutive in n0.
apply Rgt_lt in n0.
now apply Rlt_le.
destruct (Rbar_eq_dec x p_infty); try easy.
destruct x.
simpl in Hx.
exfalso; apply Hx.
easy.
simpl in Hx.
destruct (Rle_dec 0 (-l)).
destruct (Rle_lt_or_eq_dec 0 (-l)).
exfalso; apply Hx; easy.
exfalso; apply Hx; easy.
exfalso.
apply n.
apply Rnot_le_lt in n1.
apply Ropp_gt_lt_0_contravar in n1.
rewrite Ropp_involutive in n1.
apply Rgt_lt in n1.
now apply Rlt_le.
simpl in Hx.
destruct (Rle_dec 0 (-l)).
destruct (Rle_lt_or_eq_dec 0 (-l) r).
exfalso; apply Hx; easy.
exfalso; apply Hx; easy.
exfalso.
apply n.
apply Rnot_le_lt in n1.
apply Ropp_gt_lt_0_contravar in n1.
rewrite Ropp_involutive in n1.
apply Rgt_lt in n1.
now apply Rlt_le.
apply measurable_singl_Rbar.
Qed.

Lemma measurable_scal_Rbar : A l, measurable_Rbar A
   measurable_Rbar (fun xA (Rbar_mult l x)).
Proof.
intros A l H.
induction H.
2:apply measurable_empty.
2:apply measurable_compl.
2:easy.
2:now apply measurable_union_countable.
destruct H as (a,Ha).
assert (H0 : measurable_Rbar (fun x:RbarRbar_le a (Rbar_mult l x))).
destruct l as [l | | ].
apply measurable_scalR_Rbar.
apply measurable_ext with
              (fun xA (p_infty_finite_Rbar x)).
intros x; split; intros Ho.
apply Ha in Ho.
replace (Rbar_mult p_infty x) with (p_infty_finite_Rbar x); try easy.
unfold p_infty_finite_Rbar, p_infty_finite, Rbar_mult, Rbar_mult'.
case x; try (simpl; reflexivity).
intros r; destruct (Rle_dec 0 r); try reflexivity.
destruct (Rle_lt_or_eq_dec 0 r r0); try reflexivity.
apply Ha.
replace (Rbar_mult p_infty x) with (p_infty_finite_Rbar x) in Ho; try easy.
unfold p_infty_finite_Rbar, p_infty_finite, Rbar_mult, Rbar_mult'.
case x; try (simpl; reflexivity).
intros r; destruct (Rle_dec 0 r); try reflexivity.
destruct (Rle_lt_or_eq_dec 0 r r0); try reflexivity.
eapply measurable_ext.
intros x; symmetry; apply Ha.
apply measurable_p_infty_finite_Rbar.
apply measurable_ext with
      (fun xA (m_infty_finite_Rbar x)).
intros x; split; intros Ho.
apply Ha in Ho.
replace (Rbar_mult m_infty x) with (m_infty_finite_Rbar x); try easy.
unfold m_infty_finite_Rbar, m_infty_finite, Rbar_mult, Rbar_mult'.
case x; try (simpl; reflexivity).
intros r; destruct (Rle_dec 0 r); try reflexivity.
destruct (Rle_lt_or_eq_dec 0 r r0); try reflexivity.
apply Ha.
replace (Rbar_mult m_infty x) with (m_infty_finite_Rbar x) in Ho; try easy.
unfold m_infty_finite_Rbar, m_infty_finite, Rbar_mult, Rbar_mult'.
case x; try (simpl; reflexivity).
intros r; destruct (Rle_dec 0 r); try reflexivity.
destruct (Rle_lt_or_eq_dec 0 r r0); try reflexivity.
eapply measurable_ext.
intros x; symmetry; apply Ha.
apply measurable_m_infty_finite_Rbar.
eapply measurable_ext.
intros x; symmetry; now apply Ha.
apply H0.
Qed.

End sigma_algebra_Rbar.

Section sigma_algebra_R2.

Definition gen_R2_oo := Gen_Product gen_R_oo gen_R_oo.
Definition gen_R2_cc := Gen_Product gen_R_cc gen_R_cc.

Definition gen_R2 := gen_R2_cc.

Definition measurable_R2 := measurable gen_R2.


Lemma measurable_R2_open :
   (A : R × R Prop), measurable_R2 A measurable open A.
Proof.
intros A.
apply iff_trans with (measurable (Gen_Product gen_R_Qoo gen_R_Qoo) A).
apply measurable_Gen_Product_equiv; clear A; intros A.
1,2: now rewrite measurable_R_equiv_cc, measurable_R_equiv_Qoo.
apply measurable_gen_open; clear A; intros A.
intros (B,(C,(Y1,(Y2,Y3)))).
eapply open_ext.
intros X; split; apply Y3.
apply open_and.
case Y1.
intros (l1,(m1,H1)).
eapply open_ext.
intros X; split; apply H1.
apply open_and.
apply open_fst.
apply open_gt.
apply (open_fst (fun zz < Q2R m1)).
apply open_lt.
intros Y4; rewrite Y4.
apply open_true.
case Y2.
intros (l2,(m2,H2)).
eapply open_ext.
intros X; split; apply H2.
apply open_and.
apply open_snd.
apply open_gt.
apply (open_snd (fun zz < Q2R m2)).
apply open_lt.
intros Y4; rewrite Y4.
apply open_true.
intros HA.
destruct (proj2 R2_second_countable A HA) as (P,HP).
(fun n XP n topo_basis_R2 n X).
split; try easy.
intros n.
case (in_dec P n); intros K.
eexists; eexists.
unfold topo_basis_R2, topo_basis_Prod.
split;[idtac|split].
3: split; easy.
left; unfold topo_basis_R; destruct (bij_NQ2 (fst (bij_NN2 n))).
eexists; eexists; split; easy.
left; unfold topo_basis_R; destruct (bij_NQ2 (snd (bij_NN2 n))).
eexists; eexists; split; easy.
(fun _False); (fun _False).
assert (gen_R_Qoo (fun _ : RFalse)).
(Qmake 1 xH); (Qmake 0 xH).
intros x; unfold Q2R; simpl; split; try easy.
intros T; absurd (1×/1 < 0×/1)%R.
apply Rle_not_lt; rewrite Rmult_0_l.
apply Rle_trans with 1%R; auto with real.
right; field.
apply Rlt_trans with x; easy.
split; try (left; easy); split; try easy.
left; easy.
Qed.

End sigma_algebra_R2.