measure_R.v

apply cal_L_ray_cl.
apply cal_L_ray_cr.
Qed.

(* Lem 641 p. 102 *)
Lemma cal_L_intoc : forall a b, cal_L (fun x => a < x <= b).
Proof.
intros.
apply cal_L_intersection.
apply cal_L_ray_l.
apply cal_L_ray_cr.
Qed.

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

Lemma cal_L_singleton : forall a, cal_L (fun x => x = a).
Proof.
intros a.
apply cal_L_ext with (fun x => a <= 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.

(* From Lem 642 pp. 102,103 *)
Lemma cal_L_sigma_algebra :
  forall (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.

(* Lem 644 p. 103 *)
Lemma measurable_R_is_measurable_L :
  forall (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 :
  forall (E : nat -> R -> Prop),
    (forall n, measurable_L (E n)) ->
    (forall n p x, E n x -> E p x -> n = p) ->
    lambda_star (fun x => exists n, E n x) =
      Sup_seq (fun N => sum_Rbar N (fun n => lambda_star (E n))).
Proof.
intros.
rewrite cal_L_lambda_star_sigma_additivity; try easy.
intros; now apply cal_L_sigma_algebra.
Qed.

(* Lem 643 p. 103 *)
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 :
  forall a b,
    Lebesgue_measure (fun x => a <= x <= b) = Rmax 0 (b - a) /\
    Lebesgue_measure (fun x => a < x < b) = Rmax 0 (b - a) /\
    Lebesgue_measure (fun x => a < x <= b) = Rmax 0 (b - a) /\
    Lebesgue_measure (fun x => a <= 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 :
  forall (E : nat -> R -> Prop),
    (forall n, measurable_R (E n)) ->
    (forall n p x, E n x -> E p x -> n = p) ->
    lambda_star (fun x => exists n, E n x) =
      Sup_seq (fun N => sum_Rbar N (fun n => lambda_star (E n))).
Proof.
intros.
apply Lebesgue_sigma_additivity; try easy.
intros; now apply measurable_R_is_measurable_L.
Qed.

(* Lem 645 p. 103 *)
Definition Borel_Lebesgue_measure : measure gen_R :=
  mk_measure gen_R lambda_star
    lambda_star_emptyset lambda_star_nonneg Borel_Lebesgue_sigma_additivity.

(* Thm 646 Uniqueness pp. 103,104 *)
Theorem Caratheodory :
  forall (mu : measure gen_R),
    (forall a b, mu (fun x => a < x <= b) = Rmax 0 (b - a)) ->
    forall (A : R -> Prop),
      measurable gen_R A -> mu A = Borel_Lebesgue_measure A.
Proof.
assert (H : forall 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 x => IZR (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]].
exists (Rmax a c); exists (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].
exists (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 x => a < x <= b); try easy.
rewrite lambda_star_ext with (B := fun x => a < 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 :
  forall (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 E => gen_R E \/ lambda_star E = 0.

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

(*
Lemma measurable_L_gen_equiv :
  forall (E : R -> Prop), measurable_L_gen E <-> measurable_L E.
Proof.
apply measurable_gen_ext; intros E H.
(* *)
apply cal_L_sigma_algebra.
destruct H as [H | H].
now apply cal_L_gen_R.
now apply cal_L_lambda_star_0.
(* *)

aglop.

Aglopted.
*)

End L_gen.


Section Lebesgue_measure_Facts.

Lemma Lebesgue_measure_is_sigma_finite_disj :
  is_sigma_finite_measure cal_L Lebesgue_measure.
Proof.
exists (fun n x => IZR (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].
exists (bij_ZN z); now rewrite bij_NZN.
(* *)
intros n; rewrite is_finite_correct; exists 1.
edestruct Lebesgue_measure_is_length as [_ [_ [_ H]]]; rewrite H.
f_equal; rewrite Rmax_right; [ring | left; lra].
Defined.

(* WIP.
Lemma Lebesgue_measure_is_sigma_finite_incr :
  is_sigma_finite_measure cal_L Lebesgue_measure.
Proof.
exists (fun n x => - INR n <= x <= INR n); repeat split.
(* *)
intros; apply measurable_gen, cal_L_intcc.
(* *)
intros x; destruct (archimed_ceil_ex (Rabs x)) as [n Hn].

aglop.

(* *)
intros n; rewrite is_finite_correct; exists (2 * INR n).
edestruct Lebesgue_measure_is_length as [H _]; rewrite H.
f_equal; rewrite Rmax_right; try ring.
replace (INR n - - INR n) with (2 * INR n) by ring.
apply Rmult_le_pos; auto with real.
Aglopted.
*)

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

(* WIP.
Lemma Borel_Lebesgue_measure_is_sigma_finite_disj :
  is_sigma_finite_measure gen_R Borel_Lebesgue_measure.
Proof.
Aglopted.

Lemma Borel_Lebesgue_measure_is_sigma_finite_incr :
  is_sigma_finite_measure gen_R Borel_Lebesgue_measure.
Proof.
Aglopted.
*)

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

End Lebesgue_measure_Facts.