Built with
Alectryon , running Coq+SerAPI v8.15.0+0.15.0. Bubbles (
) indicate interactive fragments: hover for details, tap to reveal contents. Use
Ctrl+↑ Ctrl+↓ to navigate,
Ctrl+🖱️ to focus. On Mac, use
⌘ instead of
Ctrl .
(* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C. *)
From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint interval.Notation "[ predI _ & _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]Notation "[ predU _ & _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]Notation "[ predD _ & _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]Notation "[ predC _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]Notation "[ preim _ of _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]Notation "_ + _" was already used in scope nat_scope.
[notation-overridden,parsing]Notation "_ - _" was already used in scope nat_scope.
[notation-overridden,parsing]Notation "_ <= _" was already used in scope nat_scope.
[notation-overridden,parsing]Notation "_ < _" was already used in scope nat_scope.
[notation-overridden,parsing]Notation "_ >= _" was already used in scope nat_scope.
[notation-overridden,parsing]Notation "_ > _" was already used in scope nat_scope.
[notation-overridden,parsing]Notation "_ <= _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing]Notation "_ < _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing]Notation "_ <= _ < _" was already used in scope
nat_scope. [notation-overridden,parsing]Notation "_ < _ < _" was already used in scope
nat_scope. [notation-overridden,parsing]Notation "_ * _" was already used in scope nat_scope.
[notation-overridden,parsing]New coercion path [GRing.subring_closedM;
GRing.smulr_closedN] : GRing.subring_closed >-> GRing.oppr_closed is ambiguous with existing
[GRing.subring_closedB; GRing.zmod_closedN] : GRing.subring_closed >-> GRing.oppr_closed.
[ambiguous-paths,typechecker] New coercion path [GRing.subring_closed_semi;
GRing.semiring_closedM] : GRing.subring_closed >-> GRing.mulr_closed is ambiguous with existing
[GRing.subring_closedM; GRing.smulr_closedM] : GRing.subring_closed >-> GRing.mulr_closed.
New coercion path [GRing.subring_closed_semi;
GRing.semiring_closedD] : GRing.subring_closed >-> GRing.addr_closed is ambiguous with existing
[GRing.subring_closedB; GRing.zmod_closedD] : GRing.subring_closed >-> GRing.addr_closed.
[ambiguous-paths,typechecker] New coercion path [GRing.sdivr_closed_div;
GRing.divr_closedM] : GRing.sdivr_closed >-> GRing.mulr_closed is ambiguous with existing
[GRing.sdivr_closedM; GRing.smulr_closedM] : GRing.sdivr_closed >-> GRing.mulr_closed.
[ambiguous-paths,typechecker] New coercion path [GRing.subalg_closedBM;
GRing.subring_closedB] : GRing.subalg_closed >-> GRing.zmod_closed is ambiguous with existing
[GRing.subalg_closedZ; GRing.submod_closedB] : GRing.subalg_closed >-> GRing.zmod_closed.
[ambiguous-paths,typechecker] New coercion path [GRing.divring_closed_div;
GRing.sdivr_closedM] : GRing.divring_closed >-> GRing.smulr_closed is ambiguous with existing
[GRing.divring_closedBM; GRing.subring_closedM] : GRing.divring_closed >-> GRing.smulr_closed.
[ambiguous-paths,typechecker] New coercion path [GRing.divalg_closedBdiv;
GRing.divring_closedBM] : GRing.divalg_closed >-> GRing.subring_closed is ambiguous with existing
[GRing.divalg_closedZ; GRing.subalg_closedBM] : GRing.divalg_closed >-> GRing.subring_closed.
[ambiguous-paths,typechecker] New coercion path [GRing.Pred.subring_smul;
GRing.Pred.smul_mul] : GRing.Pred.subring >-> GRing.Pred.mul is ambiguous with existing
[GRing.Pred.subring_semi; GRing.Pred.semiring_mul] : GRing.Pred.subring >-> GRing.Pred.mul.
[ambiguous-paths,typechecker]
From mathcomp Require Import finmap fingroup perm rat.
From mathcomp.classical Require Import boolp classical_sets functions.
From mathcomp.classical Require Import cardinality fsbigop mathcomp_extra.
Require Import reals ereal signed topology numfun normedtype.
From HB Require Import structures.
Require Import sequences esum measure real_interval realfun.
(******************************************************************************)
(* Lebesgue Measure *)
(* *)
(* This file contains a formalization of the Lebesgue measure using the *)
(* Caratheodory's theorem available in measure.v and further develops the *)
(* theory of measurable functions. *)
(* *)
(* Main reference: *)
(* - Daniel Li, Intégration et applications, 2016 *)
(* - Achim Klenke, Probability Theory 2nd edition, 2014 *)
(* *)
(* hlength A == length of the hull of the set of real numbers A *)
(* ocitv == set of open-closed intervals ]x, y] where *)
(* x and y are real numbers *)
(* lebesgue_measure == the Lebesgue measure *)
(* *)
(* ps_infty == inductive definition of the powerset *)
(* {0, {-oo}, {+oo}, {-oo,+oo}} *)
(* emeasurable G == sigma-algebra over \bar R built out of the *)
(* measurables G of a sigma-algebra over R *)
(* elebesgue_measure == the Lebesgue measure extended to \bar R *)
(* *)
(* The modules RGenOInfty, RGenInftyO, RGenCInfty, RGenOpens provide proofs *)
(* of equivalence between the sigma-algebra generated by list of intervals *)
(* and the sigma-algebras generated by open rays, closed rays, and open *)
(* intervals. *)
(* *)
(* The modules ErealGenOInfty, ErealGenCInfty, ErealGenInftyO provide proofs *)
(* of equivalence between emeasurable and the sigma-algebras generated open *)
(* rays and closed rays. *)
(* *)
(******************************************************************************)
Set Implicit Arguments .
Unset Strict Implicit .
Unset Printing Implicit Defensive .
Import Order.TTheory GRing.Theory Num.Def Num.Theory.
Import numFieldTopology.Exports.
Local Open Scope classical_set_scope.
Local Open Scope ring_scope.
Reserved Notation "R .-ocitv" (at level 1 , format "R .-ocitv" ).
Reserved Notation "R .-ocitv.-measurable"
(at level 2 , format "R .-ocitv.-measurable" ).
Section hlength .
Local Open Scope ereal_scope.
Variable R : realType.
Implicit Types i j : interval R.
Definition hlength (A : set R) : \bar R := let i := Rhull A in i.2 - i.1 .
Lemma hlength0 : hlength (set0 : set R) = 0 .
Proof . by rewrite /hlength Rhull0 /= subee. Qed .
Lemma hlength_singleton (r : R) : hlength `[r, r] = 0 .
Proof .
rewrite /hlength /= asboolT// sup_itvcc//= asboolT//.
by rewrite asboolT inf_itvcc//= ?subee // inE.
Qed .
Lemma hlength_setT : hlength setT = +oo%E :> \bar R.
Proof . by rewrite /hlength RhullT. Qed .
Lemma hlength_itv i : hlength [set ` i] = if i.2 > i.1 then i.2 - i.1 else 0 .
Proof .
case : ltP => [/lt_ereal_bnd/neitvP i12|]; first by rewrite /hlength set_itvK.
rewrite le_eqVlt => /orP[|/lt_ereal_bnd i12]; last first .
rewrite (_ : [set ` i] = set0) ?hlength0 //.
by apply /eqP/negPn; rewrite -/(neitv _) neitvE -leNgt (ltW i12).
case : i => -[ba a|[|]] [bb b|[|]] //=.
- rewrite /= => /eqP[->{b}]; move : ba bb => -[] []; try
by rewrite set_itvE hlength0.
by rewrite hlength_singleton.
- by move => _; rewrite set_itvE hlength0.
- by move => _; rewrite set_itvE hlength0.
Qed .
Lemma hlength_finite_fin_num i : neitv i -> hlength [set ` i] < +oo ->
((i.1 : \bar R) \is a fin_num) /\ ((i.2 : \bar R) \is a fin_num).
Proof .
move : i => [[ba a|[]] [bb b|[]]] /neitvP //=; do ?by rewrite ?set_itvE ?eqxx .
by move => _; rewrite hlength_itv /= ltry.
by move => _; rewrite hlength_itv /= ltNyr.
by move => _; rewrite hlength_itv.
Qed .
Lemma finite_hlengthE i : neitv i -> hlength [set ` i] < +oo ->
hlength [set ` i] = (fine i.2 )%:E - (fine i.1 )%:E.
Proof .
move => i0 ioo; have [ri1 ri2] := hlength_finite_fin_num i0 ioo.
rewrite !fineK// hlength_itv; case : ifPn => //.
rewrite -leNgt le_eqVlt => /predU1P[->|]; first by rewrite subee.
by move /lt_ereal_bnd/ltW; rewrite leNgt; move : i0 => /neitvP => ->.
Qed .
Lemma hlength_infty_bnd b r :
hlength [set ` Interval -oo%O (BSide b r)] = +oo :> \bar R.
Proof . by rewrite hlength_itv /= ltNyr. Qed .
Lemma hlength_bnd_infty b r :
hlength [set ` Interval (BSide b r) +oo%O] = +oo :> \bar R.
Proof . by rewrite hlength_itv /= ltry. Qed .
Lemma pinfty_hlength i : hlength [set ` i] = +oo ->
(exists s r , i = Interval -oo%O (BSide s r) \/ i = Interval (BSide s r) +oo%O)
\/ i = `]-oo, +oo[.
Proof .
rewrite hlength_itv; case : i => -[ba a|[]] [bb b|[]] //= => [|_|_|].
- by case : ifPn.
- by left ; exists ba , a; right .
- by left ; exists bb , b; left .
- by right .
Qed .
Lemma hlength_ge0 i : 0 <= hlength [set ` i].
Proof .
rewrite hlength_itv; case : ifPn => //; case : (i.1 : \bar _) => [r| |].
- by rewrite suber_ge0//; exact : ltW.
- by rewrite ltNge leey.
- by case : (i.2 : \bar _) => //= [r _]; rewrite leey.
Qed .
Local Hint Extern 0 (0 %:E <= hlength _) => solve [apply : hlength_ge0] : core.
Lemma hlength_Rhull (A : set R) : hlength [set ` Rhull A] = hlength A.
Proof . by rewrite /hlength Rhull_involutive. Qed .
Lemma le_hlength_itv i j : {subset i <= j} -> hlength [set ` i] <= hlength [set ` j].
Proof .
set I := [set ` i]; set J := [set ` j].
have [->|/set0P I0] := eqVneq I set0; first by rewrite hlength0 hlength_ge0.
have [J0|/set0P J0] := eqVneq J set0.
by move /subset_itvP; rewrite -/J J0 subset0 -/I => ->.
move => /subset_itvP ij; apply : lee_sub => /=.
have [ui|ui] := asboolP (has_ubound I).
have [uj /=|uj] := asboolP (has_ubound J); last by rewrite leey.
by rewrite lee_fin le_sup // => r Ir; exists r ; split => //; apply : ij.
have [uj /=|//] := asboolP (has_ubound J).
by move : ui; have := subset_has_ubound ij uj.
have [lj /=|lj] := asboolP (has_lbound J); last by rewrite leNye.
have [li /=|li] := asboolP (has_lbound I); last first .
by move : li; have := subset_has_lbound ij lj.
rewrite lee_fin ler_oppl opprK le_sup// ?has_inf_supN //; last exact /nonemptyN.
move => r [r' Ir' <-{r}]; exists (- r')%R.
by split => //; exists r' => //; apply : ij.
Qed .
Lemma le_hlength : {homo hlength : A B / (A `<=` B) >-> A <= B}.
Proof .
move => a b /le_Rhull /le_hlength_itv.
by rewrite (hlength_Rhull a) (hlength_Rhull b).
Qed .
End hlength .
Arguments hlength {R}.
#[global ] Hint Extern 0 (0 %:E <= hlength _) => solve [apply : hlength_ge0] : core.
Section itv_semiRingOfSets .
Variable R : realType.
Implicit Types (I J K : set R).
Definition ocitv_type : Type := R.
Definition ocitv := [set `]x.1 , x.2 ]%classic | x in [set : R * R]].
Lemma is_ocitv a b : ocitv `]a, b]%classic.
Proof . by exists (a , b); split => //=; rewrite in_itv/= andbT. Qed .
Hint Extern 0 (ocitv _) => solve [apply : is_ocitv] : core.
Lemma ocitv0 : ocitv set0.
Proof . by exists (1 , 0 ); rewrite //= set_itv_ge ?bnd_simp //= ltr10. Qed .
Hint Resolve ocitv0 : core.
Lemma ocitvP X : ocitv X <-> X = set0 \/ exists2 x, x.1 < x.2 & X = `]x.1 , x.2 ]%classic.
Proof .
split => [[x _ <-]|[->//|[x xlt ->]]]//.
case : (boolP (x.1 < x.2 )) => x12; first by right ; exists x .
by left ; rewrite set_itv_ge.
Qed .
Lemma ocitvD : semi_setD_closed ocitv.
Proof .
move => _ _ [a _ <-] /ocitvP[|[b ltb]] ->.
rewrite setD0; exists [set `]a.1 , a.2 ]%classic].
by split => [//|? ->//||? ? -> ->//]; rewrite bigcup_set1.
rewrite setDE setCitv/= setIUr -!set_itvI.
rewrite /Order.meet/= /Order.meet/= /Order.join/=
?(andbF, orbF)/= ?(meetEtotal, joinEtotal).
rewrite -negb_or le_total/=; set c := minr _ _; set d := maxr _ _.
have inside : a.1 < c -> d < a.2 -> `]a.1 , c] `&` `]d, a.2 ] = set0.
rewrite -subset0 lt_minr lt_maxl => /andP[a12 ab1] /andP[_ ba2] x /= [].
have b1a2 : b.1 <= a.2 by rewrite ltW// (lt_trans ltb).
have a1b2 : a.1 <= b.2 by rewrite ltW// (lt_trans _ ltb).
rewrite /c /d (min_idPr _)// (max_idPr _)// !in_itv /=.
move => /andP[a1x xb1] /andP[b2x xa2].
by have := lt_le_trans b2x xb1; case : ltgtP ltb.
exists ((if a.1 < c then [set `]a.1 , c]%classic] else set0) `|`
(if d < a.2 then [set `]d, a.2 ]%classic] else set0)); split .
- by rewrite finite_setU; do ! case : ifP.
- by move => ? []; case : ifP => ? // ->//=.
- by rewrite bigcup_setU; congr (_ `|` _);
case : ifPn => ?; rewrite ?bigcup_set1 ?bigcup_set0 // set_itv_ge.
- move => I J/=; case : ifP => //= ac; case : ifP => //= da [] // -> []// ->.
by rewrite inside // => -[].
by rewrite setIC inside // => -[].
Qed .
Lemma ocitvI : setI_closed ocitv.
Proof .
move => _ _ [a _ <-] [b _ <-]; rewrite -set_itvI/=.
rewrite /Order.meet/= /Order.meet /Order.join/=
?(andbF, orbF)/= ?(meetEtotal, joinEtotal).
by rewrite -negb_or le_total/=.
Qed .
Definition ocitv_display : Type -> measure_display. Proof . exact . Qed .
HB.instance Definition _ :=
@isSemiRingOfSets.Build (ocitv_display R)
ocitv_type (Pointed.class R) ocitv ocitv0 ocitvI ocitvD.
Notation "R .-ocitv" := (ocitv_display R) : measure_display_scope.
Notation "R .-ocitv.-measurable" := (measurable : set (set (ocitv_type))) :
classical_set_scope.
Lemma hlength_ge0' (I : set ocitv_type) : (0 <= hlength I)%E.
Proof . by rewrite -hlength0 le_hlength. Qed .
(* Unused *)
(* Lemma hlength_semi_additive2 : semi_additive2 hlength. *)
(* Proof. *)
(* move=> I J /ocitvP[|[a a12]] ->; first by rewrite set0U hlength0 add0e. *)
(* move=> /ocitvP[|[b b12]] ->; first by rewrite setU0 hlength0 adde0. *)
(* rewrite -subset0 => + ab0 => /ocitvP[|[x x12] abx]. *)
(* by rewrite setU_eq0 => -[-> ->]; rewrite setU0 hlength0 adde0. *)
(* rewrite abx !hlength_itv//= ?lte_fin a12 b12 x12/= -!EFinB -EFinD. *)
(* wlog ab1 : a a12 b b12 ab0 abx / a.1 <= b.1 => [hwlog|]. *)
(* have /orP[ab1|ba1] := le_total a.1 b.1; first by apply: hwlog. *)
(* by rewrite [in RHS]addrC; apply: hwlog => //; rewrite (setIC, setUC). *)
(* have := ab0; rewrite subset0 -set_itv_meet/=. *)
(* rewrite /Order.join /Order.meet/= ?(andbF, orbF)/= ?(meetEtotal, joinEtotal). *)
(* rewrite -negb_or le_total/=; set c := minr _ _; set d := maxr _ _. *)
(* move=> /eqP/neitvP/=; rewrite bnd_simp/= /d/c (max_idPr _)// => /negP. *)
(* rewrite -leNgt le_minl orbC lt_geF//= => {c} {d} a2b1. *)
(* have ab i j : i \in `]a.1, a.2] -> j \in `]b.1, b.2] -> i <= j. *)
(* by move=> ia jb; rewrite (le_le_trans _ _ a2b1) ?(itvP ia) ?(itvP jb). *)
(* have /(congr1 sup) := abx; rewrite sup_setU// ?sup_itv_bounded// => bx. *)
(* have /(congr1 inf) := abx; rewrite inf_setU// ?inf_itv_bounded// => ax. *)
(* rewrite -{}ax -{x}bx in abx x12 *. *)
(* case: ltgtP a2b1 => // a2b1 _; last first. *)
(* by rewrite a2b1 [in RHS]addrC subrKA. *)
(* exfalso; pose c := (a.2 + b.1) / 2%:R. *)
(* have /predeqP/(_ c)[_ /(_ _)/Box[]] := abx. *)
(* apply: subset_itv_oo_oc; have := mid_in_itvoo a2b1. *)
(* by apply/subitvP; rewrite subitvE ?bnd_simp/= ?ltW. *)
(* apply/not_orP; rewrite /= !in_itv/=. *)
(* by rewrite lt_geF ?midf_lt//= andbF le_gtF ?midf_le//= ltW. *)
(* Qed. *)
Lemma hlength_semi_additive : semi_additive (hlength : set ocitv_type -> _).
Proof .
move => /= I n /(_ _)/cid2-/all_sig[b]/all_and2[_]/(_ _)/esym-/funext {I}->.
move => Itriv [[/= a1 a2] _] /esym /[dup] + ->.
rewrite hlength_itv ?lte_fin /= -EFinB.
case : ifPn => a12; last first .
pose I i := `](b i).1 , (b i).2 ]%classic.
rewrite set_itv_ge//= -(bigcup_mkord _ I) /I => /bigcup0P I0.
by under eq_bigr => i _ do rewrite I0//= hlength0; rewrite big1.
set A := `]a1, a2]%classic.
rewrite -bigcup_pred; set P := xpredT; rewrite (eq_bigl P)//.
move : P => P; have [p] := ubnP #|P|; elim : p => // p IHp in P a2 a12 A *.
rewrite ltnS => cP /esym AE.
have : A a2 by rewrite /A /= in_itv/= lexx andbT.
rewrite AE/= => -[i /= Pi] a2bi.
case : (boolP ((b i).1 < (b i).2 )) => bi; last by rewrite itv_ge in a2bi.
have {}a2bi : a2 = (b i).2 .
apply /eqP; rewrite eq_le (itvP a2bi)/=.
suff : A (b i).2 by move => /itvP->.
by rewrite AE; exists i => //=; rewrite in_itv/= lexx andbT.
rewrite {a2}a2bi in a12 A AE *.
rewrite (bigD1 i)//= hlength_itv ?lte_fin /= bi !EFinD -addeA.
congr (_ + _)%E; apply /eqP; rewrite addeC -sube_eq// 1 ?adde_defC //.
rewrite ?EFinN oppeK addeC; apply /eqP.
case : (eqVneq a1 (b i).1 ) => a1bi.
rewrite {a1}a1bi in a12 A AE {IHp} *; rewrite subee ?big1 // => j.
move => /andP[Pj Nji]; rewrite hlength_itv ?lte_fin /=; case : ifPn => bj//.
exfalso ; have /trivIsetP/(_ j i I I Nji) := Itriv.
pose m := ((b j).1 + (b j).2 ) / 2 %:R.
have mbj : `](b j).1 , (b j).2 ]%classic m.
by rewrite /= !in_itv/= ?(midf_lt, midf_le)//= ltW.
rewrite -subset0 => /(_ m); apply ; split => //.
by suff : A m by []; rewrite AE; exists j => //.
have a1b2 j : P j -> (b j).1 < (b j).2 -> a1 <= (b j).2 .
move => Pj bj; suff /itvP-> : A (b j).2 by [].
by rewrite AE; exists j => //=; rewrite ?in_itv /= bj//=.
have a1b j : P j -> (b j).1 < (b j).2 -> a1 <= (b j).1 .
move => Pj bj; case : ltP=> // bj1a.
suff : A a1 by rewrite /A/= in_itv/= ltxx.
by rewrite AE; exists j ; rewrite //= in_itv/= bj1a//= a1b2.
have bbi2 j : P j -> (b j).1 < (b j).2 -> (b j).2 <= (b i).2 .
move => Pj bj; suff /itvP-> : A (b j).2 by [].
by rewrite AE; exists j => //=; rewrite ?in_itv /= bj//=.
apply /IHp.
- by rewrite lt_neqAle a1bi/= a1b.
- rewrite (leq_trans _ cP)// -(cardID (pred1 i) P).
rewrite [X in (_ < X + _)%N](@eq_card _ _ (pred1 i)); last first .
by move => j; rewrite !inE andbC; case : eqVneq => // ->.
rewrite ?card1 ?ltnS // subset_leq_card//.
by apply /fintype.subsetP => j; rewrite -topredE/= !inE andbC.
apply /seteqP; split => /= [x [j/= /andP[Pj Nji]]|x/= xabi].
case : (boolP ((b j).1 < (b j).2 )) => bj; last by rewrite itv_ge.
apply : subitvP; rewrite subitvE ?bnd_simp a1b//= leNgt.
have /trivIsetP/(_ j i I I Nji) := Itriv.
rewrite -subset0 => /(_ (b j).2 ); apply : contra_notN => /= bi1j2.
by rewrite !in_itv/= bj !lexx bi1j2 bbi2.
have : A x.
rewrite /A/= in_itv/= (itvP xabi)/= ltW//.
by rewrite (le_lt_trans _ bi) ?(itvP xabi).
rewrite AE => -[j /= Pj xbj].
exists j => //=.
apply /andP; split => //; apply : contraTneq xbj => ->.
by rewrite in_itv/= le_gtF// (itvP xabi).
Qed .
HB.instance Definition _ := isContent.Build _ R _
(hlength : set ocitv_type -> _) (@hlength_ge0') hlength_semi_additive.
Hint Extern 0 ((_ .-ocitv).-measurable _) => solve [apply : is_ocitv] : core.
Lemma hlength_sigma_sub_additive :
sigma_sub_additive (hlength : set ocitv_type -> _).
Proof .
move => I A /(_ _)/cid2-/all_sig[b]/all_and2[_]/(_ _)/esym AE.
move => [a _ <-]; rewrite hlength_itv ?lte_fin /= -EFinB => lebig.
case : ifPn => a12; last by rewrite nneseries_esum// esum_ge0.
apply : lee_adde => e.
rewrite [e%:num]splitr [in leRHS]EFinD addeA -lee_subl_addr//.
apply : le_trans (epsilon_trick _ _ _) => //=.
have eVn_gt0 n : 0 < e%:num / 2 / (2 ^ n.+1 )%:R.
by rewrite divr_gt0// ltr0n// expn_gt0.
have eVn_ge0 n := ltW (eVn_gt0 n).
pose Aoo i : set ocitv_type :=
`](b i).1 , (b i).2 + e%:num / 2 / (2 ^ i.+1 )%:R[%classic.
pose Aoc i : set ocitv_type :=
`](b i).1 , (b i).2 + e%:num / 2 / (2 ^ i.+1 )%:R]%classic.
have : `[a.1 + e%:num / 2 , a.2 ] `<=` \bigcup_i Aoo i.
apply : (@subset_trans _ `]a.1 , a.2 ]).
move => x; rewrite /= !in_itv /= => /andP[+ -> //].
by move => /lt_le_trans-> //; rewrite ltr_addl.
apply : (subset_trans lebig); apply : subset_bigcup => i _; rewrite AE /Aoo/=.
move => x /=; rewrite !in_itv /= => /andP[-> /le_lt_trans->]//=.
by rewrite ltr_addl.
have := @segment_compact _ (a.1 + e%:num / 2 ) a.2 ; rewrite compact_cover.
move => /[apply ]-[i _|X _ Xc]; first exact : interval_open.
have : `](a.1 + e%:num / 2 ), a.2 ] `<=` \bigcup_(i in [set ` X]) Aoc i.
move => x /subset_itv_oc_cc /Xc [i /= Xi] Aooix.
by exists i => //; apply : subset_itv_oo_oc Aooix.
have /[apply ] := @content_sub_fsum _ _ _
[the content _ _ of hlength : set ocitv_type -> _] _ [set ` X].
move => /(_ _ _ _)/Box[]//=; apply : le_le_trans.
rewrite hlength_itv ?lte_fin -?EFinD /= -addrA -opprD.
by case : ltP => //; rewrite lee_fin subr_le0.
rewrite nneseries_esum//; last by move => *; rewrite adde_ge0//= ?lee_fin .
rewrite esum_ge//; exists [set ` X] => //; rewrite fsbig_finite// ?set_fsetK //=.
rewrite fsbig_finite//= set_fsetK//.
rewrite lee_sum // => i _; rewrite ?AE // !hlength_itv/= ?lte_fin -?EFinD /=.
do !case : ifPn => //= ?; do ?by rewrite ?adde_ge0 ?lee_fin // ?subr_ge0 // ?ltW .
by rewrite addrAC.
by rewrite addrAC lee_fin ler_add// subr_le0 leNgt.
Qed .
Lemma hlength_sigma_finite : sigma_finite [set : ocitv_type] hlength.
Proof .
exists (fun k : nat => `] (- k%:R)%R, k%:R]%classic).
apply /esym; rewrite -subTset => x _ /=; exists `|(floor `|x| + 1 )%R|%N => //=.
rewrite in_itv/= !natr_absz intr_norm intrD.
suff : `|x| < `|(floor `|x|)%:~R + 1 | by rewrite ltr_norml => /andP[-> /ltW->].
by rewrite ger0_norm ?addr_ge0 ?ler0z ?floor_ge0 // lt_succ_floor.
by move => k; split => //; rewrite hlength_itv/= -EFinB; case : ifP; rewrite ltry.
Qed .
Definition lebesgue_measure := Hahn_ext
[the content _ _ of hlength : set ocitv_type -> _].
Let lebesgue_measure0 : lebesgue_measure set0 = 0 %E.
Proof . by []. Qed .
Let lebesgue_measure_ge0 : forall x , (0 <= lebesgue_measure x)%E.
Proof . exact : measure .Hahn_ext_ge0. Qed .
Let lebesgue_measure_semi_sigma_additive : semi_sigma_additive lebesgue_measure.
Proof . exact /measure .Hahn_ext_sigma_additive/hlength_sigma_sub_additive. Qed .
HB.instance Definition _ := isMeasure.Build _ _ _ lebesgue_measure
lebesgue_measure0 lebesgue_measure_ge0 lebesgue_measure_semi_sigma_additive.
End itv_semiRingOfSets .
Arguments lebesgue_measure {R}.
Notation "R .-ocitv" := (ocitv_display R) : measure_display_scope.
Notation "R .-ocitv.-measurable" := (measurable : set (set (ocitv_type R))) :
classical_set_scope.
Section lebesgue_measure .
Variable R : realType.
Let gitvs := [the measurableType _ of salgebraType (@ocitv R)].
Lemma lebesgue_measure_unique (mu : {measure set gitvs -> \bar R}) :
(forall X , ocitv X -> hlength X = mu X) ->
forall X , measurable X -> lebesgue_measure X = mu X.
Proof .
move => muE X mX; apply : Hahn_ext_unique => //=.
- exact : hlength_sigma_sub_additive.
- exact : hlength_sigma_finite.
Qed .
End lebesgue_measure .
Section ps_infty .
Context {T : Type }.
Local Open Scope ereal_scope.
Inductive ps_infty : set \bar T -> Prop :=
| ps_infty0 : ps_infty set0
| ps_ninfty : ps_infty [set -oo]
| ps_pinfty : ps_infty [set +oo]
| ps_inftys : ps_infty [set -oo; +oo].
Lemma ps_inftyP (A : set \bar T) : ps_infty A <-> A `<=` [set -oo; +oo].
Proof .
split => [[]//|Aoo].
by have [] := subset_set2 Aoo; move => ->; constructor .
Qed .
Lemma setCU_Efin (A : set T) (B : set \bar T) : ps_infty B ->
~` (EFin @` A) `&` ~` B = (EFin @` ~` A) `|` ([set -oo%E; +oo%E] `&` ~` B).
Proof .
move => ps_inftyB.
have -> : ~` (EFin @` A) = EFin @` (~` A) `|` [set -oo; +oo]%E.
by rewrite EFin_setC setDKU // => x [|] -> -[].
rewrite setIUl; congr (_ `|` _); rewrite predeqE => -[x| |]; split ; try by case .
by move => [] x' Ax' [] <-{x}; split ; [exists x' |case : ps_inftyB => // -[]].
Qed .
End ps_infty .
Section salgebra_ereal .
Variables (R : realType) (G : set (set R)).
Let measurableR : set (set R) := G.-sigma.-measurable.
Definition emeasurable : set (set \bar R) :=
[set EFin @` A `|` B | A in measurableR & B in ps_infty].
Lemma emeasurable0 : emeasurable set0.
Proof .
exists set0 ; first exact : measurable0.
by exists set0 ; rewrite ?setU0 // ?image_set0 //; constructor .
Qed .
Lemma emeasurableC (X : set \bar R) : emeasurable X -> emeasurable (~` X).
Proof .
move => -[A mA] [B PooB <-]; rewrite setCU setCU_Efin //.
exists (~` A); [exact : measurableC | exists ([set -oo%E; +oo%E] `&` ~` B) => //].
case : PooB.
- by rewrite setC0 setIT; constructor .
- rewrite setIUl setICr set0U -setDE.
have [_ ->] := @setDidPl (\bar R) [set +oo%E] [set -oo%E]; first by constructor .
by rewrite predeqE => x; split => // -[->].
- rewrite setIUl setICr setU0 -setDE.
have [_ ->] := @setDidPl (\bar R) [set -oo%E] [set +oo%E]; first by constructor .
by rewrite predeqE => x; split => // -[->].
- by rewrite setICr; constructor .
Qed .
Lemma bigcupT_emeasurable (F : (set \bar R)^nat) :
(forall i , emeasurable (F i)) -> emeasurable (\bigcup_i (F i)).
Proof .
move => mF; pose P := fun i j => measurableR j.1 /\ ps_infty j.2 /\
F i = [set x%:E | x in j.1 ] `|` j.2 .
have [f fi] : {f : nat -> (set R) * (set \bar R) & forall i , P i (f i) }.
by apply : choice => i; have [x mx [y PSoo'y] xy] := mF i; exists (x , y).
exists (\bigcup_i (f i).1 ).
by apply : bigcupT_measurable => i; exact : (fi i).1 .
exists (\bigcup_i (f i).2 ).
apply /ps_inftyP => x [n _] fn2x.
have /ps_inftyP : ps_infty(f n).2 by have [_ []] := fi n.
exact .
rewrite [RHS](@eq_bigcupr _ _ _ _
(fun i => [set x%:E | x in (f i).1 ] `|` (f i).2 )); last first .
by move => i; have [_ []] := fi i.
rewrite bigcupU; congr (_ `|` _).
rewrite predeqE => i /=; split => [[r [n _ fn1r <-{i}]]|[n _ [r fn1r <-{i}]]];
by [exists n => //; exists r | exists r => //; exists n ].
Qed .
Definition ereal_isMeasurable :
isMeasurable default_measure_display (\bar R) :=
isMeasurable.Build _ _ (Pointed.class _)
emeasurable0 emeasurableC bigcupT_emeasurable.
End salgebra_ereal .
Section puncture_ereal_itv .
Variable R : realDomainType.
Implicit Types (y : R) (b : bool).
Local Open Scope ereal_scope.
Lemma punct_eitv_bnd_pinfty b y : [set ` Interval (BSide b y%:E) +oo%O] =
EFin @` [set ` Interval (BSide b y) +oo%O] `|` [set +oo].
Proof .
rewrite predeqE => x; split ; rewrite /= in_itv andbT.
- move : x => [x| |] yxb; [|by right |by case : b yxb].
by left ; exists x => //; rewrite in_itv /= andbT; case : b yxb.
- move => [[r]|->].
+ by rewrite in_itv /= andbT => yxb <-; case : b yxb.
+ by case : b => /=; rewrite ?(ltry, leey).
Qed .
Lemma punct_eitv_ninfty_bnd b y : [set ` Interval -oo%O (BSide b y%:E)] =
[set -oo%E] `|` EFin @` [set x | x \in Interval -oo%O (BSide b y)].
Proof .
rewrite predeqE => x; split ; rewrite /= in_itv.
- move : x => [x| |] yxb; [|by case : b yxb|by left ].
by right ; exists x => //; rewrite in_itv /= andbT; case : b yxb.
- move => [->|[r]].
+ by case : b => /=; rewrite ?(ltNyr, leNye).
+ by rewrite in_itv /= => yxb <-; case : b yxb.
Qed .
Lemma punct_eitv_setTR : range (@EFin R) `|` [set +oo] = [set ~ -oo].
Proof .
rewrite eqEsubset; split => [a [[a' _ <-]|->]|] //.
by move => [x| |] //= _; [left ; exists x |right ].
Qed .
Lemma punct_eitv_setTL : range (@EFin R) `|` [set -oo] = [set ~ +oo].
Proof .
rewrite eqEsubset; split => [a [[a' _ <-]|->]|] //.
by move => [x| |] //= _; [left ; exists x |right ].
Qed .
End puncture_ereal_itv .
Lemma set1_bigcap_oc (R : realType) (r : R) :
[set r] = \bigcap_i `]r - i.+1 %:R^-1 , r]%classic.
Proof .
apply /seteqP; split => [x ->|].
by move => i _/=; rewrite in_itv/= lexx ltr_subl_addr ltr_addl invr_gt0 ltr0n.
move => x rx; apply /esym/eqP; rewrite eq_le (itvP (rx 0 %N _))// andbT.
apply /ler_addgt0Pl => e e_gt0; rewrite -ler_subl_addl ltW//.
have := rx `|floor e^-1 %R|%N I; rewrite /= in_itv => /andP[/le_lt_trans->]//.
rewrite ler_add2l ler_opp2 -lef_pinv ?invrK //; last by rewrite qualifE.
by rewrite -natr1 natr_absz ger0_norm ?floor_ge0 ?invr_ge0 1 ?ltW // lt_succ_floor.
Qed .
Lemma itv_bnd_open_bigcup (R : realType) b (r s : R) :
[set ` Interval (BSide b r) (BLeft s)] =
\bigcup_n [set ` Interval (BSide b r) (BRight (s - n.+1 %:R^-1 ))].
Proof .
apply /seteqP; split => [x/=|]; last first .
move => x [n _ /=] /[!in_itv] /andP[-> /le_lt_trans]; apply .
by rewrite ltr_subl_addr ltr_addl invr_gt0 ltr0n.
rewrite in_itv/= => /andP[sx xs]; exists `|ceil ((s - x)^-1 )|%N => //=.
rewrite in_itv/= sx/= ler_subr_addl addrC -ler_subr_addl.
rewrite -[in X in _ <= X](invrK (s - x)) ler_pinv.
- rewrite -natr1 natr_absz ger0_norm; last first .
by rewrite ceil_ge0// invr_ge0 subr_ge0 ltW.
by rewrite (@le_trans _ _ (ceil (s - x)^-1 )%:~R)// ?ler_addl // ceil_ge.
- by rewrite inE unitfE ltr0n andbT pnatr_eq0.
- by rewrite inE invr_gt0 subr_gt0 xs andbT unitfE invr_eq0 subr_eq0 gt_eqF.
Qed .
Lemma itv_open_bnd_bigcup (R : realType) b (r s : R) :
[set ` Interval (BRight s) (BSide b r)] =
\bigcup_n [set ` Interval (BLeft (s + n.+1 %:R^-1 )) (BSide b r)].
Proof .
have /(congr1 (fun x => -%R @` x)) := itv_bnd_open_bigcup (~~ b) (- r) (- s).
rewrite opp_itv_bnd_bnd/= !opprK negbK => ->; rewrite image_bigcup.
apply eq_bigcupr => k _; apply /seteqP; split => [_/= [y ysr] <-|x/= xsr].
by rewrite oppr_itv/= opprD.
by exists (- x); rewrite ?oppr_itv //= opprK// negbK opprB opprK addrC.
Qed .
Lemma itv_bnd_infty_bigcup (R : realType) b (x : R) :
[set ` Interval (BSide b x) +oo%O] =
\bigcup_i [set ` Interval (BSide b x) (BRight (x + i%:R))].
Proof .
apply /seteqP; split => y; rewrite /= !in_itv/= andbT; last first .
by move => [k _ /=]; move : b => [|] /=; rewrite in_itv/= => /andP[//] /ltW.
move => xy; exists `|ceil (y - x)|%N => //=; rewrite in_itv/= xy/= -ler_subl_addl.
rewrite !natr_absz/= ger0_norm ?ceil_ge0 ?subr_ge0 ?ceil_ge //.
by case : b xy => //= /ltW.
Qed .
Lemma itv_infty_bnd_bigcup (R : realType) b (x : R) :
[set ` Interval -oo%O (BSide b x)] =
\bigcup_i [set ` Interval (BLeft (x - i%:R)) (BSide b x)].
Proof .
have /(congr1 (fun x => -%R @` x)) := itv_bnd_infty_bigcup (~~ b) (- x).
rewrite opp_itv_bnd_infty negbK opprK => ->; rewrite image_bigcup.
apply eq_bigcupr => k _; apply /seteqP; split => [_ /= -[r rbxk <-]|y/= yxkb].
by rewrite oppr_itv/= opprB addrC.
by exists (- y); [rewrite oppr_itv/= negbK opprD opprK|rewrite opprK].
Qed .
Section salgebra_R_ssets .
Variable R : realType.
Definition measurableTypeR := salgebraType (R.-ocitv.-measurable).
Definition measurableR : set (set R) :=
(R.-ocitv.-measurable).-sigma.-measurable.
HB.instance Definition R_isMeasurable :
isMeasurable default_measure_display R :=
@isMeasurable.Build _ measurableTypeR (Pointed.class R) measurableR
measurable0 (@measurableC _ _) (@bigcupT_measurable _ _).
(*HB.instance (Real.sort R) R_isMeasurable.*)
Lemma measurable_set1 (r : R) : measurable [set r].
Proof .
rewrite set1_bigcap_oc; apply : bigcap_measurable => k // _.
by apply : sub_sigma_algebra; exact /is_ocitv.
Qed .
#[local] Hint Resolve measurable_set1 : core.
Lemma measurable_itv (i : interval R) : measurable [set ` i].
Proof .
have moc (a b : R) : measurable `]a, b]%classic.
by apply : sub_sigma_algebra; apply : is_ocitv.
have mopoo (x : R) : measurable `]x, +oo[%classic.
by rewrite itv_bnd_infty_bigcup; exact : bigcup_measurable.
have mnooc (x : R) : measurable `]-oo, x]%classic.
by rewrite -setCitvr; exact /measurableC.
have ooE (a b : R) : `]a, b[%classic = `]a, b]%classic `\ b.
case : (boolP (a < b)) => ab; last by rewrite !set_itv_ge ?set0D .
by rewrite -setUitv1// setUDK// => x [->]; rewrite /= in_itv/= ltxx andbF.
have moo (a b : R) : measurable `]a, b[%classic.
by rewrite ooE; exact : measurableD.
have mcc (a b : R) : measurable `[a, b]%classic.
case : (boolP (a <= b)) => ab; last by rewrite set_itv_ge.
by rewrite -setU1itv//; apply /measurableU.
have mco (a b : R) : measurable `[a, b[%classic.
case : (boolP (a < b)) => ab; last by rewrite set_itv_ge.
by rewrite -setU1itv//; apply /measurableU.
have oooE (b : R) : `]-oo, b[%classic = `]-oo, b]%classic `\ b.
by rewrite -setUitv1// setUDK// => x [->]; rewrite /= in_itv/= ltxx.
case : i => [[[] a|[]] [[] b|[]]] => //; do ?by rewrite set_itv_ge.
- by rewrite -setU1itv//; exact /measurableU.
- by rewrite oooE; exact /measurableD.
- by rewrite set_itv_infty_infty.
Qed .
HB.instance Definition _ :=
(ereal_isMeasurable (R.-ocitv.-measurable)).
(* NB: Until we dropped support for Coq 8.12, we were using
HB.instance (\bar (Real.sort R))
(ereal_isMeasurable (@measurable (@itvs_semiRingOfSets R))).
This was producing a warning but the alternative was failing with Coq 8.12 with
the following message (according to the CI):
# [redundant-canonical-projection,typechecker]
# forall (T : measurableType) (f : T -> R), measurable_fun setT f
# : Prop
# File "./theories/lebesgue_measure.v", line 4508, characters 0-88:
# Error: Anomaly "Uncaught exception Failure("sep_last")."
# Please report at http://coq.inria.fr/bugs/.
*)
Lemma measurable_EFin (A : set R) : measurableR A -> measurable (EFin @` A).
Proof .
by move => mA; exists A => //; exists set0 ; [constructor |rewrite setU0].
Qed .
Lemma emeasurable_set1 (x : \bar R) : measurable [set x].
Proof .
case : x => [r| |].
- by rewrite -image_set1; apply : measurable_EFin; apply : measurable_set1.
- exists set0 => //; [exists [set +oo%E]; [by constructor |]].
by rewrite image_set0 set0U.
- exists set0 => //; [exists [set -oo%E]; [by constructor |]].
by rewrite image_set0 set0U.
Qed .
#[local] Hint Resolve emeasurable_set1 : core.
Lemma __deprecated__itv_cpinfty_pinfty : `[+oo%E, +oo[%classic = [set +oo%E] :> set (\bar R).
Proof . by rewrite itv_cyy. Qed .
#[deprecated(since="mathcomp-analysis 0.6.0" , note="renamed `itv_cyy`" )]
Notation itv_cpinfty_pinfty := __deprecated__itv_cpinfty_pinfty.
Lemma __deprecated__itv_opinfty_pinfty : `]+oo%E, +oo[%classic = set0 :> set (\bar R).
Proof . by rewrite itv_oyy. Qed .
#[deprecated(since="mathcomp-analysis 0.6.0" , note="renamed `itv_oyy`" )]
Notation itv_opinfty_pinfty := __deprecated__itv_opinfty_pinfty.
Lemma __deprecated__itv_cninfty_pinfty : `[-oo%E, +oo[%classic = setT :> set (\bar R).
Proof . by rewrite itv_cNyy. Qed .
#[deprecated(since="mathcomp-analysis 0.6.0" , note="renamed `itv_cNyy`" )]
Notation itv_cninfty_pinfty := __deprecated__itv_cninfty_pinfty.
Lemma __deprecated__itv_oninfty_pinfty :
`]-oo%E, +oo[%classic = ~` [set -oo]%E :> set (\bar R).
Proof . by rewrite itv_oNyy. Qed .
#[deprecated(since="mathcomp-analysis 0.6.0" , note="renamed `itv_oNyy`" )]
Notation itv_oninfty_pinfty := __deprecated__itv_oninfty_pinfty.
Lemma emeasurable_itv_bnd_pinfty b (y : \bar R) :
measurable [set ` Interval (BSide b y) +oo%O].
Proof .
move : y => [y| |].
- exists [set ` Interval (BSide b y) +oo%O]; first exact : measurable_itv.
by exists [set +oo%E]; [constructor |rewrite -punct_eitv_bnd_pinfty].
- by case : b; rewrite ?itv_oyy ?itv_cyy .
- case : b; first by rewrite itv_cNyy.
by rewrite itv_oNyy; exact /measurableC.
Qed .
Lemma emeasurable_itv_ninfty_bnd b (y : \bar R) :
measurable [set ` Interval -oo%O (BSide b y)].
Proof .
by rewrite -setCitvr; exact /measurableC/emeasurable_itv_bnd_pinfty.
Qed .
Definition elebesgue_measure : set \bar R -> \bar R :=
fun S => lebesgue_measure (fine @` (S `\` [set -oo; +oo]%E)).
Lemma elebesgue_measure0 : elebesgue_measure set0 = 0 %E.
Proof . by rewrite /elebesgue_measure set0D image_set0 measure0. Qed .
Lemma measurable_fine (X : set \bar R) : measurable X ->
measurable [set fine x | x in X `\` [set -oo; +oo]%E].
Proof .
case => Y mY [X' [ | <-{X} | <-{X} | <-{X} ]].
- rewrite setU0 => <-{X}.
rewrite [X in measurable X](_ : _ = Y) // predeqE => r; split .
by move => [x [[x' Yx' <-{x}/= _ <-//]]].
by move => Yr; exists r %:E; split => [|[]//]; exists r .
- rewrite [X in measurable X](_ : _ = Y) // predeqE => r; split .
move => [x [[[x' Yx' <- _ <-//]|]]].
by move => <-; rewrite not_orP => -[]/(_ erefl).
by move => Yr; exists r %:E => //; split => [|[]//]; left ; exists r .
- rewrite [X in measurable X](_ : _ = Y) // predeqE => r; split .
move => [x [[[x' Yx' <-{x} _ <-//]|]]].
by move => ->; rewrite not_orP => -[_]/(_ erefl).
by move => Yr; exists r %:E => //; split => [|[]//]; left ; exists r .
- rewrite [X in measurable X](_ : _ = Y) // predeqE => r; split .
by rewrite setDUl setDv setU0 => -[_ [[x' Yx' <-]] _ <-].
by move => Yr; exists r %:E => //; split => [|[]//]; left ; exists r .
Qed .
Lemma elebesgue_measure_ge0 X : (0 <= elebesgue_measure X)%E.
Proof . exact /measure_ge0. Qed .
Lemma semi_sigma_additive_elebesgue_measure :
semi_sigma_additive elebesgue_measure.
Proof .
move => /= F mF tF mUF; rewrite /elebesgue_measure.
rewrite [X in lebesgue_measure X](_ : _ =
\bigcup_n (fine @` (F n `\` [set -oo; +oo]%E))); last first .
rewrite predeqE => r; split .
by move => [x [[n _ Fnx xoo <-]]]; exists n => //; exists x .
by move => [n _ [x [Fnx xoo <-{r}]]]; exists x => //; split => //; exists n .
apply : (@measure_semi_sigma_additive _ _ _ [the measure _ _ of (@lebesgue_measure R)]
(fun n => fine @` (F n `\` [set -oo; +oo]%E))).
- move => n; have := mF n.
move => [X mX [X' mX']] XX'Fn.
apply : measurable_fine.
rewrite -XX'Fn.
apply : measurableU; first exact : measurable_EFin.
by case : mX' => //; exact : measurableU.
- move => i j _ _ [x [[a [Fia aoo ax] [b [Fjb boo] bx]]]].
move : tF => /(_ i j Logic.I Logic.I); apply .
suff ab : a = b by exists a ; split => //; rewrite ab.
move : a b {Fia Fjb} aoo boo ax bx.
move => [a| |] [b| |] /=.
+ by move => _ _ -> ->.
+ by move => _; rewrite not_orP => -[_]/(_ erefl).
+ by move => _; rewrite not_orP => -[]/(_ erefl).
+ by rewrite not_orP => -[_]/(_ erefl).
+ by rewrite not_orP => -[_]/(_ erefl).
+ by rewrite not_orP => -[_]/(_ erefl).
+ by rewrite not_orP => -[]/(_ erefl).
+ by rewrite not_orP => -[]/(_ erefl).
+ by rewrite not_orP => -[]/(_ erefl).
- move : mUF.
rewrite {1 }/measurable /emeasurable /= => -[X mX [Y []]] {Y}.
- rewrite setU0 => h.
rewrite [X in measurable X](_ : _ = X) // predeqE => r; split => [|Xr].
move => -[n _ [x [Fnx xoo <-{r}]]].
have : (\bigcup_n F n) x by exists n .
by rewrite -h => -[x' Xx' <-].
have [n _ Fnr] : (\bigcup_n F n) r%:E by rewrite -h; exists r .
by exists n => //; exists r %:E => //; split => //; case .
- move => h.
rewrite [X in measurable X](_ : _ = X) // predeqE => r; split => [|Xr].
move => -[n _ [x [Fnx xoo <-]]].
have : (\bigcup_n F n) x by exists n .
by rewrite -h => -[[x' Xx' <-//]|xoo']; move /not_orP : xoo => -[].
have [n _ Fnr] : (\bigcup_n F n) r%:E by rewrite -h; left ; exists r .
by exists n => //; exists r %:E => //; split => //; case .
- (* NB: almost the same as the previous one, factorize?*)
move => h.
rewrite [X in measurable X](_ : _ = X) // predeqE => r; split => [|Xr].
move => -[n _ [x [Fnx xoo <-]]].
have : (\bigcup_n F n) x by exists n .
by rewrite -h => -[[x' Xx' <-//]|xoo']; move /not_orP : xoo => -[].
have [n _ Fnr] : (\bigcup_n F n) r%:E by rewrite -h; left ; exists r .
by exists n => //; exists r %:E => //; split => //; case .
- move => h.
rewrite [X in measurable X](_ : _ = X) // predeqE => r; split => [|Xr].
move => -[n _ [x [Fnx xoo <-]]].
have : (\bigcup_n F n) x by exists n .
by rewrite -h => -[[x' Xx' <-//]|].
have [n _ Fnr] : (\bigcup_n F n) r%:E by rewrite -h; left ; exists r .
by exists n => //; exists r %:E => //; split => //; case .
Qed .
HB.instance Definition _ := isMeasure.Build _ _ _ elebesgue_measure
elebesgue_measure0 elebesgue_measure_ge0
semi_sigma_additive_elebesgue_measure.
End salgebra_R_ssets .
#[global ]
Hint Extern 0 (measurable [set _]) => solve [apply : measurable_set1|
apply : emeasurable_set1] : core.
Lemma measurable_fun_fine (R : realType) (D : set (\bar R)) : measurable D ->
measurable_fun D fine.
Proof .
move => mD _ /= B mB; rewrite [X in measurable X](_ : _ `&` _ = if 0 %R \in B then
D `&` ((EFin @` B) `|` [set -oo; +oo]%E) else D `&` EFin @` B); last first .
apply /seteqP; split => [[r [Dr Br]|[Doo B0]|[Doo B0]]|[r| |]].
- by case : ifPn => _; split => //; left ; exists r .
- by rewrite mem_set//; split => //; right ; right .
- by rewrite mem_set//; split => //; right ; left .
- by case : ifPn => [_ [Dr [[s + [sr]]|[]//]]|_ [Dr [s + [sr]]]]; rewrite sr.
- by case : ifPn => [/[!inE] B0 [Doo [[]//|]] [//|_]|B0 [Doo//] []].
- by case : ifPn => [/[!inE] B0 [Doo [[]//|]] [//|_]|B0 [Doo//] []].
case : ifPn => B0; apply /measurableI => //; last exact : measurable_EFin.
by apply : measurableU; [exact : measurable_EFin|exact : measurableU].
Qed .
Section lebesgue_measure_itv .
Variable R : realType.
Let lebesgue_measure_itvoc (a b : R) :
(lebesgue_measure (`]a, b] : set R) = hlength `]a, b])%classic.
Proof .
rewrite /lebesgue_measure/= /Hahn_ext measurable_mu_extE//; last first .
by exists (a , b).
exact : hlength_sigma_sub_additive.
Qed .
Let lebesgue_measure_itvoo_subr1 (a : R) :
lebesgue_measure (`]a - 1 , a[%classic : set R) = 1 %E.
Proof .
rewrite itv_bnd_open_bigcup//; transitivity (lim (lebesgue_measure \o
(fun k => `]a - 1 , a - k.+1 %:R^-1 ]%classic : set R))).
apply /esym/cvg_lim => //; apply : nondecreasing_cvg_mu.
- by move => ?; exact : measurable_itv.
- by apply : bigcup_measurable => k _; exact : measurable_itv.
- move => n m nm; apply /subsetPset => x /=; rewrite !in_itv/= => /andP[->/=].
by move /le_trans; apply ; rewrite ler_sub// ler_pinv ?ler_nat //;
rewrite inE ltr0n andbT unitfE.
rewrite (_ : _ \o _ = (fun n => (1 - n.+1 %:R^-1 )%:E)); last first .
apply /funext => n /=; rewrite lebesgue_measure_itvoc.
have [->|n0] := eqVneq n 0 %N; first by rewrite invr1 subrr set_itvoc0.
rewrite hlength_itv/= lte_fin ifT; last first .
by rewrite ler_lt_sub// invr_lt1 ?unitfE // ltr1n ltnS lt0n.
by rewrite !(EFinB,EFinN) fin_num_oppeB// addeAC addeA subee// add0e.
apply /cvg_lim => //=; apply /fine_cvgP; split => /=; first exact : nearW.
apply /(@cvgrPdist_lt _ [pseudoMetricNormedZmodType R of R^o]) => _/posnumP[e].
near=> n; rewrite opprB addrCA subrr addr0 ger0_norm//.
by near: n; exact : near_infty_natSinv_lt.
Unshelve . all : by end_near. Qed .
Lemma lebesgue_measure_set1 (a : R) : lebesgue_measure [set a] = 0 %E.
Proof .
suff : (lebesgue_measure (`]a - 1 , a]%classic%R : set R) =
lebesgue_measure (`]a - 1 , a[%classic%R : set R) +
lebesgue_measure [set a])%E.
rewrite lebesgue_measure_itvoo_subr1 lebesgue_measure_itvoc => /eqP.
rewrite hlength_itv lte_fin ltr_subl_addr ltr_addl ltr01.
rewrite [in X in X == _]/= EFinN EFinB fin_num_oppeB// addeA subee// add0e.
by rewrite addeC -sube_eq ?fin_num_adde_defl // subee// => /eqP.
rewrite -setUitv1// ?bnd_simp ; last by rewrite ltr_subl_addr ltr_addl.
rewrite measureU//; first exact : measurable_itv.
apply /seteqP; split => // x []/=; rewrite in_itv/= => + xa.
by rewrite xa ltxx andbF.
Qed .
Let lebesgue_measure_itvoo (a b : R) :
(lebesgue_measure (`]a, b[ : set R) = hlength `]a, b[)%classic.
Proof .
have [ab|ba] := ltP a b; last by rewrite set_itv_ge ?measure0 // -leNgt.
have := lebesgue_measure_itvoc a b.
rewrite 2 !hlength_itv => <-; rewrite -setUitv1// measureU//.
- by have /= -> := lebesgue_measure_set1 b; rewrite adde0.
- exact : measurable_itv.
- by apply /seteqP; split => // x [/= + xb]; rewrite in_itv/= xb ltxx andbF.
Qed .
Let lebesgue_measure_itvcc (a b : R) :
(lebesgue_measure (`[a, b] : set R) = hlength `[a, b])%classic.
Proof .
have [ab|ba] := leP a b; last by rewrite set_itv_ge ?measure0 // -leNgt.
have := lebesgue_measure_itvoc a b.
rewrite 2 !hlength_itv => <-; rewrite -setU1itv// measureU//.
- by have /= -> := lebesgue_measure_set1 a; rewrite add0e.
- exact : measurable_itv.
- by apply /seteqP; split => // x [/= ->]; rewrite in_itv/= ltxx.
Qed .
Let lebesgue_measure_itvco (a b : R) :
(lebesgue_measure (`[a, b[ : set R) = hlength `[a, b[)%classic.
Proof .
have [ab|ba] := ltP a b; last by rewrite set_itv_ge ?measure0 // -leNgt.
have := lebesgue_measure_itvoo a b.
rewrite 2 !hlength_itv => <-; rewrite -setU1itv// measureU//.
- by have /= -> := lebesgue_measure_set1 a; rewrite add0e.
- exact : measurable_itv.
- by apply /seteqP; split => // x [/= ->]; rewrite in_itv/= ltxx.
Qed .
Let lebesgue_measure_itv_bnd (x y : bool) (a b : R) :
lebesgue_measure ([set ` Interval (BSide x a) (BSide y b)] : set R) =
hlength [set ` Interval (BSide x a) (BSide y b)].
Proof .
by move : x y => [|] [|]; [exact : lebesgue_measure_itvco |
exact : lebesgue_measure_itvcc | exact : lebesgue_measure_itvoo |
exact : lebesgue_measure_itvoc].
Qed .
Let limnatR : lim (fun k => (k%:R)%:E : \bar R) = +oo%E.
Proof . by apply /cvg_lim => //; apply /cvgenyP. Qed .
Let lebesgue_measure_itv_bnd_infty x (a : R) :
lebesgue_measure ([set ` Interval (BSide x a) +oo%O] : set R) = +oo%E.
Proof .
rewrite itv_bnd_infty_bigcup; transitivity (lim (lebesgue_measure \o
(fun k => [set ` Interval (BSide x a) (BRight (a + k%:R))] : set R))).
apply /esym/cvg_lim => //; apply : nondecreasing_cvg_mu.
+ by move => k; exact : measurable_itv.
+ by apply : bigcup_measurable => k _; exact : measurable_itv.
+ move => m n mn; apply /subsetPset => r/=; rewrite !in_itv/= => /andP[->/=].
by move => /le_trans; apply ; rewrite ler_add// ler_nat.
rewrite (_ : _ \o _ = (fun k => k%:R%:E))//.
apply /funext => n /=; rewrite lebesgue_measure_itv_bnd hlength_itv/=.
rewrite lte_fin; have [->|n0] := eqVneq n 0 %N; first by rewrite addr0 ltxx.
by rewrite ltr_addl ltr0n lt0n n0 EFinD addeAC EFinN subee ?add0e .
Qed .
Let lebesgue_measure_itv_infty_bnd y (b : R) :
lebesgue_measure ([set ` Interval -oo%O (BSide y b)] : set R) = +oo%E.
Proof .
rewrite itv_infty_bnd_bigcup; transitivity (lim (lebesgue_measure \o
(fun k => [set ` Interval (BLeft (b - k%:R)) (BSide y b)] : set R))).
apply /esym/cvg_lim => //; apply : nondecreasing_cvg_mu.
+ by move => k; exact : measurable_itv.
+ by apply : bigcup_measurable => k _; exact : measurable_itv.
+ move => m n mn; apply /subsetPset => r/=; rewrite !in_itv/= => /andP[+ ->].
by rewrite andbT; apply : le_trans; rewrite ler_sub// ler_nat.
rewrite (_ : _ \o _ = (fun k : nat => k%:R%:E))//.
apply /funext => n /=; rewrite lebesgue_measure_itv_bnd hlength_itv/= lte_fin.
have [->|n0] := eqVneq n 0 %N; first by rewrite subr0 ltxx.
rewrite ltr_subl_addr ltr_addl ltr0n lt0n n0 EFinN EFinB fin_num_oppeB// addeA.
by rewrite subee// add0e.
Qed .
Lemma lebesgue_measure_itv (i : interval R) :
lebesgue_measure ([set ` i] : set R) = hlength [set ` i].
Proof .
move : i => [[x a|[|]]] [y b|[|]]; first exact : lebesgue_measure_itv_bnd.
- by rewrite set_itvE ?measure0 .
- by rewrite lebesgue_measure_itv_bnd_infty hlength_bnd_infty.
- by rewrite lebesgue_measure_itv_infty_bnd hlength_infty_bnd.
- by rewrite set_itvE ?measure0 .
- rewrite set_itvE hlength_setT.
rewrite (_ : setT = [set ` `]-oo, 0 [] `|` [set ` `[0 , +oo[]); last first .
by apply /seteqP; split => // => x _; have [x0|x0] := leP 0 x; [right |left ];
rewrite /= in_itv//= x0.
rewrite measureU//=; try exact : measurable_itv.
+ by rewrite lebesgue_measure_itv_infty_bnd lebesgue_measure_itv_bnd_infty.
+ by apply /seteqP; split => // x []/=; rewrite !in_itv/= andbT leNgt => ->.
- by rewrite set_itvE ?measure0 .
- by rewrite set_itvE ?measure0 .
- by rewrite set_itvE ?measure0 .
Qed .
End lebesgue_measure_itv .
Lemma lebesgue_measure_rat (R : realType) :
lebesgue_measure (range ratr : set R) = 0 %E.
Proof .
have /pcard_eqP/bijPex[f bijf] := card_rat; set f1 := 'pinv_(fun => 0 ) setT f.
rewrite (_ : range _ = \bigcup_n [set ratr (f1 n)]); last first .
apply /seteqP; split => [_ [q _ <-]|_ [n _ /= ->]]; last by exists (f1 n ).
exists (f q ) => //=; rewrite /f1 pinvKV// ?in_setE // => x y _ _.
by apply : bij_inj; rewrite -setTT_bijective.
rewrite measure_bigcup//; last first .
apply /trivIsetP => i j _ _ ij; apply /seteqP; split => //= _ [/= ->].
move => /fmorph_inj.
have /set_bij_inj /[apply ] := bijpinv_bij (fun => 0 ) bijf.
by rewrite in_setE => /(_ Logic.I Logic.I); exact /eqP.
by rewrite eseries0// => n _; exact : lebesgue_measure_set1.
Qed .
Section measurable_fun_measurable .
Local Open Scope ereal_scope.
Context d (T : measurableType d) (R : realType).
Variables (D : set T) (f : T -> \bar R).
Hypotheses (mD : measurable D) (mf : measurable_fun D f).
Implicit Types y : \bar R.
Lemma emeasurable_fun_c_infty y : measurable (D `&` [set x | y <= f x]).
Proof .
by rewrite -preimage_itv_c_infty; exact /mf/emeasurable_itv_bnd_pinfty.
Qed .
Lemma emeasurable_fun_o_infty y : measurable (D `&` [set x | y < f x]).
Proof .
by rewrite -preimage_itv_o_infty; exact /mf/emeasurable_itv_bnd_pinfty.
Qed .
Lemma emeasurable_fun_infty_o y : measurable (D `&` [set x | f x < y]).
Proof .
by rewrite -preimage_itv_infty_o; exact /mf/emeasurable_itv_ninfty_bnd.
Qed .
Lemma emeasurable_fun_infty_c y : measurable (D `&` [set x | f x <= y]).
Proof .
by rewrite -preimage_itv_infty_c; exact /mf/emeasurable_itv_ninfty_bnd.
Qed .
Lemma emeasurable_fin_num : measurable (D `&` [set x | f x \is a fin_num]).
Proof .
rewrite [X in measurable X](_ : _ =
\bigcup_k (D `&` ([set x | - k%:R%:E <= f x] `&` [set x | f x <= k%:R%:E]))).
apply : bigcupT_measurable => k; rewrite -(setIid D) setIACA.
by apply : measurableI; [exact : emeasurable_fun_c_infty|
exact : emeasurable_fun_infty_c].
rewrite predeqE => t; split => [/= [Dt ft]|].
have [ft0|ft0] := leP 0 %R (fine (f t)).
exists `|ceil (fine (f t))|%N => //=; split => //; split .
by rewrite -{2 }(fineK ft)// lee_fin (le_trans _ ft0)// ler_oppl oppr0.
by rewrite natr_absz ger0_norm ?ceil_ge0 // -(fineK ft) lee_fin ceil_ge.
exists `|floor (fine (f t))|%N => //=; split => //; split .
rewrite natr_absz ltr0_norm ?floor_lt0 // EFinN.
by rewrite -{2 }(fineK ft) lee_fin mulrNz opprK floor_le.
by rewrite -(fineK ft)// lee_fin (le_trans (ltW ft0)).
move => [n _] [/= Dt [nft fnt]]; split => //; rewrite fin_numElt.
by rewrite (lt_le_trans _ nft) ?ltNyr //= (le_lt_trans fnt)// ltry.
Qed .
Lemma emeasurable_neq y : measurable (D `&` [set x | f x != y]).
Proof .
rewrite (_ : [set x | f x != y] = f @^-1 ` (setT `\ y)).
exact /mf/measurableD.
rewrite predeqE => t; split ; last by rewrite /preimage /= => -[_ /eqP].
by rewrite /= => ft0; rewrite /preimage /=; split => //; exact /eqP.
Qed .
End measurable_fun_measurable .
Module RGenOInfty .
Section rgenoinfty .
Variable R : realType.
Implicit Types x y z : R.
Definition G := [set A | exists x , A = `]x, +oo[%classic].
Lemma measurable_itv_bnd_infty b x :
G.-sigma.-measurable [set ` Interval (BSide b x) +oo%O].
Proof .
case : b; last by apply : sub_sigma_algebra; eexists ; reflexivity .
rewrite itv_c_inftyEbigcap; apply : bigcapT_measurable => k.
by apply : sub_sigma_algebra; eexists ; reflexivity .
Qed .
Lemma measurable_itv_bounded a b x : a != +oo%O ->
G.-sigma.-measurable [set ` Interval a (BSide b x)].
Proof .
case : a => [a r _|[_|//]].
by rewrite set_itv_splitD; apply : measurableD => //;
exact : measurable_itv_bnd_infty.
by rewrite -setCitvr; apply : measurableC; apply : measurable_itv_bnd_infty.
Qed .
Lemma measurableE :
(R.-ocitv.-measurable).-sigma.-measurable = G.-sigma.-measurable.
Proof .
rewrite eqEsubset; split => A.
apply : smallest_sub; first exact : smallest_sigma_algebra.
by move => I [x _ <-]; exact : measurable_itv_bounded.
apply : smallest_sub; first exact : smallest_sigma_algebra.
by move => A' /= [x ->]; exact : measurable_itv.
Qed .
End rgenoinfty .
End RGenOInfty .
Module RGenInftyO .
Section rgeninftyo .
Variable R : realType.
Implicit Types x y z : R.
Definition G := [set A | exists x , A = `]-oo, x[%classic].
Lemma measurable_itv_bnd_infty b x :
G.-sigma.-measurable [set ` Interval -oo%O (BSide b x)].
Proof .
case : b; first by apply sub_sigma_algebra; eexists ; reflexivity .
rewrite -setCitvr itv_o_inftyEbigcup; apply /measurableC/bigcupT_measurable => n.
rewrite -setCitvl; apply : measurableC.
by apply : sub_sigma_algebra; eexists ; reflexivity .
Qed .
Lemma measurable_itv_bounded a b x : a != -oo%O ->
G.-sigma.-measurable [set ` Interval (BSide b x) a].
Proof .
case : a => [a r _|[//|_]].
by rewrite set_itv_splitD; apply /measurableD => //;
rewrite -setCitvl; apply : measurableC; exact : measurable_itv_bnd_infty.
by rewrite -setCitvl; apply : measurableC; apply : measurable_itv_bnd_infty.
Qed .
Lemma measurableE :
(R.-ocitv.-measurable).-sigma.-measurable = G.-sigma.-measurable.
Proof .
rewrite eqEsubset; split => A.
apply : smallest_sub; first exact : smallest_sigma_algebra.
by move => I [x _ <-]; apply : measurable_itv_bounded.
apply : smallest_sub; first exact : smallest_sigma_algebra.
by move => A' /= [x ->]; apply : measurable_itv.
Qed .
End rgeninftyo .
End RGenInftyO .
Module RGenCInfty .
Section rgencinfty .
Variable R : realType.
Implicit Types x y z : R.
Definition G : set (set R) := [set A | exists x , A = `[x, +oo[%classic].
Lemma measurable_itv_bnd_infty b x :
G.-sigma.-measurable [set ` Interval (BSide b x) +oo%O].
Proof .
case : b; first by apply : sub_sigma_algebra; exists x ; rewrite set_itv_c_infty.
rewrite itv_o_inftyEbigcup; apply : bigcupT_measurable => k.
by apply : sub_sigma_algebra; eexists ; reflexivity .
Qed .
Lemma measurable_itv_bounded a b y : a != +oo%O ->
G.-sigma.-measurable [set ` Interval a (BSide b y)].
Proof .
case : a => [a r _|[_|//]].
rewrite set_itv_splitD.
by apply : measurableD; apply : measurable_itv_bnd_infty.
by rewrite -setCitvr; apply : measurableC; apply : measurable_itv_bnd_infty.
Qed .
Lemma measurableE :
(R.-ocitv.-measurable).-sigma.-measurable = G.-sigma.-measurable.
Proof .
rewrite eqEsubset; split => A.
apply : smallest_sub; first exact : smallest_sigma_algebra.
by move => I [x _ <-]; apply : measurable_itv_bounded.
apply : smallest_sub; first exact : smallest_sigma_algebra.
by move => A' /= [x ->]; apply : measurable_itv.
Qed .
End rgencinfty .
End RGenCInfty .
Module RGenOpens .
Section rgenopens .
Variable R : realType.
Implicit Types x y z : R.
Definition G := [set A | exists x y , A = `]x, y[%classic].
Local Lemma measurable_itvoo x y : G.-sigma.-measurable `]x, y[%classic.
Proof . by apply sub_sigma_algebra; eexists ; eexists ; reflexivity . Qed .
Local Lemma measurable_itv_o_infty x : G.-sigma.-measurable `]x, +oo[%classic.
Proof .
rewrite itv_bnd_inftyEbigcup; apply : bigcupT_measurable => i.
exact : measurable_itvoo.
Qed .
Lemma measurable_itv_bnd_infty b x :
G.-sigma.-measurable [set ` Interval (BSide b x) +oo%O].
Proof .
case : b; last exact : measurable_itv_o_infty.
rewrite itv_c_inftyEbigcap; apply : bigcapT_measurable => k.
exact : measurable_itv_o_infty.
Qed .
Lemma measurable_itv_infty_bnd b x :
G.-sigma.-measurable [set ` Interval -oo%O (BSide b x)].
Proof .
by rewrite -setCitvr; apply : measurableC; exact : measurable_itv_bnd_infty.
Qed .
Lemma measurable_itv_bounded a x b y :
G.-sigma.-measurable [set ` Interval (BSide a x) (BSide b y)].
Proof .
move : a b => [] []; rewrite -[X in measurable X]setCK setCitv;
apply : measurableC; apply : measurableU; try solve [
exact : measurable_itv_infty_bnd|exact : measurable_itv_bnd_infty].
Qed .
Lemma measurableE :
(R.-ocitv.-measurable).-sigma.-measurable = G.-sigma.-measurable.
Proof .
rewrite eqEsubset; split => A.
apply : smallest_sub; first exact : smallest_sigma_algebra.
by move => I [x _ <-]; apply : measurable_itv_bounded.
apply : smallest_sub; first exact : smallest_sigma_algebra.
by move => A' /= [x [y ->]]; apply : measurable_itv.
Qed .
End rgenopens .
End RGenOpens .
Section erealwithrays .
Variable R : realType.
Implicit Types (x y z : \bar R) (r s : R).
Local Open Scope ereal_scope.
Lemma EFin_itv_bnd_infty b r : EFin @` [set ` Interval (BSide b r) +oo%O] =
[set ` Interval (BSide b r%:E) +oo%O] `\ +oo.
Proof .
rewrite eqEsubset; split => [x [s /itvP rs <-]|x []].
split => //=; rewrite in_itv /=.
by case : b in rs *; rewrite /= ?(lee_fin, lte_fin) rs.
move : x => [s|_ /(_ erefl)|] //=; rewrite in_itv /= andbT; last first .
by case : b => /=; rewrite 1 ?(leNgt,ltNge) 1 ?(ltNyr, leNye).
by case : b => /=; rewrite 1 ?(lte_fin,lee_fin) => rs _;
exists s => //; rewrite in_itv /= rs.
Qed .
Lemma EFin_itv r : [set s | r%:E < s%:E] = `]r, +oo[%classic.
Proof .
by rewrite predeqE => s; split => [|]; rewrite /= lte_fin in_itv/= andbT.
Qed .
Lemma preimage_EFin_setT : @EFin R @^-1 ` [set x | x \in `]-oo%E, +oo[] = setT.
Proof .
by rewrite set_itvE predeqE => r; split => // _; rewrite /preimage /= ltNyr.
Qed .
Lemma eitv_bnd_infty b r : `[r%:E, +oo[%classic =
\bigcap_k [set ` Interval (BSide b (r - k.+1 %:R^-1 )%:E) +oo%O] :> set _.
Proof .
rewrite predeqE => x; split => [|].
- move : x => [s /=| _ n _|//].
+ rewrite in_itv /= andbT lee_fin => rs n _ /=; rewrite in_itv/= andbT.
case : b => /=.
* by rewrite lee_fin ler_subl_addl (le_trans rs)// ler_addr.
* by rewrite lte_fin ltr_subl_addl (le_lt_trans rs)// ltr_addr.
+ by rewrite /= in_itv /= andbT; case : b => /=; rewrite lteey.
- move : x => [s| |/(_ 0 %N Logic.I)] /=; rewrite ?in_itv /= ?leey //; last first .
by case : b.
move => h; rewrite lee_fin leNgt andbT; apply /negP => /ltr_add_invr[k skr].
have {h} := h k Logic.I; rewrite /= in_itv /= andbT; case : b => /=.
+ by rewrite lee_fin ler_subl_addr leNgt skr.
+ by rewrite lte_fin ltr_subl_addr ltNge (ltW skr).
Qed .
Lemma eitv_infty_bnd b r : `]-oo, r%:E]%classic =
\bigcap_k [set ` Interval -oo%O (BSide b (r%:E + k.+1 %:R^-1 %:E))] :> set _.
Proof .
rewrite predeqE => x; split => [|].
- move : x => [s /=|//|_ n _].
+ rewrite in_itv /= lee_fin => sr n _; rewrite /= in_itv /= -EFinD.
case : b => /=.
* by rewrite lte_fin (le_lt_trans sr)// ltr_addl.
* by rewrite lee_fin (le_trans sr)// ler_addl.
+ by rewrite /= in_itv /= -EFinD; case : b => //=; rewrite lteNye.
- move : x => [s|/(_ 0 %N Logic.I)|]/=; rewrite !in_itv/= ?leNye //; last first .
by case : b.
move => h; rewrite lee_fin leNgt; apply /negP => /ltr_add_invr[k rks].
have {h} := h k Logic.I; rewrite /= in_itv /= -EFinD; case : b => /=.
+ by rewrite lte_fin ltNge (ltW rks).
+ by rewrite lee_fin leNgt rks.
Qed .
Lemma eset1_ninfty :
[set -oo] = \bigcap_k `]-oo, (-k%:R%:E)[%classic :> set (\bar R).
Proof .
rewrite eqEsubset; split => [_ -> i _ |]; first by rewrite /= in_itv /= ltNyr.
move => [r|/(_ O Logic.I)|]//.
move => /(_ `|floor r|%N Logic.I); rewrite /= in_itv/= ltNge.
rewrite lee_fin; have [r0|r0] := leP 0 %R r.
by rewrite (le_trans _ r0) // ler_oppl oppr0 ler0n.
rewrite ler_oppl -abszN natr_absz gtr0_norm; last first .
by rewrite ltr_oppr oppr0 floor_lt0.
by rewrite mulrNz ler_oppl opprK floor_le.
Qed .
Lemma eset1_pinfty :
[set +oo] = \bigcap_k `]k%:R%:E, +oo[%classic :> set (\bar R).
Proof .
rewrite eqEsubset; split => [_ -> i _/=|]; first by rewrite in_itv /= ltry.
move => [r| |/(_ O Logic.I)] // /(_ `|ceil r|%N Logic.I); rewrite /= in_itv /=.
rewrite andbT lte_fin ltNge.
have [r0|r0] := ltP 0 %R r; last by rewrite (le_trans r0).
by rewrite natr_absz gtr0_norm // ?ceil_ge // ceil_gt0.
Qed .
End erealwithrays .
Module ErealGenOInfty .
Section erealgenoinfty .
Variable R : realType.
Implicit Types (x y z : \bar R) (r s : R).
Local Open Scope ereal_scope.
Definition G := [set A : set \bar R | exists r , A = `]r%:E, +oo[%classic].
Lemma measurable_set1_ninfty : G.-sigma.-measurable [set -oo].
Proof .
rewrite eset1_ninfty; apply : bigcap_measurable => i _.
rewrite -setCitvr; apply : measurableC; rewrite (eitv_bnd_infty false).
apply : bigcap_measurable => j _; apply : sub_sigma_algebra.
by exists (- (i%:R + j.+1 %:R^-1 ))%R; rewrite opprD.
Qed .
Lemma measurable_set1_pinfty : G.-sigma.-measurable [set +oo].
Proof .
rewrite eset1_pinfty; apply : bigcapT_measurable => i.
by apply : sub_sigma_algebra; exists i %:R.
Qed .
Lemma measurableE : emeasurable (R.-ocitv.-measurable) = G.-sigma.-measurable.
Proof .
apply /seteqP; split ; last first .
apply : smallest_sub.
split ; first exact : emeasurable0.
by move => *; rewrite setTD; exact : emeasurableC.
by move => *; exact : bigcupT_emeasurable.
move => _ [r ->]; rewrite /emeasurable /=.
exists `]r, +oo[%classic.
rewrite RGenOInfty.measurableE.
exact : RGenOInfty.measurable_itv_bnd_infty.
by exists [set +oo]; [constructor |rewrite -punct_eitv_bnd_pinfty].
move => A [B mB [C mC]] <-; apply : measurableU; last first .
case : mC; [by []|exact : measurable_set1_ninfty
|exact : measurable_set1_pinfty|].
- by apply : measurableU; [exact : measurable_set1_ninfty|
exact : measurable_set1_pinfty].
rewrite RGenOInfty.measurableE in mB.
have smB := smallest_sub _ _ mB.
(* BUG: elim/smB : _. fails !! *)
apply : (smB (G.-sigma.-measurable \o (image^~ EFin))); last first .
move => _ [r ->]/=; rewrite EFin_itv_bnd_infty; apply : measurableD.
by apply : sub_sigma_algebra => /=; exists r .
exact : measurable_set1_pinfty.
split => /= [|D mD|F mF]; first by rewrite image_set0.
- rewrite setTD EFin_setC; apply : measurableD; first exact : measurableC.
by apply : measurableU; [exact : measurable_set1_ninfty|
exact : measurable_set1_pinfty].
- by rewrite EFin_bigcup; apply : bigcup_measurable => i _ ; exact : mF.
Qed .
End erealgenoinfty .
End ErealGenOInfty .
Module ErealGenCInfty .
Section erealgencinfty .
Variable R : realType.
Implicit Types (x y z : \bar R) (r s : R).
Local Open Scope ereal_scope.
Definition G := [set A : set \bar R | exists r , A = `[r%:E, +oo[%classic].
Lemma measurable_set1_ninfty : G.-sigma.-measurable [set -oo].
Proof .
rewrite eset1_ninfty; apply : bigcapT_measurable=> i; rewrite -setCitvr.
by apply : measurableC; apply : sub_sigma_algebra; exists (- i%:R)%R.
Qed .
Lemma measurable_set1_pinfty : G.-sigma.-measurable [set +oo].
Proof .
rewrite eset1_pinfty; apply : bigcap_measurable => i _.
rewrite -setCitvl; apply : measurableC; rewrite (eitv_infty_bnd true).
apply : bigcap_measurable => j _; rewrite -setCitvr; apply : measurableC.
by apply : sub_sigma_algebra; exists (i %:R + j.+1 %:R^-1 )%R.
Qed .
Lemma measurableE : emeasurable (R.-ocitv.-measurable) = G.-sigma.-measurable.
Proof .
apply /seteqP; split ; last first .
apply : smallest_sub.
split ; first exact : emeasurable0.
by move => *; rewrite setTD; exact : emeasurableC.
by move => *; exact : bigcupT_emeasurable.
move => _ [r ->]/=; exists `[r, +oo[%classic.
rewrite RGenOInfty.measurableE.
exact : RGenOInfty.measurable_itv_bnd_infty.
by exists [set +oo]; [constructor | rewrite -punct_eitv_bnd_pinfty].
move => _ [A' mA' [C mC]] <-; apply : measurableU; last first .
case : mC; [by []|exact : measurable_set1_ninfty|
exact : measurable_set1_pinfty|].
by apply : measurableU; [exact : measurable_set1_ninfty|
exact : measurable_set1_pinfty].
rewrite RGenCInfty.measurableE in mA'.
have smA' := smallest_sub _ _ mA'.
(* BUG: elim/smA' : _. fails !! *)
apply : (smA' (G.-sigma.-measurable \o (image^~ EFin))); last first .
move => _ [r ->]/=; rewrite EFin_itv_bnd_infty; apply : measurableD.
by apply : sub_sigma_algebra => /=; exists r .
exact : measurable_set1_pinfty.
split => /= [|D mD|F mF]; first by rewrite image_set0.
- rewrite setTD EFin_setC; apply : measurableD; first exact : measurableC.
by apply : measurableU; [exact : measurable_set1_ninfty|
exact : measurable_set1_pinfty].
- by rewrite EFin_bigcup; apply : bigcup_measurable => i _; exact : mF.
Qed .
End erealgencinfty .
End ErealGenCInfty .
Module ErealGenInftyO .
Section erealgeninftyo .
Variable R : realType.
Definition G := [set A : set \bar R | exists r , A = `]-oo, r%:E[%classic].
Lemma measurableE : emeasurable (R.-ocitv.-measurable) = G.-sigma.-measurable.
Proof .
rewrite ErealGenCInfty.measurableE eqEsubset; split => A.
apply : smallest_sub; first exact : smallest_sigma_algebra.
move => _ [x ->]; rewrite -[X in _.-measurable X]setCK; apply : measurableC.
by apply : sub_sigma_algebra; exists x ; rewrite setCitvr.
apply : smallest_sub; first exact : smallest_sigma_algebra.
move => x Gx; rewrite -(setCK x); apply : measurableC; apply : sub_sigma_algebra.
by case : Gx => y ->; exists y ; rewrite setCitvl.
Qed .
End erealgeninftyo .
End ErealGenInftyO .
Section trace .
Variable (T : Type ).
Implicit Types (G : set (set T)) (A D : set T).
(* intended as a trace sigma-algebra *)
Definition strace G D := [set x `&` D | x in G].
Lemma stracexx G D : G D -> strace G D D.
Proof . by rewrite /strace /=; exists D => //; rewrite setIid. Qed .
Lemma sigma_algebra_strace G D :
sigma_algebra setT G -> sigma_algebra D (strace G D).
Proof .
move => [G0 GC GU]; split ; first by exists set0 => //; rewrite set0I.
- move => S [A mA ADS]; have mCA := GC _ mA.
have : strace G D (D `&` ~` A).
by rewrite setIC; exists (setT `\` A) => //; rewrite setTD.
rewrite -setDE => trDA.
have DADS : D `\` A = D `\` S by rewrite -ADS !setDE setCI setIUr setICr setU0.
by rewrite DADS in trDA.
- move => S mS; have /choice[M GM] : forall n , exists A , G A /\ S n = A `&` D.
by move => n; have [A mA ADSn] := mS n; exists A .
exists (\bigcup_i (M i)); first by apply GU => i; exact : (GM i).1 .
by rewrite setI_bigcupl; apply eq_bigcupr => i _; rewrite (GM i).2 .
Qed .
End trace .
Lemma strace_measurable d (T : measurableType d) (A : set T) : measurable A ->
strace measurable A `<=` measurable.
Proof . by move => mA=> _ [C mC <-]; apply : measurableI. Qed .
(* more properties of measurable functions *)
Lemma is_interval_measurable (R : realType) (I : set R) :
is_interval I -> measurable I.
Proof . by move /is_intervalP => ->; exact : measurable_itv. Qed .
Section coutinuous_measurable .
Variable R : realType.
Lemma open_measurable (U : set R) : open U -> measurable U.
Proof .
move => /open_bigcup_rat ->; rewrite bigcup_mkcond; apply : bigcupT_measurable_rat.
move => q; case : ifPn => // qfab; apply : is_interval_measurable => //.
exact : is_interval_bigcup_ointsub.
Qed .
Lemma open_measurable_subspace (D : set R) (U : set (subspace D)) :
measurable D -> open U -> measurable (D `&` U).
Proof .
move => mD /open_subspaceP [V [oV] VD]; rewrite setIC -VD.
by apply : measurableI => //; exact : open_measurable.
Qed .
Lemma subspace_continuous_measurable_fun (D : set R) (f : subspace D -> R) :
measurable D -> continuous f -> measurable_fun D f.
Proof .
move => mD /continuousP cf; apply : (measurability (RGenOpens.measurableE R)).
move => _ [_ [a [b ->] <-]]; apply : open_measurable_subspace => //.
by exact /cf/interval_open.
Qed .
Corollary open_continuous_measurable_fun (D : set R) (f : R -> R) :
open D -> {in D, continuous f} -> measurable_fun D f.
Proof .
move => oD; rewrite -(continuous_open_subspace f oD).
by apply : subspace_continuous_measurable_fun; exact : open_measurable.
Qed .
Lemma continuous_measurable_fun (f : R -> R) :
continuous f -> measurable_fun setT f.
Proof .
by move => cf; apply : open_continuous_measurable_fun => //; exact : openT.
Qed .
End coutinuous_measurable .
Section standard_measurable_fun .
Lemma measurable_fun_opp (R : realType) : measurable_fun [set : R] -%R.
Proof .
apply : continuous_measurable_fun.
by have := @opp_continuous R [the normedModType R of R^o].
Qed .
Lemma measurable_fun_normr (R : realType) (D : set R) :
measurable_fun D (@normr _ R).
Proof .
move => mD; apply : (measurability (RGenOInfty.measurableE R)) => //.
move => /= _ [_ [x ->] <-]; apply : measurableI => //.
have [x0|x0] := leP 0 x.
rewrite [X in measurable X](_ : _ = `]-oo, (- x)[ `|` `]x, +oo[)%classic.
by apply : measurableU; apply : measurable_itv.
rewrite predeqE => r; split => [|[|]]; rewrite preimage_itv ?in_itv ?andbT /=.
- have [r0|r0] := leP 0 r; [rewrite ger0_norm|rewrite ltr0_norm] => // xr;
rewrite 2 !in_itv/=.
+ by right ; rewrite xr.
+ by left ; rewrite ltr_oppr.
- move => rx /=.
by rewrite ler0_norm 1 ?ltr_oppr // (le_trans (ltW rx))// ler_oppl oppr0.
- by rewrite in_itv /= andbT => xr; rewrite (lt_le_trans _ (ler_norm _)).
rewrite [X in measurable X](_ : _ = setT)// predeqE => r.
by split => // _; rewrite /= in_itv /= andbT (lt_le_trans x0).
Qed .
End standard_measurable_fun .
#[global ] Hint Extern 0 (measurable_fun _ normr) =>
solve [exact : measurable_fun_normr] : core.
Section measurable_fun_realType .
Context d (T : measurableType d) (R : realType).
Implicit Types (D : set T) (f g : T -> R).
Lemma measurable_funD D f g :
measurable_fun D f -> measurable_fun D g -> measurable_fun D (f \+ g).
Proof .
move => mf mg mD; apply : (measurability (RGenOInfty.measurableE R)) => //.
move => /= _ [_ [a ->] <-]; rewrite preimage_itv_o_infty.
rewrite [X in measurable X](_ : _ = \bigcup_(q : rat)
((D `&` [set x | ratr q < f x]) `&` (D `&` [set x | a - ratr q < g x]))).
apply : bigcupT_measurable_rat => q; apply : measurableI.
- by rewrite -preimage_itv_o_infty; apply : mf => //; apply : measurable_itv.
- by rewrite -preimage_itv_o_infty; apply : mg => //; apply : measurable_itv.
rewrite predeqE => x; split => [|[r _] []/= [Dx rfx]] /= => [[Dx]|[_]].
rewrite -ltr_subl_addr => /rat_in_itvoo[r]; rewrite inE /= => /itvP h.
exists r => //; rewrite setIACA setIid; split => //; split => /=.
by rewrite h.
by rewrite ltr_subl_addr addrC -ltr_subl_addr h.
by rewrite ltr_subl_addr=> afg; rewrite (lt_le_trans afg)// addrC ler_add2r ltW.
Qed .
Lemma measurable_funrM D f (k : R) : measurable_fun D f ->
measurable_fun D (fun x => k * f x).
Proof .
apply : (@measurable_funT_comp _ _ _ _ _ _ ( *%R k)).
by apply : continuous_measurable_fun; apply : mulrl_continuous.
Qed .
Lemma measurable_funN D f : measurable_fun D f -> measurable_fun D (-%R \o f).
Proof .
move => mf mD; rewrite (_ : _ \o _ = (fun x => - 1 * f x)).
exact : measurable_funrM.
by under eq_fun do rewrite mulN1r.
Qed .
Lemma measurable_funB D f g : measurable_fun D f ->
measurable_fun D g -> measurable_fun D (f \- g).
Proof .
by move => ? ? ?; apply : measurable_funD => //; exact : measurable_funN.
Qed .
Lemma measurable_fun_exprn D n f :
measurable_fun D f -> measurable_fun D (fun x => f x ^+ n).
Proof .
apply : measurable_funT_comp ((@GRing.exp R)^~ n) _ _ _.
by apply : continuous_measurable_fun; apply : exprn_continuous.
Qed .
Lemma measurable_fun_sqr D f :
measurable_fun D f -> measurable_fun D (fun x => f x ^+ 2 ).
Proof . exact : measurable_fun_exprn. Qed .
Lemma measurable_funM D f g :
measurable_fun D f -> measurable_fun D g -> measurable_fun D (f \* g).
Proof .
move => mf mg mD; rewrite (_ : (_ \* _) = (fun x => 2 %:R^-1 * (f x + g x) ^+ 2 )
\- (fun x => 2 %:R^-1 * (f x ^+ 2 )) \- (fun x => 2 %:R^-1 * ( g x ^+ 2 ))).
apply : measurable_funB => //; last first .
by apply : measurable_funrM => //; exact : measurable_fun_sqr.
apply : measurable_funB => //; last first .
by apply : measurable_funrM => //; exact : measurable_fun_sqr.
apply : measurable_funrM => //.
by apply : measurable_fun_sqr => //; exact : measurable_funD.
rewrite funeqE => x /=; rewrite -2 !mulrBr sqrrD (addrC (f x ^+ 2 )) -addrA.
rewrite -(addrA (f x * g x *+ 2 )) -opprB opprK (addrC (g x ^+ 2 )) addrK.
by rewrite -(mulr_natr (f x * g x)) -(mulrC 2 ) mulrA mulVr ?mul1r // unitfE.
Qed .
Lemma measurable_fun_max D f g :
measurable_fun D f -> measurable_fun D g -> measurable_fun D (f \max g).
Proof .
move => mf mg mD; apply (measurability (RGenCInfty.measurableE R)) => //.
move => _ [_ [x ->] <-]; rewrite [X in measurable X](_ : _ =
(D `&` f @^-1 ` `[x, +oo[) `|` (D `&` g @^-1 ` `[x, +oo[)); last first .
rewrite predeqE => t /=; split .
by rewrite /= !in_itv /= !andbT le_maxr => -[Dx /orP[|]]; tauto .
by move => [|]; rewrite !in_itv/= !andbT le_maxr => -[Dx ->]//; rewrite orbT.
by apply : measurableU; [apply : mf|apply : mg] =>//; apply : measurable_itv.
Qed .
Lemma measurable_fun_sups D (h : (T -> R)^nat) n :
(forall t , D t -> has_ubound (range (h ^~ t))) ->
(forall m , measurable_fun D (h m)) ->
measurable_fun D (fun x => sups (h ^~ x) n).
Proof .
move => f_ub mf mD; apply : (measurability (RGenOInfty.measurableE R)) => //.
move => _ [_ [x ->] <-]; rewrite sups_preimage // setI_bigcupr.
by apply : bigcup_measurable => k /= nk; apply : mf => //; exact : measurable_itv.
Qed .
Lemma measurable_fun_infs D (h : (T -> R)^nat) n :
(forall t , D t -> has_lbound (range (h ^~ t))) ->
(forall n , measurable_fun D (h n)) ->
measurable_fun D (fun x => infs (h ^~ x) n).
Proof .
move => lb_f mf mD; apply : (measurability (RGenInftyO.measurableE R)) =>//.
move => _ [_ [x ->] <-]; rewrite infs_preimage // setI_bigcupr.
by apply : bigcup_measurable => k /= nk; apply : mf => //; exact : measurable_itv.
Qed .
Lemma measurable_fun_lim_sup D (h : (T -> R)^nat) :
(forall t , D t -> has_ubound (range (h ^~ t))) ->
(forall t , D t -> has_lbound (range (h ^~ t))) ->
(forall n , measurable_fun D (h n)) ->
measurable_fun D (fun x => lim_sup (h ^~ x)).
Proof .
move => f_ub f_lb mf.
have : {in D, (fun x => inf [set sups (h ^~ x) n | n in [set n | 0 <= n]%N])
=1 (fun x => lim_sup (h^~ x))}.
move => t; rewrite inE => Dt; apply /esym/cvg_lim; first exact : Rhausdorff.
rewrite [X in _ --> X](_ : _ = inf (range (sups (h^~t)))).
by apply : cvg_sups_inf; [exact : f_ub|exact : f_lb].
by congr (inf [set _ | _ in _]); rewrite predeqE.
move /eq_measurable_fun; apply ; apply : measurable_fun_infs => //.
move => t Dt; have [M hM] := f_lb _ Dt; exists M => _ [m /= nm <-].
rewrite (@le_trans _ _ (h m t)) //; first by apply hM => /=; exists m .
by apply : sup_ub; [exact /has_ubound_sdrop/f_ub|exists m => /=].
by move => k; exact : measurable_fun_sups.
Qed .
Lemma measurable_fun_cvg D (h : (T -> R)^nat) f :
(forall m , measurable_fun D (h m)) -> (forall x , D x -> h ^~ x --> f x) ->
measurable_fun D f.
Proof .
move => mf_ f_f; have fE x : D x -> f x = lim_sup (h ^~ x).
move => Dx; have /cvg_lim <-// := @cvg_sups _ (h ^~ x) (f x) (f_f _ Dx).
exact : Rhausdorff.
apply : (@eq_measurable_fun _ _ _ _ D (fun x => lim_sup (h ^~ x))).
by move => x; rewrite inE => Dx; rewrite -fE.
apply : (@measurable_fun_lim_sup _ h) => // t Dt.
- apply /bounded_fun_has_ubound/(@cvg_seq_bounded _ [normedModType R of R^o]).
by apply /cvg_ex; eexists ; exact : f_f.
- apply /bounded_fun_has_lbound/(@cvg_seq_bounded _ [normedModType R of R^o]).
by apply /cvg_ex; eexists ; exact : f_f.
Qed .
End measurable_fun_realType .
Section standard_emeasurable_fun .
Variable R : realType.
Lemma measurable_fun_EFin (D : set R) : measurable_fun D EFin.
Proof .
move => mD; apply : (measurability (ErealGenOInfty.measurableE R)) => //.
move => /= _ [_ [x ->]] <-; apply : measurableI => //.
by rewrite preimage_itv_o_infty EFin_itv; exact : measurable_itv.
Qed .
Lemma measurable_fun_abse (D : set (\bar R)) : measurable_fun D abse.
Proof .
move => mD; apply : (measurability (ErealGenOInfty.measurableE R)) => //.
move => /= _ [_ [x ->] <-].
rewrite [X in _ @^-1 ` X](punct_eitv_bnd_pinfty _ x) preimage_setU setIUr.
apply : measurableU; last first .
by rewrite preimage_abse_pinfty; apply : measurableI => //; exact : measurableU.
apply : measurableI => //; exists (normr @^-1 ` `]x, +oo[%classic).
rewrite -[X in measurable X]setTI.
by apply : measurable_fun_normr => //; exact : measurable_itv.
exists set0 ; first by constructor .
rewrite setU0 predeqE => -[y| |]; split => /= => -[r];
rewrite ?/= /= ?in_itv /= ?andbT => xr//.
+ by move => [ry]; exists `|y| => //=; rewrite in_itv/= andbT -ry.
+ by move => [ry]; exists y => //=; rewrite /= in_itv/= andbT -ry.
Qed .
Lemma emeasurable_fun_minus (D : set (\bar R)) :
measurable_fun D (-%E : \bar R -> \bar R).
Proof .
move => mD; apply : (measurability (ErealGenCInfty.measurableE R)) => //.
move => _ [_ [x ->] <-]; rewrite (_ : _ @^-1 ` _ = `]-oo, (- x)%:E]%classic).
by apply : measurableI => //; exact : emeasurable_itv_ninfty_bnd.
by rewrite predeqE => y; rewrite preimage_itv !in_itv/= andbT in_itv lee_oppr.
Qed .
End standard_emeasurable_fun .
#[global ] Hint Extern 0 (measurable_fun _ abse) =>
solve [exact : measurable_fun_abse] : core.
#[global ] Hint Extern 0 (measurable_fun _ EFin) =>
solve [exact : measurable_fun_EFin] : core.
(* NB: real-valued function *)
Lemma EFin_measurable_fun d (T : measurableType d) (R : realType) (D : set T)
(g : T -> R) :
measurable_fun D (EFin \o g) <-> measurable_fun D g.
Proof .
split => [mf mD A mA|]; last by move => mg; exact : measurable_funT_comp.
rewrite [X in measurable X](_ : _ = D `&` (EFin \o g) @^-1 ` (EFin @` A)).
by apply : mf => //; exists A => //; exists set0 ; [constructor |rewrite setU0].
congr (_ `&` _);rewrite eqEsubset; split => [|? []/= _ /[swap ] -[->//]].
by move => ? ?; exact : preimage_image.
Qed .
Section emeasurable_fun .
Local Open Scope ereal_scope.
Context d (T : measurableType d) (R : realType).
Implicit Types (D : set T).
Lemma emeasurable_fun_bool (D : set T) (f : T -> bool) b :
measurable (f @^-1 ` [set b]) -> measurable_fun D f.
Proof .
have FNT : [set false] = [set ~ true] by apply /seteqP; split => -[]//=.
wlog {b}-> : b / b = true.
case : b => [|h]; first exact .
by rewrite FNT -preimage_setC => /measurableC; rewrite setCK; exact : h.
move => mfT mD /= Y; have := @subsetT _ Y; rewrite setT_bool => YT.
have [-> _|-> _|-> _ |-> _] := subset_set2 YT.
- by rewrite preimage0 ?setI0 .
- by apply : measurableI => //; exact : mfT.
- rewrite -[X in measurable X]setCK; apply : measurableC; rewrite setCI.
apply : measurableU; first exact : measurableC.
by rewrite FNT preimage_setC setCK; exact : mfT.
- by rewrite -setT_bool preimage_setT setIT.
Qed .
Arguments emeasurable_fun_bool {D f} b.
Lemma measurable_fun_einfs D (f : (T -> \bar R)^nat) :
(forall n , measurable_fun D (f n)) ->
forall n , measurable_fun D (fun x => einfs (f ^~ x) n).
Proof .
move => mf n mD.
apply : (measurability (ErealGenCInfty.measurableE R)) => //.
move => _ [_ [x ->] <-]; rewrite einfs_preimage -bigcapIr; last by exists n => /=.
by apply : bigcap_measurable => ? ?; exact /mf/emeasurable_itv_bnd_pinfty.
Qed .
Lemma measurable_fun_esups D (f : (T -> \bar R)^nat) :
(forall n , measurable_fun D (f n)) ->
forall n , measurable_fun D (fun x => esups (f ^~ x) n).
Proof .
move => mf n mD; apply : (measurability (ErealGenOInfty.measurableE R)) => //.
move => _ [_ [x ->] <-];rewrite esups_preimage setI_bigcupr.
by apply : bigcup_measurable => ? ?; exact /mf/emeasurable_itv_bnd_pinfty.
Qed .
Lemma emeasurable_fun_max D (f g : T -> \bar R) :
measurable_fun D f -> measurable_fun D g ->
measurable_fun D (fun x => maxe (f x) (g x)).
Proof .
move => mf mg mD; apply : (measurability (ErealGenCInfty.measurableE R)) => //.
move => _ [_ [x ->] <-]; rewrite [X in measurable X](_ : _ =
(D `&` f @^-1 ` `[x%:E, +oo[) `|` (D `&` g @^-1 ` `[x%:E, +oo[)); last first .
rewrite predeqE => t /=; split .
by rewrite !/= /= !in_itv /= !andbT le_maxr => -[Dx /orP[|]];
tauto .
by move => [|]; rewrite !/= /= !in_itv/= !andbT le_maxr;
move => [Dx ->]//; rewrite orbT.
by apply : measurableU; [exact /mf/emeasurable_itv_bnd_pinfty|
exact /mg/emeasurable_itv_bnd_pinfty].
Qed .
Lemma emeasurable_funN D (f : T -> \bar R) :
measurable_fun D f -> measurable_fun D (\- f).
Proof . by apply : measurable_funT_comp => //; exact : emeasurable_fun_minus. Qed .
Lemma emeasurable_fun_funepos D (f : T -> \bar R) :
measurable_fun D f -> measurable_fun D f^\+.
Proof .
by move => mf; apply : emeasurable_fun_max => //; exact : measurable_fun_cst.
Qed .
Lemma emeasurable_fun_funeneg D (f : T -> \bar R) :
measurable_fun D f -> measurable_fun D f^\-.
Proof .
by move => mf; apply : emeasurable_fun_max => //;
[exact : emeasurable_funN|exact : measurable_fun_cst].
Qed .
Lemma emeasurable_fun_min D (f g : T -> \bar R) :
measurable_fun D f -> measurable_fun D g ->
measurable_fun D (fun x => mine (f x) (g x)).
Proof .
move => /emeasurable_funN mf /emeasurable_funN mg.
have /emeasurable_funN := emeasurable_fun_max mf mg.
by apply eq_measurable_fun => i Di; rewrite -oppe_min oppeK.
Qed .
Lemma measurable_fun_lim_esup D (f : (T -> \bar R)^nat) :
(forall n , measurable_fun D (f n)) ->
measurable_fun D (fun x => lim_esup (f ^~ x)).
Proof .
move => mf mD; rewrite (_ : (fun _ => _) =
(fun x => ereal_inf [set esups (f^~ x) n | n in [set n | n >= 0 ]%N])).
by apply : measurable_fun_einfs => // k; exact : measurable_fun_esups.
rewrite funeqE => t; apply /cvg_lim => //.
rewrite [X in _ --> X](_ : _ = ereal_inf (range (esups (f^~t)))).
exact : cvg_esups_inf.
by congr (ereal_inf [set _ | _ in _]); rewrite predeqE.
Qed .
#[deprecated(since="mathcomp-analysis 0.6.0" ,
note="renamed `measurable_fun_lim_esup`" )]
Notation measurable_fun_elim_sup := measurable_fun_lim_esup.
Lemma emeasurable_fun_cvg D (f_ : (T -> \bar R)^nat) (f : T -> \bar R) :
(forall m , measurable_fun D (f_ m)) ->
(forall x , D x -> f_ ^~ x --> f x) -> measurable_fun D f.
Proof .
move => mf_ f_f; have fE x : D x -> f x = lim_esup (f_^~ x).
by move => Dx; have /cvg_lim <-// := @cvg_esups _ (f_^~x) (f x) (f_f x Dx).
apply : (measurable_fun_ext (fun x => lim_esup (f_ ^~ x))) => //.
by move => x; rewrite inE => Dx; rewrite fE.
exact : measurable_fun_lim_esup.
Qed .
End emeasurable_fun .
Arguments emeasurable_fun_cvg {d T R D} f_.