proposition: Lemma product_measure_unique (m' : {measure set [the semiRingOfSetsType _ of T1 * T2] -> \bar R}) : (forall A1 A2, measurable A1 -> measurable A2 -> m' (A1 `*` A2) = m1 A1 * m2 A2) -> forall X : set (T1 * T2), measurable X -> (m1 \x m2) X = m' X.
proof: 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_k (F k `*` G k) = setT. rewrite -setMTT 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 (set (T1 * T2)) := [set C | exists A, measurable A /\ exists B, measurable B /\ C = A `*` B]. have CI : setI_closed C. move=> /= _ _ [X1 [mX1 [X2 [mX2 ->]]]] [Y1 [mY1 [Y2 [mY2 ->]]]]. rewrite -setMI; exists (X1 `&` Y1); split; first exact: measurableI. by exists (X2 `&` Y2); split => //; exact: measurableI. move=> X mX; apply: (measure_unique C (fun n => F n `*` G n)) => //. - rewrite measurable_prod_measurableType //; 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.
imports: HB(structures) mathcomp(all_ssreflect ssralg ssrnum ssrint interval finmap) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(cardinality fsbigop ) signed reals ereal topology normedtype sequences real_interval esum measure lebesgue_measure numfun