Library Lebesgue.Tonelli

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

Formalization and proof of the Tonelli theorem.

Description

References to pen-and-paper statements are from RR-9386-v2, https://hal.inria.fr/hal-03105815v2/
This file refers to Sections 9.4 (pp. 98-101) and 13.4 (pp. 175-184).
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 Rbar_compl sum_Rbar_nonneg.
From Lebesgue Require Import Subset_system_base Subset_system.
From Lebesgue Require Import sigma_algebra sigma_algebra_R_Rbar.
From Lebesgue Require Import measurable_fun measure simple_fun Mp LInt_p.

Local Open Scope R_scope.

Section Section_Facts.

Sections are partial applications of the curried version of functions defined on a cartesian product.
This is instantiated for subsets and numeric functions.

Context {X1 X2 : Type}.

Definition section : X1 (X1 × X2 Prop) X2 Prop :=
  fun x1 A x2A (x1, x2).

Definition section_fun : X1 (X1 × X2 Rbar) X2 Rbar :=
  fun x1 f x2f (x1, x2).

Properties of sections of subsets.

Lemma section_prod_in :
   (A1 : X1 Prop) (A2 : X2 Prop) x1,
    A1 x1 section x1 (prod A1 A2) = A2.
Proof.
intros A1 A2 x1 H.
apply subset_ext; intros x2; split; intros H1.
apply H1.
split.
apply H.
apply H1.
Qed.

Lemma section_prod_out :
   (A1 : X1 Prop) (A2 : X2 Prop) x1,
    compl A1 x1 section x1 (prod A1 A2) = emptyset.
Proof.
intros A1 A2 x1 H.
apply subset_ext; intros x2; split; intros H1.
apply H.
apply H1.
split; easy.
Qed.

Context {genX1 : (X1 Prop) Prop}.
Context {genX2 : (X2 Prop) Prop}.

Let genX1xX2 := Gen_Product genX1 genX2.

Lemma section_measurable :
   A x1, measurable genX1xX2 A measurable genX2 (section x1 A).
Proof.
intros A x1 H.
induction H.
destruct H as (B1,(B2,(H1,(H2,H3)))).
apply measurable_ext with (fun x2B1 x1 B2 x2).
intros x2.
apply iff_sym.
eapply iff_trans.
apply H3.
simpl; easy.
apply measurable_inter.
apply measurable_Prop.
case H2; intros H4.
apply measurable_gen; easy.
rewrite H4; apply measurable_full.
apply measurable_empty.
apply measurable_compl; easy.
apply measurable_union_countable; easy.
Qed.

Lemma section_union_count_measurable :
   x1 A, measurable_seq genX1xX2 A
    measurable genX2 (section x1 (fun xunion_seq A x)).
Proof.
intros x1 A H1.
apply measurable_union_countable.
intros n; apply section_measurable; auto.
Qed.

Lemma section_inter_count_measurable :
   x1 A, measurable_seq genX1xX2 A
    measurable genX2 (section x1 (fun xinter_seq A x)).
Proof.
intros x1 A H1.
apply measurable_inter_countable.
intros n; apply section_measurable; auto.
Qed.

Properties of sections of numeric functions.

Lemma section_fun_monot :
   f g,
    ( x, Rbar_le (f x) (g x))
     x1 x2, Rbar_le (section_fun x1 f x2) (section_fun x1 g x2).
Proof.
now unfold section_fun.
Qed.

Lemma section_fun_charac :
   (A : X1 × X2 Prop) x1,
    section_fun x1 (charac A) = fun x2charac (section x1 A) x2.
Proof.
intros A x1; apply fun_ext; intros x2; unfold section_fun.
destruct (in_dec (section x1 A) x2) as [H | H];
    [rewrite !charac_is_1 | rewrite !charac_is_0]; easy.
Qed.

Lemma section_fun_Mplus :
   f x1, Mplus genX1xX2 f Mplus genX2 (section_fun x1 f).
Proof.
intros f x1 [Hf1 Hf2]; split.
now unfold section_fun.
intros A HA.
apply section_measurable with (A := fun XA (f X)).
apply Hf2; easy.
Qed.

End Section_Facts.

Section Measure_Of_Section_Facts1.

Definition and measurability of the measure of sections of subsets (finite case).

Context {X1 X2 : Type}.

Context {genX2 : (X2 Prop) Prop}.

Variable muX2 : measure genX2.
Hypothesis HmuX2 : is_finite_measure muX2.

Definition meas_section : (X1 × X2 Prop) X1 Rbar :=
  fun A x1muX2 (section x1 A).

Lemma meas_section_prod :
   A1 A2 x1,
    meas_section (prod A1 A2) x1 = Rbar_mult (muX2 A2) (charac A1 x1).
Proof.
intros A1 A2 x1.
case (ClassicalDescription.excluded_middle_informative (A1 x1)).
intros H; unfold meas_section.
rewrite section_prod_in; try easy.
case (charac_or A1 x1).
2: intros H2; rewrite H2.
2: rewrite Rbar_mult_1_r; auto.
intros H2; rewrite H2, Rbar_mult_0_r.
replace A2 with (fun x2 : X2False).
apply meas_emptyset.
apply subset_ext; intros x2; split.
intros H3; intuition.
intros H3; apply charac_0 in H2; intuition.
intros H; unfold meas_section.
rewrite section_prod_out; try easy.
case (charac_or A1 x1).
intros H2; rewrite H2.
rewrite meas_emptyset.
symmetry.
apply Rbar_mult_0_r.
intros H2; rewrite H2.
rewrite Rbar_mult_1_r.
apply measure_ext.
intros x2; split; intros H3; try easy.
apply charac_1 in H2; intuition.
Qed.

Context {genX1 : (X1 Prop) Prop}.

Let genX1xX2 := Gen_Product genX1 genX2.

Lemma monotone_class_and_measurable :
   (Q : (X1 × X2 Prop) Prop),
    ( A, Algebra (Prod_Sigma_algebra genX1 genX2) A Q A)
    ( A : nat X1 × X2 Prop,
      decr_seq A measurable_seq genX1xX2 A
      ( n, Q (A n)) Q (fun x n, A n x))
    ( A : nat X1 × X2Prop,
      incr_seq A measurable_seq genX1xX2 A
      ( n, Q (A n)) Q (fun x n, A n x))
     A, measurable genX1xX2 A Q A.
Proof.
intros Q H1 H2 H3 A H4.
assert (H5 : measurable genX1xX2 A Q A); [| easy].
apply (monotone_class_Prop (Algebra genX1xX2))
  with (P := fun Ameasurable genX1xX2 A Q A).
apply Monotone_class_equiv; try easy; split.
intros B HB H; split.
apply measurable_inter_countable; intros n; apply H.
apply H2; try easy; intros n; apply H.
split.
apply measurable_union_countable, H0.
apply H3; try easy; intros n; apply H0.
intros B HB; rewrite Algebra_idem in HB; split.
rewrite measurable_Sigma_algebra; apply Incl_Algebra_Sigma_algebra; easy.
apply H1, Algebra_Gen_Prod_Prod_Sigma_algebra_Incl;
    rewrite Gen_Prod_Gen_Product; easy.
rewrite Sigma_algebra_Algebra, <- measurable_Sigma_algebra; easy.
Qed.

Lemma meas_section_measurable_finite_aux0 :
   A,
    Prod_Sigma_algebra genX1 genX2 A
    measurable_fun_Rbar genX1 (meas_section A).
Proof.
intros A [A1 [A2 [H1 [H2 H3]]]].
apply measurable_fun_ext with (f1 := fun x1Rbar_mult (muX2 A2) (charac A1 x1)).
intros x1; rewrite <- meas_section_prod.
f_equal; apply subset_ext; intros x2; now rewrite H3.
apply measurable_fun_scal.
apply measurable_fun_charac.
rewrite measurable_Sigma_algebra; easy.
Qed.

Lemma meas_section_measurable_finite_aux1 :
   A,
    Algebra (Prod_Sigma_algebra genX1 genX2) A
    measurable_fun_Rbar genX1 (meas_section A).
Proof.
intros A H1.
rewrite Algebra_product_explicit in H1.
destruct H1 as [B [N [H2 [H3 H4]]]].
assert (H2a : n, (n < S N)%nat
                measurable genX1xX2 (B n)).
intros n Hn.
destruct (H2 n Hn) as [A1 [A2 [HA1 [HA2 HB]]]]; rewrite HB.
rewrite <- measurable_Sigma_algebra in HA1.
rewrite <- measurable_Sigma_algebra in HA2.
now apply Gen_Product_is_product_measurable.
apply measurable_fun_ext with
  (f1:= fun x1 : X1muX2 (fun x2 : X2 n : nat,
                                        (n N)%nat B n (x1, x2))).
intros x1; rewrite H3; apply measure_ext.
intros x; split.
intros (n,(Hn1,Hn2)); n; split; auto with arith.
intros (n,(Hn1,Hn2)); n; split; auto with arith.
apply measurable_fun_ext with
   (f1:= fun x1 : X1sum_Rbar N (fun m : natmuX2 (fun x2 : X2B m (x1, x2)))).
intros x1; symmetry; apply measure_additivity_finite.
intros n H5; apply Nat.lt_succ_r in H5.
apply (section_measurable _ _ (H2a n H5)).
rewrite <- Subset_finite.disj_finite_equiv in H4.
intros n m x2 Hn Hm HBn HBm.
apply (H4 n m (x1, x2)); now try lia.
clear H3 H4.
assert (H2b : n, (n < S N)%nat Prod_Sigma_algebra genX1 genX2 (B n)).
intros n Hn.
destruct (H2 n Hn) as [A1 [A2 [HA1 [HA2 HB]]]].
rewrite HB; now A1, A2.
induction N; simpl.
apply meas_section_measurable_finite_aux0; auto.
apply Mplus_plus.
split.
intro x1; apply meas_nonneg.
apply meas_section_measurable_finite_aux0; auto.
split.
2: apply IHN; auto.
clear IHN.
induction N; simpl.
intro x1; apply meas_nonneg.
apply nonneg_plus.
2: apply IHN; auto.
intro x1; apply meas_nonneg.
Qed.

Lemma meas_section_measurable_finite_aux2 :
   A, measurable_seq genX1xX2 A decr_seq A
    ( n, measurable_fun_Rbar genX1 (meas_section (A n)))
    measurable_fun_Rbar genX1 (meas_section (inter_seq A)).
Proof.
intros A H1 H2 H3.
apply measurable_fun_ext with
   (f1:= fun x1 : X1Inf_seq (fun n : natmuX2 (fun x2A n (x1, x2)))).
intros x1; symmetry.
2: apply measurable_fun_Inf_seq; easy.
apply measure_continuous_from_above.
intros n x2; apply H2 with (x:= (x1,x2)).
intros n.
apply (section_measurable _ _ (H1 _)).
0%nat.
apply Rbar_bounded_is_finite with 0 (muX2 (fun _ : X2True)); try easy.
apply meas_nonneg.
apply measure_le.
apply (section_measurable _ _ (H1 _)).
apply measurable_full.
auto.
Qed.

Lemma meas_section_measurable_finite_aux3 :
   A, measurable_seq genX1xX2 A incr_seq A
    ( n, measurable_fun_Rbar genX1 (meas_section (A n)))
    measurable_fun_Rbar genX1 (meas_section (union_seq A)).
Proof.
intros A H1 H2 H3.
apply measurable_fun_ext with
   (f1:= fun x1 : X1Sup_seq (fun n : natmuX2 (fun x2 : X2A n (x1, x2)))).
intros x1; symmetry.
2: apply measurable_fun_Sup_seq; easy.
apply measure_continuous_from_below.
intros n.
apply (section_measurable _ _ (H1 _)).
intros n x2.
apply H2 with (x:= (x1,x2)); easy.
Qed.

Lemma meas_section_Mplus_finite :
   A, measurable genX1xX2 A Mplus genX1 (meas_section A).
Proof.
intros A HA; split.
intros x; apply meas_nonneg.
apply monotone_class_and_measurable with (A := A); try easy.
intros; now apply meas_section_measurable_finite_aux1.
intros; now apply meas_section_measurable_finite_aux2.
intros; now apply meas_section_measurable_finite_aux3.
Qed.

End Measure_Of_Section_Facts1.

Section Measure_Of_Section_Facts2.

Measurability of the measure of sections of subsets (sigma-finite case).

Context {X1 X2 : Type}.

Context {genX1 : (X1 Prop) Prop}.
Context {genX2 : (X2 Prop) Prop}.

Let genX1xX2 := Gen_Product genX1 genX2.

Variable muX2 : measure genX2.
Hypothesis HmuX2 : is_sigma_finite_measure genX2 muX2.

Lemma meas_section_Mplus_sigma_finite :
   A, measurable genX1xX2 A Mplus genX1 (meas_section muX2 A).
Proof.
intros A HA.
split.
intros x; apply meas_nonneg.
rewrite is_sigma_finite_measure_equiv_def in HmuX2.
destruct HmuX2 as [B2 [H1 [H2 [H3 H4]]]].
replace (meas_section muX2 A) with
    (fun x1 : X1muX2 (inter (section x1 A)
                                (fun x2union_seq B2 x2))).
2: { apply fun_ext; intros x1.
    apply measure_ext; intros x2; split.
    intros; apply H.
    intros; split; try easy; apply H2. }
replace (fun x1 : X1muX2 (inter (section x1 A)
  (fun nunion_seq B2 n))) with
     (fun x1 : X1muX2 (fun x2 : X2 n : nat,
                            (inter (section x1 A) (B2 n)) x2)).
2: { apply fun_ext; intros x1.
    rewrite inter_union_seq_distr_l.
    auto. }
replace (fun x1 : X1muX2 (fun x2 : X2 n : nat,
                       (inter (section x1 A) (B2 n)) x2)) with
    (fun x1 : X1Sup_seq (fun n : natmuX2 ((inter (section x1 A) (B2 n))))).
2: { apply fun_ext; intros x1.
    rewrite measure_continuous_from_below; auto.
    intros n; apply measurable_inter; try easy.
    eapply section_measurable; apply HA.
    intros n x2 H5.
    split.
    apply H5.
    apply H3, H5. }
replace (fun x1 : X1Sup_seq (fun n : nat
                  muX2 ((inter (section x1 A) (B2 n))))) with
  (fun x1 : X1Sup_seq (fun n : nat
                  meas_restricted genX2 muX2 (B2 n) (H1 n) (section x1 A))).
2: { apply fun_ext; intros x1.
    apply Sup_seq_ext; intros n.
    simpl.
    rewrite inter_comm; easy. }
apply measurable_fun_Sup_seq; intros n.
apply meas_section_Mplus_finite; try easy.
unfold is_finite_measure, meas_restricted, meas_restricted_meas; simpl.
rewrite measure_ext with (A2 := B2 n); easy.
Qed.

End Measure_Of_Section_Facts2.

Section Product_Measure_Def.

Definition of the product measure.

Context {X1 X2 : Type}.

Context {genX1 : (X1 Prop) Prop}.
Context {genX2 : (X2 Prop) Prop}.

Let genX1xX2 := Gen_Product genX1 genX2.

Variable muX1 : measure genX1.
Variable muX2 : measure genX2.
Hypothesis HmuX2 : is_sigma_finite_measure genX2 muX2.

Definition is_product_measure : measure genX1xX2 Prop :=
  fun mu A1 A2, measurable genX1 A1 measurable genX2 A2
    mu (prod A1 A2) = Rbar_mult (muX1 A1) (muX2 A2).

Definition meas_prod_meas : (X1 × X2 Prop) Rbar :=
  fun ALInt_p muX1 (meas_section muX2 A).

Lemma meas_prod_emptyset : meas_prod_meas emptyset = 0.
Proof.
unfold meas_prod_meas, meas_section, section.
rewrite <- LInt_p_0 with (mu := muX1); try easy.
apply LInt_p_ext.
intros; apply meas_emptyset.
Qed.

Lemma meas_prod_nonneg : nonneg meas_prod_meas.
Proof.
intros A; apply LInt_p_nonneg; try easy.
intros x1; apply meas_nonneg.
Qed.

Lemma meas_prod_sigma_additivity :
   A, measurable_seq genX1xX2 A
    ( n m x, A n x A m x n = m)
    meas_prod_meas (fun x n, A n x) =
      Sup_seq (fun nsum_Rbar n (fun mmeas_prod_meas (A m))).
Proof.
intros A H1 H2.
unfold meas_prod_meas.
rewrite <- LInt_p_sigma_additive; try easy.
apply LInt_p_ext.
intros x1; apply meas_sigma_additivity.
intros n; apply section_measurable with (1:= H1 n).
intros n m x2; intros; apply H2 with (x := (x1,x2)); try easy.
intros n; now apply meas_section_Mplus_sigma_finite.
Qed.

Definition meas_prod : measure genX1xX2 :=
  mk_measure genX1xX2 meas_prod_meas
    meas_prod_emptyset meas_prod_nonneg (meas_prod_sigma_additivity).

Lemma meas_prod_is_product_measure : is_product_measure meas_prod.
Proof.
intros A1 A2 HA1 _; simpl; unfold meas_prod_meas.
rewrite LInt_p_ext with (g := fun x1Rbar_mult (muX2 A2) (charac A1 x1)).
rewrite LInt_p_scal; try easy.
rewrite LInt_p_charac; try easy.
apply Rbar_mult_comm.
apply meas_nonneg.
now apply Mplus_charac.
intros; now rewrite meas_section_prod.
Qed.

End Product_Measure_Def.

Section Product_measure_Facts.

Properties of the product measure.

Context {X1 X2 : Type}.

Context {genX1 : (X1 Prop) Prop}.
Context {genX2 : (X2 Prop) Prop}.

Let genX1xX2 := Gen_Product genX1 genX2.

Variable muX1 : measure genX1.
Variable muX2 : measure genX2.

Lemma meas_prod_finite :
  is_finite_measure muX1 is_finite_measure muX2
   mu : measure genX1xX2, is_product_measure muX1 muX2 mu
    is_finite_measure mu.
Proof.
intros Hmu1 Hmu2 mu Hmu; unfold is_finite_measure.
rewrite measure_ext with (A2 := prod (@fullset X1) (@fullset X2)); try easy.
rewrite Hmu; try apply measurable_full.
now rewrite <- Hmu1, <- Hmu2.
Qed.

Lemma meas_prod_sigma_finite :
  is_sigma_finite_measure genX1 muX1 is_sigma_finite_measure genX2 muX2
  ( A, measurable_seq genX1xX2 A
    ( x, n, A n x)
    ( n x, A n x A (S n) x)
    ( n, A1, A2,
      measurable genX1 A1 measurable genX2 A2
      is_finite (muX1 A1) is_finite (muX2 A2)
      A n = prod A1 A2)
    ( mu : measure genX1xX2, is_product_measure muX1 muX2 mu
       n, is_finite (mu (A n)))).
Proof.
intros H1 H2.
rewrite is_sigma_finite_measure_equiv_def in H1.
destruct H1 as [A1 [HA11 [HA12 [HA13 HA14]]]].
rewrite is_sigma_finite_measure_equiv_def in H2.
destruct H2 as [A2 [HA21 [HA22 [HA23 HA24]]]].
pose (A := fun nprod (A1 n) (A2 n)).
A; repeat split.
intros n; apply Gen_Product_is_product_measurable; try easy.
intros X.
destruct (HA12 (fst X)) as (n1, Hn1).
destruct (HA22 (snd X)) as (n2, Hn2).
(max n1 n2).
unfold A, prod; split.
apply incr_seq_le with n1; try easy; auto with arith.
apply incr_seq_le with n2; try easy; auto with arith.
apply HA13, H.
apply HA23, H.
intros n; (A1 n); (A2 n); repeat split; easy.
intros mu Hmu n.
unfold A; rewrite Hmu; try easy.
rewrite <- (HA14 n), <- (HA24 n); easy.
Qed.

Lemma meas_prod_sigma_finite_alt :
  is_sigma_finite_measure genX1 muX1 is_sigma_finite_measure genX2 muX2
   mu : measure genX1xX2,is_product_measure muX1 muX2 mu
    is_sigma_finite_measure genX1xX2 mu.
Proof.
intros Hmu1 Hmu2 mu Hmu.
apply is_sigma_finite_measure_equiv_def.
destruct (meas_prod_sigma_finite Hmu1 Hmu2) as (A,HA).
A; repeat split; now try apply HA.
Qed.

End Product_measure_Facts.

Section Product_measure_Uniqueness1.

Uniqueness of the product measure (finite case).

Context {X1 X2 : Type}.

Context {genX1 : (X1 Prop) Prop}.
Context {genX2 : (X2 Prop) Prop}.

Let genX1xX2 := Gen_Product genX1 genX2.

Variable muX1 : measure genX1.
Variable muX2 : measure genX2.
Hypothesis HmuX1 : is_finite_measure muX1.
Hypothesis HmuX2 : is_finite_measure muX2.

Variable mu : measure genX1xX2.
Variable nu : measure genX1xX2.
Hypothesis Hmu : is_product_measure muX1 muX2 mu.
Hypothesis Hnu : is_product_measure muX1 muX2 nu.

Lemma meas_prod_uniqueness_aux0 :
   A, Prod_Sigma_algebra genX1 genX2 A mu A = nu A.
Proof.
intros A [A1 [A2 [HA1 [HA2 H]]]].
rewrite H, Hmu, Hnu; try easy.
all: rewrite measurable_Sigma_algebra; easy.
Qed.

Lemma meas_prod_uniqueness_aux1 :
   A, Algebra (Prod_Sigma_algebra genX1 genX2) A mu A = nu A.
Proof.
intros A HA; rewrite Algebra_product_explicit in HA.
destruct HA as [B [N [HB1 [HA HB2]]]]; rewrite HA.
rewrite measure_ext with (A2 := fun x n, (n N)%nat B n x).
rewrite (measure_ext _ nu _ (fun x n, (n N)%nat B n x)).
2,3: intros x; split; intros [n [Hn Hx]]; n; split; now try lia.
assert (HB1' : n, (n N)%nat measurable genX1xX2 (B n)).
intros n Hn; rewrite measurable_Sigma_algebra.
unfold genX1xX2; rewrite <- Gen_Prod_Gen_Product, <- Sigma_algebra_Prod_eq.
apply Sigma_algebra_Gen, HB1; lia.
assert (HB2' : n m x, (n N)%nat (m N)%nat B n x B m x n = m).
rewrite <- Subset_finite.disj_finite_equiv in HB2.
intros n m x2 Hn Hm HBn HBm; apply (HB2 n m x2); now try lia.
rewrite 2!measure_additivity_finite; try easy.
apply sum_Rbar_ext; intros i Hi; apply meas_prod_uniqueness_aux0, HB1; lia.
Qed.

Lemma meas_prod_uniqueness_aux2 :
   A, measurable_seq genX1xX2 A decr_seq A
    ( n, mu (A n) = nu (A n))
    mu (inter_seq A) = nu (inter_seq A).
Proof.
intros A HA1 HA2 HA3; unfold inter_seq, inter_any; unfold decr_seq in HA2.
rewrite 2!measure_continuous_from_above; try easy.
apply Inf_seq_ext; intros; apply HA3.
1,2: 0%nat; apply finite_measure_is_finite; try easy;
    now apply (meas_prod_finite muX1 muX2).
Qed.

Lemma meas_prod_uniqueness_aux3 :
   A, measurable_seq genX1xX2 A incr_seq A
    ( n, mu (A n) = nu (A n))
    mu (union_seq A) = nu (union_seq A).
Proof.
intros A HA1 HA2 HA3; unfold union_seq, union_any; unfold incr_seq in HA2.
rewrite 2!measure_continuous_from_below; try easy.
apply Sup_seq_ext; intros; apply HA3.
Qed.

Lemma meas_prod_uniqueness_finite :
   A, measurable genX1xX2 A mu A = nu A.
Proof.
intros A HA; eapply (monotone_class_and_measurable (fun Amu A = nu A)).
4: apply HA.
intros; now apply meas_prod_uniqueness_aux1.
intros; now apply meas_prod_uniqueness_aux2.
intros; now apply meas_prod_uniqueness_aux3.
Qed.

End Product_measure_Uniqueness1.

Section Product_measure_Uniqueness2.

Uniqueness of the product measure (sigma-finite case).

Context {X1 X2 : Type}.

Context {genX1 : (X1 Prop) Prop}.
Context {genX2 : (X2 Prop) Prop}.

Let genX1xX2 := Gen_Product genX1 genX2.

Variable muX1 : measure genX1.
Variable muX2 : measure genX2.
Hypothesis HmuX1 : is_sigma_finite_measure genX1 muX1.
Hypothesis HmuX2 : is_sigma_finite_measure genX2 muX2.

Variable mu : measure genX1xX2.
Variable nu : measure genX1xX2.
Hypothesis Hmu : is_product_measure muX1 muX2 mu.
Hypothesis Hnu : is_product_measure muX1 muX2 nu.

Lemma meas_prod_uniqueness_sigma_finite :
   A, measurable genX1xX2 A mu A = nu A.
Proof.
intros A HA.
destruct (meas_prod_sigma_finite muX1 muX2)
  as (B, (HB1, (HB2,(HB3,(HB4,HB5))))); try easy.
pose (mun := fun nmeas_restricted _ mu (B n) (HB1 n)).
pose (nun := fun nmeas_restricted _ nu (B n) (HB1 n)).
replace A with (inter A (union_seq B)).
rewrite inter_union_seq_distr_l.
unfold union_seq, union_any; rewrite 2!measure_continuous_from_below.
apply Sup_seq_ext; intros n.
apply trans_eq with (mun n A).
unfold mun, meas_restricted, meas_restricted_meas; simpl.
apply measure_ext; intros X; rewrite inter_comm; easy.
apply sym_eq, trans_eq with (nun n A).
unfold nun, meas_restricted, meas_restricted_meas; simpl.
apply measure_ext; intros X; rewrite inter_comm; easy.
destruct (HB4 n) as (A1,(A2, (HA1,(HA2,(HA3, (HA4,HA5)))))).
apply meas_prod_uniqueness_finite with
   (meas_restricted _ muX1 A1 HA1)
   (meas_restricted _ muX2 A2 HA2); try easy.
unfold is_finite_measure, meas_restricted, meas_restricted_meas; simpl.
rewrite (measure_ext _ _ _ A1); try tauto.
unfold is_finite_measure, meas_restricted, meas_restricted_meas; simpl.
rewrite (measure_ext _ _ _ A2); try tauto.
intros C1 C2 HC1 HC2.
unfold nun, meas_restricted, meas_restricted_meas; simpl.
rewrite HA5.
apply trans_eq with (nu (prod (inter A1 C1) (inter A2 C2))).
apply measure_ext.
rewrite <- prod_inter; easy.
rewrite Hnu; f_equal; try easy.
apply measurable_inter; easy.
apply measurable_inter; easy.
intros C1 C2 HC1 HC2.
unfold mun, meas_restricted, meas_restricted_meas; simpl.
rewrite HA5.
apply trans_eq with (mu (prod (inter A1 C1) (inter A2 C2))).
apply measure_ext.
rewrite <- prod_inter; easy.
rewrite Hmu; f_equal; try easy.
apply measurable_inter; easy.
apply measurable_inter; easy.
intros n; apply measurable_inter; try easy.
intros n X; apply inter_incr_seq_compat_l; try easy.
intros n; apply measurable_inter; try easy.
intros n X; apply inter_incr_seq_compat_l; try easy.
replace (union_seq B) with (@fullset (X1×X2)).
apply inter_full_r.
apply subset_ext; unfold union_seq, union_any; easy.
Qed.

End Product_measure_Uniqueness2.

Section Integral_Of_Section_Fun_Facts.

Definition and properties of the integral of sections of functions.

Context {X1 X2 : Type}.

Context {genX1 : (X1 Prop) Prop}.
Context {genX2 : (X2 Prop) Prop}.

Let genX1xX2 := Gen_Product genX1 genX2.

Variable muX1 : measure genX1.
Variable muX2 : measure genX2.
Hypothesis HmuX2 : is_sigma_finite_measure genX2 muX2.

Definition LInt_p_section_fun : (X1 × X2 Rbar) X1 Rbar :=
  fun f x1LInt_p muX2 (section_fun x1 f).

Lemma LInt_p_section_fun_monot :
   f g,
    ( x, Rbar_le (f x) (g x))
     x1, Rbar_le (LInt_p_section_fun f x1) (LInt_p_section_fun g x1).
Proof.
intros; now apply LInt_p_monotone, section_fun_monot.
Qed.

Lemma LInt_p_section_fun_nonneg :
   f, nonneg f nonneg (LInt_p_section_fun f).
Proof.
intros f Hf x1; apply LInt_p_nonneg; auto.
intros x2; apply Hf.
Qed.

Let P0 : (X1 × X2 Rbar) Prop :=
  fun fMplus genX1 (LInt_p_section_fun f).

Lemma LInt_p_section_fun_charac :
   A x1, measurable genX1xX2 A
    LInt_p_section_fun (charac A) x1 = meas_section muX2 A x1.
Proof.
intros A x1 HA; unfold meas_section; rewrite <- LInt_p_charac.
unfold LInt_p_section_fun; rewrite section_fun_charac; easy.
apply section_measurable with (1 := HA).
Qed.

Lemma LInt_p_section_fun_Mplus_charac :
   A, measurable genX1xX2 A P0 (charac A).
Proof.
intros A; intros.
apply Mplus_ext with (meas_section muX2 A).
intros; now rewrite <- LInt_p_section_fun_charac.
now apply meas_section_Mplus_sigma_finite.
Qed.

Lemma LInt_p_section_fun_scal :
   a f x1, 0 a Mplus genX1xX2 f
    LInt_p_section_fun (fun xRbar_mult a (f x)) x1 =
      Rbar_mult a (LInt_p_section_fun f x1).
Proof.
intros a f x1 Ha Hf.
apply LInt_p_scal; try easy.
apply (section_fun_Mplus _ _ Hf).
Qed.

Lemma LInt_p_section_fun_Mplus_scal :
   a f, 0 a Mplus genX1xX2 f
    P0 f P0 (fun xRbar_mult a (f x)).
Proof.
intros a f; intros.
apply Mplus_ext with (fun x1Rbar_mult a (LInt_p_section_fun f x1)).
intros; now rewrite LInt_p_section_fun_scal.
now apply Mplus_scal.
Qed.

Lemma LInt_p_section_fun_plus :
   f g x1, Mplus genX1xX2 f Mplus genX1xX2 g
    (LInt_p_section_fun (fun xRbar_plus (f x) (g x))) x1 =
      Rbar_plus (LInt_p_section_fun f x1) (LInt_p_section_fun g x1).
Proof.
intros f g x1 Hf Hg.
unfold LInt_p_section_fun, section_fun.
rewrite LInt_p_plus; try easy.
apply (section_fun_Mplus _ _ Hf).
apply (section_fun_Mplus _ _ Hg).
Qed.

Lemma LInt_p_section_fun_Mplus_plus :
   f g, Mplus genX1xX2 f Mplus genX1xX2 g
    P0 f P0 g P0 (fun xRbar_plus (f x) (g x)).
Proof.
intros f g; intros.
apply Mplus_ext with
    (fun x1Rbar_plus (LInt_p_section_fun f x1) (LInt_p_section_fun g x1)).
intros; now rewrite LInt_p_section_fun_plus.
now apply Mplus_plus.
Qed.

Lemma LInt_p_section_fun_Sup_seq :
   f x1, incr_fun_seq f Mplus_seq genX1xX2 f
    LInt_p_section_fun (fun xSup_seq (fun nf n x)) x1 =
      Sup_seq (fun nLInt_p_section_fun (f n) x1).
Proof.
intros f x1 Hf1 Hf2.
apply Beppo_Levi; try easy.
intros n; apply (section_fun_Mplus _ _ (Hf2 n)).
Qed.

Lemma LInt_p_section_fun_Mplus_Sup_seq :
   f, incr_fun_seq f Mplus_seq genX1xX2 f
    ( n, P0 (f n)) P0 (fun xSup_seq (fun nf n x)).
Proof.
intros f; intros.
apply Mplus_ext with (fun x1Sup_seq (fun nLInt_p_section_fun (f n) x1)).
intros; now rewrite LInt_p_section_fun_Sup_seq.
now apply Mplus_Sup_seq.
Qed.

End Integral_Of_Section_Fun_Facts.

Section Iterated_Integrals_Facts.

Definition and properties of the iterated integrals, ie the integral of the integral of sections of functions.

Context {X1 X2 : Type}.

Context {genX1 : (X1 Prop) Prop}.
Context {genX2 : (X2 Prop) Prop}.

Let genX1xX2 := Gen_Product genX1 genX2.

Variable muX1 : measure genX1.
Variable muX2 : measure genX2.
Hypothesis HmuX2 : is_sigma_finite_measure genX2 muX2.


Let muX1xX2 := meas_prod muX1 muX2 HmuX2.

Lemma P_ext :
   {X : Type} (P : (X Rbar) Prop) f1 f2,
    ( x, f1 x = f2 x) P f1 P f2.
Proof.
intros X P f1 f2 H; apply fun_ext in H; now subst.
Qed.

Let P : (X1 × X2 Rbar) Prop :=
  fun fMplus genX1 (LInt_p_section_fun muX2 f)
    LInt_p muX1xX2 f = LInt_p muX1 (LInt_p_section_fun muX2 f).

Lemma LInt_p_section_fun_meas_prod_charac :
   A, measurable genX1xX2 A P (charac A).
Proof.
intros A HA; split.
now apply LInt_p_section_fun_Mplus_charac.
rewrite LInt_p_charac; try easy.
apply LInt_p_ext; intros.
erewrite <- LInt_p_section_fun_charac; try easy; apply HA.
Qed.

Lemma LInt_p_section_fun_meas_prod_scal :
   a f, 0 a Mplus genX1xX2 f
    P f P (fun xRbar_mult a (f x)).
Proof.
intros a f Ha Hf1 [Hf2 Hf3]; split.
now apply LInt_p_section_fun_Mplus_scal.
rewrite (LInt_p_ext muX1) with
    (g := fun x1Rbar_mult a (LInt_p_section_fun muX2 f x1)).
rewrite 2!LInt_p_scal, Hf3; try easy.
intros; eapply LInt_p_section_fun_scal; now try apply Hf1.
Qed.

Lemma LInt_p_section_fun_meas_prod_plus :
   f g, Mplus genX1xX2 f Mplus genX1xX2 g
    P f P g P (fun xRbar_plus (f x) (g x)).
Proof.
intros f g Hf1 Hg1 [Hf2 Hf3] [Hg2 Hg3]; split.
now apply LInt_p_section_fun_Mplus_plus.
rewrite (LInt_p_ext muX1) with
  (g := fun x1
    Rbar_plus (LInt_p_section_fun muX2 f x1) (LInt_p_section_fun muX2 g x1)).
rewrite 2!LInt_p_plus, Hf3, Hg3; try easy.
intros; eapply LInt_p_section_fun_plus; try apply Hf1; now try apply Hg1.
Qed.

Lemma LInt_p_section_fun_meas_prod_Sup_seq :
   f, Mplus_seq genX1xX2 f incr_fun_seq f
    ( n, P (f n)) P (fun xSup_seq (fun nf n x)).
Proof.
intros f Hf1 Hf2 Hf3; split.
apply LInt_p_section_fun_Mplus_Sup_seq; now try apply Hf3.
rewrite (LInt_p_ext muX1) with
    (g := fun x1Sup_seq (fun nLInt_p_section_fun muX2 (f n) x1)).
rewrite 2!Beppo_Levi; try easy.
apply Sup_seq_ext, Hf3.
intros n; apply Hf3.
intros x1 n; apply LInt_p_section_fun_monot; intros x; apply Hf2.
intros; eapply LInt_p_section_fun_Sup_seq; now try apply Hf1.
Qed.

End Iterated_Integrals_Facts.

Section Tonelli_aux1.

First formula of the Tonelli theorem.

Context {X1 X2 : Type}.

Context {genX1 : (X1 Prop) Prop}.
Context {genX2 : (X2 Prop) Prop}.

Let genX1xX2 := Gen_Product genX1 genX2.

Variable muX1 : measure genX1.
Variable muX2 : measure genX2.
Hypothesis HmuX2 : is_sigma_finite_measure genX2 muX2.

Let muX1xX2 := meas_prod muX1 muX2 HmuX2.

Lemma Tonelli_aux1 :
   f, Mplus genX1xX2 f
    Mplus genX1 (LInt_p_section_fun muX2 f)
    LInt_p muX1xX2 f = LInt_p muX1 (LInt_p_section_fun muX2 f).
Proof.
intros f Hf.
apply Mp_correct in Hf; try easy.
induction Hf.
now apply LInt_p_section_fun_meas_prod_charac.
apply LInt_p_section_fun_meas_prod_scal; now try apply Mp_correct.
apply LInt_p_section_fun_meas_prod_plus; now try apply Mp_correct.
apply LInt_p_section_fun_meas_prod_Sup_seq; now try apply Mp_seq_correct.
Qed.

End Tonelli_aux1.

Section Tonelli_aux2.

Second formula of the Tonelli theorem.

Context {X1 X2 : Type}.

Context {genX1 : (X1 Prop) Prop}.
Context {genX2 : (X2 Prop) Prop}.

Let genX1xX2 := Gen_Product genX1 genX2.
Let genX2xX1 := Gen_Product genX2 genX1.

Variable muX1 : measure genX1.
Variable muX2 : measure genX2.
Hypothesis HmuX1 : is_sigma_finite_measure genX1 muX1.
Hypothesis HmuX2 : is_sigma_finite_measure genX2 muX2.

Let muX1xX2 : measure genX1xX2 := meas_prod muX1 muX2 HmuX2.
Let muX2xX1 : measure genX2xX1 := meas_prod muX2 muX1 HmuX1.

Let meas_prod_swap : measure genX1xX2 := meas_image _ measurable_fun_swap_var muX2xX1.

Lemma meas_prod_swap_is_product_measure :
  is_product_measure muX1 muX2 meas_prod_swap.
Proof.
intros A1 A2 HA1 HA2; rewrite Rbar_mult_comm.
rewrite <- (meas_prod_is_product_measure _ _ HmuX1); try easy.
unfold meas_prod_swap; simpl.
f_equal; now rewrite <- (prod_swap_c A1 A2).
Qed.

Lemma Tonelli_aux2 :
   f, Mplus genX1xX2 f
    Mplus genX2 (LInt_p_section_fun muX1 (swap f))
    LInt_p muX1xX2 f = LInt_p muX2 (LInt_p_section_fun muX1 (swap f)).
Proof.
intros f Hf.
destruct (Tonelli_aux1 muX2 _ HmuX1 (swap f)) as [Y1 Y2]; try easy.
now apply Mplus_swap.
split; try easy.
rewrite <- Y2.
apply trans_eq with (LInt_p meas_prod_swap f).
apply LInt_p_mu_ext.
intros A HA; unfold meas_prod.
apply meas_prod_uniqueness_sigma_finite with muX1 muX2; try easy.
apply meas_prod_is_product_measure.
apply meas_prod_swap_is_product_measure.
unfold swap; apply LInt_p_change_meas; easy.
Qed.

End Tonelli_aux2.

Section Tonelli.

The Tonelli theorem.

Context {X1 X2 : Type}.

Context {genX1 : (X1 Prop) Prop}.
Context {genX2 : (X2 Prop) Prop}.

Let genX1xX2 := Gen_Product genX1 genX2.

Variable muX1 : measure genX1.
Variable muX2 : measure genX2.
Hypothesis HmuX1 : is_sigma_finite_measure genX1 muX1.
Hypothesis HmuX2 : is_sigma_finite_measure genX2 muX2.

Let muX1xX2 := meas_prod muX1 muX2 HmuX2.

Theorem Tonelli :
   f, Mplus genX1xX2 f
    (Mplus genX1 (LInt_p_section_fun muX2 f)
     LInt_p muX1xX2 f = LInt_p muX1 (LInt_p_section_fun muX2 f))
    (Mplus genX2 (LInt_p_section_fun muX1 (swap f))
     LInt_p muX1xX2 f = LInt_p muX2 (LInt_p_section_fun muX1 (swap f))).
Proof.
intros; split.
apply Tonelli_aux1; easy.
apply Tonelli_aux2; easy.
Qed.

Lemma Tonelli_formulas :
   f, Mplus genX1xX2 f
    LInt_p muX1xX2 f = LInt_p muX1 (LInt_p_section_fun muX2 f)
    LInt_p muX1xX2 f = LInt_p muX2 (LInt_p_section_fun muX1 (swap f)).
Proof.
intros; split; now apply Tonelli.
Qed.

End Tonelli.