Files

Module mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral_fubini

From HB Require Import structures.
From mathcomp Require Import boot order ssralg ssrnum ssrint interval.
From mathcomp Require Import interval_inference archimedean finmap.
From mathcomp Require Import boolp classical_sets functions cardinality fsbigop.
From mathcomp Require Import reals real_interval topology ereal.
From mathcomp Require Import normedtype sequences esum measure.
From mathcomp Require Import real_measure numfun realfun simple_functions.
From mathcomp Require Import measurable_fun_approximation.
From mathcomp Require Import lebesgue_integral_definition.
From mathcomp Require Import lebesgue_integral_monotone_convergence.
From mathcomp Require Import lebesgue_integral_nonneg lebesgue_integrable.

# Fubini theorems for the Lebesgue Integral This file contains a formalization of the product measure, of Tonelli- -Fubini' theorem, and Fubini's theorem. Main references: - Daniel Li, Intégration et applications, 2016 - R. Affeldt, C. Cohen. Measure Construction by Extension in Dependent Type Theory with Application to Integration. JAR 2023 Detailed contents: ``` m1 \x m2 == product measure over T1 * T2, m1 is a measure over T1, and m2 is a sigma finite measure over T2 product_subprobability P == P.1 \x P.2 where P is a pair of subprobability measures m1 \x^ m2 == product measure over T1 * T2, m2 is a measure over T1, and m1 is a sigma finite measure over T2 ```

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Import Order.TTheory GRing.Theory Num.Def Num.Theory.
Import numFieldNormedType.Exports.

Local Open Scope classical_set_scope.
Local Open Scope ring_scope.

Reserved Notation "m1 '\x' m2" (at level 40, left associativity).
Reserved Notation "m1 '\x^' m2" (at level 40, left associativity).

Product measure

Section ndseq_closed_B.
Context d1Source code d2Source code (T1Source code : measurableType d1) (T2Source code : measurableType d2) (RSource code : realType).
Implicit Types A : set (T1 * T2).

Section xsection.
Context (pt2Source code : T2) (m2Source code : T1 -> {measure set T2 -> \bar R}).
Let phiSource code ASource code xSource code := m2 x (xsection A x).
Let BSource code := [set ASource code | measurable A /\ measurable_fun setT (phi A)].

Lemma xsection_ndseq_closedUsed by
  • mathcomp.analysis.kernel
Source code : ndseq_closed B.
Proof.
move=> F ndF; rewrite /B /= => BF; split.
  by apply: bigcupT_measurable => n; have [] := BF n.
have phiF x : phi (F i) x @[iSource code \oo] --> phi (\bigcup_iSource code F i) x.
  rewrite /phi /= xsection_bigcup; apply: nondecreasing_cvg_measure.
  - by move=> n; apply: measurable_xsection; case: (BF n).
  - by apply: bigcupT_measurable => i; apply: measurable_xsection; case: (BF i).
  - by move=> m n mn; exact/subsetPset/le_xsection/subsetPset/ndF.
apply: (emeasurable_fun_cvg (phi \o F)) => //.
- by move=> i; have [] := BF i.
- by move=> x _; exact: phiF.
Qed.
End xsection.

Section ysection.
Context (m1Source code : {measure set T1 -> \bar R}).
Let psiSource code ASource code := m1 \o ysection A.
Let BSource code := [set ASource code | measurable A /\ measurable_fun setT (psi A)].

Lemma ysection_ndseq_closedSource code : ndseq_closed B.
Proof.
move=> F ndF; rewrite /B /= => BF; split.
  by apply: bigcupT_measurable => n; have [] := BF n.
have psiF x : psi (F i) x @[iSource code \oo] --> psi (\bigcup_iSource code F i) x.
  rewrite /psi /= ysection_bigcup; apply: nondecreasing_cvg_measure.
  - by move=> n; apply: measurable_ysection; case: (BF n).
  - by apply: bigcupT_measurable => i; apply: measurable_ysection; case: (BF i).
  - by move=> m n mn; exact/subsetPset/le_ysection/subsetPset/ndF.
apply: (emeasurable_fun_cvg (psi \o F)) => //.
- by move=> i; have [] := BF i.
- by move=> x _; exact: psiF.
Qed.
End ysection.

End ndseq_closed_B.

Section measurable_prod_subset.
Context d1Source code d2Source code (T1Source code : measurableType d1) (T2Source code : measurableType d2) (RSource code : realType).
Implicit Types A : set (T1 * T2).

Section xsection.
Context (m2Source code : {measure set T2 -> \bar R}) (DSource code : set T2) (mDSource code : measurable D).
Let m2DSource code := mrestr m2 mD.
HBSource code.instanceSource code DefinitionSource code _Source code :=Source code MeasureSource code.on m2D.
Let phiSource code ASource code := m2D \o xsection A.
Let BSource code := [set ASource code | measurable A /\ measurable_fun setT (phi A)].

Lemma measurable_prod_subset_xsectionSource code
    (m2D_boundedSource code : exists MSource code, forall XSource code, measurable X -> (m2D X < M%:E)%E) :
  measurable `<=` B.
Proof.
rewrite prod_measurable_rectangle; set C := rectangle _ _.
have CI : setI_closed C by apply: setI_closed_rectangle=> *; exact: measurableI.
have CT : C setT by rewrite -setXTT; exact: rectangle_setX.
have CB : C `<=` B.
  move=> X [X1 mX1 [X2 mX2 <-{X}]]; split; first exact: measurableX.
  have -> : phi (X1 `*` X2) = (fun xSource code => m2D X2 * (\1_X1 x)%:E)%E.
    rewrite funeqE => x; rewrite indicE /phi /m2/= /mrestr.
    have [xX1|xX1] := boolP (x \in X1); first by rewrite mule1 in_xsectionX.
    by rewrite mule0 notin_xsectionX// set0I measure0.
  exact/measurable_funeM/measurable_EFinP.
suff lsystemB : lambda_system setT B by exact: lambda_system_subset.
split => //; [exact: CB| |exact: xsection_ndseq_closed].
move=> X Y XY [mX mphiX] [mY mphiY]; split; first exact: measurableD.
suff -> : phi (X `\` Y) = (fun xSource code => phi X x - phi Y x)%E.
  exact: emeasurable_funB.
rewrite funeqE => x; rewrite /phi/= xsectionD// /m2D measureD/=.
- exact: measurable_xsection.
- exact: measurable_xsection.
- move: m2D_bounded => [M m2M].
  rewrite (lt_le_trans (m2M (xsection X x) _))// ?leey//.
  exact: measurable_xsection.
- by rewrite setIidr//; exact: le_xsection.
Qed.

End xsection.

Section ysection.
Context (m1Source code : {measure set T1 -> \bar R}) (DSource code : set T1) (mDSource code : measurable D).
Let m1DSource code := mrestr m1 mD.
HBSource code.instanceSource code DefinitionSource code _Source code :=Source code MeasureSource code.on m1D.
Let psiSource code ASource code := m1D \o ysection A.
Let BSource code := [set ASource code | measurable A /\ measurable_fun setT (psi A)].

Lemma measurable_prod_subset_ysectionSource code
    (m1_boundedSource code : exists MSource code, forall XSource code, measurable X -> (m1D X < M%:E)%E) :
  measurable `<=` B.
Proof.
rewrite prod_measurable_rectangle; set C := rectangle _ _.
have CI : setI_closed C by apply: setI_closed_rectangle=> *; exact: measurableI.
have CT : C setT by rewrite -setXTT; exact: rectangle_setX.
have CB : C `<=` B.
  move=> X [X1 mX1 [X2 mX2 <-{X}]]; split; first exact: measurableX.
  have -> : psi (X1 `*` X2) = (fun xSource code => m1D X1 * (\1_X2 x)%:E)%E.
    rewrite funeqE => y; rewrite indicE /psi /m1/= /mrestr.
    have [yX2|yX2] := boolP (y \in X2); first by rewrite mule1 in_ysectionX.
    by rewrite mule0 notin_ysectionX// set0I measure0.
  exact/measurable_funeM/measurable_EFinP.
suff lsystemB : lambda_system setT B by exact: lambda_system_subset.
split => //; [exact: CB| |exact: ysection_ndseq_closed].
move=> X Y XY [mX mphiX] [mY mphiY]; split; first exact: measurableD.
rewrite (_ : psi _ = (psi X \- psi Y)%E); last exact: emeasurable_funB.
rewrite funeqE => y; rewrite /psi/= ysectionD// /m1D measureD/=.
- exact: measurable_ysection.
- exact: measurable_ysection.
- have [M m1M] := m1_bounded.
  rewrite (lt_le_trans (m1M (ysection X y) _))// ?leey//.
  exact: measurable_ysection.
- by rewrite setIidr//; exact: le_ysection.
Qed.

End ysection.

End measurable_prod_subset.

Section measurable_fun_xsection.
Context {d1Source code} {d2Source code} {T1Source code : measurableType d1} {T2Source code : measurableType d2}
  {RSource code : realType} (m2Source code : {sigma_finite_measure set T2 -> \bar R}).
Implicit Types A : set (T1 * T2).

Let phiSource code ASource code := m2 \o xsection A.
Let BSource code := [set ASource code | measurable A /\ measurable_fun setT (phi A)].

Lemma measurable_fun_xsectionSource code ASource code : measurable A -> measurable_fun setT (phi A).
Proof.
move: A; suff : measurable `<=` B by move=> + A => /[apply] -[].
have /sigma_finiteP [F [F_T F_nd F_oo]] := sigma_finiteT m2 => X mX.
have -> : X = \bigcup_nSource code (X `&` (setT `*` F n)).
  by rewrite -setI_bigcupr -setX_bigcupr -F_T setXTT setIT.
apply: xsection_ndseq_closed.
  move=> m n mn; apply/subsetPset; apply: setIS; apply: setSX => //.
  exact/subsetPset/F_nd.
move=> n; rewrite -/B; have [? ?] := F_oo n.
pose m2Fn := mrestr m2 (F_oo n).1.
have m2Fn_bounded : exists MSource code, forall XSource code, measurable X -> (m2Fn X < M%:E)%E.
  exists (fine (m2Fn (F n)) + 1) => Y mY.
  rewrite [in ltRHS]EFinD lte_spadder// fineK.
    by rewrite ge0_fin_numE ?measure_ge0//= /m2Fn /mrestr setIid.
  by rewrite /m2Fn /mrestr/= setIid le_measure// inE//; exact: measurableI.
pose phi' ASource code := m2Fn \o xsection A.
pose B' := [set ASource code | measurable A /\ measurable_fun setT (phi' A)].
have subset_B' : measurable `<=` B' by exact: measurable_prod_subset_xsection.
split=> [|_ Y mY]; first by apply: measurableI => //; exact: measurableX.
have [_ /(_ measurableT Y mY)] := subset_B' X mX.
have ->// : phi' X = m2 \o xsection (X `&` setT `*` F n).
by apply/funext => x/=; rewrite /phi' setTX xsectionI xsection_preimage_snd.
Qed.

End measurable_fun_xsection.

Section measurable_fun_ysection.
Context {d1Source code} {d2Source code} {T1Source code : measurableType d1} {T2Source code : measurableType d2}
  {RSource code : realType} (m1Source code : {sigma_finite_measure set T1 -> \bar R}).
Implicit Types A : set (T1 * T2).

Let phiSource code ASource code := m1 \o ysection A.
Let BSource code := [set ASource code | measurable A /\ measurable_fun setT (phi A)].

Lemma measurable_fun_ysectionSource code ASource code : measurable A -> measurable_fun setT (phi A).
Proof.
move: A; suff : measurable `<=` B by move=> + A => /[apply] -[].
have /sigma_finiteP[F [F_T F_nd F_oo]] := sigma_finiteT m1 => X mX.
have -> : X = \bigcup_nSource code (X `&` (F n `*` setT)).
  by rewrite -setI_bigcupr -setX_bigcupl -F_T setXTT setIT.
apply: ysection_ndseq_closed.
  move=> m n mn; apply/subsetPset; apply: setIS; apply: setSX => //.
  exact/subsetPset/F_nd.
move=> n; have [? ?] := F_oo n; rewrite -/B.
pose m1Fn := mrestr m1 (F_oo n).1.
have m1Fn_bounded : exists MSource code, forall XSource code, measurable X -> (m1Fn X < M%:E)%E.
  exists (fine (m1Fn (F n)) + 1) => Y mY.
  rewrite [in ltRHS]EFinD lte_spadder// fineK.
    by rewrite ge0_fin_numE ?measure_ge0// /m1Fn/= /mrestr setIid.
  by rewrite /m1Fn/= /mrestr setIid le_measure// inE//=; exact: measurableI.
pose psi' ASource code := m1Fn \o ysection A.
pose B' := [set ASource code | measurable A /\ measurable_fun setT (psi' A)].
have subset_B' : measurable `<=` B' by exact: measurable_prod_subset_ysection.
split=> [|_ Y mY]; first by apply: measurableI => //; exact: measurableX.
have [_ /(_ measurableT Y mY)] := subset_B' X mX.
have ->// : psi' X = m1 \o (ysection (X `&` F n `*` setT)).
by apply/funext => y/=; rewrite /psi' setXT ysectionI// ysection_preimage_fst.
Qed.

End measurable_fun_ysection.

Section product_measures.
Context d1Source code d2Source code (T1Source code : measurableType d1) (T2Source code : measurableType d2) (RSource code : realType).
Context (m1Source code : set T1 -> \bar R) (m2Source code : set T2 -> \bar R).

Definition product_measure1

product_measure1 : forall [d1 d2 : measure_display] [T1 : measurableType d1] [T2 : measurableType d2] [R : realType], (set T1 -> \bar R) -> (set T2 -> \bar R) -> set (T1 * T2) -> GRing.BaseAddMagma.sort \bar R product_measure1 is not universe polymorphic Arguments product_measure1 [d1 d2]%_measure_display_scope [T1 T2 R] (m1 m2)%_function_scope A%_classical_set_scope product_measure1 is transparent Expands to: Constant mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral_fubini.product_measure1 Declared in library mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral_fubini, line 256, characters 11-27

Source code := (fun ASource code => \int[m1]_xSource code (m2 \o xsection A) x)%E.
Definition product_measure2

product_measure2 : forall [d1 d2 : measure_display] [T1 : measurableType d1] [T2 : measurableType d2] [R : realType], (set T1 -> \bar R) -> (set T2 -> \bar R) -> set (T1 * T2) -> GRing.BaseAddMagma.sort \bar R product_measure2 is not universe polymorphic Arguments product_measure2 [d1 d2]%_measure_display_scope [T1 T2 R] (m1 m2)%_function_scope A%_classical_set_scope product_measure2 is transparent Expands to: Constant mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral_fubini.product_measure2 Declared in library mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral_fubini, line 257, characters 11-27

Source code := (fun ASource code => \int[m2]_xSource code (m1 \o ysection A) x)%E.

End product_measures.

Notation "m1 '\x' m2"Source code := (product_measure1 m1 m2) : ereal_scope.
Notation "m1 '\x^' m2"Source code := (product_measure2 m1 m2) : ereal_scope.

Section product_measure1.
Local Open Scope ereal_scope.
Context {d1Source code} {d2Source code} {T1Source code : measurableType d1} {T2Source code : measurableType d2}
  {RSource code : realType} (m1Source code : {measure set T1 -> \bar R})
  (m2Source code : {sigma_finite_measure set T2 -> \bar R}).
Implicit Types A : set (T1 * T2).

Let pm10Source code : (m1 \x m2) set0 = 0.
Proof.
by rewrite [LHS]integral0_eq// => x/= _; rewrite xsection0. Qed.

Let pm1_ge0Source code ASource code : 0 <= (m1 \x m2) A.
Proof.
by apply: integral_ge0 => // *. Qed.

Let pm1_sigma_additiveSource code : semi_sigma_additive (m1 \x m2).
Proof.
move=> F mF tF mUF.
rewrite [X in _ --> X](_ : _ = \sum_(nSource code <oo) (m1 \x m2) (F n)); last first.
  by apply/cvg_closeP; split; [exact: is_cvg_nneseries|rewrite closeE].
rewrite -integral_nneseries//; first by move=> n; exact: measurable_fun_xsection.
apply: eq_integral => x _; apply/esym/cvg_lim => //=; rewrite xsection_bigcup.
apply: (measure_sigma_additive _ (trivIset_xsection tF)) => ?.
exact: measurable_xsection.
Qed.

HBSource code.instanceSource code DefinitionSource code _Source code :=Source code isMeasureSource code.Build _ _ _ (m1 \x m2)
  pm10 pm1_ge0 pm1_sigma_additive.

End product_measure1.

Section product_measure1E.
Local Open Scope ereal_scope.
Context {d1Source code d2Source code} {T1Source code : measurableType d1} {T2Source code : measurableType d2} {RSource code : realType}
  (m1Source code : {measure set T1 -> \bar R}) (m2Source code : {sigma_finite_measure set T2 -> \bar R}).
Implicit Types A : set (T1 * T2).

Import MeasurableR.

Lemma product_measure1EUsed by
  • mathcomp.analysis.probability_theory.independence
  • mathcomp.analysis.lebesgue_integral_theory.giry
Source code (A1Source code : set T1) (A2Source code : set T2) :
  measurable A1 -> measurable A2 -> (m1 \x m2) (A1 `*` A2) = m1 A1 * m2 A2.
Proof.
move=> mA1 mA2 /=; rewrite /product_measure1 /=.
rewrite (eq_integral (fun xSource code => (\1_A1 x)%:E * m2 A2)).
  by move=> x _; rewrite indicE; have [xA1|xA1] /= := boolP (x \in A1);
    [rewrite in_xsectionX// mul1e|rewrite mul0e notin_xsectionX].
by rewrite ge0_integralZr ?integral_indic ?setIT//; exact: measurableT_comp.
Qed.

End product_measure1E.

Section product_subprobability.
Local Open Scope classical_set_scope.
Local Open Scope ring_scope.
Local Open Scope ereal_scope.
Context {d1Source code} {d2Source code} {T1Source code : measurableType d1} {T2Source code : measurableType d2}
  {RSource code : realType} (m12Source code : subprobability T1 R * subprobability T2 R).

Let prodSource code := m12.1 \x m12.2.

HBSource code.instanceSource code DefinitionSource code _Source code :=Source code MeasureSource code.on prod.

Let prod_setTSource code : prod setT <= 1.
Proof.
rewrite -setXTT [leLHS]product_measure1E// -[leRHS]mule1.
by rewrite lee_pmul// sprobability_setT.
Qed.

HBSource code.instanceSource code DefinitionSource code _Source code :=Source code
  Measure_isSubProbability.Build _ _ _ prod prod_setT.

Definition product_subprobability

product_subprobability : forall {d1 d2 : measure_display} {T1 : measurableType d1} {T2 : measurableType d2} {R : realType}, subprobability T1 R * subprobability T2 R -> subprobability (T1 * T2)%type R product_subprobability is not universe polymorphic Arguments product_subprobability {d1 d2}%_measure_display_scope {T1 T2 R} m12 product_subprobability is transparent Expands to: Constant mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral_fubini.product_subprobability Declared in library mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral_fubini, line 333, characters 11-33

Used by
  • mathcomp.analysis.lebesgue_integral_theory.giry
Source code : subprobability (T1 * T2)%type R := prod.

End product_subprobability.

Section product_subprobability_setC.
Local Open Scope classical_set_scope.
Local Open Scope ereal_scope.
Context {d1Source code} {d2Source code} {T1Source code : measurableType d1} {T2Source code : measurableType d2}
  {RSource code : realType}.

Lemma product_subprobability_setCUsed by
  • mathcomp.analysis.lebesgue_integral_theory.giry
Source code (PSource code : subprobability T1 R * subprobability T2 R)
    (ASource code : set (T1 * T2)) : measurable A ->
  (P.1 \x P.2) (~` A) = (P.1 \x P.2) [set: T1 * T2] - (P.1 \x P.2) A.
Proof.
move=> mA.
rewrite -(setvU A) measureU//=; [exact: measurableC|exact: setICl|].
by rewrite addeK// (_ : (_ \x _)%E = product_subprobability P)// fin_num_measure.
Qed.

End product_subprobability_setC.

Section product_measure_unique.
Local Open Scope ereal_scope.
Context {d1Source code} {d2Source code} {T1Source code : measurableType d1} {T2Source code : measurableType d2}
  {RSource code : realType} (m1Source code : {sigma_finite_measure set T1 -> \bar R})
  (m2Source code : {sigma_finite_measure set T2 -> \bar R}).

Let product_measure_sigma_finiteSource code : sigma_finite setT (m1 \x m2).
Proof.
have /sigma_finiteP[F [TF ndF Foo]] := sigma_finiteT m1.
have /sigma_finiteP[G [TG ndG Goo]] := sigma_finiteT m2.
exists (fun nSource code => F n `*` G n).
 rewrite -setXTT TF TG predeqE => -[x y]; split.
    move=> [/= [n _ Fnx] [k _ Gky]]; exists (maxn n k) => //; split.
    - by move: x Fnx; exact/subsetPset/ndF/leq_maxl.
    - by move: y Gky; exact/subsetPset/ndG/leq_maxr.
  by move=> [n _ []/= ? ?]; split; exists n.
move=> k; have [? ?] := Foo k; have [? ?] := Goo k.
split; first exact: measurableX.
by rewrite product_measure1E// lte_mul_pinfty// ge0_fin_numE.
Qed.


Lemma product_measure_uniqueUsed by
  • mathcomp.analysis.probability_theory.independence
Source code
    (m'Source code : {measure set (T1 * T2) -> \bar R}) :
    (forall ASource code BSource code, measurable A -> measurable B -> m' (A `*` B) = m1 A * m2 B) ->
  forall XSource code : set (T1 * T2), measurable X -> (m1 \x m2) X = m' X.
Proof.
move=> m'E.
have /sigma_finiteP[F [TF ndF Foo]] := sigma_finiteT m1.
have /sigma_finiteP[G [TG ndG Goo]] := sigma_finiteT m2.
have UFGT : \bigcup_kSource code (F k `*` G k) = setT.
  rewrite -setXTT TF TG predeqE => -[x y]; split.
    by move=> [n _ []/= ? ?]; split; exists n.
  move=> [/= [n _ Fnx] [k _ Gky]]; exists (maxn n k) => //; split.
  - by move: x Fnx; exact/subsetPset/ndF/leq_maxl.
  - by move: y Gky; exact/subsetPset/ndG/leq_maxr.
pose C : set_system (T1 * T2) :=
  [set CSource code | exists ASource code, measurable A /\ exists BSource code, measurable B /\ C = A `*` B].
have CI : setI_closed C.
  move=> /= _ _ [X1 [mX1 [X2 [mX2 ->]]]] [Y1 [mY1 [Y2 [mY2 ->]]]].
  rewrite -setXI; exists (X1 `&` Y1); split; first exact: measurableI.
  by exists (X2 `&` Y2); split => //; exact: measurableI.
move=> X mX; apply: (measure_unique C (fun nSource code => F n `*` G n)) => //.
- rewrite prod_measurable_rectangle//; congr (<<s _ >>).
  rewrite predeqE; split => [[A mA [B mB <-]]|[A [mA [B [mB ->]]]]].
    by exists A; split => //; exists B.
  by exists A => //; exists B.
- move=> n; rewrite /C /=; exists (F n); split; first by have [] := Foo n.
  by exists (G n); split => //; have [] := Goo n.
- by move=> A [A1 [mA1 [A2 [mA2 ->]]]]; rewrite m'E//= product_measure1E.
- move=> k; have [? ?] := Foo k; have [? ?] := Goo k.
  by rewrite /= product_measure1E// lte_mul_pinfty// ge0_fin_numE.
Qed.

End product_measure_unique.

Section product_measure2.
Local Open Scope ereal_scope.
Context {d1Source code} {d2Source code} {T1Source code : measurableType d1} {T2Source code : measurableType d2}
  {RSource code : realType} (m1Source code : {sigma_finite_measure set T1 -> \bar R})
  (m2Source code : {measure set T2 -> \bar R}).
Implicit Types A : set (T1 * T2).

Let pm20Source code : (m1 \x^ m2) set0 = 0.
Proof.
by rewrite /(_ \x^ _) integral0_eq// => y/= _; rewrite ysection0 measure0.
Qed.

Let pm2_ge0Source code ASource code : 0 <= (m1 \x^ m2) A.
Proof.
by apply: integral_ge0 => // *; exact/measure_ge0/measurable_ysection.
Qed.

Let pm2_sigma_additiveSource code : semi_sigma_additive (m1 \x^ m2).
Proof.
move=> F mF tF mUF.
rewrite [X in _ --> X](_ : _ = \sum_(nSource code <oo) (m1 \x^ m2) (F n)); last first.
  apply/cvg_closeP; split; last by rewrite closeE.
  by apply: is_cvg_nneseries => *; exact: integral_ge0.
rewrite -integral_nneseries//.
  by move=> n; apply: measurable_fun_ysection => //; rewrite inE.
apply: eq_integral => y _; apply/esym/cvg_lim => //=; rewrite ysection_bigcup.
apply: (measure_sigma_additive _ (trivIset_ysection tF)) => ?.
exact: measurable_ysection.
Qed.

HBSource code.instanceSource code DefinitionSource code _Source code :=Source code isMeasureSource code.Build _ _ _ (m1 \x^ m2)
  pm20 pm2_ge0 pm2_sigma_additive.

End product_measure2.

Section product_measure2E.
Local Open Scope ereal_scope.
Context {d1Source code d2Source code} {T1Source code : measurableType d1} {T2Source code : measurableType d2} {RSource code : realType}
  (m1Source code : {sigma_finite_measure set T1 -> \bar R})
  (m2Source code : {measure set T2 -> \bar R}).

Import MeasurableR.

Lemma product_measure2ESource code (A1Source code : set T1) (A2Source code : set T2)
    (mA1Source code : measurable A1) (mA2Source code : measurable A2) :
  (m1 \x^ m2) (A1 `*` A2) = m1 A1 * m2 A2.
Proof.
have mA1A2 : measurable (A1 `*` A2) by apply: measurableX.
transitivity (\int[m2]_ySource code (m1 \o ysection (A1 `*` A2)) y) => //.
rewrite (_ : _ \o _ = fun ySource code => m1 A1 * (\1_A2 y)%:E); last first.
  by rewrite ge0_integralZl ?integral_indic ?setIT//; exact: measurableT_comp.
rewrite funeqE => y; rewrite indicE.
have [yA2|yA2] := boolP (y \in A2); first by rewrite mule1 /= in_ysectionX.
by rewrite mule0 /= notin_ysectionX.
Qed.

End product_measure2E.

Section product_probability_measures.
Context {d1Source code} {T1Source code : measurableType d1} {d2Source code} {T2Source code : measurableType d2}
  (RSource code : realType) (P1Source code : probability T1 R) (P2Source code : probability T2 R).
Local Open Scope ereal_scope.

Local Notation pro1Source code := (P1 \x P2).

Let pro1_setTSource code : pro1 [set: T1 * T2] = 1.
Proof.
rewrite -setXTT product_measure1E// -[RHS]mule1.
by rewrite -{1}(probability_setT P1) -(probability_setT P2).
Qed.

HBSource code.instanceSource code DefinitionSource code _Source code :=Source code Measure_isProbabilitySource code.Build _ _ _ pro1 pro1_setT.

Local Notation pro2Source code := (P1 \x^ P2).

Let pro2_setTSource code : pro2 setT = 1.
Proof.
rewrite -setXTT product_measure2E// -[RHS]mule1.
by rewrite -{1}(probability_setT P1) -(probability_setT P2).
Qed.

HBSource code.instanceSource code DefinitionSource code _Source code :=Source code Measure_isProbabilitySource code.Build _ _ _ pro2 pro2_setT.

End product_probability_measures.

Section fubini_functions.
Local Open Scope ereal_scope.
Context {d1Source code} {d2Source code} {T1Source code : measurableType d1} {T2Source code : measurableType d2}
  {RSource code : realType} (m1Source code : {measure set T1 -> \bar R})
  (m2Source code : {measure set T2 -> \bar R}) (fSource code : T1 * T2 -> \bar R).

Definition fubini_F

fubini_F : forall {d1 d2 : measure_display} {T1 : measurableType d1} {T2 : measurableType d2} {R : realType}, {measure set T2 -> \bar R}%R -> (T1 * T2 -> \bar R) -> T1 -> GRing.BaseAddMagma.sort \bar R fubini_F is not universe polymorphic Arguments fubini_F {d1 d2}%_measure_display_scope {T1 T2 R} m2 f%_function_scope x fubini_F is transparent Expands to: Constant mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral_fubini.fubini_F Declared in library mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral_fubini, line 504, characters 11-19

Used by
  • mathcomp.analysis.probability_theory.independence
Source code xSource code := \int[m2]_ySource code f (x, y).
Definition fubini_G

fubini_G : forall {d1 d2 : measure_display} {T1 : measurableType d1} {T2 : measurableType d2} {R : realType}, {measure set T1 -> \bar R}%R -> (T1 * T2 -> \bar R) -> T2 -> GRing.BaseAddMagma.sort \bar R fubini_G is not universe polymorphic Arguments fubini_G {d1 d2}%_measure_display_scope {T1 T2 R} m1 f%_function_scope y fubini_G is transparent Expands to: Constant mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral_fubini.fubini_G Declared in library mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral_fubini, line 505, characters 11-19

Source code ySource code := \int[m1]_xSource code f (x, y).

End fubini_functions.

Section fubini_tonelli.
Local Open Scope ereal_scope.
Context {d1Source code} {d2Source code} {T1Source code : measurableType d1} {T2Source code : measurableType d2}
 {RSource code : realType} (m1Source code : {sigma_finite_measure set T1 -> \bar R})
 (m2Source code : {sigma_finite_measure set T2 -> \bar R}).

Section indic_fubini_tonelli.
Context (ASource code : set (T1 * T2)) (mASource code : measurable A).
Implicit Types A : set (T1 * T2).
Let fSource code : (T1 * T2) -> R := \1_A.

Let FSource code := fubini_F m2 (EFin \o f).
Let GSource code := fubini_G m1 (EFin \o f).

Lemma indic_fubini_tonelli_F_ge0Source code xSource code : 0 <= F x.
Proof.
by apply: integral_ge0 => // y _; rewrite lee_fin. Qed.

Lemma indic_fubini_tonelli_G_ge0Source code xSource code : 0 <= G x.
Proof.
by apply: integral_ge0 => // y _; rewrite lee_fin. Qed.

Lemma indic_fubini_tonelli_FESource code : F = m2 \o xsection A.
Proof.
apply/funext => x/=.
rewrite -[RHS]mul1e -integral_cst//; first exact: measurable_xsection.
rewrite /F /fubini_F /f [in RHS]integral_mkcond.
by apply: eq_integral => y _ /=; rewrite patchE mem_xsection indicE; case: ifPn.
Qed.

Lemma indic_fubini_tonelli_GESource code : G = m1 \o ysection A.
Proof.
apply/funext => x/=.
rewrite -[RHS]mul1e -integral_cst//; first exact: measurable_ysection.
rewrite /G /fubini_G /f [in RHS]integral_mkcond.
by apply: eq_integral => y _ /=; rewrite patchE mem_ysection indicE; case: ifPn.
Qed.

Lemma indic_measurable_fun_fubini_tonelli_FSource code : measurable_fun setT F.
Proof.
by rewrite indic_fubini_tonelli_FE//; exact: measurable_fun_xsection.
Qed.

Lemma indic_measurable_fun_fubini_tonelli_GSource code : measurable_fun setT G.
Proof.
by rewrite indic_fubini_tonelli_GE//; exact: measurable_fun_ysection.
Qed.

Lemma indic_fubini_tonelli1Source code : \int[m1 \x m2]_zSource code (f z)%:E = \int[m1]_xSource code F x.
Proof.
by rewrite /f integral_indic// setIT indic_fubini_tonelli_FE. Qed.

Lemma indic_fubini_tonelli2Source code : \int[m1 \x^ m2]_zSource code (f z)%:E = \int[m2]_ySource code G y.
Proof.
by rewrite /f integral_indic// setIT indic_fubini_tonelli_GE. Qed.

Lemma indic_fubini_tonelliSource code : \int[m1]_xSource code F x = \int[m2]_ySource code G y.
Proof.
rewrite -indic_fubini_tonelli1// -indic_fubini_tonelli2// integral_indic//=.
rewrite integral_indic//= !setIT.
by apply: product_measure_unique => //= ? ? ? ?; rewrite product_measure2E.
Qed.

End indic_fubini_tonelli.

Section sfun_fubini_tonelli.
Context (fSource code : {nnsfun T1 * T2 >-> R}).

Import HBNNSimple.
Import MeasurableR.

Let FSource code := fubini_F m2 (EFin \o f).
Let GSource code := fubini_G m1 (EFin \o f).

Lemma sfun_fubini_tonelli_FESource code : F = fun xSource code =>
  \sum_(kSource code \in range f) k%:E * m2 (xsection (f @^-1` [set k]) x).
Proof.
rewrite funeqE => x; rewrite /F /fubini_F [in LHS]/=.
under eq_fun do rewrite fimfunE -fsumEFin//.
rewrite ge0_integral_fsum //.
- move=> i; apply/measurable_EFinP/measurableT_comp => //=.
  exact: measurableT_comp.
- by move=> r y _; rewrite EFinM nnfun_muleindic_ge0.
apply: eq_fsbigr => i; rewrite inE => -[/= t _ <-{i}].
under eq_fun do rewrite EFinM.
rewrite ge0_integralZl//; first exact/measurable_EFinP/measurableT_comp.
by rewrite -/((m2 \o xsection _) x) -indic_fubini_tonelli_FE.
Qed.

Lemma sfun_measurable_fun_fubini_tonelli_FSource code : measurable_fun [set: T1] F.
Proof.
rewrite sfun_fubini_tonelli_FE//; apply: emeasurable_fsum => // r.
exact/measurable_funeM/measurable_fun_xsection.
Qed.

Lemma sfun_fubini_tonelli_GESource code : G = fun ySource code =>
  \sum_(kSource code \in range f) k%:E * m1 (ysection (f @^-1` [set k]) y).
Proof.
rewrite funeqE => y; rewrite /G /fubini_G [in LHS]/=.
under eq_fun do rewrite fimfunE -fsumEFin//.
rewrite ge0_integral_fsum //.
- move=> i; apply/measurable_EFinP/measurableT_comp => //=.
  exact: measurableT_comp.
- by move=> r x _; rewrite EFinM nnfun_muleindic_ge0.
apply: eq_fsbigr => i; rewrite inE => -[/= t _ <-{i}].
under eq_fun do rewrite EFinM.
rewrite ge0_integralZl//; first exact/measurable_EFinP/measurableT_comp.
by rewrite -/((m1 \o ysection _) y) -indic_fubini_tonelli_GE.
Qed.

Lemma sfun_measurable_fun_fubini_tonelli_GSource code : measurable_fun setT G.
Proof.
rewrite sfun_fubini_tonelli_GE//; apply: emeasurable_fsum => // r.
exact/measurable_funeM/measurable_fun_ysection.
Qed.

Let EFinfSource code xSource code : (f x)%:E =
  \sum_(kSource code \in range f) k%:E * (\1_(f @^-1` [set k]) x)%:E.
Proof.
by rewrite fsumEFin //= fimfunE. Qed.

Lemma sfun_fubini_tonelli1Source code : \int[m1 \x m2]_zSource code (f z)%:E = \int[m1]_xSource code F x.
Proof.
under [LHS]eq_integral
  do rewrite EFinf; rewrite ge0_integral_fsum //.
  - by move=> r; exact/measurable_EFinP/measurableT_comp.
  - by move=> r /= z _; exact: nnfun_muleindic_ge0.
transitivity (\sum_(kSource code \in range f)
  \int[m1]_xSource code (k%:E * fubini_F m2 (EFin \o \1_(f @^-1` [set k])) x)).
  apply: eq_fsbigr => i; rewrite inE => -[z _ <-{i}].
  rewrite ge0_integralZl//=; first exact/measurable_EFinP.
  rewrite indic_fubini_tonelli1// -ge0_integralZl//.
    by move=> /= x _; exact: indic_fubini_tonelli_F_ge0.
  exact: indic_measurable_fun_fubini_tonelli_F.
rewrite -ge0_integral_fsum; [by []| | |by []|]; first 2 last.
- apply: eq_integral => x _; rewrite sfun_fubini_tonelli_FE.
  by under eq_fsbigr do rewrite indic_fubini_tonelli_FE//.
- by move=> r; exact/measurable_funeM/indic_measurable_fun_fubini_tonelli_F.
move=> r x _; rewrite /fubini_F.
have [r0|r0] := leP 0%R r.
  by rewrite mule_ge0//; exact: indic_fubini_tonelli_F_ge0.
rewrite integral0_eq ?mule0// => y _.
by rewrite preimage_nnfun0//= indicE in_set0.
Qed.

Lemma sfun_fubini_tonelli2Source code : \int[m1 \x^ m2]_zSource code (f z)%:E = \int[m2]_ySource code G y.
Proof.
under [LHS]eq_integral
  do rewrite EFinf; rewrite ge0_integral_fsum //.
  - by move=> i; exact/measurable_EFinP/measurableT_comp.
  - by move=> r /= z _; exact: nnfun_muleindic_ge0.
transitivity (\sum_(kSource code \in range f)
  \int[m2]_xSource code (k%:E * (fubini_G m1 (EFin \o \1_(f @^-1` [set k])) x))).
  apply: eq_fsbigr => i; rewrite inE => -[z _ <-{i}].
  rewrite ge0_integralZl//=; first exact/measurable_EFinP.
  rewrite indic_fubini_tonelli2// -ge0_integralZl//.
    by move=> /= x _; exact: indic_fubini_tonelli_G_ge0.
  exact: indic_measurable_fun_fubini_tonelli_G.
rewrite -ge0_integral_fsum; [by []| | |by []|]; first 2 last.
- apply: eq_integral => x _; rewrite sfun_fubini_tonelli_GE.
  by under eq_fsbigr do rewrite indic_fubini_tonelli_GE//.
- by move=> r; apply/measurable_funeM/indic_measurable_fun_fubini_tonelli_G.
move=> r y _; rewrite /fubini_G.
have [r0|r0] := leP 0%R r.
  by rewrite mule_ge0//; exact: indic_fubini_tonelli_G_ge0.
rewrite integral0_eq ?mule0// => x _.
by rewrite preimage_nnfun0//= indicE in_set0.
Qed.

Lemma sfun_fubini_tonelliSource code :
  \int[m1 \x m2]_zSource code (f z)%:E = \int[m1 \x^ m2]_zSource code (f z)%:E.
Proof.
apply: eq_measure_integral => /= A Ameasurable _.
by apply: product_measure_unique => //= *; rewrite product_measure2E.
Qed.

End sfun_fubini_tonelli.

Section fubini_tonelli.
Context (fSource code : T1 * T2 -> \bar R).
Hypothesis mfSource code : measurable_fun setT f.
Hypothesis f0Source code : forall xSource code, 0 <= f x.
Let TSource code : measurableType _ := (T1 * T2)%type.

Let FSource code := fubini_F m2 f.
Let GSource code := fubini_G m1 f.

Import HBNNSimple.
Import MeasurableR.

Let F_Source code (gSource code : {nnsfun T >-> R}^nat) nSource code xSource code := \int[m2]_ySource code (g n (x, y))%:E.
Let G_Source code (gSource code : {nnsfun T >-> R}^nat) nSource code ySource code := \int[m1]_xSource code (g n (x, y))%:E.

Lemma measurable_fun_fubini_tonelli_FSource code : measurable_fun setT F.
Proof.
pose g := nnsfun_approx measurableT mf.
apply: (emeasurable_fun_cvg (F_ g)) => //.
  by move=> n; exact: sfun_measurable_fun_fubini_tonelli_F.
move=> x _.
rewrite /F_ /F /fubini_F [in X in _ --> X](_ : (fun _ => _) =
    fun ySource code => limn (EFin \o g ^~ (x, y))).
  by rewrite funeqE => y; apply/esym/cvg_lim => //; exact: cvg_nnsfun_approx.
apply: cvg_monotone_convergence => //.
- by move=> n; apply/measurable_EFinP => //; exact/measurableT_comp.
- by move=> n y _; rewrite lee_fin//; exact: fun_ge0.
- by move=> y _ a b ab; rewrite lee_fin; exact/lefP/nd_nnsfun_approx.
Qed.

Lemma measurable_fun_fubini_tonelli_GSource code : measurable_fun setT G.
Proof.
pose g := nnsfun_approx measurableT mf.
apply: (emeasurable_fun_cvg (G_ g)) => //.
  by move=> n; exact: sfun_measurable_fun_fubini_tonelli_G.
move=> y _; rewrite /G_ /G /fubini_G [in X in _ --> X](_ : (fun _ => _) =
    fun xSource code => limn (EFin \o g ^~ (x, y))).
  by rewrite funeqE => x; apply/esym/cvg_lim => //; exact: cvg_nnsfun_approx.
apply: cvg_monotone_convergence => //.
- by move=> n; apply/measurable_EFinP => //; exact/measurableT_comp.
- by move=> n x _; rewrite lee_fin; exact: fun_ge0.
- by move=> x _ a b ab; rewrite lee_fin; exact/lefP/nd_nnsfun_approx.
Qed.

Lemma fubini_tonelli1Used by
  • mathcomp.analysis.probability_theory.independence
  • mathcomp.analysis.lebesgue_integral_theory.giry
Source code : \int[m1 \x m2]_zSource code f z = \int[m1]_xSource code F x.
Proof.
pose g := nnsfun_approx measurableT mf.
have F_F x : F x = limn (F_ g ^~ x).
  rewrite [RHS](_ : _ = limn (fun nSource code => \int[m2]_ySource code (EFin \o g n) (x, y)))//.
  rewrite -monotone_convergence//.
  - by move=> n; exact/measurable_EFinP/measurableT_comp.
  - by move=> n /= y _; rewrite lee_fin; exact: fun_ge0.
  - by move=> y /= _ a b ab; rewrite lee_fin; exact/lefP/nd_nnsfun_approx.
  by apply: eq_integral => y _; apply/esym/cvg_lim => //; exact: cvg_nnsfun_approx.
rewrite [RHS](_ : _ = limn (fun nSource code => \int[m1 \x m2]_zSource code (EFin \o g n) z)); last first.
  rewrite -monotone_convergence //.
  - by move=> n; exact/measurable_EFinP.
  - by move=> n /= x _; rewrite lee_fin; exact: fun_ge0.
  - by move=> y /= _ a b ab; rewrite lee_fin; exact/lefP/nd_nnsfun_approx.
  by apply: eq_integral => /= x _; apply/esym/cvg_lim => //; exact: cvg_nnsfun_approx.
rewrite [LHS](_ : _ =
    limn (fun nSource code => \int[m1]_xSource code (\int[m2]_ySource code (EFin \o g n) (x, y)))); last first.
  set r := fun _ => _; set l := fun _ => _; have -> // : l = r.
  by apply/funext  => n; rewrite /l /r sfun_fubini_tonelli1.
rewrite [RHS](_ : _ = limn (fun nSource code => \int[m1]_xSource code F_ g n x))//.
rewrite -monotone_convergence => [//||||]; last exact: eq_integral.
- by move=> n; exact: sfun_measurable_fun_fubini_tonelli_F.
- move=> n x _; apply: integral_ge0 => // y _ /=; rewrite lee_fin.
  exact: fun_ge0.
move=> x /= _ a b ab; apply: ge0_le_integral => //.
- by move=> y _; rewrite lee_fin; exact: fun_ge0.
- exact/measurable_EFinP/measurableT_comp.
- exact/measurable_EFinP/measurableT_comp.
- by move=> y _; rewrite lee_fin; exact/lefP/nd_nnsfun_approx.
Qed.

Lemma fubini_tonelli2Used by
  • mathcomp.analysis.lebesgue_integral_theory.giry
Source code : \int[m1 \x m2]_zSource code f z = \int[m2]_ySource code G y.
Proof.
pose g := nnsfun_approx measurableT mf.
have G_G y : G y = limn (G_ g ^~ y).
  rewrite /G /fubini_G.
  rewrite [RHS](_ : _ = limn (fun nSource code => \int[m1]_xSource code (EFin \o g n) (x, y)))//.
  rewrite -monotone_convergence//.
  - by move=> n; exact/measurable_EFinP/measurableT_comp.
  - by move=> n /= x _; rewrite lee_fin; exact: fun_ge0.
  - by move=> x /= _ a b ab; rewrite lee_fin; exact/lefP/nd_nnsfun_approx.
  by apply: eq_integral => x _; apply/esym/cvg_lim => //; exact: cvg_nnsfun_approx.
rewrite [RHS](_ : _ = limn (fun nSource code => \int[m1 \x m2]_zSource code (EFin \o g n) z)); last first.
  rewrite -monotone_convergence //.
  - by move=> n; exact/measurable_EFinP.
  - by move=> n /= x _; rewrite lee_fin; exact: fun_ge0.
  - by move=> y /= _ a b ab; rewrite lee_fin; exact/lefP/nd_nnsfun_approx.
  by apply: eq_integral => /= x _; apply/esym/cvg_lim => //; exact: cvg_nnsfun_approx.
rewrite [LHS](_ : _ = limn
    (fun nSource code => \int[m2]_ySource code (\int[m1]_xSource code (EFin \o g n) (x, y)))); last first.
  set r := fun _ => _; set l := fun _ => _; have -> // : l = r.
  by apply/funext => n; rewrite /l /r sfun_fubini_tonelli sfun_fubini_tonelli2.
rewrite [RHS](_ : _ = limn (fun nSource code => \int[m2]_ySource code G_ g n y))//.
rewrite -monotone_convergence => [//||||]; last exact: eq_integral.
- by move=> n; exact: sfun_measurable_fun_fubini_tonelli_G.
- by move=> n y _; apply: integral_ge0 => // x _ /=; rewrite lee_fin fun_ge0.
move=> y /= _ a b ab; apply: ge0_le_integral => //.
- by move=> x _; rewrite lee_fin fun_ge0.
- exact/measurable_EFinP/measurableT_comp.
- exact/measurable_EFinP/measurableT_comp.
- by move=> x _; rewrite lee_fin; exact/lefP/nd_nnsfun_approx.
Qed.

Lemma fubini_tonelliUsed by
  • mathcomp.analysis.probability_theory.random_variable
  • mathcomp.analysis.probability_theory.normal_distribution
Source code :
  \int[m1]_xSource code \int[m2]_ySource code f (x, y) = \int[m2]_ySource code \int[m1]_xSource code f (x, y).
Proof.
by rewrite -fubini_tonelli1// fubini_tonelli2. Qed.

End fubini_tonelli.

End fubini_tonelli.
Arguments fubini_tonelli1 {d1 d2 T1 T2 R m1 m2} f.
Arguments fubini_tonelli2 {d1 d2 T1 T2 R m1 m2} f.
Arguments fubini_tonelli {d1 d2 T1 T2 R m1 m2} f.
Arguments measurable_fun_fubini_tonelli_F {d1 d2 T1 T2 R m2} f.
Arguments measurable_fun_fubini_tonelli_G {d1 d2 T1 T2 R m1} f.

Section fubini.
Local Open Scope ereal_scope.
Context {d1Source code} {d2Source code} {T1Source code : measurableType d1} {T2Source code : measurableType d2}
  {RSource code : realType} (m1Source code : {sigma_finite_measure set T1 -> \bar R})
  (m2Source code : {sigma_finite_measure set T2 -> \bar R}) (fSource code : T1 * T2 -> \bar R).

Lemma integrable12ltyPSource code : measurable_fun setT f ->
  (m1 \x m2).-integrable setT f <-> \int[m1]_xSource code \int[m2]_ySource code `|f (x, y)| < +oo.
Proof.
move=> mf; split=> [/integrableP[_]|] ioo; [|apply/integrableP; split=> [//|]].
- by rewrite -(fubini_tonelli1 (abse \o f))//=; exact: measurableT_comp.
- by rewrite fubini_tonelli1//; exact: measurableT_comp.
Qed.

Lemma integrable21ltyPSource code : measurable_fun setT f ->
  (m1 \x m2).-integrable setT f <-> \int[m2]_ySource code \int[m1]_xSource code `|f (x, y)| < +oo.
Proof.
move=> mf; split=> [/integrableP[_]|] ioo; [|apply/integrableP; split=> [//|]].
- by rewrite -(fubini_tonelli2 (abse \o f))//=; exact: measurableT_comp.
- by rewrite fubini_tonelli2//; exact: measurableT_comp.
Qed.

Let measurable_fun1Source code : measurable_fun setT f ->
  measurable_fun setT (fun xSource code => \int[m2]_ySource code `|f (x, y)|).
Proof.
move=> mf; apply: (measurable_fun_fubini_tonelli_F (abse \o f)) => //=.
exact: measurableT_comp.
Qed.

Let measurable_fun2Source code : measurable_fun setT f ->
  measurable_fun setT (fun ySource code => \int[m1]_xSource code `|f (x, y)|).
Proof.
move=> mf; apply: (measurable_fun_fubini_tonelli_G (abse \o f)) => //=.
exact: measurableT_comp.
Qed.

Hypothesis imfSource code : (m1 \x m2).-integrable setT f.
Let mfSource code : measurable_fun setT f
Proof.
exact: measurable_int imf. Qed.

Lemma ae_integrable1Source code :
  {ae m1, forall xSource code, m2.-integrable setT (fun ySource code => f (x, y))}.
Proof.
have : m1.-integrable setT (fun xSource code => \int[m2]_ySource code `|f (x, y)|).
  apply/integrableP; split; first exact/measurable_fun1.
  rewrite (le_lt_trans _  ((integrable12ltyP mf).1 imf))// ge0_le_integral //.
  - by apply: measurableT_comp => //; exact: measurable_fun1.
  - exact: measurable_fun1.
  - by move=> *; rewrite gee0_abs//; exact: integral_ge0.
move/integrable_ae => /(_ measurableT); apply: filterS => x /= /(_ I) im2f.
apply/integrableP; split; first exact/measurableT_comp.
by move/fin_numPlt : im2f => /andP[].
Qed.

Lemma ae_integrable2Source code :
  {ae m2, forall ySource code, m1.-integrable setT (fun xSource code => f (x, y))}.
Proof.
have : m2.-integrable setT (fun ySource code => \int[m1]_xSource code `|f (x, y)|).
  apply/integrableP; split; first exact/measurable_fun2.
  rewrite (le_lt_trans _ ((integrable21ltyP mf).1 imf))// ge0_le_integral //.
  - by apply: measurableT_comp => //; exact: measurable_fun2.
  - exact: measurable_fun2.
  - by move=> *; rewrite gee0_abs//; exact: integral_ge0.
move/integrable_ae => /(_ measurableT); apply: filterS => x /= /(_ I) im2f.
apply/integrableP; split; first exact/measurableT_comp.
by move/fin_numPlt : im2f => /andP[].
Qed.

Let FSource code := fubini_F m2 f.

Let FplusSource code xSource code := \int[m2]_ySource code f^\+ (x, y).
Let FminusSource code xSource code := \int[m2]_ySource code f^\- (x, y).

Let FESource code : F = Fplus \- Fminus.
Proof.
apply/funext=> x; rewrite [LHS]integralE.
under eq_integral do rewrite funepos_comp/=.
by under [X in _ - X = _]eq_integral do rewrite funeneg_comp/=.
Qed.

Let measurable_FplusSource code : measurable_fun setT Fplus.
Proof.
by apply: measurable_fun_fubini_tonelli_F => //; exact: measurable_funepos.
Qed.

Let measurable_FminusSource code : measurable_fun setT Fminus.
Proof.
by apply: measurable_fun_fubini_tonelli_F => //; exact: measurable_funeneg.
Qed.

Lemma measurable_fubini_FSource code : measurable_fun setT F.
Proof.
rewrite FE.
by apply: emeasurable_funB; [exact: measurable_Fplus|exact: measurable_Fminus].
Qed.

Let integrable_FplusSource code : m1.-integrable setT Fplus.
Proof.
apply/integrableP; split=> //.
apply: le_lt_trans ((integrable12ltyP mf).1 imf).
apply: ge0_le_integral; [by []|by []|..].
- by apply: measurableT_comp; last apply: measurable_Fplus.
- exact: measurable_fun1.
- move=> x _; apply: le_trans.
    apply: le_abse_integral => //; apply: measurableT_comp => //.
    exact: measurable_funepos.
  apply: ge0_le_integral => //.
  + apply: measurableT_comp => //.
    by apply: measurableT_comp => //; exact: measurable_funepos.
  + by apply: measurableT_comp => //; exact/measurableT_comp.
  + by move=> y _; rewrite gee0_abs// -/((abse \o f) _) -funeposDneg leeDl.
Qed.

Let integrable_FminusSource code : m1.-integrable setT Fminus.
Proof.
apply/integrableP; split=> //.
apply: le_lt_trans ((integrable12ltyP mf).1 imf).
apply: ge0_le_integral; [by []|by []|..].
- exact: measurableT_comp.
- exact: measurable_fun1.
- move=> x _; apply: le_trans.
    apply: le_abse_integral => //; apply: measurableT_comp => //.
    exact: measurable_funeneg.
  apply: ge0_le_integral => //.
  + apply: measurableT_comp => //; apply: measurableT_comp => //.
    exact: measurable_funeneg.
  + by apply: measurableT_comp => //; exact: measurableT_comp.
  + by move=> y _; rewrite gee0_abs// -/((abse \o f) _) -funeposDneg leeDr.
Qed.

Lemma integrable_fubini_FSource code : m1.-integrable setT F.
Proof.
by rewrite FE; exact: integrableB. Qed.

Let GSource code := fubini_G m1 f.

Let GplusSource code ySource code := \int[m1]_xSource code f^\+ (x, y).
Let GminusSource code ySource code := \int[m1]_xSource code f^\- (x, y).

Let GESource code : G = Gplus \- Gminus.
Proof.
apply/funext=> x; rewrite [LHS]integralE.
under eq_integral do rewrite funepos_comp/=.
by under [X in _ - X = _]eq_integral do rewrite funeneg_comp/=.
Qed.

Let measurable_GplusSource code : measurable_fun setT Gplus.
Proof.
by apply: measurable_fun_fubini_tonelli_G => //; exact: measurable_funepos.
Qed.

Let measurable_GminusSource code : measurable_fun setT Gminus.
Proof.
by apply: measurable_fun_fubini_tonelli_G => //; exact: measurable_funeneg.
Qed.

Lemma measurable_fubini_GSource code : measurable_fun setT G.
Proof.
by rewrite GE; exact: emeasurable_funB. Qed.

Let integrable_GplusSource code : m2.-integrable setT Gplus.
Proof.
apply/integrableP; split=> //; apply: le_lt_trans ((integrable21ltyP mf).1 imf).
apply: ge0_le_integral; [by []|by []|exact: measurableT_comp|..].
- exact: measurable_fun2.
- move=> y _; apply: le_trans.
    apply: le_abse_integral => //; apply: measurableT_comp => //.
    exact: measurable_funepos.
  apply: ge0_le_integral => //.
  + apply: measurableT_comp => //.
    by apply: measurableT_comp => //; exact: measurable_funepos.
  + by apply: measurableT_comp => //; exact: measurableT_comp.
  + by move=> x _; rewrite gee0_abs// -/((abse \o f) _) -funeposDneg leeDl.
Qed.

Let integrable_GminusSource code : m2.-integrable setT Gminus.
Proof.
apply/integrableP; split=> //; apply: le_lt_trans ((integrable21ltyP mf).1 imf).
apply: ge0_le_integral; [by []|by []|exact: measurableT_comp|..].
- exact: measurable_fun2.
- move=> y _; apply: le_trans.
    apply: le_abse_integral => //; apply: measurableT_comp => //.
    exact: measurable_funeneg.
  apply: ge0_le_integral => //.
  + apply: measurableT_comp => //.
    by apply: measurableT_comp => //; exact: measurable_funeneg.
  + by apply: measurableT_comp => //; exact: measurableT_comp.
  + by move=> x _; rewrite gee0_abs// -/((abse \o f) _) -funeposDneg leeDr.
Qed.

Lemma integral12_prod_meas1Source code : \int[m1]_xSource code F x = \int[m1 \x m2]_zSource code f z.
Proof.
rewrite FE integralB; [by[]|exact: integrable_Fplus|exact: integrable_Fminus|].
by rewrite [in RHS]integralE ?fubini_tonelli1//;
  [exact: measurable_funepos|exact: measurable_funeneg].
Qed.

Lemma integral21_prod_meas1Source code : \int[m2]_xSource code G x = \int[m1 \x m2]_zSource code f z.
Proof.
rewrite GE integralB; [by[]|exact: integrable_Gplus|exact: integrable_Gminus|].
by rewrite [in RHS]integralE ?fubini_tonelli2//;
  [exact: measurable_funepos|exact: measurable_funeneg].
Qed.

Lemma integral21_prod_meas2Source code : \int[m2]_xSource code G x = \int[m1 \x^ m2]_zSource code f z.
Proof.
rewrite integral21_prod_meas1; apply: eq_measure_integral => //= A mA _.
by apply: product_measure_unique => // B C mB mC/=; rewrite product_measure2E.
Qed.

Lemma integral12_prod_meas2Source code : \int[m1]_xSource code F x = \int[m1 \x^ m2]_zSource code f z.
Proof.
rewrite integral12_prod_meas1//; apply: eq_measure_integral => //= A mA _.
by apply: product_measure_unique => // B C mB mC/=; rewrite product_measure2E.
Qed.

Theorem FubiniSource code :
  \int[m1]_xSource code \int[m2]_ySource code f (x, y) = \int[m2]_ySource code \int[m1]_xSource code f (x, y).
Proof.
by rewrite integral12_prod_meas1 -integral21_prod_meas1. Qed.

End fubini.

Section sfinite_fubini.
Local Open Scope ereal_scope.
Context {dSource code} {d'Source code} {XSource code : measurableType d} {YSource code : measurableType d'} {RSource code : realType}
  (m1Source code : {sfinite_measure set X -> \bar R})
  (m2Source code : {sfinite_measure set Y -> \bar R}) (fSource code : X * Y -> \bar R).

Hypotheses (f0Source code : forall xySource code, 0 <= f xy) (mfSource code : measurable_fun [set: X * Y] f).

Lemma sfinite_FubiniSource code :
  \int[m1]_xSource code \int[m2]_ySource code f (x, y) = \int[m2]_ySource code \int[m1]_xSource code f (x, y).
Proof.
pose s1 := sfinite_measure_seq m1.
pose s2 := sfinite_measure_seq m2.
rewrite [LHS](eq_measure_integral (mseries s1 0)).
  by move=> A mA _; rewrite /=; exact: sfinite_measure_seqP.
transitivity (\int[mseries s1 0]_xSource code \int[mseries s2 0]_ySource code f (x, y)).
  apply: eq_integral => x _; apply: eq_measure_integral => ? ? _.
  exact: sfinite_measure_seqP.
transitivity (\sum_(nSource code <oo) \int[s1 n]_xSource code \sum_(mSource code <oo) \int[s2 m]_ySource code f (x, y)).
  rewrite ge0_integral_measure_series; [by []| | |].
    by move=> t _; exact: integral_ge0.
    rewrite [X in measurable_fun _ X](_ : _ =
        fun xSource code => \sum_(nSource code <oo) \int[s2 n]_ySource code f (x, y)).
      apply/funext => x.
      by rewrite ge0_integral_measure_series//; exact/measurableT_comp.
    apply: ge0_emeasurable_sum; first by move=> k x *; exact: integral_ge0.
    by move=> k _; exact: measurable_fun_fubini_tonelli_F.
  apply: eq_eseriesr => n _; apply: eq_integral => x _.
  by rewrite ge0_integral_measure_series//; exact/measurableT_comp.
transitivity (\sum_(nSource code <oo) \sum_(mSource code <oo) \int[s1 n]_xSource code \int[s2 m]_ySource code f (x, y)).
  apply: eq_eseriesr => n _; rewrite integral_nneseries => [//|||//].
    by move=> m; exact: measurable_fun_fubini_tonelli_F.
  by move=> m x _; exact: integral_ge0.
transitivity (\sum_(nSource code <oo) \sum_(mSource code <oo) \int[s2 m]_ySource code \int[s1 n]_xSource code f (x, y)).
  apply: eq_eseriesr => n _; apply: eq_eseriesr => m _.
  by rewrite fubini_tonelli//; exact: finite_measure_sigma_finite.
transitivity (\sum_(nSource code <oo) \int[mseries s2 0]_ySource code \int[s1 n]_xSource code f (x, y)).
  apply: eq_eseriesr => n _; rewrite ge0_integral_measure_series => [//|||//].
    by move=> y _; exact: integral_ge0.
  exact: measurable_fun_fubini_tonelli_G.
transitivity (\int[mseries s2 0]_ySource code \sum_(nSource code <oo) \int[s1 n]_xSource code f (x, y)).
  rewrite integral_nneseries => [//|||//].
    by move=> n; apply: measurable_fun_fubini_tonelli_G.
  by move=> n y _; exact: integral_ge0.
transitivity (\int[mseries s2 0]_ySource code \int[mseries s1 0]_xSource code f (x, y)).
  apply: eq_integral => y _.
  by rewrite ge0_integral_measure_series//; exact/measurableT_comp.
transitivity (\int[m2]_ySource code \int[mseries s1 0]_xSource code f (x, y)).
  by apply: eq_measure_integral => A mA _ /=; rewrite sfinite_measure_seqP.
apply: eq_integral => y _; apply: eq_measure_integral => A mA _ /=.
by rewrite sfinite_measure_seqP.
Qed.

End sfinite_fubini.
Arguments sfinite_Fubini {d d' X Y R} m1 m2 f.
Generated by rocqnavi
Source
Uses
Used By