Library Lebesgue.measure

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

Description

References to pen-and-paper statements are from RR-9386-v2, https://hal.inria.fr/hal-03105815v2/
This file refers to Sections 11.1 and 11.2 (pp. 117-128), and 11.4 (pp. 131-132).
Some proof paths may differ.

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 Subsets Require Import Subsets_wDep Subset_seq.
From Lebesgue Require Import subset_compl Rbar_compl sum_Rbar_nonneg.
From Lebesgue Require Import sigma_algebra.

Local Open Scope R_scope.

Section Measure_def.

Context {E : Type}.
Variable gen : (E Prop) Prop.

Record measure := mk_measure {
  meas :> (E Prop) Rbar ;
  meas_emptyset : meas emptyset = 0 ;
  meas_nonneg: nonneg meas;
  meas_sigma_additivity :
     A : nat E Prop,
      ( n, measurable gen (A n))
      ( n m x, A n x A m x n = m)
      meas (fun x n, A n x) =
        Sup_seq (fun nsum_Rbar n (fun mmeas (A m)))
}.

Lemma measure_ext :
   (mu : measure) A1 A2, ( x, A1 x A2 x) mu A1 = mu A2.
Proof.
intros mu A1 A2 H.
f_equal; apply subset_ext; easy.
Qed.

Lemma measure_additivity_finite :
   (mu : measure) (A : nat E Prop) N,
    ( n, (n N)%nat measurable gen (A n))
    ( n m x, (n N)%nat (m N)%nat A n x A m x n = m)
    mu (fun x n, (n N)%nat A n x) = sum_Rbar N (fun mmu (A m)).
Proof.
intros mu A N H1 H2.
pose (B:= fun n (x:E) ⇒ match (le_lt_dec n N) with
    | left _A n x
    | right _False
  end).
assert (K1: i x, (i N)%nat B i x = A i x).
intros i x Hi.
unfold B; case (le_lt_dec _ _); intros T; try easy.
contradict T; auto with arith.
assert (K2: i x, (N < i)%nat B i x = False).
intros i x Hi.
unfold B; case (le_lt_dec _ _); intros T; try easy.
contradict T; auto with arith.
apply trans_eq with (mu (fun x : E n : nat, B n x)).
apply measure_ext.
intros x; split; intros (n,Hn).
n.
rewrite K1; try apply K1; apply Hn.
case (le_lt_dec n N); intros T.
n; split; try easy.
rewrite <- K1; easy.
exfalso.
rewrite <- (K2 n x); try easy.
rewrite meas_sigma_additivity.
rewrite Sup_seq_sum_Rbar_stable with
  (fun n : natmu (B n)) N.
apply sum_Rbar_ext.
intros i Hi; apply sym_eq, measure_ext.
intros x; rewrite K1; easy.
intros x; apply meas_nonneg.
intros i Hi.
rewrite <- meas_emptyset with mu.
apply sym_eq, measure_ext.
intros x; rewrite K2; auto; split; easy.
intros n; unfold B; case (le_lt_dec _ _); intros H.
apply H1; auto.
apply measurable_empty.
intros n p x J1 J2.
case (le_lt_dec n N); intros J3.
case (le_lt_dec p N); intros J4.
apply H2 with x; try easy.
rewrite K1 in J1; auto.
rewrite K1 in J2; auto.
contradict J2.
rewrite K2; auto with arith.
contradict J1.
rewrite K2; auto with arith.
Qed.

Lemma measure_additivity :
   (mu : measure) A1 A2,
    measurable gen A1 measurable gen A2
    ( x, A1 x A2 x False)
    mu (fun xA1 x A2 x) = Rbar_plus (mu A1) (mu A2).
Proof.
intros mu A0 A1 H0 H1 H.
pose (B := (fun nmatch n with | 0 ⇒ A0 | S _A1 end)).
replace (fun xA0 x A1 x) with (fun x n, (n 1)%nat B n x).
replace (Rbar_plus (mu A0) (mu A1)) with (sum_Rbar 1%nat (fun mmu (B m))).
apply measure_additivity_finite.
intros n Hn.
case n; simpl; [ now apply H0 | intros; now apply H1 ].
intros n m x Hn Hm Kn Km.
assert (Hn': n = 0%nat n = 1%nat); try lia.
assert (Hm': m = 0%nat m = 1%nat); try lia.
destruct Hn' as [Hn0|Hn1]; destruct Hm' as [Hm0|Hm1].
now rewrite Hn0, Hm0.
rewrite Hn0 in Kn; simpl in Kn.
rewrite Hm1 in Km; simpl in Km.
destruct (H x Kn Km).
rewrite Hn1 in Kn; simpl in Kn.
rewrite Hm0 in Km; simpl in Km.
destruct (H x Km Kn).
now rewrite Hn1, Hm1.
simpl; now rewrite Rbar_plus_comm.
apply subset_ext; intros x; split.
intros [n [Hn H']].
replace (A0 x) with (B 0%nat x); try auto.
replace (A1 x) with (B 1%nat x); try auto.
assert (Hn': n = 0%nat n = 1%nat); try lia.
now destruct Hn' as [Hn0|Hn1]; [ left; rewrite <- Hn0 | right; rewrite <- Hn1 ].
intros [K0|K1]; [ 0%nat | 1%nat ]; auto.
Qed.

Lemma measure_le_0_eq_0 :
   (mu : measure) A, measurable gen A Rbar_le (mu A) 0 mu A = 0.
Proof.
intros mu A H1 H2.
apply Rbar_le_antisym; try assumption.
now apply meas_nonneg.
Qed.

Lemma measure_gt_0_exists :
   (mu : measure) A, Rbar_lt 0 (mu A) x, A x.
Proof.
intros mu A H.
case (classic ( x : E, A x)); try easy.
intros H1.
absurd (Rbar_le (mu A) 0).
now apply Rbar_lt_not_le.
rewrite measure_ext with mu A (fun _False).
rewrite meas_emptyset.
apply Rbar_le_refl.
intros x; split; try easy.
intros H2; apply H1; x; easy.
Qed.

Lemma measure_decomp :
   (mu : measure) A (B : nat E Prop),
    measurable gen A
    ( n, measurable gen (B n))
    ( x, n, B n x)
    ( n p x, B n x B p x n = p)
    mu A = Sup_seq (fun N
      sum_Rbar N (fun nmu (fun xA x B n x))).
Proof.
intros mu A B H1 H2 H3 H4.
rewrite <- meas_sigma_additivity.
apply measure_ext.
intros x; split.
intros K; destruct (H3 x) as (n,Hn).
n; split; auto.
intros (n,(J1,J2)); auto.
intros n; apply measurable_inter; auto.
intros n m x (J1,J2) (J3,J4).
now apply H4 with x.
Qed.

Lemma measure_decomp_finite :
   (mu : measure) A N (B : nat E Prop),
    measurable gen A
    ( n, (n N)%nat measurable gen (B n))
    ( x, n, (n N)%nat B n x)
    ( n p x, (n N)%nat (p N)%nat
      B n x B p x n = p)
    mu A = sum_Rbar N (fun nmu (fun xA x B n x)).
Proof.
intros mu A N B H1 H2 H3 H4.
rewrite <- measure_additivity_finite.
apply measure_ext.
intros x; split.
intros Hx; destruct (H3 x) as (n,(Hn1,Hn2)).
n; repeat split; auto.
intros (n,(Hn1,(Hn2,Hn3))); easy.
intros n Hn; apply measurable_inter; try easy.
now apply H2.
intros n m x J1 J2 (J3,J4) (J5,J6).
now apply (H4 n m x).
Qed.

Lemma measure_le_aux :
   (mu : measure) A B,
    measurable gen A measurable gen B
    ( x, A x B x)
    mu B = Rbar_plus (mu (fun xB x ¬ A x)) (mu A).
Proof.
intros mu A B HA HB H.
pose (C := fun x : EB x ¬ A x).
replace (fun x : EB x ¬ A x) with C; try easy.
replace B with (fun xC x A x).
apply measure_additivity; try easy.
now apply measurable_inter; [ | apply measurable_compl_rev ].
intros x KC KA; unfold C in KC; now contradict KC.
apply subset_ext; intros x; split.
intros [[KB KA']|KA]; auto.
now intros KB; case (in_dec A x); intros KA; [ right | left ].
Qed.

Lemma measure_le :
   (mu : measure) A B,
    measurable gen A measurable gen B
    ( x, A x B x)
    Rbar_le (mu A) (mu B).
Proof.
intros mu A B HA HB H.
replace (mu A) with (Rbar_plus 0 (mu A)); try now apply Rbar_plus_0_l.
replace (mu B) with (Rbar_plus (mu (fun xB x ¬ A x)) (mu A)).
apply Rbar_plus_le_compat_r; now apply meas_nonneg.
symmetry; now apply measure_le_aux.
Qed.

Lemma measure_set_diff :
   (mu : measure) A B,
    measurable gen A measurable gen B
    ( x, A x B x)
    is_finite (mu A)
    mu (fun xB x ¬ A x) = Rbar_minus (mu B) (mu A).
Proof.
intros mu A B HA HB H H'.
rewrite measure_le_aux with mu A B; try easy.
now apply Rbar_minus_plus_r.
Qed.

Lemma measure_set_not :
   mu : measure,
     A, measurable gen A is_finite (mu A)
      mu (fun t¬A t) = Rbar_minus (mu (fun _True)) (mu A).
Proof.
intros mu A HA1 HA2.
rewrite <- measure_set_diff; try easy.
apply measure_ext; try easy.
apply measurable_full.
Qed.

Lemma measure_Boole_ineq_finite :
   (mu : measure) (A : nat E Prop) N,
    ( n, (n N)%nat measurable gen (A n))
    Rbar_le (mu (fun x n, (n N)%nat A n x))
            (sum_Rbar N (fun mmu (A m))).
Proof.
intros mu A.
induction N; intros H.
apply Rbar_eq_le; unfold sum_Rbar.
f_equal; apply subset_ext; intros x; split.
intros [n [Hn K]].
replace 0%nat with n; [ easy | lia ].
intros K; now 0%nat.
pose (B := fun x n, (n N)%nat A n x).
replace (fun x n, (n S N)%nat A n x)
  with (fun xA (S N) x B x).
simpl.
replace (fun xA (S N) x B x)
    with (fun xA (S N) x ¬ B x B x).
replace (mu (fun xA (S N) x ¬ B x B x))
    with (Rbar_plus (mu (fun xA (S N) x ¬ B x)) (mu B)).
apply Rbar_plus_le_compat.
apply measure_le; try now apply H.
apply measurable_inter; try now apply H.
apply measurable_compl_rev, measurable_union_finite; intros n Hn; apply H; auto.
now intros x [HSN HN'].
apply IHN; intros n Hn; apply H; auto.
apply sym_eq, measure_additivity.
apply measurable_inter; try now apply H.
apply measurable_compl_rev, measurable_union_finite; intros n Hn; apply H; auto.
apply measurable_union_finite; intros n Hn; apply H; auto.
intros x [HSN HN'] HN; auto.
apply subset_ext; intros x; split; tauto.
apply subset_ext; intros x; split.
now intros [HSN|[n [HN K]]]; [ (S N) | n; split; [ lia | ] ].
intros [n [Hn K]]; case (in_dec (A (S N)) x); intros HSN.
now left.
right; n; split; try easy; case (Nat.eq_dec n (S N)); intros J.
contradict HSN; now rewrite <- J.
apply Nat.lt_succ_r; now destruct Hn; [ | auto with arith ].
Qed.

Lemma measure_union :
   (mu : measure) A1 A2,
    measurable gen A1 measurable gen A2
    Rbar_le (mu (fun xA1 x A2 x)) (Rbar_plus (mu A1) (mu A2)).
Proof.
intros mu A0 A1 H0 H1.
pose (B := (fun nmatch n with | 0 ⇒ A0 | S _A1 end)).
replace (fun xA0 x A1 x) with (fun x n, (n 1)%nat B n x).
replace (Rbar_plus (mu A0) (mu A1)) with (sum_Rbar 1%nat (fun mmu (B m))).
apply measure_Boole_ineq_finite.
intros n Hn.
now case n; simpl; [ apply H0 | intros; apply H1 ].
simpl; now rewrite Rbar_plus_comm.
apply subset_ext; intros x; split.
intros [n [Hn H]].
replace (A0 x) with (B 0%nat x) by auto.
replace (A1 x) with (B 1%nat x) by auto.
assert (Hn': n = 0%nat n = 1%nat) by lia.
now destruct Hn' as [Hn0|Hn1]; [ left; rewrite <- Hn0 | right; rewrite <- Hn1 ].
intros [K0|K1]; [ 0%nat | 1%nat ]; auto.
Qed.

Definition continuous_from_below : ((E Prop) Rbar) Prop :=
  fun mu A : nat E Prop,
    ( n, measurable gen (A n))
    ( n x, A n x A (S n) x)
    mu (fun x n, A n x) = Sup_seq (fun nmu (A n)).

Lemma measure_continuous_from_below :
     (mu : measure), continuous_from_below mu.
Proof.
intros mu; unfold continuous_from_below; intros A HA HA'.
pose (B := layers A).
replace (fun x n, A n x)
    with (fun x n : nat, B n x).
replace (fun nmu (A n))
    with (fun nmu (fun x m, (m n)%nat B m x)).
rewrite meas_sigma_additivity; try now apply measurable_layers.
replace (fun nmu (fun x m, (m n)%nat B m x))
    with (fun nsum_Rbar n (fun mmu (B m))); try easy.
apply fun_ext; intros n; symmetry; apply measure_additivity_finite.
intros; now apply measurable_layers.
intros n' m' x Hn' Hm' HBn' HBm'; now apply layers_disjoint with A x.
now apply layers_disjoint.
apply fun_ext; intros n; f_equal.
apply subset_ext; intros x; split.
  now apply layers_union_alt.
  now apply layers_union.
symmetry; apply subset_ext; intros x; split.
now apply layers_union_countable.
intros [n HBn]; n; now apply layers_incl.
Qed.

Lemma subset_decr_shift_meas_finite :
   (mu : measure) (A : nat E Prop),
    ( n x, A (S n) x A n x)
    ( n, measurable gen (A n))
     n0, is_finite (mu (A n0))
     n, is_finite (mu (A (n0 + n)%nat)).
Proof.
intros mu A HA HAn n0 HAn0 n.
apply Rbar_bounded_is_finite with 0 (mu (A n0)); try easy.
apply meas_nonneg.
apply measure_le; try easy; now apply subset_decr_shift.
Qed.

Lemma layers_from_above_measurable :
   A : nat E Prop,
    ( n, measurable gen (A n))
     n0 n, measurable gen (layers_from_above A n0 n).
Proof.
intros A HA n0 n.
now apply measurable_inter, measurable_compl_rev.
Qed.

Lemma layers_from_above_sup_seq :
   (mu : measure) (A : nat E Prop),
    ( n x, A (S n) x A n x)
    ( n, measurable gen (A n))
     n0,
      is_finite (mu (A n0))
      Sup_seq (fun nmu (layers_from_above A n0 n)) =
        Rbar_minus (mu (A n0)) (Inf_seq (fun nmu (A (n0 + n)%nat))).
Proof.
intros mu A HA HAn n0 HAn0.
unfold layers_from_above.
replace (Sup_seq (fun nmu (fun xA n0 x ¬ A (n0 + n)%nat x)))
    with (Sup_seq (fun nRbar_minus (mu (A n0)) (mu (A (n0 + n)%nat)))).
apply Sup_seq_minus_compat_l; try easy.
apply Sup_seq_ext; intros n; symmetry.
rewrite <- measure_set_diff; try easy.
now apply subset_decr_shift.
now apply subset_decr_shift_meas_finite.
Qed.

Definition is_continuous_from_above : ((E Prop) Rbar) Prop :=
  fun mu A : nat E Prop,
    ( n x, A (S n) x A n x)
    ( n, measurable gen (A n))
    ( n0, is_finite (mu (A n0)))
    mu (fun x n, A n x) = Inf_seq (fun nmu (A n)).

Lemma measure_continuous_from_above :
     (mu : measure), is_continuous_from_above mu.
Proof.
intros mu A HA HAn [n0 HAn0].
replace (fun x : E n, A n x)
    with (fun x : E n, A (n0 + n)%nat x).
replace (Inf_seq (fun nmu (A n)))
    with (Inf_seq (fun nmu (A (n0 + n)%nat))).
apply Rbar_minus_eq_reg_l with (mu (A n0)); try easy.
rewrite <- measure_set_diff; try easy.
rewrite <- layers_from_above_sup_seq; try easy.
replace (fun xA n0 x ¬ ( n : nat, A (n0 + n)%nat x))
    with (fun x n1, layers_from_above A n0 n1 x).
apply measure_continuous_from_below.

now apply layers_from_above_measurable.
now apply layers_from_above_incr.
apply subset_ext; intros x; now apply layers_from_above_union.
now apply measurable_inter_countable.
intros x Hx; replace n0 with (n0 + 0)%nat; [easy|ring].
apply Rbar_bounded_is_finite with 0 (mu (A n0)); try easy.
  apply meas_nonneg.
  apply measure_le; try easy.
  now apply measurable_inter_countable.
  intros x Hx; replace n0 with (n0 + 0)%nat; [easy|ring].
apply Inf_seq_decr_shift with (u := fun nmu (A n)); intros n;
    apply measure_le; try easy; apply HA.
apply subset_ext; intros x; split; intros H n; try easy.
  case (Nat.le_gt_cases n0 n); intros Hn.
  replace n with (n0 + (n - n0))%nat; [easy|auto with arith].
  apply subset_decr_shift with (n0 - n)%nat; try easy.
  replace (n + (n0 - n))%nat with (n0 + 0)%nat; [easy|lia].
Qed.

Lemma partial_union_measurable :
   A : nat E Prop,
    ( n, measurable gen (A n))
     n, measurable gen (partial_union A n).
Proof.
intros A HA n.
apply measurable_union_countable.
intros m; apply measurable_inter; try easy.
case (le_lt_dec m n); intros Hm.
  apply measurable_ext with (2:=measurable_full _); now intros.
  apply measurable_ext with (2:=measurable_empty _); intros.
  split; intros H; [ easy | contradict H; lia ].
Qed.

Lemma partial_union_union_measure :
   (mu : measure) (A : nat E Prop),
    ( n, measurable gen (A n))
    mu (fun x n, partial_union A n x) =
      Sup_seq (fun nmu (partial_union A n)).
Proof.
intros mu A HA.
apply measure_continuous_from_below.
now apply partial_union_measurable.
apply partial_union_nondecr.
Qed.

Lemma measure_Boole_ineq :
   (mu : measure) (A : nat E Prop),
    ( n, measurable gen (A n))
    Rbar_le (mu (fun x n, A n x))
            (Sup_seq (fun nsum_Rbar n (fun mmu (A m)))).
Proof.
intros mu A HA.
replace (fun x n, A n x)
  with (fun x n, partial_union A n x).
rewrite partial_union_union_measure; try easy.
apply Sup_seq_le.
intros n; now apply measure_Boole_ineq_finite.
symmetry; apply subset_ext; intros x.
apply partial_union_union.
Qed.

Definition is_finite_measure : ((E Prop) Rbar) Prop :=
  fun muis_finite (mu (fun _True)).

Lemma finite_measure_is_finite :
   (mu : measure), is_finite_measure mu
     A, measurable gen A is_finite (mu A).
Proof.
intros mu Hmu A HA.
apply Rbar_bounded_is_finite with (x := 0) (z := mu (fun _True)); try easy.
apply meas_nonneg.
apply measure_le; try easy.
apply measurable_full.
Qed.

Definition is_sigma_finite_measure : ((E Prop) Rbar) Prop :=
  fun mu A : nat E Prop,
    ( n, measurable gen (A n))
    ( x, n, A n x)
    ( n, is_finite (mu (A n))).

Lemma finite_measure_is_sigma_finite :
   mu : (E Prop) Rbar,
    is_finite_measure mu
    is_sigma_finite_measure mu.
Proof.
intros mu Hmu; (fun _ _True).
split; [ | split]; intros _; try easy.
apply measurable_full.
now 0%nat.
Qed.


Lemma is_sigma_finite_measure_equiv_def :
   (mu : measure),
  (is_sigma_finite_measure mu
    ( A : nat E Prop,
      ( n, measurable gen (A n))
      ( x, n, A n x)
      ( n x, A n x A (S n) x)
      ( n, is_finite (mu (A n))))).
Proof.
intros mu.
split; intros H1.
unfold is_sigma_finite_measure in H1.
destruct H1 as [A [H2 [H3 H4]]].
(partial_union A); repeat split.
apply partial_union_measurable; easy.
intros x; rewrite <- partial_union_union; easy.
apply partial_union_nondecr.
intros n; eapply (Rbar_bounded_is_finite 0).
apply meas_nonneg.
apply measure_Boole_ineq_finite; easy.
easy.
induction n; simpl.
apply H4.
rewrite <- IHn.
rewrite <- (H4 (S n)); easy.
destruct H1 as [A H].
A; easy.
Qed.

Definition is_diffuse_measure : ((E Prop) Rbar) Prop :=
   fun mu x, mu (fun zz = x) = 0.

Definition meas_restricted_meas (mu : (E Prop) Rbar) (A : E Prop) :=
    fun (B : E Prop) ⇒
         mu (fun x : EA x B x).

Variable mu : measure.

Lemma meas_restricted_emptyset :
   A, meas_restricted_meas mu A emptyset = 0.
Proof.
intros A; unfold meas_restricted_meas.
erewrite measure_ext.
apply meas_emptyset.
intros x; split; easy.
Qed.

Lemma meas_restricted_nonneg :
   A, nonneg (meas_restricted_meas mu A).
Proof.
intros A B; apply meas_nonneg.
Qed.

Lemma meas_restricted_sigma_additivity :
   A, measurable gen A
   ( B : nat E Prop,
     ( n, measurable gen (B n))
     ( n m x, B n x B m x n = m)
     meas_restricted_meas mu A (fun x n, B n x) =
        Sup_seq (fun nsum_Rbar n (fun mmeas_restricted_meas mu A (B m)))).
Proof.
intros A HA B H1 H2.
unfold meas_restricted_meas.
rewrite <- meas_sigma_additivity.
f_equal; apply (inter_union_seq_distr_l A B).
intros n; apply measurable_inter; try easy.
intros n m x2 H5 H6; apply (H2 n m x2).
apply H5.
apply H6.
Qed.

Definition meas_restricted : A, measurable gen A measure :=
   fun A HA
     mk_measure (meas_restricted_meas mu A)
       (meas_restricted_emptyset A)
       (meas_restricted_nonneg A)
       (meas_restricted_sigma_additivity A HA).


End Measure_def.

Section More_Measure_Facts.

Context {E : Type}.

Variable gen gen1 gen2 : (E Prop) Prop.

Hypothesis Hgen :
     (A : E Prop), measurable gen1 A measurable gen2 A.

Lemma measure_gen_sigma_additivity :
   (mu : measure gen1) (A : nat E Prop),
    ( n, measurable gen2 (A n))
    ( n m x, A n x A m x n = m)
    mu (fun x n, A n x) =
      Sup_seq (fun nsum_Rbar n (fun pmu (A p))).
Proof.
intros mu A HA1 HA2.
apply (meas_sigma_additivity _ mu); try easy.
intros n; now rewrite Hgen.
Qed.

Definition mk_measure_gen : measure gen1 measure gen2 :=
  fun (mu : measure gen1) ⇒
    mk_measure gen2 mu
      (meas_emptyset _ mu) (meas_nonneg _ mu) (measure_gen_sigma_additivity mu).

Lemma mk_measure_ext :
   (mu : measure gen1) (A : E Prop), mu A = mk_measure_gen mu A.
Proof.
easy.
Qed.

Definition sub_measure_meas :
    ((E Prop) Rbar) (E Prop) (E Prop) Rbar :=
  fun mu U Amu (fun xA x U x).

Lemma sub_measure_emptyset :
   (mu : measure gen) (U : E Prop),
    let mu_U := sub_measure_meas mu U in
    mu_U emptyset = 0.
Proof.
intros.
unfold mu_U, sub_measure_meas.
rewrite measure_ext with (A2 := emptyset); try easy.
apply meas_emptyset.
Qed.

Lemma sub_measure_nonneg :
   (mu : measure gen) (U : E Prop),
    let mu_U := sub_measure_meas mu U in
    nonneg mu_U.
Proof.
intros; intros A; apply meas_nonneg.
Qed.

Lemma sub_measure_sigma_additivity :
   (mu : measure gen) (U : E Prop) (HU : measurable gen U)
      (A : nat E Prop),
    ( n, measurable gen (A n))
    ( n m x, A n x A m x n = m)
    let mu_U := sub_measure_meas mu U in
    mu_U (fun x n, A n x) =
      Sup_seq (fun nsum_Rbar n (fun pmu_U (A p))).
Proof.
intros mu U HU A HA1 HA2 mu_U.
unfold mu_U, sub_measure_meas.
rewrite measure_ext with (A2 := fun x n, A n x U x).
apply (meas_sigma_additivity _ mu).
intros n; now apply measurable_inter.
intros n m x [Hn _] [Hm _]; now apply (HA2 _ _ x).
intros x; split.
intros [[n Hn] H]; now n.
intros [n [Hn H]]; split; [now n | easy].
Qed.

Definition mk_sub_measure :=
  fun (mu : measure gen) (U : E Prop) (HU : measurable gen U) ⇒
    let mu_U := sub_measure_meas mu U in
    mk_measure gen (sub_measure_meas mu U)
      (sub_measure_emptyset mu U) (sub_measure_nonneg mu U)
      (sub_measure_sigma_additivity mu U HU).

End More_Measure_Facts.

Section Negligible_subset.

Context {E F : Type}.
Context {gen : (E Prop) Prop}.
Variable mu : measure gen.

Definition negligible : (E Prop) Prop :=
  fun f A : E Prop,
    ( x, f x A x)
    (measurable gen A)
    mu A = 0.

Lemma negligible_null_set :
   A, measurable gen A mu A = 0 negligible A.
Proof.
intros A H1 H2; A; repeat split; easy.
Qed.

Lemma negligible_emptyset : negligible (fun _False).
Proof.
apply negligible_null_set.
apply measurable_empty.
apply (meas_emptyset).
Qed.

Lemma negligible_ext :
   A1 A2, ( x, A1 x A2 x) negligible A1 negligible A2.
Proof.
intros A1 A2 H (f,(J1,(J2,J3))).
f; split; try split; try easy.
intros x Hx; now apply J1,H.
Qed.

Lemma negligible_le :
   (A1 A2 : E Prop),
    ( x, A1 x A2 x)
    negligible A2 negligible A1.
Proof.
intros A1 A2 H (f,(J1,(J2,J3))).
f; split; try split; try easy.
intros x Hx; now apply J1, H.
Qed.

Lemma negligible_union_countable :
   A : nat E Prop,
    ( n, negligible (A n))
    negligible (fun x n, A n x).
Proof.
intros A Hn.
assert ( f: nat E Prop, n,
   ( x:E, A n x f n x) (measurable gen (f n))
       mu (f n) = 0).
destruct (choice
  (fun (n:nat) (g:EProp) ⇒
      ( x : E, A n x g x)
         measurable gen g mu g = 0)).
intros n.
destruct (Hn n) as (f,(J1,(J2,J3))).
f; repeat split; easy.
x; easy.
destruct H as (f,Hf).
(fun x n, f n x).
split.
intros x (n,Kn).
n; now apply Hf.
split.
apply measurable_union_countable.
intros n; apply Hf.
apply measure_le_0_eq_0.
apply measurable_union_countable.
intros n; apply Hf.
replace (Finite 0) with
  (Sup_seq (fun nsum_Rbar n (fun mmu (f m)))).
apply measure_Boole_ineq.
intros n; apply Hf.
apply trans_eq with (Sup_seq (fun _ ⇒ 0)).
apply Sup_seq_ext.
intros n; induction n; simpl.
apply Hf.
rewrite IHn.
rewrite (proj2 (proj2 (Hf (S n)))).
simpl; now rewrite Rplus_0_r.
apply is_sup_seq_unique.
simpl; intros eps; split.
intros _; rewrite Rplus_0_l.
apply eps.
0%nat.
rewrite Rminus_0_l, <- Ropp_0.
apply Ropp_lt_contravar, eps.
Qed.

Lemma negligible_union:
   A1 A2,
    negligible A1 negligible A2
    negligible (fun xA1 x A2 x).
Proof.
intros A1 A2 (f1,(J11,(J12,J13))) (f2,(J21,(J22,J23))).
(fun xf1 x f2 x); split; try split.
intros x [H1|H2].
left; now apply J11.
right;now apply J21.
now apply measurable_union.
eapply measure_le_0_eq_0.
apply measurable_union.
apply J12.
apply J22.
assert ((Finite 0)=(Rbar_plus (mu f1) (mu f2))).
rewrite J23;rewrite J13;symmetry;now rewrite Rbar_plus_0_r.
rewrite H.
apply (measure_union gen mu f1 f2 J12 J22).
Qed.

Definition ae : (E Prop) Prop := fun Anegligible (fun x¬ A x).

Lemma ae_ext : A1 A2, ( x, A1 x A2 x) ae A1 ae A2.
Proof.
intros A1 A2 H HA1.
unfold ae.
unfold ae in HA1.
apply (negligible_ext (fun x : E¬ A1 x)
  (fun x : E¬ A2 x));auto.
red.
red in H.
intro.
split;destruct (H x) as (H1,H2);auto.
Qed.

Lemma ae_everywhere : (A : E Prop), ( x, A x) ae A.
Proof.
intros A H.
destruct negligible_emptyset as [B [H1 [H2 H3]]].
B; repeat split; try easy.
intuition.
Qed.

Lemma ae_everywhere_alt :
   (P : F Prop) (f g : E F),
    ( x, P (f x))
    ae (fun xf x = g x)
    ae (fun xP (g x)).
Proof.
intros P f g HP Hfg.
apply negligible_le with (A2 := fun x¬ P (f x) ¬ f x = g x).
intros x Hx1; right; intros Hx2; apply Hx1; now rewrite <- Hx2.
apply negligible_union; try easy.
apply negligible_ext with (A1 := fun _False); try intuition.
apply negligible_emptyset.
Qed.

Lemma ae_modus_ponens_gen :
   (P Q : nat (nat F) Prop),
    ( f, ae (fun x( j, P j (fun if i x))
                            ( k, Q k (fun if i x))))
     f, ( j, ae (fun xP j (fun if i x)))
              ( k, ae (fun xQ k (fun if i x))).
Proof.
intros P Q H f HP k.
pose (PP := fun f j, P j f).
pose (QQ := fun f k, Q k f).
pose (Ax := fun (XX : (nat F) Prop) f (x : E) ⇒ XX (fun if i x)).
pose (B := fun x(Ax PP f x Ax QQ f x) Ax PP f x).
apply negligible_le with (fun x¬ (Ax PP f x Ax QQ f x) ¬ Ax PP f x).
intros x HQ; apply not_and_or; intuition.
apply negligible_union; unfold Ax, PP, QQ.
unfold ae in H; try easy.
apply negligible_ext with (fun x j, ¬ P j (fun if i x)).
intros; split; [apply ex_not_not_all | apply not_all_ex_not].
apply negligible_union_countable; easy.
Qed.

Lemma ae_imply_gen :
   (P Q : nat (nat F) Prop),
    ( (f : nat E F) x,
      ( j, P j (fun if i x)) ( k, Q k (fun if i x)))
     f, ( j, ae (fun xP j (fun if i x)))
              ( k, ae (fun xQ k (fun if i x))).
Proof.
intros P Q H; apply ae_modus_ponens_gen; intros f.
apply ae_everywhere; auto.
Qed.

Lemma ae_modus_ponens :
   (A1 A2 : E Prop), ae (fun xA1 x A2 x) ae A1 ae A2.
Proof.
intros A1 A2 H H1.
apply negligible_le with (A2 := fun x¬ (A1 x A2 x) ¬ A1 x).
intros; tauto.
now apply negligible_union.
Qed.

Lemma ae_imply :
   (A1 A2 : E Prop), ( x, A1 x A2 x) ae A1 ae A2.
Proof.
intros A1 A2 H; apply ae_modus_ponens.
now apply ae_everywhere.
Qed.

Lemma ae_True : ae (fun _True).
Proof.
now apply ae_everywhere.
Qed.

Lemma ae_inter_countable :
   A : nat E Prop,
    ( n, ae (A n))
    ae (fun x n, A n x).
Proof.
intros A H1; unfold ae.
apply negligible_ext with
  (fun x : E n : nat, ¬ A n x).
intros x; split.
intros (n,Hn) H.
apply Hn, H.
apply not_all_ex_not.
apply negligible_union_countable.
apply H1.
Qed.

Lemma ae_inter : A B, ae A ae B ae (fun xA x B x).
Proof.
intros A B HA HB.
pose (C := fun n xmatch n with | 0 ⇒ A x | S _B x end).
apply ae_ext with (fun x n, C n x).
intros x; split.
intros Hx; split; [apply (Hx 0%nat) | apply (Hx 1%nat)].
intros [Hx1 Hx2]; intros n; now destruct n.
apply ae_inter_countable; intros n; now destruct n.
Qed.

Global Instance ae_filter : Filter ae.
Proof.
constructor.
exact ae_True.
exact ae_inter.
exact ae_imply.
Qed.

Lemma ae_not_empty : mu (fun _True) 0 ¬ ae (fun _False).
Proof.
intros H [A [HA1 [HA2 HA3]]].
apply H; rewrite <- HA3.
apply measure_ext; intros; split; try easy.
intros; now apply HA1.
Qed.

Global Instance ae_properfilter' : mu (fun _True) 0 ProperFilter' ae.
Proof.
intros.
constructor.
now apply ae_not_empty.
exact ae_filter.
Qed.

Lemma ae_ex : mu (fun _True) 0 A, ae A x, A x.
Proof.
intros H; apply ae_not_empty in H; intros A HA1.
apply not_all_not_ex; intros HA2; apply H.
apply ae_ext with A; try easy.
intros; split; try easy.
intros; now apply (HA2 x).
Qed.

Global Instance ae_properfilter : mu (fun _True) 0 ProperFilter ae.
Proof.
constructor.
now apply ae_ex.
exact ae_filter.
Qed.

Definition ae_rel : (F F Prop) (E F) (E F) Prop :=
  fun P f gae (fun xP (f x) (g x)).

Lemma ae_rel_refl :
   (P : F F Prop) (f : E F),
    ( y, P y y)
    ae_rel P f f.
Proof.
intros; now apply ae_everywhere.
Qed.

Lemma ae_rel_sym :
   (P : F F Prop) (f g : E F),
    ( y z, P y z P z y)
    ae_rel P f g ae_rel P g f.
Proof.
intros P f g H.
apply ae_imply.
intros; now apply H.
Qed.

Definition ae_eq : (E F) (E F) Prop := fun f gae_rel eq f g.

Lemma ae_eq_refl : f, ae_eq f f.
Proof.
intros; now apply ae_rel_refl.
Qed.

Lemma ae_eq_sym : f g, ae_eq f g ae_eq g f.
Proof.
intros; now apply ae_rel_sym.
Qed.

Lemma ae_eq_trans : f g h, ae_eq f g ae_eq g h
    ae_eq f h.
Proof.
intros f g h; unfold ae_eq, ae.
intros H1 H2.
apply negligible_le with
   (fun x(f x g x) (g x h x)).
intros x K.
case (classic (f x = g x)); intros K'.
right; rewrite <- K'; easy.
left; easy.
apply negligible_union; easy.
Qed.

End Negligible_subset.

Section Negligible_subset_bis.

Context {E : Type}.
Context {F : Type}.
Context {gen : (E Prop) Prop}.
Variable mu : measure gen.

Lemma ae_op_compat_new :
   (R1 R2 : F F Prop) (op : (nat F) F),
    ( (f g : nat E F) x,
      ( n, R1 (f n x) (g n x))
      R2 (op (fun if i x)) (op (fun ig i x)))
    ( (f g : nat E F),
      ( n, ae mu (fun xR1 (f n x) (g n x)))
      ae mu (fun xR2 (op (fun if i x)) (op (fun ig i x)))).
Proof.
intros R1 R2 op H f g H1.
pose (Q := fun k fgmatch k with
  | 0%natR2 (op (fun ifst (fg i))) (op (fun isnd (fg i)))
  | S _True
  end).
apply ae_ext with (fun xQ 0%nat (fun i(f i x, g i x))); try easy.
assert (HQ : k, ae mu (fun xQ k (fun i(f i x, g i x)))); try easy.
pose (P := fun j fgmatch j with
  | 0%nat i : nat, R1 (fst (fg i)) (snd (fg i))
  | S _True
  end).
apply ae_imply_gen with P.
intros fg x HP k; destruct k; try easy; simpl.
apply H with (f := fun i xfst (fg i x)) (g := fun i xsnd (fg i x)).
apply (HP 0%nat).
intros j; destruct j; simpl; try apply ae_True.
apply ae_inter_countable; easy.
Qed.

Lemma ae_op_compat :
   (P Q : F F Prop) (op : (nat F) F) (y0 : F),
    ( x, P x x)
    ( (f g : nat E F),
      ( n x, P (f n x) (g n x))
       x, Q (op (fun if i x)) (op (fun ig i x)))
    ( (f g : nat E F),
      ( n, ae mu (fun xP (f n x) (g n x)))
      ae mu (fun xQ (op (fun if i x)) (op (fun ig i x)))).
Proof.
intros P Q op y0 H1 H2 f g H3.
pose (B_i := fun i ⇒ (fun xP (f i x) (g i x))).
pose (B := fun x i, B_i i x).
pose (f_t := fun i x
        match (in_dec B x) with
     | left _f i x
     | right _y0
  end).
pose (g_t := fun i x
        match (in_dec B x) with
     | left _g i x
     | right _y0
  end).
assert (J0: i, ae mu (B_i i)).
intros i; unfold B_i.
apply H3.
assert (J1: ae mu B).
now apply ae_inter_countable.
assert (J2: i x, P (f_t i x) (g_t i x)).
intros i x; unfold f_t, g_t.
case (in_dec B x); intros Hx.
2: apply H1.
apply Hx.
generalize (H2 _ _ J2); intros H5.
assert (J3: x, B x
   op (fun i : natf_t i x) = op (fun i : natf i x)).
intros x Hx.
f_equal; apply fun_ext.
intros i; unfold f_t.
case (in_dec B x); easy.
assert (J4: x, B x
   op (fun i : natg_t i x) = op (fun i : natg i x)).
intros x Hx.
f_equal; apply fun_ext.
intros i; unfold g_t.
case (in_dec B x); easy.
apply ae_imply with B; try assumption.
intros x Hx.
rewrite <- J3, <- J4; try assumption.
now apply H5.
Qed.

Lemma ae_op_eq_compat :
   (op : (nat F) F) (y0 : F) (f g : nat E F),
  ( n, ae mu (fun xf n x = g n x))
    ae mu (fun xop (fun if i x) = op (fun ig i x)).
Proof.
intros op y0 f g H1.
apply ae_op_compat with eq; try easy.
clear; intros f g H x.
f_equal; apply fun_ext; easy.
Qed.

Lemma ae_op1_eq_compat :
   (op : F F) (y0 : F) (f g : E F),
    ae mu (fun xf x = g x) ae mu (fun xop (f x) = op (g x)).
Proof.
intros op y0 f g H.
pose (op' := fun h'op (h' 0%nat)).
pose (f' := fun nmatch n with | 0%natf | S _fun _y0 end).
pose (g' := fun nmatch n with | 0%natg | S _fun _y0 end).
apply ae_ext with (A1 := fun xop' (fun if' i x) = op' (fun ig' i x)).
now intros x.
apply ae_op_eq_compat; try easy.
intros n; case n; try easy.
intros n'.
apply ae_ext with (fun _True); try now intros.
apply ae_True.
Qed.

Lemma ae_op2_eq_compat :
   (op : F F F) (y0 : F) (f1 f2 g1 g2 : E F),
    ae mu (fun xf1 x = g1 x)
    ae mu (fun xf2 x = g2 x)
    ae mu (fun xop (f1 x) (f2 x) = op (g1 x) (g2 x)).
Proof.
intros op y0 f1 f2 g1 g2 H1 H2.
pose (op' := fun h'op (h' 0%nat) (h' 1%nat)).
pose (f' := fun nmatch n with | 0%natf1 | 1%natf2 | S (S _) ⇒ fun _y0 end).
pose (g' := fun nmatch n with | 0%natg1 | 1%natg2 | S (S _) ⇒ fun _y0 end).
apply ae_ext with (A1 := fun xop' (fun if' i x) = op' (fun ig' i x)).
now intros x.
apply ae_op_eq_compat; try easy.
intros n; case n; try easy.
intros n'; case n'; try easy.
intros n''.
apply ae_ext with (fun _True); try now intros.
apply ae_True.
Qed.


Lemma ae_definite_compat :
   (op : F F) (y0 : F),
    ( y, op y = op y0 y = y0)
     f : E F,
      ae_eq mu (fun xop (f x)) (fun _op y0)
      ae_eq mu f (fun _y0).
Proof.
intros op y0 H f; apply ae_imply.
intros; now apply H.
Qed.

End Negligible_subset_bis.

Section Dirac_measure.

Context {E : Type}.

Variable gen : (E Prop) Prop.

Definition Dirac : E (E Prop) Rbar := fun a Acharac A a.

Lemma Dirac_emptyset : a, Dirac a emptyset = 0.
Proof.
intros a; now apply Rbar_finite_eq, charac_is_0.
Qed.

Lemma Dirac_nonneg : a, nonneg (Dirac a).
Proof.
intros a A; unfold Dirac.
case (in_dec A a); intros Ha.
rewrite charac_is_1; try assumption; simpl; apply Rle_0_1.
rewrite charac_is_0; try assumption; apply Rbar_le_refl.
Qed.

Lemma Dirac_sigma_additivity :
   a A,
    ( n, measurable gen (A n))
    ( n m x, A n x A m x n = m)
    Dirac a (fun x n, A n x) =
      Sup_seq (fun nsum_Rbar n (fun mDirac a (A m))).
Proof.
intros a A HA1 HA2.
unfold Dirac.
case (classic ( n0, A n0 a)); intros Ha.
rewrite charac_is_1; try assumption.
destruct Ha as [n0 Ha].
rewrite Sup_seq_sum_Rbar_singl with _ n0.
rewrite charac_is_1; easy.
intros n; replace (Finite (charac (A n) a)) with (Dirac a (A n));
    try easy; apply Dirac_nonneg.
intros n Hn; rewrite charac_is_0; try easy;
    intros HA'; contradict Hn; now apply HA2 with a.
assert (H0 : n, sum_Rbar n (fun m : natcharac (A m) a) = 0).
intros n; apply sum_Rbar_0; intros i.
rewrite charac_is_0; try easy.
intros HA'; contradict Ha; i; assumption.

rewrite charac_is_0; try assumption.
rewrite Sup_seq_stable with _ 0%nat.
simpl; rewrite charac_is_0; try easy;
    intros H; apply Ha; 0%nat; assumption.
intros n; repeat rewrite H0; simpl; auto with real.
intros n Hn; repeat rewrite H0; simpl; auto with real.
Qed.

Definition Dirac_measure (a : E) :=
    mk_measure gen (Dirac a)
      (Dirac_emptyset a) (Dirac_nonneg a) (Dirac_sigma_additivity a).

End Dirac_measure.