Library Lebesgue.measure_R

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

Construction of the Lebesgue measure on real numbers.

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 Coquelicot Require Import Coquelicot.
Close Scope R_scope.

From Numbers Require Import countable_sets.
From Subsets Require Import Subsets_wDep.
From Lebesgue Require Import subset_compl R_compl Rbar_compl.
From Lebesgue Require Import LF_subcover sum_Rbar_nonneg.
From Lebesgue Require Import sigma_algebra sigma_algebra_R_Rbar.
From Lebesgue Require Import measure measure_uniq.

Local Open Scope R_scope.

Section Lambda_star.

Definition len_int_union : (nat R) (nat R) Rbar :=
    fun a bSup_seq (fun nsum_Rbar n (fun pb p - a p)).

Definition open_int_cover : (R Prop) (nat R) (nat R) Prop :=
  fun A a b
    ( n, a n b n)
    ( x, A x n, a n < x < b n).

Lemma open_int_cover_is_nonempty :
   (A : R Prop), open_int_cover A (fun n- (INR n)) INR.
Proof.
intros A; split.
intros n.
apply Rle_trans with 0.
rewrite <- Ropp_0; apply Ropp_le_contravar.
1,2: apply pos_INR.
intros x Hx.
destruct (nfloor_ex (Rabs x)) as [n [_ Hn]].
apply Rabs_pos.
apply Rabs_def2 in Hn.
(n + 1)%nat; now rewrite plus_INR.
Qed.

Definition len_open_int_cover : (R Prop) Rbar Prop :=
  fun A l a b, open_int_cover A a b len_int_union a b = l.

Lemma len_open_int_cover_ge_0 :
   (A : R Prop) (l : Rbar), len_open_int_cover A l Rbar_le 0 l.
Proof.
intros A l [a [b [[H1 _] H2]]].
rewrite <- H2.
apply Sup_seq_minor_le with 0%nat; simpl.
now rewrite <- Rminus_le_0.
Qed.

Definition lambda_star : (R Prop) Rbar :=
  fun ARbar_glb (len_open_int_cover A).

Lemma lambda_star_ext :
   (A B : R Prop),
    ( x, A x B x)
    lambda_star A = lambda_star B.
Proof.
intros.
f_equal; now apply subset_ext.
Qed.

Lemma lambda_star_nonneg : nonneg lambda_star.
Proof.
intros x.
apply Rbar_glb_correct.
intros y [a [b [[H1 _] H2]]].
rewrite <- H2.
pose (u := fun nsum_Rbar n (fun pb p - a p)).
trans (u 0%nat).
now applyRminus_le_0.
apply Sup_seq_ub.
Qed.

Lemma lambda_star_not_m_infty :
   (A : R Prop), lambda_star A m_infty.
Proof.
intros; apply not_eq_sym, Rbar_lt_not_eq; trans 0 2; apply lambda_star_nonneg.
Qed.

Lemma lambda_star_emptyset : lambda_star (fun _False) = 0.
Proof.
apply Rbar_le_antisym.
2: apply lambda_star_nonneg.
apply Rbar_glb_correct.
(fun _ ⇒ 0); (fun _ ⇒ 0); repeat split; try easy.
pose (u := fun nsum_Rbar n (fun p ⇒ 0 - 0)).
apply trans_eq with (u 0%nat).
2: unfold u; simpl; apply Rbar_finite_eq; auto with real.
apply Sup_seq_sum_Rbar_stable.
intros _; simpl; auto with real.
intros _ _; apply Rbar_finite_eq; auto with real.
Qed.

Lemma lambda_star_le :
   (A B : R Prop),
    ( x, A x B x)
    Rbar_le (lambda_star A) (lambda_star B).
Proof.
intros A B H.
apply Rbar_glb_subset.
intros x [a [b [[HB1 HB2] Hx]]].
a; b; repeat split; try easy.
intros y Hy.
destruct (HB2 y) as [n HB3].
now apply H.
now n.
Qed.

Lemma lambda_star_sigma_subadditivity :
   (A : nat R Prop),
    Rbar_le (lambda_star (fun x n, A n x))
      (Sup_seq (fun nsum_Rbar n (fun plambda_star (A p)))).
Proof.
intros A.
case (classic ( n, Rbar_le p_infty (lambda_star (A n)))).
intros [n Hn].
rewrite Sup_seq_p_infty.
apply Rbar_le_p_infty.
n.
apply sum_Rbar_p_infty.
intros; apply lambda_star_nonneg.
n; split; try easy.
now apply Rbar_ge_p_infty.
intros H'.
assert (H : n, Rbar_lt (lambda_star (A n)) p_infty).
intros n; apply Rbar_not_le_lt; generalize n; now apply not_ex_all_not.
clear H'.
assert (Heps' : (eps : posreal) p, ap bp lp,
          open_int_cover (A p) ap bp
          len_int_union ap bp = lp
          Rbar_le lp (Rbar_plus (lambda_star (A p)) (eps × (/ 2) ^ S p))).
intros eps p.
destruct (Rbar_glb_finite_ex (len_open_int_cover (A p)))
    with (mk_pos_mult_half_pow eps p) as [l [[a [b [H1 H2]]] H3]].
0; intros l; apply len_open_int_cover_ge_0.
apply Rbar_bounded_is_finite_p with 0; try easy.
apply lambda_star_nonneg.
apply H.
a; b; l; tauto.
assert (Heps : (eps : posreal), a b l, p,
          open_int_cover (A p) (a p) (b p)
          len_int_union (a p) (b p) = l p
          Rbar_le (l p) (Rbar_plus (lambda_star (A p)) (eps × (/ 2) ^ S p))).
intros eps.
destruct (choice (fun p (ablp : (nat R) × (nat R) × Rbar) ⇒
    let ap := fst (fst ablp) in
    let bp := snd (fst ablp) in
    let lp := snd ablp in
    open_int_cover (A p) ap bp
    len_int_union ap bp = lp
    Rbar_le lp (Rbar_plus (lambda_star (A p)) (eps × (/ 2) ^ S p)))).
intros p.
destruct (Heps' eps p) as [ap [bp [lp [H1 [H2 H3]]]]].
(x := ((ap, bp), lp)); now repeat split 2.
(fun pfst (fst (x p))).
(fun psnd (fst (x p))).
(fun psnd (x p)).
now intros.
clear Heps'.
apply Rbar_le_epsilon; intros eps.
rewrite <- (Rbar_mult_1_r eps).
rewrite <- series_geom_half.
rewrite <- Sup_seq_scal_l.
2: apply Rlt_le, cond_pos.
rewrite <- Sup_seq_plus.
2: { intros; simpl.
    rewrite <- Rbar_plus_0_l at 1.
    apply Rbar_plus_le_compat_r.
    apply lambda_star_nonneg. }
2: { intros; apply Rbar_mult_le_compat_l.
    apply Rlt_le, cond_pos.
    rewrite <- Rbar_plus_0_l at 1.
    apply Rbar_plus_le_compat_r; simpl.
    repeat apply Rmult_le_pos; [ | | apply pow_le]; lra. }
2: { apply ex_Rbar_plus_ge_0; apply Sup_seq_minor_le with 0%nat.
    apply sum_Rbar_ge_0_alt, lambda_star_nonneg.
    simpl; apply Rmult_le_pos; [apply Rlt_le, cond_pos | lra]. }
rewrite Sup_seq_ext with
    (v := fun nsum_Rbar n
      (fun pRbar_plus (lambda_star (A p)) (Rbar_mult eps ((/ 2) ^ S p)))).
2: { intros; rewrite sum_Rbar_plus.
    apply Rbar_plus_eq_compat_l.
    rewrite sum_Rbar_scal_l; try easy.
    2: apply Rlt_le, cond_pos.
    all: intros p.
    2: apply lambda_star_nonneg.
    all: repeat apply Rmult_le_pos; try apply pow_le; try lra.
    apply Rlt_le, cond_pos. }

destruct (Heps eps) as [a [b [l HH]]].
trans (Sup_seq (fun nsum_Rbar n (fun plen_int_union (a p) (b p)))).
2: { apply Sup_seq_le; intros n.
    apply sum_Rbar_le; intros p Hp.
    destruct (HH p) as [H1 [H2 H3]].
    rewrite (Rbar_finite_mult (pos eps) ((/ 2) ^ S p)).
    rewrite <- H2 in H3.
    apply H3. }

unfold len_int_union; rewrite double_series with (phi := bij_NN2).
2: { intros n p; destruct (HH n) as [[Hab _] _].
    simpl; now rewrite <- Rminus_le_0. }
2: bij_N2N; split; [apply bij_N2NN2 | apply bij_NN2N].
destruct (Rbar_glb_correct (len_open_int_cover (fun x n, A n x))) as [H' _].
apply H'.
(fun ja (fst (bij_NN2 j)) (snd (bij_NN2 j))).
(fun jb (fst (bij_NN2 j)) (snd (bij_NN2 j))).
repeat split.
intros j; pose (p := fst (bij_NN2 j)).
destruct (HH p) as [[H1 _] _]; apply H1.
intros x [p Hp].
destruct (HH p) as [[_ H2] _].
destruct (H2 x Hp) as [q Hq].
(bij_N2N (p, q)).
now rewrite bij_NN2N.
Qed.

Lemma lambda_star_union :
   (A B : R Prop),
    Rbar_le (lambda_star (fun xA x B x))
      (Rbar_plus (lambda_star A) (lambda_star B)).
Proof.
intros A B.
pose (C := fun nmatch n with | 0 ⇒ A | 1 ⇒ B | S (S _) ⇒ fun _False end).
rewrite lambda_star_ext with
    (A := fun x : RA x B x) (B := fun x n, C n x).
replace (Rbar_plus (lambda_star A) (lambda_star B))
    with (Sup_seq (fun nsum_Rbar n (fun plambda_star (C p)))).
apply lambda_star_sigma_subadditivity.
rewrite (Sup_seq_sum_Rbar_stable _ 1%nat).
simpl; apply Rbar_plus_comm.
intros p; apply lambda_star_nonneg.
intros n Hn; destruct n.
contradict Hn; lia.
destruct n.
contradict Hn; lia.
simpl; apply lambda_star_emptyset.
intros; split.
intros [H | H].
  now 0%nat.
  now 1%nat.
intros [n Hn]; destruct n.
  now left.
  destruct n.
  now right.
  destruct Hn.
Qed.

Lemma lambda_star_int_cc :
   a b, lambda_star (fun xa x b) = Rmax 0 (b - a).
Proof.
intros a b.
case (Rle_lt_dec a b); intros H.
2: { rewrite Rmax_left.
    rewrite <- lambda_star_emptyset.
    apply lambda_star_ext; intros x; intuition.
    absurd (a b); try auto with real.
    now apply Rle_trans with x.
    left; now apply Rlt_minus. }
apply Rbar_le_antisym.
rewrite Rminus_le_0 in H.
rewrite Rmax_right; try easy.
apply Rbar_le_epsilon; intros eps.
simpl (Rbar_plus _ _).
replace (b - a + eps) with (b + eps × / 2 - (a - eps × / 2)) by field.
destruct (Rbar_glb_correct (len_open_int_cover (fun xa x b))) as [H' _].
apply H'.
pose (alp := fun nmatch n with 0 ⇒ a - eps × / 2 | _ ⇒ 0 end).
pose (bet := fun nmatch n with 0 ⇒ b + eps × / 2 | _ ⇒ 0 end).
alp; bet; repeat split.
intros n; destruct n; simpl; try apply Rle_refl.
apply Rplus_le_reg_r with (eps × / 2 - a).
replace (a - eps × / 2 + (eps × / 2 - a)) with (0 + 0) by field.
replace (b + eps × / 2 + (eps × / 2 - a)) with (b - a + eps) by field.
apply Rplus_le_compat; try easy.
apply Rlt_le, cond_pos.
intros x [H1 H2]; 0%nat; split.
apply Rlt_le_trans with a; try easy.
apply Rlt_eps_l_alt, pos_half_prf.
apply Rle_lt_trans with b; try easy.
apply Rlt_eps_r_alt, pos_half_prf.
unfold len_int_union; rewrite Sup_seq_stable with (N := 0%nat); try easy.
intros n; apply sum_Rbar_nondecreasing.
intros p; destruct p; simpl; try lra.
replace (b + eps × / 2 - (a - eps × / 2)) with (b - a + eps) by field.
apply Rlt_le, Rle_lt_trans with (b - a); try easy.
apply Rlt_eps_r.
intros n Hn; simpl.
now rewrite Rminus_eq_0, Rbar_plus_0_l.
rewrite Rmax_right; try now rewrite <- Rminus_le_0.
destruct (Rbar_glb_correct (len_open_int_cover (fun xa x b))) as [_ H'].
apply H'; intros l [an [bn [[H1 H2] H3]]].
rewrite <- H3; clear l H3.
destruct (LF_finite_subcover a b an bn)
    as [q [i [Hi [Hi0 [Hiq Hip]]]]]; try easy.
trans (sum_Rbar q (fun pbn (i p) - an (i p))).
trans (bn (i q) - an (i 0%nat)).
apply Rlt_le, Rplus_lt_compat; try easy.
now apply Ropp_lt_contravar.
assert (HH : p', (p' q)%nat
    Rbar_le (bn (i p') - an (i 0%nat))
      (sum_Rbar p' (fun pbn (i p) - an (i p)))).
induction p'.
intros _; apply Rbar_le_refl.
intros Hp'; simpl sum_Rbar.
trans (Rbar_plus (bn (i (S p')) - an (i (S p'))) (bn (i p') - an (i 0%nat))).
2: apply Rbar_plus_le_compat_l, IHp'; lia.
simpl.
replace (bn (i (S p')) - an (i (S p')) + (bn (i p') - an (i 0%nat)))
    with (bn (i (S p')) + (bn (i p') - an (i (S p')) - an (i 0%nat))) by field.
replace (bn (i (S p')) - an (i 0%nat))
    with (bn (i (S p')) + (0 - an (i 0%nat))) by field.
apply Rplus_le_compat_l, Rplus_le_compat_r.
rewrite <- Rminus_le_0.
now apply Rlt_le, Hip.
now apply (HH q).
trans (sum_Rbar (max_n i q) (fun pbn p - an p)).
apply sum_Rbar_perm_le with (u := fun pFinite (bn p - an p)); try easy.
intros p; simpl; now rewrite <- Rminus_le_0.
unfold len_int_union.
apply Sup_seq_ub with (u := fun nsum_Rbar n (fun pFinite (bn p - an p))).
Qed.

Lemma lambda_star_singleton : a, lambda_star (fun xx = a) = 0.
Proof.
intros a; rewrite lambda_star_ext with (B := fun xa x a).
rewrite lambda_star_int_cc; rewrite Rmax_left; [easy | right; ring].
intros; split; auto with real; intros; now apply Rle_antisym.
Qed.

Lemma lambda_star_int_oo :
   a b, lambda_star (fun xa < x < b) = Rmax 0 (b - a).
Proof.
intros a b.
case (Rlt_le_dec a b); intros H.
2: { rewrite Rmax_left.
    rewrite <- lambda_star_emptyset.
    apply lambda_star_ext; intros x; intuition; lra.
    now apply Rle_minus. }
apply Rbar_le_antisym.
rewrite <- lambda_star_int_cc.
apply lambda_star_le; intros x [H1 H2]; split; now left.
rewrite Rminus_lt_0 in H.
apply Rbar_le_epsilon_alt; (mkposreal _ H).
intros eps Heps; simpl in Heps.
apply Rbar_plus_le_reg_l with (- eps); try easy.
rewrite <- Rbar_finite_opp.
rewrite (Rbar_plus_comm (lambda_star _)).
rewrite <- Rbar_minus_plus_l; try easy.
simpl (Rbar_plus _ _).
replace (- eps + Rmax 0 (b - a))
    with (Rmax 0 (b - eps × / 2 - (a + eps × / 2))).
2: repeat rewrite Rmax_right; [field | now left | lra].
rewrite <- lambda_star_int_cc.
apply lambda_star_le; intros x [H1 H2]; split.
apply Rlt_le_trans with (a + eps × / 2); try easy.
apply Rlt_eps_r_alt, pos_half_prf.
apply Rle_lt_trans with (b - eps × / 2); try easy.
apply Rlt_eps_l_alt, pos_half_prf.
Qed.

Lemma lambda_star_int_oc :
   a b, lambda_star (fun xa < x b) = Rmax 0 (b - a).
Proof.
intros a b.
case (Rlt_le_dec a b); intros H.
2: { rewrite Rmax_left.
    rewrite <- lambda_star_emptyset.
    apply lambda_star_ext; intros x; intuition; lra.
    now apply Rle_minus. }
apply Rbar_le_antisym.
rewrite <- lambda_star_int_cc.
apply lambda_star_le; intros x [H1 H2]; split; try easy; now left.
rewrite Rminus_lt_0 in H.
apply Rbar_le_epsilon_alt; (mkposreal _ H).
intros eps Heps; simpl in Heps.
apply Rbar_plus_le_reg_l with (- eps); try easy.
rewrite <- Rbar_finite_opp.
rewrite (Rbar_plus_comm (lambda_star _)).
rewrite <- Rbar_minus_plus_l; try easy.
simpl (Rbar_plus _ _).
replace (-eps + Rmax 0 (b - a)) with (Rmax 0 (b - (a + eps))).
2: repeat rewrite Rmax_right; [field | now left | lra].
rewrite <- lambda_star_int_cc.
apply lambda_star_le; intros x [H1 H2]; split; try easy.
apply Rlt_le_trans with (a + eps); try easy.
apply Rlt_eps_r.
Qed.

Lemma lambda_star_int_co :
   a b, lambda_star (fun xa x < b) = Rmax 0 (b - a).
Proof.
intros a b.
case (Rlt_le_dec a b); intros H.
2: { rewrite Rmax_left.
    rewrite <- lambda_star_emptyset.
    apply lambda_star_ext; intros x; intuition; lra.
    now apply Rle_minus. }
apply Rbar_le_antisym.
rewrite <- lambda_star_int_cc.
apply lambda_star_le; intros x [H1 H2]; split; try easy; now left.
rewrite Rminus_lt_0 in H.
apply Rbar_le_epsilon_alt; (mkposreal _ H).
intros eps Heps; simpl in Heps.
apply Rbar_plus_le_reg_l with (- eps); try easy.
rewrite <- Rbar_finite_opp.
rewrite (Rbar_plus_comm (lambda_star _)).
rewrite <- Rbar_minus_plus_l; try easy.
simpl (Rbar_plus _ _).
replace (-eps + Rmax 0 (b - a)) with (Rmax 0 (b - eps - a)).
2: repeat rewrite Rmax_right; [field | now left | lra].
rewrite <- lambda_star_int_cc.
apply lambda_star_le; intros x [H1 H2]; split; try easy.
apply Rle_lt_trans with (b - eps); try easy.
apply Rlt_eps_l.
Qed.

Lemma lambda_star_int_partition :
   a b c,
    Rbar_plus
      (lambda_star (fun xa < x < b c < x))
      (lambda_star (fun xa < x < b x c)) = Rmax 0 (b - a).
Proof.
assert (H : P Q R, ¬ R P (Q R) P Q) by tauto.
intros a b c.
rewrite Rbar_plus_eq_compat_r with (y := lambda_star (fun xRmax a c < x < b)).
2: apply lambda_star_ext; intros x; rewrite Rmax_lt; tauto.
rewrite lambda_star_int_oo.
case (Rle_lt_dec b c); intros Hbc.
rewrite Rbar_plus_eq_compat_l with (y := lambda_star (fun xa < x < b)).
2: apply lambda_star_ext; intros x; lra.
rewrite lambda_star_int_oo; simpl; rewrite Rbar_finite_eq.
case (Rle_lt_dec a c); intros Hac.
replace (Rmax a c) with c; try now rewrite Rmax_right.
rewrite Rmax_left; try now apply Rle_minus.
ring.
replace (Rmax a c) with a; try now rewrite Rmax_left; try apply Rlt_le.
rewrite Rmax_left; try ring.
now apply Rle_minus, Rlt_le, Rle_lt_trans with c.
rewrite Rbar_plus_eq_compat_l with (y := lambda_star (fun xa < x c)).
2: apply lambda_star_ext; intros x; lra.
rewrite lambda_star_int_oc; simpl; rewrite Rbar_finite_eq.
case (Rle_lt_dec a c); intros Hac.
replace (Rmax a c) with c; try now rewrite Rmax_right.
repeat rewrite Rmax_right.
ring.
1,2,3: rewrite <- Rminus_le_0; try easy.
1,2: apply Rlt_le; try easy.
now apply Rle_lt_trans with c.
replace (Rmax a c) with a; try now rewrite Rmax_left; try apply Rlt_le.
replace (Rmax 0 (c - a)) with 0; try ring.
rewrite Rmax_left at 1; auto with real.
Qed.

End Lambda_star.

Section L_calligraphic.

Definition cal_L : (R Prop) Prop :=
  fun E
     (A : R Prop),
      lambda_star A =
        Rbar_plus (lambda_star (fun xA x E x))
                  (lambda_star (fun xA x ¬ E x)).

Lemma cal_L_equiv_def :
   (E : R Prop),
    ( (A : R Prop),
      Rbar_le (Rbar_plus (lambda_star (fun xA x E x))
                         (lambda_star (fun xA x ¬ E x)))
              (lambda_star A))
    cal_L E.
Proof.
intros E H A.
apply Rbar_le_antisym; try easy.
apply Rbar_le_eq
    with (lambda_star (fun x(A x E x) (A x ¬ E x))).
2: apply lambda_star_union.
apply lambda_star_ext; intros x; tauto.
Qed.

Lemma cal_L_ext :
   (E F : R Prop),
    ( x, E x F x)
    cal_L E cal_L F.
Proof.
intros E F H HE A.
rewrite lambda_star_ext
    with (A := fun xA x F x) (B := fun xA x E x).
rewrite lambda_star_ext
    with (A := fun xA x ¬ F x) (B := fun xA x ¬ E x); try easy.
all: intros x; rewrite H; tauto.
Qed.

Lemma cal_L_empty : cal_L (fun _False).
Proof.
intros A.
rewrite lambda_star_ext
    with (A := fun xA x False) (B := fun _False) by tauto.
rewrite lambda_star_ext
    with (A := fun xA x ¬ False) (B := A) by tauto.
rewrite lambda_star_emptyset.
now rewrite Rbar_plus_0_l.
Qed.

Lemma cal_L_compl :
   (E : R Prop), cal_L (fun x¬ E x) cal_L E.
Proof.
intros E HE A.
rewrite (HE A), Rbar_plus_comm.
apply Rbar_plus_eq_compat_r.
apply lambda_star_ext; intros x; tauto.
Qed.

Lemma cal_L_compl_rev :
   (E : R Prop), cal_L E cal_L (fun x¬ E x).
Proof.
intros E HE A.
rewrite (HE A), Rbar_plus_comm.
apply Rbar_plus_eq_compat_l.
apply lambda_star_ext; intros x; tauto.
Qed.

Lemma cal_L_union :
   (E F : R Prop),
    cal_L E cal_L F
    cal_L (fun xE x F x).
Proof.
intros E1 E2 H1 H2.
apply cal_L_equiv_def; intros A.
rewrite (H1 A).
rewrite (H2 (fun xA x ¬ E1 x)).
rewrite <- Rbar_plus_assoc.
rewrite lambda_star_ext
    with (A := fun xA x (E1 x E2 x))
         (B := fun xA x E1 x (A x ¬ E1 x) E2 x)
    by (intros x; tauto).
rewrite lambda_star_ext
    with (A := fun xA x ¬ (E1 x E2 x))
         (B := fun x(A x ¬ E1 x) ¬ E2 x) by tauto.
apply Rbar_plus_le_compat_r.
apply lambda_star_union.
all: apply lambda_star_nonneg.
Qed.

Lemma cal_L_union_finite:
   (E : nat R Prop) N,
    ( n, (n N)%nat cal_L (E n))
    cal_L (fun x n, (n N)%nat E n x).
Proof.
intros E N; induction N; intros H.
apply cal_L_ext with (E 0%nat).
2: now apply (H 0%nat).
intros x; split.
intros Hx; 0%nat; try easy.
intros [n [Hn Hx]].
rewrite Nat.le_0_r in Hn.
now rewrite Hn in Hx.
apply cal_L_ext with (fun x( n, (n N)%nat E n x) E (S N) x).
2: { apply cal_L_union.
    apply IHN; intros n Hn.
    all: apply H; lia. }
intros x; split.
intros [[n [Hn Hx]] | Hx].
n; split; try easy; lia.
(S N); now split.
intros [n [Hn Hx]].
case (le_lt_eq_dec n (S N)). try easy; clear Hn; intros Hn.
apply Nat.lt_succ_r in Hn.
now left; n; split; try easy; try apply Nat.succ_le_mono.
now intros ->; right.
Qed.

Lemma cal_L_intersection_finite:
   (E : nat R Prop) N,
    ( n, (n N)%nat cal_L (E n))
    cal_L (fun x n, (n N)%nat E n x).
Proof.
intros E N HE.
apply cal_L_compl.
apply cal_L_ext with (fun x n, (n N)%nat ¬ E n x).
2: apply cal_L_union_finite; intros n Hn; now apply cal_L_compl_rev, HE.
intros x; split.
intros [n [Hn Hx]].
apply ex_not_not_all.
n; intros H.
contradiction (H Hn).
intros H.
apply not_all_ex_not in H.
destruct H as [n H].
apply imply_to_and in H.
now n.
Qed.

Lemma cal_L_intersection :
   (E F : R Prop),
    cal_L E cal_L F
    cal_L (fun xE x F x).
Proof.
intros E1 E2 H1 H2.
pose (E := fun nmatch n with 0 ⇒ E1 | S _E2 end).
apply cal_L_ext with (fun x n, (n 1)%nat E n x).
2: { apply cal_L_intersection_finite; intros n Hn.
    case (le_lt_eq_dec n 1); try easy; clear Hn; intros Hn.
    apply Nat.lt_succ_r, Nat.le_0_r in Hn.
    all: now rewrite Hn. }
intros x; split.
intros H; split; [apply (H 0%nat) | apply (H 1%nat)]; lia.
intros [Hx1 Hx2] n Hn.
case (le_lt_eq_dec n 1); try easy; clear Hn; intros Hn.
apply Nat.lt_succ_r, Nat.le_0_r in Hn.
all: now rewrite Hn.
Qed.

Lemma cal_L_lambda_star_additivity :
   (E F : R Prop),
    cal_L E cal_L F
    ( x, ¬ (E x F x))
     (A : R Prop),
      lambda_star (fun xA x (E x F x)) =
        Rbar_plus (lambda_star (fun xA x E x))
                  (lambda_star (fun xA x F x)).
Proof.
intros E F HE HF H A.
rewrite lambda_star_ext
    with (A := fun xA x (E x F x))
         (B := fun xA x E x A x F x) by tauto.
rewrite HE.
rewrite lambda_star_ext
    with (A := fun x(A x E x A x F x) E x)
         (B := fun xA x E x) by tauto.
rewrite lambda_star_ext
    with (A := fun x(A x E x A x F x) ¬ E x)
         (B := fun x ⇒ (A x F x)); try easy.
intuition; now apply (H x).
Qed.

Lemma cal_L_lambda_star_additivity_finite :
   (E : nat R Prop) N,
    ( n, (n N)%nat cal_L (E n))
    ( n p x, (n N)%nat (p N)%nat E n x E p x n = p)
     (A : R Prop),
      lambda_star (fun xA x ( n, (n N)%nat E n x)) =
        sum_Rbar N (fun nlambda_star (fun xA x E n x)).
Proof.
intros E N HE H A; induction N.
apply lambda_star_ext; intros x; split.
intros [HAx [n [Hn HEx]]].
rewrite Nat.le_0_r in Hn; rewrite Hn in HEx; tauto.
intros [HAx HEx]; split; [easy | now 0%nat].
simpl.
rewrite <- IHN.
rewrite <- cal_L_lambda_star_additivity.
apply lambda_star_ext; intros x; split.
intros [HAx [n [Hn HEx]]]; split; try easy.
case (le_lt_eq_dec n (S N)); try easy; clear Hn; intros Hn.
right; n; split; [lia | easy].
left; now rewrite Hn in HEx.
intros [HAx [HEx | [n [Hn HEx]]]].
split; [easy | now (S N)].
split; [easy | n]; split; [lia | easy].
now apply HE.
apply cal_L_union_finite.
1,3: intros n Hn; apply HE; lia.
intros x [HEx' [n [Hn HEx]]].
specialize (H n (S N) x); rewrite H in Hn; now try lia.
intros n p x Hn Hp; apply H; lia.
Qed.

Lemma cal_L_lambda_star_sigma_additivity :
   (E : nat R Prop),
    ( n, cal_L (E n))
    ( n p x, E n x E p x n = p)
    lambda_star (fun x n, E n x) =
      Sup_seq (fun Nsum_Rbar N (fun nlambda_star (E n))).
Proof.
intros E HE H.
apply Rbar_le_antisym.
apply lambda_star_sigma_subadditivity.
apply Sup_seq_lub; intros n.
rewrite sum_Rbar_ext with (f2 := fun nlambda_star (fun xTrue E n x)).
2: intros i Hi; apply lambda_star_ext; now intros x.
rewrite <- cal_L_lambda_star_additivity_finite with (A := fun _True); try easy.
2: intros n' p' x _ _; apply H.
apply lambda_star_le.
intros x [_ [m [Hm HEx]]]; now m.
Qed.

Lemma cal_L_union_countable_aux :
   (E : nat R Prop),
    ( n, cal_L (E n))
    ( n, cal_L (DU E n))
    ( n p x, DU E n x DU E p x n = p)
    ( n x, ( p, (p n)%nat E p x)
                 ( p, (p n)%nat DU E p x)).
Proof.
intros E HE; repeat split;
    [ | apply DU_disjoint | apply DU_union | apply DU_union_alt].
induction n.
apply HE.
apply cal_L_intersection; try apply HE.
apply cal_L_compl_rev, cal_L_union_finite.
intros p _; apply HE.
Qed.

Lemma cal_L_union_countable :
   (E : nat R Prop),
    ( n, cal_L (E n))
    cal_L (fun x n, E n x).
Proof.
intros E HE.
destruct (cal_L_union_countable_aux E) as [HF1 [HF2 HF3]]; try easy.
apply cal_L_equiv_def; intros A.
rewrite lambda_star_ext
    with (A := fun xA x ( n, E n x))
         (B := fun xA x ( n, DU E n x)).
2: { intros x; split; intros [Hx [n Hnx]]; split; try easy.
    2: destruct (HF3 n x) as [_ [p [_ Hp]]].
    destruct (HF3 n x) as [[p [_ Hp]] _].
    1,3: n; split; [lia | easy].
    all: now p. }
trans (Rbar_plus
        (Sup_seq (fun nsum_Rbar n (fun p
          lambda_star (fun xA x DU E p x))))
        (lambda_star (fun xA x ¬ ( n, E n x)))).
apply Rbar_plus_le_compat_r.
rewrite lambda_star_ext
    with (A := fun xA x ( n, DU E n x))
         (B := fun x n, A x DU E n x).
apply lambda_star_sigma_subadditivity.
intros x; split.
intros [Hx [n Hn]]; n; now split.
intros [n [Hx Hn]]; split; try easy.
now n.
rewrite Rbar_plus_comm.
apply Rbar_le_eq
    with (y := Sup_seq (fun n
            Rbar_plus (lambda_star (fun xA x ¬ ( n, E n x)))
                      (sum_Rbar n (fun p
                        lambda_star (fun xA x DU E p x))))).
case_eq (lambda_star (fun xA x ¬ ( n, E n x))).
  intros r Hr; now rewrite <- Sup_seq_plus_compat_l.
  2: intros H; contradict H; apply lambda_star_not_m_infty.
  intros H.
  rewrite Rbar_plus_comm, Rbar_plus_pos_pinfty.
  symmetry.
  apply Sup_seq_p_infty.
   0%nat; simpl.
  apply Rbar_plus_pos_pinfty, lambda_star_nonneg.
  apply Sup_seq_minor_le with 0%nat, lambda_star_nonneg.
apply Sup_seq_lub; intros n; rewrite Rbar_plus_comm.
  assert (H: cal_L (fun x p, (p n)%nat DU E p x)).
  apply cal_L_union_finite; now intros p _.
rewrite H with A; clear H.
rewrite cal_L_lambda_star_additivity_finite.
2: now intros p _.
2: intros p q x _ _; apply HF2.
apply Rbar_plus_le_compat_l.
apply lambda_star_le.
intros x [H H1]; split; try easy.
intros H2.
rewrite <- (HF3 n x) in H2; destruct H2 as [p [_ Hp]].
contradict H1; now p.
Qed.

Lemma cal_L_ray_l : a, cal_L (fun xa < x).
Proof.
intros c.
apply cal_L_equiv_def; intros A.
case_eq (lambda_star A).
2: intros _; apply Rbar_le_p_infty.
2: intros H; contradict H; apply lambda_star_not_m_infty.
intros lA HlA; unfold lambda_star in HlA.
apply Rbar_le_epsilon; intros eps.
destruct (Rbar_glb_finite_ex (len_open_int_cover A))
    with eps as [l [[a [b [[H1 H2] H3]]] H4]].
   0; intros l; apply len_open_int_cover_ge_0.
  now rewrite HlA.
rewrite HlA in H4.
trans l.
pose (I1 := fun n xa n < x < b n c < x).
pose (I2 := fun n xa n < x < b n x c).
unfold len_int_union in H3.
rewrite Sup_seq_ext
    with (v := fun n
      sum_Rbar n (fun p
        Rbar_plus (lambda_star (I1 p)) (lambda_star (I2 p)))) in H3.
2: { intros n; apply sum_Rbar_ext; intros p Hp.
    unfold I1, I2.
    rewrite lambda_star_int_partition, Rbar_finite_eq, Rmax_right; try easy.
    now rewrite <- Rminus_le_0. }
rewrite Sup_seq_ext
    with (v := fun n
      Rbar_plus
        (sum_Rbar n (fun plambda_star (I1 p)))
        (sum_Rbar n (fun plambda_star (I2 p)))) in H3.
2: intros n; apply sum_Rbar_plus; intros p; apply lambda_star_nonneg.
rewrite Sup_seq_plus in H3.
2,3: intros n; apply sum_Rbar_nondecreasing; intros p; apply lambda_star_nonneg.
2: { apply ex_Rbar_plus_ge_0.
    pose (u1 := fun nsum_Rbar n (fun plambda_star (I1 p))); trans (u1 0%nat).
    apply sum_Rbar_ge_0_alt, lambda_star_nonneg.
    apply Sup_seq_ub.
    pose (u2 := fun nsum_Rbar n (fun plambda_star (I2 p))); trans (u2 0%nat).
    apply sum_Rbar_ge_0_alt, lambda_star_nonneg.
    apply Sup_seq_ub. }
trans (Rbar_plus (lambda_star (fun x : R n : nat, I1 n x))
                 (lambda_star (fun x : R n : nat, I2 n x))).
2: rewrite <- H3; apply Rbar_plus_le_compat; apply lambda_star_sigma_subadditivity.
apply Rbar_plus_le_compat.
all: apply lambda_star_le; intros x [HAx HEx].
all: destruct (H2 _ HAx) as [n Hn]; n.
unfold I1; tauto.
unfold I2; apply Rnot_lt_le in HEx; tauto.
Qed.

Lemma cal_L_ray_cr : b, cal_L (fun xx b).
Proof.
intros b.
apply cal_L_ext with (fun x¬ b < x).
2: apply cal_L_compl_rev, cal_L_ray_l.
intros x; split.
apply Rnot_lt_le.
apply Rle_not_lt.
Qed.

Lemma cal_L_ray_r : b, cal_L (fun xx < b).
Proof.
intros b.
apply cal_L_ext with (fun x n, x b - / (INR n + 1)).
2: apply cal_L_union_countable; intros n; apply cal_L_ray_cr.
intros x; split.
intros [n Hn].
apply Rle_lt_trans with (b - / (INR n + 1)); try easy.
apply Rminus_lt_compat_pos, Rinv_0_lt_compat, INRp1_pos.
intros H.
apply Rlt_0_minus in H.
destruct (nfloor_ex (/ (b - x))) as [n [_ Hn]].
now apply Rlt_le, Rinv_0_lt_compat.
n.
rewrite Rle_minus_r, Rplus_comm, <- Rle_minus_r; apply Rlt_le.
rewrite <- Rinv_inv.
apply Rinv_lt_contravar; try easy.
apply Rmult_lt_0_compat.
now apply Rinv_0_lt_compat.
apply INRp1_pos.
Qed.

Lemma cal_L_ray_cl : a, cal_L (fun xa x).
Proof.
intros a.
apply cal_L_ext with (fun x¬ x < a).
2: apply cal_L_compl_rev, cal_L_ray_r.
intros x; split.
apply Rnot_lt_le.
apply Rle_not_lt.
Qed.

Lemma cal_L_intoo : a b, cal_L (fun xa < x < b).
Proof.
intros.
apply cal_L_intersection.
apply cal_L_ray_l.
apply cal_L_ray_r.
Qed.

Lemma cal_L_intco : a b, cal_L (fun xa x < b).
Proof.
intros.
apply cal_L_intersection.
apply cal_L_ray_cl.
apply cal_L_ray_r.
Qed.

Lemma cal_L_intcc : a b, cal_L (fun xa x b).
Proof.
intros.
apply cal_L_intersection.
apply cal_L_ray_cl.
apply cal_L_ray_cr.
Qed.

Lemma cal_L_intoc : a b, cal_L (fun xa < x b).
Proof.
intros.
apply cal_L_intersection.
apply cal_L_ray_l.
apply cal_L_ray_cr.
Qed.

Lemma cal_L_gen_R : (E : R Prop), gen_R E cal_L E.
Proof.
intros E [a [b H]].
apply cal_L_ext with (fun xa < x < b); try easy.
apply cal_L_intoo.
Qed.

Lemma cal_L_singleton : a, cal_L (fun xx = a).
Proof.
intros a.
apply cal_L_ext with (fun xa x a).
intros; split; auto with real; intros; now apply Rle_antisym.
apply cal_L_intcc.
Qed.

End L_calligraphic.

Section Lebesgue_sigma_algebra.

Definition measurable_L : (R Prop) Prop := @measurable R cal_L.

Lemma cal_L_sigma_algebra :
   (E : R Prop), cal_L E measurable_L E.
Proof.
intros E; split; intros H.
now apply measurable_gen.
induction H; try easy.
apply cal_L_empty.
now apply cal_L_compl.
now apply cal_L_union_countable.
Qed.

Lemma measurable_R_is_measurable_L :
   (E : R Prop), measurable_R E measurable_L E.
Proof.
intros.
apply measurable_gen_monotone with gen_R; try easy.
apply cal_L_gen_R.
Qed.

End Lebesgue_sigma_algebra.

Section Lebesgue_measure.

Lemma Lebesgue_sigma_additivity :
   (E : nat R Prop),
    ( n, measurable_L (E n))
    ( n p x, E n x E p x n = p)
    lambda_star (fun x n, E n x) =
      Sup_seq (fun Nsum_Rbar N (fun nlambda_star (E n))).
Proof.
intros.
rewrite cal_L_lambda_star_sigma_additivity; try easy.
intros; now apply cal_L_sigma_algebra.
Qed.

Definition Lebesgue_measure : measure cal_L :=
  mk_measure cal_L lambda_star
    lambda_star_emptyset lambda_star_nonneg Lebesgue_sigma_additivity.

Lemma Lebesgue_measure_is_length :
   a b,
    Lebesgue_measure (fun xa x b) = Rmax 0 (b - a)
    Lebesgue_measure (fun xa < x < b) = Rmax 0 (b - a)
    Lebesgue_measure (fun xa < x b) = Rmax 0 (b - a)
    Lebesgue_measure (fun xa x < b) = Rmax 0 (b - a).
Proof.
intros; repeat split.
apply lambda_star_int_cc.
apply lambda_star_int_oo.
apply lambda_star_int_oc.
apply lambda_star_int_co.
Qed.

Lemma Borel_Lebesgue_sigma_additivity :
   (E : nat R Prop),
    ( n, measurable_R (E n))
    ( n p x, E n x E p x n = p)
    lambda_star (fun x n, E n x) =
      Sup_seq (fun Nsum_Rbar N (fun nlambda_star (E n))).
Proof.
intros.
apply Lebesgue_sigma_additivity; try easy.
intros; now apply measurable_R_is_measurable_L.
Qed.

Definition Borel_Lebesgue_measure : measure gen_R :=
  mk_measure gen_R lambda_star
    lambda_star_emptyset lambda_star_nonneg Borel_Lebesgue_sigma_additivity.

Theorem Caratheodory :
   (mu : measure gen_R),
    ( a b, mu (fun xa < x b) = Rmax 0 (b - a))
     (A : R Prop),
      measurable gen_R A mu A = Borel_Lebesgue_measure A.
Proof.
assert (H : A, measurable gen_R A measurable gen_R_oc A).
intros; now rewrite measurable_R_equiv_oo, measurable_R_equiv_oc.

intros mu Hmu A HA.
rewrite (mk_measure_ext _ gen_R_oc H mu).
rewrite (mk_measure_ext _ gen_R_oc H Borel_Lebesgue_measure).
pose (U := fun n xIZR (bij_NZ n) - 1 < x IZR (bij_NZ n)).
apply measure_uniqueness with U.
5,6: simpl.
7: now apply H.
all: clear HA A H.
intros A B [a [ b Hab]] [c [d Hcd]].
(Rmax a c); (Rmin b d).
intros x; rewrite (Hab x), (Hcd x).
apply interval_inter_oc.
intros n; eexists; eexists; now unfold U.
intros n1 n2 x Hn1 Hn2.
rewrite <- (bij_ZNZ n1); rewrite <- (bij_ZNZ n2).
apply f_equal with (f := bij_ZN).
now apply archimed_ceil_uniq with x.
intros x; generalize (archimed_ceil_ex x); intros [n Hn].
(bij_ZN n); unfold U; now rewrite bij_NZN.
intros n; unfold U; now rewrite Hmu.
intros A [a [b H]].
rewrite measure_ext with (A2 := fun xa < x b); try easy.
rewrite lambda_star_ext with (B := fun xa < x b); try easy.
rewrite Hmu.
now rewrite lambda_star_int_oc.
Qed.

End Lebesgue_measure.

Section L_gen.

Lemma cal_L_lambda_star_0 :
   (E : R Prop), lambda_star E = 0 cal_L E.
Proof.
intros E HE.
apply cal_L_equiv_def; intros A.
rewrite <- Rbar_plus_0_l.
apply Rbar_plus_le_compat.
rewrite <- HE.
all: apply lambda_star_le; now intros.
Qed.

Definition L_gen : (R Prop) Prop :=
  fun Egen_R E lambda_star E = 0.

Definition measurable_L_gen : (R Prop) Prop := @measurable R L_gen.


End L_gen.

Section Lebesgue_measure_Facts.

Lemma Lebesgue_measure_is_sigma_finite_disj :
  is_sigma_finite_measure cal_L Lebesgue_measure.
Proof.
(fun n xIZR (bij_NZ n) x < IZR (bij_NZ n) + 1); repeat split.
intros; apply measurable_gen, cal_L_intco.
intros x; destruct (archimed_floor_ex x) as [z Hz].
(bij_ZN z); now rewrite bij_NZN.
intros n; rewrite is_finite_correct; 1.
edestruct Lebesgue_measure_is_length as [_ [_ [_ H]]]; rewrite H.
f_equal; rewrite Rmax_right; [ring | left; lra].
Defined.


Lemma Lebesgue_measure_is_diffuse :
  is_diffuse_measure Lebesgue_measure.
Proof.
intros x; apply lambda_star_singleton.
Qed.


Lemma Borel_Lebesgue_measure_is_diffuse :
  is_diffuse_measure Borel_Lebesgue_measure.
Proof.
apply Lebesgue_measure_is_diffuse.
Qed.

End Lebesgue_measure_Facts.