diff --git a/.nix/config.nix b/.nix/config.nix index 1dbcc48de0..3d2c9c457b 100644 --- a/.nix/config.nix +++ b/.nix/config.nix @@ -55,7 +55,6 @@ in bundles."8.20".coqPackages = common-bundle // { coq.override.version = "8.20"; - mathcomp.override.version = "2.2.0"; }; bundles."9.0".coqPackages = common-bundle // { diff --git a/_CoqProject b/_CoqProject index 53b84d50c3..41bbb4a235 100644 --- a/_CoqProject +++ b/_CoqProject @@ -67,6 +67,7 @@ theories/homotopy_theory/homotopy.v theories/homotopy_theory/wedge_sigT.v theories/homotopy_theory/continuous_path.v +theories/ess_sup_inf.v theories/separation_axioms.v theories/function_spaces.v theories/ereal.v @@ -97,3 +98,4 @@ theories/gauss_integral.v theories/showcase/summability.v analysis_stdlib/Rstruct_topology.v analysis_stdlib/showcase/uniform_bigO.v +theories/lspace.v diff --git a/classical/boolp.v b/classical/boolp.v index 3c3b726907..80607a9dab 100644 --- a/classical/boolp.v +++ b/classical/boolp.v @@ -329,6 +329,30 @@ Proof. by rewrite /asbool; case: pselect=> h; constructor. Qed. Lemma asboolW (P : Prop) : `[

] -> P. Proof. by case: asboolP. Qed. +Lemma orW A B : A \/ B -> A + B. +Proof. +have [|NA] := asboolP A; first by left. +have [|NB] := asboolP B; first by right. +by move=> AB; exfalso; case: AB. +Qed. + +Lemma or3W A B C : [\/ A, B | C] -> A + B + C. +Proof. +have [|NA] := asboolP A; first by left; left. +have [|NB] := asboolP B; first by left; right. +have [|NC] := asboolP C; first by right. +by move=> ABC; exfalso; case: ABC. +Qed. + +Lemma or4W A B C D : [\/ A, B, C | D] -> A + B + C + D. +Proof. +have [|NA] := asboolP A; first by left; left; left. +have [|NB] := asboolP B; first by left; left; right. +have [|NC] := asboolP C; first by left; right. +have [|ND] := asboolP D; first by right. +by move=> ABCD; exfalso; case: ABCD. +Qed. + (* Shall this be a coercion ?*) Lemma asboolT (P : Prop) : P -> `[

]. Proof. by case: asboolP. Qed. diff --git a/classical/classical_sets.v b/classical/classical_sets.v index c550fdeaa8..5427168b9b 100644 --- a/classical/classical_sets.v +++ b/classical/classical_sets.v @@ -1523,6 +1523,9 @@ Proof. by move=> b [x [Aa Ba <-]]; split; apply: imageP. Qed. Lemma nonempty_image f A : f @` A !=set0 -> A !=set0. Proof. by case=> b [a]; exists a. Qed. +Lemma image_nonempty f A : A !=set0 -> f @` A !=set0. +Proof. by move=> [x] Ax; exists (f x), x. Qed. + Lemma image_subset f A B : A `<=` B -> f @` A `<=` f @` B. Proof. by move=> AB _ [a Aa <-]; exists a => //; apply/AB. Qed. @@ -1645,6 +1648,8 @@ Proof. by rewrite preimage_false; under eq_fun do rewrite inE. Qed. End image_lemmas. Arguments sub_image_setI {aT rT f A B} t _. +Arguments subset_set1 {_ _ _}. +Arguments subset_set2 {_ _ _ _}. Lemma image2_subset {aT bT rT : Type} (f : aT -> bT -> rT) (A B : set aT) (C D : set bT) : A `<=` B -> C `<=` D -> diff --git a/classical/mathcomp_extra.v b/classical/mathcomp_extra.v index 1795e300d6..7572527453 100644 --- a/classical/mathcomp_extra.v +++ b/classical/mathcomp_extra.v @@ -681,3 +681,17 @@ Proof. exact: comparable_max_le_max. Qed. Lemma real_sqrtC {R : numClosedFieldType} (x : R) : 0 <= x -> sqrtC x \in Num.real. Proof. by rewrite -sqrtC_ge0; apply: ger0_real. Qed. + +Lemma eq_exists2l (A : Type) (P P' Q : A -> Prop) : + (forall x, P x <-> P' x) -> + (exists2 x, P x & Q x) <-> (exists2 x, P' x & Q x). +Proof. +by move=> eqQ; split=> -[x p q]; exists x; move: p q; rewrite ?eqQ. +Qed. + +Lemma eq_exists2r (A : Type) (P Q Q' : A -> Prop) : + (forall x, Q x <-> Q' x) -> + (exists2 x, P x & Q x) <-> (exists2 x, P x & Q' x). +Proof. +by move=> eqP; split=> -[x p q]; exists x; move: p q; rewrite ?eqP. +Qed. diff --git a/experimental_reals/discrete.v b/experimental_reals/discrete.v index 63ca0e73b8..412877a07b 100644 --- a/experimental_reals/discrete.v +++ b/experimental_reals/discrete.v @@ -4,7 +4,7 @@ (* Copyright (c) - 2016--2018 - Polytechnique *) (* -------------------------------------------------------------------- *) -From Corelib Require Setoid. +From Coq Require Setoid. From HB Require Import structures. From mathcomp Require Import all_ssreflect all_algebra. From mathcomp.classical Require Import boolp. diff --git a/reals/reals.v b/reals/reals.v index 6d747774d5..2e0ae6052b 100644 --- a/reals/reals.v +++ b/reals/reals.v @@ -38,7 +38,7 @@ (* *) (******************************************************************************) -From Corelib Require Import Setoid. +From Coq Require Import Setoid. From HB Require Import structures. From mathcomp Require Import all_ssreflect all_algebra archimedean. From mathcomp Require Import boolp classical_sets set_interval. diff --git a/theories/Make b/theories/Make index aac6828d70..ff9334288c 100644 --- a/theories/Make +++ b/theories/Make @@ -9,6 +9,7 @@ ereal.v landau.v +ess_sup_inf.v topology_theory/topology.v topology_theory/bool_topology.v topology_theory/compact.v diff --git a/theories/all_analysis.v b/theories/all_analysis.v index b567c76901..2a745ee6ac 100644 --- a/theories/all_analysis.v +++ b/theories/all_analysis.v @@ -25,3 +25,4 @@ From mathcomp Require Export charge. From mathcomp Require Export kernel. From mathcomp Require Export pi_irrational. From mathcomp Require Export gauss_integral. +From mathcomp Require Export ess_sup_inf. diff --git a/theories/charge.v b/theories/charge.v index 6ae5e0979a..d9a8c59484 100644 --- a/theories/charge.v +++ b/theories/charge.v @@ -1866,7 +1866,7 @@ have nuf A : d.-measurable A -> nu A = \int[mu]_(x in A) f x. move=> A mA; rewrite nuf ?inE//; apply: ae_eq_integral => //. - exact/measurable_funTS. - exact/measurable_funTS. -- exact: ae_eq_subset ff'. +- exact: (@ae_eq_subset _ _ _ _ mu setT A f f' (@subsetT _ A)). Qed. End radon_nikodym_sigma_finite. @@ -2092,6 +2092,10 @@ move=> mE; apply: integral_ae_eq => //. by rewrite -Radon_Nikodym_SigmaFinite.f_integral. Qed. +(* TODO: move back to measure.v, current version incompatible *) +Lemma ae_eq_mul2l (f g h : T -> \bar R) D : f = g %[ae mu in D] -> (h \* f) = (h \* g) %[ae mu in D]. +Proof. by apply: filterS => x /= /[apply] ->. Qed. + Lemma Radon_Nikodym_change_of_variables f E : measurable E -> nu.-integrable E f -> \int[mu]_(x in E) (f x * ('d (charge_of_finite_measure nu) '/d mu) x) = diff --git a/theories/ereal.v b/theories/ereal.v index d673952373..181b04e4b9 100644 --- a/theories/ereal.v +++ b/theories/ereal.v @@ -463,6 +463,21 @@ rewrite lteNl => /ereal_sup_gt[_ [y Sy <-]]. by rewrite lteNl oppeK => xlty; exists y. Qed. +Lemma ereal_infEN S : ereal_inf S = - ereal_sup [set - x | x in S]. +Proof. by []. Qed. + +Lemma ereal_supN S : ereal_sup [set - x | x in S] = - ereal_inf S. +Proof. by rewrite oppeK. Qed. + +Lemma ereal_infN S : ereal_inf [set - x | x in S] = - ereal_sup S. +Proof. +rewrite /ereal_inf; congr (- ereal_sup _) => /=. +by rewrite image_comp/=; under eq_imagel do rewrite /= oppeK; rewrite image_id. +Qed. + +Lemma ereal_supEN S : ereal_sup S = - ereal_inf [set - x | x in S]. +Proof. by rewrite ereal_infN oppeK. Qed. + End ereal_supremum. Section ereal_supremum_realType. @@ -523,7 +538,7 @@ Proof. by move=> Soo; apply/eqP; rewrite eq_le leey/=; exact: ereal_sup_ubound. Qed. -Lemma ereal_sup_le S x : (exists2 y, S y & x <= y) -> x <= ereal_sup S. +Lemma ereal_sup_ge S x : (exists2 y, S y & x <= y) -> x <= ereal_sup S. Proof. by move=> [y Sy] /le_trans; apply; exact: ereal_sup_ubound. Qed. Lemma ereal_sup_ninfty S : ereal_sup S = -oo <-> S `<=` [set -oo]. @@ -591,11 +606,84 @@ rewrite -ereal_sup_EFin; [|exact/has_lb_ubN|exact/nonemptyN]. by rewrite !image_comp. Qed. +Lemma ereal_supP S x : + reflect (forall y : \bar R, S y -> y <= x) (ereal_sup S <= x). +Proof. +apply/(iffP idP) => [+ y Sy|]. + by move=> /(le_trans _)->//; rewrite ereal_sup_ge//; exists y. +apply: contraPP => /negP; rewrite -ltNge -existsPNP. +by move=> /ereal_sup_gt[y Sy ltyx]; exists y => //; rewrite lt_geF. +Qed. + +Lemma ereal_infP S x : + reflect (forall y : \bar R, S y -> x <= y) (x <= ereal_inf S). +Proof. +rewrite leeNr; apply/(equivP (ereal_supP _ _)); setoid_rewrite leeNr. +split=> [ge_x y Sy|ge_x _ [y Sy <-]]; rewrite ?oppeK// ?ge_x//. +by rewrite -[y]oppeK ge_x//; exists y. +Qed. + +Lemma ereal_sup_gtP S x : + reflect (exists2 y : \bar R, S y & x < y) (x < ereal_sup S). +Proof. +rewrite ltNge; apply/(equivP negP); rewrite -(rwP (ereal_supP _ _)) -existsPNP. +by apply/eq_exists2r => y; rewrite (rwP2 negP idP) -ltNge. +Qed. + +Lemma ereal_inf_ltP S x : + reflect (exists2 y : \bar R, S y & y < x) (ereal_inf S < x). +Proof. +rewrite ltNge; apply/(equivP negP); rewrite -(rwP (ereal_infP _ _)) -existsPNP. +by apply/eq_exists2r => y; rewrite (rwP2 negP idP) -ltNge. +Qed. + +Lemma ereal_inf_leP S x : S (ereal_inf S) -> + reflect (exists2 y : \bar R, S y & y <= x) (ereal_inf S <= x). +Proof. +move=> Sinf; apply: (iffP idP); last exact: ereal_inf_le. +by move=> Sx; exists (ereal_inf S). +Qed. + +Lemma ereal_sup_geP S x : S (ereal_sup S) -> + reflect (exists2 y : \bar R, S y & x <= y) (x <= ereal_sup S). +Proof. +move=> Ssup; apply: (iffP idP); last exact: ereal_sup_ge. +by move=> Sx; exists (ereal_sup S). +Qed. + +Lemma lb_ereal_infNy_adherent S e : + ereal_inf S = -oo -> exists2 x : \bar R, S x & x < e%:E. +Proof. by move=> infNy; apply/ereal_inf_ltP; rewrite infNy ltNyr. Qed. + +Lemma ereal_sup_real : @ereal_sup R (range EFin) = +oo. +Proof. +rewrite hasNub_ereal_sup//; last by exists 0%R. +by apply/has_ubPn => x; exists (x+1)%R => //; rewrite ltrDl. +Qed. + +Lemma ereal_inf_real : @ereal_inf R (range EFin) = -oo. +Proof. +rewrite /ereal_inf [X in ereal_sup X](_ : _ = range EFin); last first. + apply/seteqP; split => x/=[y]. + by move=> [z] _ <- <-; exists (-z)%R. + by move=> _ <-; exists (-y%:E); first (by exists (-y)%R); rewrite oppeK. +by rewrite ereal_sup_real. +Qed. + End ereal_supremum_realType. #[deprecated(since="mathcomp-analysis 1.3.0", note="Renamed `ereal_sup_ubound`.")] Notation ereal_sup_ub := ereal_sup_ubound (only parsing). #[deprecated(since="mathcomp-analysis 1.3.0", note="Renamed `ereal_inf_lbound`.")] Notation ereal_inf_lb := ereal_inf_lbound (only parsing). +#[deprecated(since="mathcomp-analysis 1.10.0", note="Renamed `ereal_sup_ge`.")] +Notation ereal_sup_le := ereal_sup_ge. + +Arguments ereal_supP {R S x}. +Arguments ereal_infP {R S x}. +Arguments ereal_sup_gtP {R S x}. +Arguments ereal_inf_ltP {R S x}. +Arguments ereal_sup_geP {R S x}. +Arguments ereal_inf_leP {R S x}. Lemma restrict_abse T (R : numDomainType) (f : T -> \bar R) (D : set T) : (abse \o f) \_ D = abse \o (f \_ D). diff --git a/theories/ess_sup_inf.v b/theories/ess_sup_inf.v new file mode 100644 index 0000000000..71ad495f55 --- /dev/null +++ b/theories/ess_sup_inf.v @@ -0,0 +1,344 @@ +From HB Require Import structures. +From mathcomp Require Import all_ssreflect all_algebra archimedean finmap. +From mathcomp Require Import mathcomp_extra boolp classical_sets functions. +From mathcomp Require Import cardinality fsbigop reals interval_inference ereal. +From mathcomp Require Import topology normedtype sequences esum numfun. +From mathcomp Require Import measure lebesgue_measure. + +(**md**************************************************************************) +(* ``` *) +(* ess_sup f == essential supremum of the function f : T -> R where T is a *) +(* semiRingOfSetsType and R is a realType *) +(* ess_inf f == essential infimum *) +(* ``` *) +(* *) +(******************************************************************************) + +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. +Local Open Scope ereal_scope. + +Section essential_supremum. +Context d {T : measurableType d} {R : realType}. +Variable mu : {measure set T -> \bar R}. +Implicit Types (f g : T -> \bar R) (h k : T -> R). + +(* TODO: move *) +Lemma measure0_ae (P : set T) : mu [set: T] = 0 -> \forall x \ae mu, P x. +Proof. by move=> x; exists setT; split. Qed. + +Definition ess_sup f := ereal_inf [set y | \forall x \ae mu, f x <= y]. + +Lemma ess_supEae (f : T -> \bar R) : + ess_sup f = ereal_inf [set y | \forall x \ae mu, f x <= y]. +Proof. by []. Qed. + +Lemma ae_le_measureP f y : measurable_fun setT f -> + (\forall x \ae mu, f x <= y) <-> (mu (f @^-1` `]y, +oo[) = 0). +Proof. +move=> f_meas; have fVroo_meas : d.-measurable (f @^-1` `]y, +oo[). + by rewrite -[_ @^-1` _]setTI; apply/f_meas=> //; exact/emeasurable_itv. +have setCfVroo : (f @^-1` `]y, +oo[) = ~` [set x | f x <= y]. + by apply: setC_inj; rewrite preimage_setC setCitv/= set_itvxx setU0 setCK. +split. + move=> [N [dN muN0 inN]]; rewrite (subset_measure0 _ dN)// => x. + by rewrite setCfVroo; apply: inN. +set N := (X in mu X) => muN0; exists N; rewrite -setCfVroo. +by split => //; exact: fVroo_meas. +Qed. + +Lemma ess_supEmu0 (f : T -> \bar R) : measurable_fun setT f -> + ess_sup f = ereal_inf [set y | mu (f @^-1` `]y, +oo[) = 0]. +Proof. +by move=> ?; congr (ereal_inf _); apply/predeqP => r; exact: ae_le_measureP. +Qed. + +Lemma ess_sup_ge f : \forall x \ae mu, f x <= ess_sup f. +Proof. +rewrite ess_supEae//; set I := (X in ereal_inf X). +have [->|IN0] := eqVneq I set0. + by rewrite ereal_inf0; apply: nearW => ?; rewrite leey. +have [u uI uinf] := ereal_inf_seq IN0. +rewrite -(cvg_lim _ uinf)//; near=> x. +rewrite lime_ge//; first by apply/cvgP: uinf. +by apply: nearW; near: x; apply/ae_foralln => n; apply: uI. +Unshelve. all: by end_near. Qed. + +Lemma ess_supP f a : reflect (\forall x \ae mu, f x <= a) (ess_sup f <= a). +Proof. +apply: (iffP (ereal_inf_leP _)) => /=; last 2 first. +- by move=> [y fy ya]; near do apply: le_trans ya. +- by move=> fa; exists a. +by rewrite -ess_supEae//; exact: ess_sup_ge. +Unshelve. all: by end_near. Qed. + +Lemma le_ess_sup f g : (\forall x \ae mu, f x <= g x) -> ess_sup f <= ess_sup g. +Proof. +move=> fg; apply/ess_supP => //. +near do rewrite (le_trans (near fg _ _))//=. +exact: ess_sup_ge. +Unshelve. all: by end_near. Qed. + +Lemma eq_ess_sup f g : (\forall x \ae mu, f x = g x) -> ess_sup f = ess_sup g. +Proof. +move=> fg; apply/eqP; rewrite eq_le !le_ess_sup//=; + by apply: filterS fg => x ->. +Qed. + +Lemma ess_sup_cst r : 0 < mu [set: T] -> ess_sup (cst r) = r. +Proof. +move=> muT_gt0; apply/eqP; rewrite eq_le; apply/andP; split. + by apply/ess_supP => //; apply: nearW. +have ae_proper := ae_properfilter_algebraOfSetsType muT_gt0. +by near (almost_everywhere mu) => x; near: x; apply: ess_sup_ge. +Unshelve. all: by end_near. Qed. + +Lemma ess_sup_ae_cst f r : 0 < mu [set: T] -> + (\forall x \ae mu, f x = r) -> ess_sup f = r. +Proof. by move=> muT_gt0 /= /eq_ess_sup->; rewrite ess_sup_cst. Qed. + +Lemma ess_sup_gee f y : 0 < mu [set: T] -> + (\forall x \ae mu, y <= f x)%E -> y <= ess_sup f. +Proof. by move=> *; rewrite -(ess_sup_cst y)//; apply: le_ess_sup. Qed. + +Lemma abs_sup_eq0_ae_eq f : ess_sup (abse \o f) = 0 -> f = \0 %[ae mu]. +Proof. +move=> ess_sup_f_eq0; near=> x => _ /=; apply/eqP. +rewrite -abse_eq0 eq_le abse_ge0 andbT; near: x. +by apply/ess_supP; rewrite ess_sup_f_eq0. +Unshelve. all: by end_near. Qed. + +Lemma abs_ess_sup_eq0 f : mu [set: T] > 0 -> + f = \0 %[ae mu] -> ess_sup (abse \o f) = 0. +Proof. +move=> muT_gt0 f0; apply/eqP; rewrite eq_le; apply/andP; split. + by apply/ess_supP => /=; near do rewrite (near f0 _ _)//= normr0//. +by rewrite -[0]ess_sup_cst// le_ess_sup//=; near=> x; rewrite abse_ge0. +Unshelve. all: by end_near. Qed. + +Lemma ess_sup_pZl f (a : R) : (0 < a)%R -> + (ess_sup (cst a%:E \* f) = a%:E * ess_sup f). +Proof. +move=> /[dup] /ltW a_ge0 a_gt0. +gen have esc_le : a f a_ge0 a_gt0 / + (ess_sup (cst a%:E \* f) <= a%:E * ess_sup f)%E. + by apply/ess_supP; near do rewrite /cst/= lee_pmul2l//; apply/ess_supP. +apply/eqP; rewrite eq_le esc_le// -lee_pdivlMl//=. +apply: le_trans (esc_le _ _ _ _); rewrite ?invr_gt0 ?invr_ge0//. +by under eq_fun do rewrite muleA -EFinM mulVf ?mul1e ?gt_eqF//. +Unshelve. all: by end_near. Qed. + +Lemma ess_supZl f (a : R) : mu [set: T] > 0 -> (0 <= a)%R -> + (ess_sup (cst a%:E \* f) = a%:E * ess_sup f). +Proof. + +move=> muTN0; case: ltgtP => // [a_gt0|<-] _; first exact: ess_sup_pZl. +by under eq_fun do rewrite mul0e; rewrite mul0e ess_sup_cst. +Qed. + +Lemma ess_sup_eqNyP f : ess_sup f = -oo <-> \forall x \ae mu, f x = -oo. +Proof. +rewrite (rwP eqP) -leeNy_eq (eq_near (fun=> rwP eqP)). +by under eq_near do rewrite -leeNy_eq; apply/(rwP2 idP (ess_supP _ _)). +Qed. + +Lemma ess_supD f g : ess_sup (f \+ g) <= ess_sup f + ess_sup g. +Proof. +by apply/ess_supP; near do rewrite lee_add//; apply/ess_supP. +Unshelve. all: by end_near. Qed. + +Lemma ess_sup_absD f g : + ess_sup (abse \o (f \+ g)) <= ess_sup (abse \o f) + ess_sup (abse \o g). +Proof. +rewrite (le_trans _ (ess_supD _ _))// le_ess_sup//. +by apply/nearW => x; apply/lee_abs_add. +Qed. + +End essential_supremum. +Arguments ess_sup_ae_cst {d T R mu f}. +Arguments ess_supP {d T R mu f a}. + +Section real_essential_supremum. +Context d {T : measurableType d} {R : realType}. +Variable mu : {measure set T -> \bar R}. +Implicit Types f : T -> R. + +Notation ess_supr f := (ess_sup mu (EFin \o f)). + +Lemma ess_supr_bounded f : ess_supr f < +oo -> + exists M, \forall x \ae mu, (f x <= M)%R. +Proof. +set g := EFin \o f => ltfy; have [|supfNy] := eqVneq (ess_sup mu g) -oo. + by move=> /ess_sup_eqNyP fNy; exists 0%:R; apply: filterS fNy. +have supf_fin : ess_supr f \is a fin_num by case: ess_sup ltfy supfNy. +by exists (fine (ess_supr f)); near do rewrite -lee_fin fineK//; apply/ess_supP. +Unshelve. all: by end_near. Qed. + +Lemma ess_sup_eqr0_ae_eq f : ess_supr (normr \o f) = 0 -> f = 0%R %[ae mu]. +Proof. +under [X in ess_sup _ X]eq_fun do rewrite /= -abse_EFin. +move=> /abs_sup_eq0_ae_eq; apply: filterS => x /= /(_ _)/eqP. +by rewrite eqe => /(_ _)/eqP. +Qed. + +Lemma ess_suprZl f (y : R) : mu setT > 0 -> (0 <= y)%R -> + ess_supr (cst y \* f)%R = y%:E * ess_supr f. +Proof. by move=> muT_gt0 r_ge0; rewrite -ess_supZl. Qed. + +Lemma ess_sup_ger f x : 0 < mu [set: T] -> (forall t, x <= (f t)%:E) -> + x <= ess_supr f. +Proof. by move=> muT f0; apply/ess_sup_gee => //=; apply: nearW. Qed. + +Lemma ess_sup_ler f y : (forall t, (f t)%:E <= y) -> ess_supr f <= y. +Proof. by move=> ?; apply/ess_supP; apply: nearW. Qed. + +Lemma ess_sup_cstr y : (0 < mu setT)%E -> (ess_supr (cst y) = y%:E)%E. +Proof. by move=> muN0; rewrite (ess_sup_ae_cst y%:E)//=; apply: nearW. Qed. + +Lemma ess_suprD f g : ess_supr (f \+ g) <= ess_supr f + ess_supr g. +Proof. by rewrite (le_trans _ (ess_supD _ _ _)). Qed. + +Lemma ess_sup_normD f g : + ess_supr (normr \o (f \+ g)) <= ess_supr (normr \o f) + ess_supr (normr \o g). +Proof. +rewrite (le_trans _ (ess_suprD _ _))// le_ess_sup//. +by apply/nearW => x; apply/ler_normD. +Qed. + +End real_essential_supremum. +Notation ess_supr mu f := (ess_sup mu (EFin \o f)). + +Section essential_infimum. +Context d {T : measurableType d} {R : realType}. +Variable mu : {measure set T -> \bar R}. +Implicit Types f : T -> \bar R. + +Definition ess_inf f := ereal_sup [set y | \forall x \ae mu, y <= f x]. +Notation ess_sup := (ess_sup mu). + +Lemma ess_infEae (f : T -> \bar R) : + ess_inf f = ereal_sup [set y | \forall x \ae mu, y <= f x]. +Proof. by []. Qed. + +Lemma ess_infEN (f : T -> \bar R) : ess_inf f = - ess_sup (\- f). +Proof. +rewrite ess_supEae ess_infEae ereal_infEN oppeK; congr (ereal_sup _). +apply/seteqP; split=> [y /= y_le|_ [/= y y_ge <-]]. + by exists (- y); rewrite ?oppeK//=; apply: filterS y_le => x; rewrite leeN2. +by apply: filterS y_ge => x; rewrite leeNl. +Qed. + +Lemma ess_supEN (f : T -> \bar R) : ess_sup f = - ess_inf (\- f). +Proof. +by rewrite ess_infEN oppeK; apply/eq_ess_sup/nearW => ?; rewrite oppeK. +Qed. + +Lemma ess_infN (f : T -> \bar R) : ess_inf (\- f) = - ess_sup f. +Proof. by rewrite ess_supEN oppeK. Qed. + +Lemma ess_supN (f : T -> \bar R) : ess_sup (\- f) = - ess_inf f. +Proof. by rewrite ess_infEN oppeK. Qed. + +Lemma ess_infP f a : reflect (\forall x \ae mu, a <= f x) (a <= ess_inf f). +Proof. +by rewrite ess_infEN leeNr; apply: (iffP ess_supP); + apply: filterS => x; rewrite leeN2. +Qed. + +Lemma ess_inf_le f : \forall x \ae mu, ess_inf f <= f x. +Proof. exact/ess_infP. Qed. + +Lemma le_ess_inf f g : (\forall x \ae mu, f x <= g x) -> ess_inf f <= ess_inf g. +Proof. +move=> fg; apply/ess_infP => //. +near do rewrite (le_trans _ (near fg _ _))//=. +exact: ess_inf_le. +Unshelve. all: by end_near. Qed. + +Lemma eq_ess_inf f g : (\forall x \ae mu, f x = g x) -> ess_inf f = ess_inf g. +Proof. +move=> fg; apply/eqP; rewrite eq_le !le_ess_inf//=; + by apply: filterS fg => x ->. +Qed. + +Lemma ess_inf_cst r : 0 < mu [set: T] -> ess_inf (cst r) = r. +Proof. +by move=> ?; rewrite ess_infEN (ess_sup_ae_cst (- r)) ?oppeK//=; apply: nearW. +Qed. + +Lemma ess_inf_ae_cst f r : 0 < mu [set: T] -> + (\forall x \ae mu, f x = r) -> ess_inf f = r. +Proof. by move=> muT_gt0 /= /eq_ess_inf->; rewrite ess_inf_cst. Qed. + +Lemma ess_inf_gee f y : 0 < mu [set: T] -> + (\forall x \ae mu, y <= f x)%E -> y <= ess_inf f. +Proof. by move=> *; rewrite -(ess_inf_cst y)//; apply: le_ess_inf. Qed. + +Lemma ess_inf_pZl f (a : R) : (0 < a)%R -> + (ess_inf (cst a%:E \* f) = a%:E * ess_inf f). +Proof. +move=> a_gt0; rewrite !ess_infEN muleN; congr (- _)%E. +by under eq_fun do rewrite -muleN; rewrite ess_sup_pZl. +Qed. + +Lemma ess_infZl f (a : R) : mu [set: T] > 0 -> (0 <= a)%R -> + (ess_inf (cst a%:E \* f) = a%:E * ess_inf f). +Proof. +move=> muTN0; case: ltgtP => // [a_gt0|<-] _; first exact: ess_inf_pZl. +by under eq_fun do rewrite mul0e; rewrite mul0e ess_inf_cst. +Qed. + +Lemma ess_inf_eqyP f : ess_inf f = +oo <-> \forall x \ae mu, f x = +oo. +Proof. +rewrite (rwP eqP) -leye_eq (eq_near (fun=> rwP eqP)). +by under eq_near do rewrite -leye_eq; apply/(rwP2 idP (ess_infP _ _)). +Qed. + +Lemma ess_infD f g : ess_inf (f \+ g) >= ess_inf f + ess_inf g. +Proof. +by apply/ess_infP; near do rewrite lee_add//; apply/ess_infP. +Unshelve. all: by end_near. Qed. + +End essential_infimum. +Arguments ess_inf_ae_cst {d T R mu f}. +Arguments ess_infP {d T R mu f a}. + +Section real_essential_infimum. +Context d {T : measurableType d} {R : realType}. +Variable mu : {measure set T -> \bar R}. +Implicit Types f : T -> R. + +Notation ess_infr f := (ess_inf mu (EFin \o f)). + +Lemma ess_infr_bounded f : ess_infr f > -oo -> + exists M, \forall x \ae mu, (f x >= M)%R. +Proof. +set g := EFin \o f => ltfy; have [|inffNy] := eqVneq (ess_inf mu g) +oo. + by move=> /ess_inf_eqyP fNy; exists 0%:R; apply: filterS fNy. +have inff_fin : ess_infr f \is a fin_num by case: ess_inf ltfy inffNy. +by exists (fine (ess_infr f)); near do rewrite -lee_fin fineK//; apply/ess_infP. +Unshelve. all: by end_near. Qed. + +Lemma ess_infrZl f (y : R) : mu setT > 0 -> (0 <= y)%R -> + ess_infr (cst y \* f)%R = y%:E * ess_infr f. +Proof. by move=> muT_gt0 r_ge0; rewrite -ess_infZl. Qed. + +Lemma ess_inf_ger f x : 0 < mu [set: T] -> (forall t, x <= (f t)%:E) -> + x <= ess_infr f. +Proof. by move=> muT f0; apply/ess_inf_gee => //=; apply: nearW. Qed. + +Lemma ess_inf_ler f y : (forall t, y <= (f t)%:E) -> y <= ess_infr f. +Proof. by move=> ?; apply/ess_infP; apply: nearW. Qed. + +Lemma ess_inf_cstr y : (0 < mu setT)%E -> (ess_infr (cst y) = y%:E)%E. +Proof. by move=> muN0; rewrite (ess_inf_ae_cst y%:E)//=; apply: nearW. Qed. + +End real_essential_infimum. +Notation ess_infr mu f := (ess_inf mu (EFin \o f)). diff --git a/theories/hoelder.v b/theories/hoelder.v index d420694d2e..56af8b4c91 100644 --- a/theories/hoelder.v +++ b/theories/hoelder.v @@ -2,18 +2,18 @@ From HB Require Import structures. From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint interval finmap. From mathcomp Require Import mathcomp_extra boolp classical_sets functions. -From mathcomp Require Import cardinality fsbigop reals ereal. -From mathcomp Require Import topology normedtype sequences real_interval. -From mathcomp Require Import esum measure lebesgue_measure lebesgue_integral. -From mathcomp Require Import numfun exp convex interval_inference. +From mathcomp Require Import cardinality fsbigop reals interval_inference ereal. +From mathcomp Require Import topology normedtype sequences real_interval esum. +From mathcomp Require Import measure measurable_realfun lebesgue_measure. +From mathcomp Require Import lebesgue_integral numfun exp convex ess_sup_inf. (**md**************************************************************************) (* # Hoelder's Inequality *) (* *) -(* This file provides Hoelder's inequality. *) +(* This file provides Hoelder's inequality and its consequences, most notably *) +(* Minkowski's inequality and the convexity of the power function. *) (* ``` *) -(* 'N[mu]_p[f] := (\int[mu]_x (`|f x| `^ p)%:E) `^ p^-1 *) -(* The corresponding definition is Lnorm. *) +(* 'N[mu]_p[f] == the p-norm of f with measure mu *) (* ``` *) (* *) (******************************************************************************) @@ -36,18 +36,18 @@ Reserved Notation "'N_ p [ F ]" Declare Scope Lnorm_scope. +Local Open Scope ereal_scope. HB.lock Definition Lnorm {d} {T : measurableType d} {R : realType} - (mu : {measure set T -> \bar R}) (p : \bar R) (f : T -> R) := + (mu : {measure set T -> \bar R}) (p : \bar R) (f : T -> \bar R) := match p with - | p%:E => (if p == 0%R then - mu (f @^-1` (setT `\ 0%R)) - else - (\int[mu]_x (`|f x| `^ p)%:E) `^ p^-1)%E - | +oo%E => (if mu [set: T] > 0 then ess_sup mu (normr \o f) else 0)%E - | -oo%E => 0%E + | p%:E => (\int[mu]_x `|f x| `^ p) `^ p^-1 + (* (mu (f @^-1` (setT `\ 0%R))) when p = 0? *) + | +oo%E => if mu [set: T] > 0 then ess_sup mu (abse \o f) else 0 + | -oo%E => if mu [set: T] > 0 then ess_inf mu (abse \o f) else 0 end. Canonical locked_Lnorm := Unlockable Lnorm.unlock. Arguments Lnorm {d T R} mu p f. +Local Close Scope ereal_scope. Section Lnorm_properties. Context d {T : measurableType d} {R : realType}. @@ -55,47 +55,85 @@ Variable mu : {measure set T -> \bar R}. Local Open Scope ereal_scope. Implicit Types (p : \bar R) (f g : T -> R) (r : R). -Local Notation "'N_ p [ f ]" := (Lnorm mu p f). +Local Notation "'N_ p [ f ]" := (Lnorm mu p (EFin \o f)). + +Lemma Lnorm0 p : 1 <= p -> 'N_p[cst 0%R] = 0. +Proof. +rewrite unlock /Lnorm. +case: p => [r||//]. +- rewrite lee_fin => r1. + have r0 : r != 0%R by rewrite gt_eqF// (lt_le_trans _ r1). + under eq_integral => x _ do rewrite /= normr0 powR0//. + by rewrite integral0 poweR0r// invr_neq0. +case: ifPn => //mu0 _; rewrite (ess_sup_ae_cst 0)//. +by apply: nearW => x; rewrite /= normr0. +Qed. Lemma Lnorm1 f : 'N_1[f] = \int[mu]_x `|f x|%:E. Proof. -rewrite unlock oner_eq0 invr1// poweRe1//. - by apply: eq_integral => t _; rewrite powRr1. -by apply: integral_ge0 => t _; rewrite powRr1. +rewrite unlock invr1// poweRe1//; under eq_integral do [rewrite poweRe1//=] => //. +exact: integral_ge0. Qed. Lemma Lnorm_ge0 p f : 0 <= 'N_p[f]. Proof. -rewrite unlock; move: p => [r/=|/=|//]. - by case: ifPn => // r0; exact: poweR_ge0. -by case: ifPn => // /ess_sup_ge0; apply => t/=. +rewrite unlock; move: p => [r/=|/=|//]; first exact: poweR_ge0. +- by case: ifPn => // /ess_sup_ger; apply => t/=. +- by case: ifPn => // muT0; apply/ess_infP/nearW => x /=. Qed. Lemma eq_Lnorm p f g : f =1 g -> 'N_p[f] = 'N_p[g]. -Proof. by move=> fg; congr Lnorm; exact/funext. Qed. +Proof. by move=> fg; congr Lnorm; apply/eq_fun => ?; rewrite /= fg. Qed. -Lemma Lnorm_eq0_eq0 r f : (0 < r)%R -> measurable_fun setT f -> - 'N_r%:E[f] = 0 -> ae_eq mu [set: T] (fun t => (`|f t| `^ r)%:E) (cst 0). +Lemma Lnorm_eq0_eq0 (f : T -> R) p : + measurable_fun setT f -> (0 < p)%E -> 'N_p[f] = 0 -> f = 0%R %[ae mu]. Proof. -move=> r0 mf; rewrite unlock (gt_eqF r0) => /poweR_eq0_eq0 fp. -apply/ae_eq_integral_abs => //=. - apply: measurableT_comp => //. - apply: (@measurableT_comp _ _ _ _ _ _ (@powR R ^~ r)) => //. - exact: measurableT_comp. -under eq_integral => x _ do rewrite ger0_norm ?powR_ge0//. -by rewrite fp//; apply: integral_ge0 => t _; rewrite lee_fin powR_ge0. +rewrite unlock /Lnorm => mf. +case: p => [r||//]. +- rewrite lte_fin => r0 /poweR_eq0_eq0 => /(_ (integral_ge0 _ _)) h. + have : \int[mu]_x (`|f x| `^ r)%:E = 0. + by apply: h => x _; rewrite lee_fin powR_ge0. + under eq_integral => x _ do rewrite -[_%:E]gee0_abs ?lee_fin ?powR_ge0//. + have mp : measurable_fun [set: T] (fun x : T => (`|f x| `^ r)%:E). + apply: measurableT_comp => //. + apply (measurableT_comp (measurable_powR _)) => //. + exact: measurableT_comp. + move/(ae_eq_integral_abs _ measurableT mp). + apply: filterS => x/= /[apply]. + by case=> /powR_eq0_eq0 /eqP; rewrite normr_eq0 => /eqP. +- case: ifPn => [mu0 _|]. + move=> /abs_sup_eq0_ae_eq/=. + by apply: filterS => x/= /(_ I) /eqP + _; rewrite eqe => /eqP. + rewrite ltNge => /negbNE mu0 _ _. + suffices mueq0: mu setT = 0 by exact: ae_eq0. + by apply/eqP; rewrite eq_le mu0/=. Qed. Lemma powR_Lnorm f r : r != 0%R -> 'N_r%:E[f] `^ r = \int[mu]_x (`| f x | `^ r)%:E. Proof. -move=> r0; rewrite unlock (negbTE r0) -poweRrM mulVf// poweRe1//. +move=> r0; rewrite unlock -poweRrM mulVf// poweRe1//. by apply: integral_ge0 => x _; rewrite lee_fin// powR_ge0. Qed. +Lemma oppr_Lnorm f p : 'N_p[\- f]%R = 'N_p[f]. +Proof. +have NfE : abse \o (EFin \o (\- f)%R) = abse \o EFin \o f. + by apply/funext => x /=; rewrite normrN. +rewrite unlock /Lnorm NfE; case: p => /= [r|//|//]. +by under eq_integral => x _ do rewrite normrN. +Qed. + +Lemma Lnorm_cst1 r : ('N_r%:E[cst 1%R] = (mu setT)`^(r^-1)). +Proof. +rewrite unlock /Lnorm; under eq_integral do rewrite /= normr1 powR1. +by rewrite integral_cst// mul1e. +Qed. + End Lnorm_properties. #[global] + Hint Extern 0 (0 <= Lnorm _ _ _) => solve [apply: Lnorm_ge0] : core. Notation "'N[ mu ]_ p [ f ]" := (Lnorm mu p f). @@ -104,12 +142,12 @@ Section lnorm. (* l-norm is just L-norm applied to counting *) Context d {T : measurableType d} {R : realType}. Local Open Scope ereal_scope. -Local Notation "'N_ p [ f ]" := (Lnorm counting p f). +Local Notation "'N_ p [ f ]" := (Lnorm counting p (EFin \o f)). Lemma Lnorm_counting p (f : R^nat) : (0 < p)%R -> 'N_p%:E [f] = (\sum_(k p0; rewrite unlock gt_eqF// ge0_integral_count// => k. +move=> p0; rewrite unlock ge0_integral_count// => k. by rewrite lee_fin powR_ge0. Qed. @@ -125,7 +163,7 @@ Let measurableT_comp_powR f p : measurable_fun [set: T] f -> measurable_fun setT (fun x => f x `^ p)%R. Proof. exact: (@measurableT_comp _ _ _ _ _ _ (@powR R ^~ p)). Qed. -Local Notation "'N_ p [ f ]" := (Lnorm mu p f). +Local Notation "'N_ p [ f ]" := (Lnorm mu p (EFin \o f)). Let integrable_powR f p : (0 < p)%R -> measurable_fun [set: T] f -> 'N_p%:E[f] != +oo -> @@ -136,7 +174,7 @@ move=> p0 mf foo; apply/integrableP; split. exact: measurableT_comp. rewrite ltey; apply: contra foo. move=> /eqP/(@eqy_poweR _ _ p^-1); rewrite invr_gt0 => /(_ p0) <-. -rewrite unlock (gt_eqF p0); apply/eqP; congr (_ `^ _). +rewrite unlock; apply/eqP; congr (_ `^ _). by apply/eq_integral => t _; rewrite [RHS]gee0_abs// lee_fin powR_ge0. Qed. @@ -144,11 +182,12 @@ Let hoelder0 f g p q : measurable_fun setT f -> measurable_fun setT g -> (0 < p)%R -> (0 < q)%R -> (p^-1 + q^-1 = 1)%R -> 'N_p%:E[f] = 0 -> 'N_1[(f \* g)%R] <= 'N_p%:E[f] * 'N_q%:E[g]. Proof. +rewrite -lte_fin. move=> mf mg p0 q0 pq f0; rewrite f0 mul0e Lnorm1 [leLHS](_ : _ = 0)//. rewrite (ae_eq_integral (cst 0)) => [|//||//|]; first by rewrite integral0. - by do 2 apply: measurableT_comp => //; exact: measurable_funM. -- apply: filterS (Lnorm_eq0_eq0 p0 mf f0) => x /(_ I)[] /powR_eq0_eq0 + _. - by rewrite normrM => ->; rewrite mul0r. +- apply: filterS (Lnorm_eq0_eq0 mf p0 f0) => x /(_ I) + _. + by rewrite normrM => ->; rewrite normr0 mul0r. Qed. Let normalized p f x := `|f x| / fine 'N_p%:E[f]. @@ -171,10 +210,10 @@ transitivity (\int[mu]_x (`|f x| `^ p / fine ('N_p%:E[f] `^ p))%:E). rewrite -[in LHS]powR_inv1; last by rewrite fine_ge0 // Lnorm_ge0. by rewrite fine_poweR powRAC -powR_inv1 // powR_ge0. have fp0 : 0 < \int[mu]_x (`|f x| `^ p)%:E. - rewrite unlock (gt_eqF p0) in fpos. + rewrite unlock in fpos. apply: gt0_poweR fpos; rewrite ?invr_gt0//. by apply integral_ge0 => x _; rewrite lee_fin; exact: powR_ge0. -rewrite unlock (gt_eqF p0) -poweRrM mulVf ?(gt_eqF p0)// (poweRe1 (ltW fp0))//. +rewrite unlock -poweRrM mulVf ?(gt_eqF p0)// (poweRe1 (ltW fp0))//. under eq_integral do rewrite EFinM muleC. have foo : \int[mu]_x (`|f x| `^ p)%:E < +oo. move/integrableP: ifp => -[_]. @@ -355,7 +394,7 @@ Let measurableT_comp_powR f p : measurable_fun setT f -> measurable_fun setT (fun x => f x `^ p)%R. Proof. exact: (@measurableT_comp _ _ _ _ _ _ (@powR R ^~ p)). Qed. -Local Notation "'N_ p [ f ]" := (Lnorm mu p f). +Local Notation "'N_ p [ f ]" := (Lnorm mu p (EFin \o f)). Local Open Scope ereal_scope. Let minkowski1 f g p : measurable_fun setT f -> measurable_fun setT g -> @@ -382,7 +421,7 @@ have h x : (`| f x + g x | `^ p <= rewrite !normrM (@ger0_norm _ 2)// !mulrA mulVf// !mul1r => /le_trans; apply. rewrite !powRM// !mulrA -powR_inv1// -powRD ?pnatr_eq0 ?implybT//. by rewrite (addrC _ p) -mulrDr. -rewrite unlock (gt_eqF (lt_le_trans _ p1))// poweR_lty//. +rewrite unlock poweR_lty//. pose x := \int[mu]_x (2 `^ (p - 1) * (`|f x| `^ p + `|g x| `^ p))%:E. apply: (@le_lt_trans _ _ x). rewrite ge0_le_integral//=. @@ -470,7 +509,7 @@ rewrite [leRHS](_ : _ = ('N_p%:E[f] + 'N_p%:E[g]) * rewrite Lnorm1; apply: eq_integral => x _. by rewrite normrM (ger0_norm (powR_ge0 _ _)). rewrite [X in _ * X](_ : _ = 'N_(p / (p - 1))%:E[h]); last first. - rewrite unlock mulf_eq0 gt_eqF//= invr_eq0 subr_eq0 (gt_eqF p1). + rewrite unlock. rewrite onemV ?gt_eqF// invf_div; apply: congr2; last by []. apply: eq_integral => x _; congr EFin. rewrite norm_powR// normr_id -powRrM mulrCA divff ?mulr1//. @@ -484,8 +523,8 @@ rewrite [leRHS](_ : _ = ('N_p%:E[f] + 'N_p%:E[g]) * rewrite Lnorm1; apply: eq_integral => x _ . by rewrite normrM norm_powR// normr_id. rewrite [X in _ * X](_ : _ = 'N_((1 - p^-1)^-1)%:E[h])//; last first. - rewrite unlock invrK invr_eq0 subr_eq0 eq_sym invr_eq1 (gt_eqF p1). - apply: congr2; last by []. + rewrite unlock. + apply: congr2; last by rewrite invrK. apply: eq_integral => x _; congr EFin. rewrite -/(onem p^-1) onemV ?gt_eqF// norm_powR// normr_id -powRrM. by rewrite invf_div mulrCA divff ?subr_eq0 ?gt_eqF// ?mulr1. @@ -498,8 +537,34 @@ under [X in X * _]eq_integral=> x _ do rewrite mulr_powRB1 ?subr_gt0//. rewrite poweRD; last by rewrite poweRD_defE gt_eqF ?implyFb// subr_gt0 invf_lt1. rewrite poweRe1; last by apply: integral_ge0 => x _; rewrite lee_fin powR_ge0. congr (_ * _); rewrite poweRN. -- by rewrite unlock gt_eqF// fine_poweR. +- by rewrite unlock fine_poweR. - by rewrite -powR_Lnorm ?gt_eqF// fin_num_poweR// ge0_fin_numE ?Lnorm_ge0. Qed. +Lemma minkowski' f g p : + measurable_fun setT f -> measurable_fun setT g -> (1 <= p)%R -> + 'N_p%:E[f] <= 'N_p%:E[f \+ g] + 'N_p%:E[g]. +Proof. +move=> mf mg p1. +rewrite (_ : f = ((f \+ g) \+ (-%R \o g))%R); last first. + by apply: funext => x /=; rewrite -addrA subrr addr0. +rewrite [X in _ <= 'N__[X] + _](_ : ((f \+ g \- g) \+ g)%R = (f \+ g)%R); last first. + by apply: funext => x /=; rewrite -addrA [X in _ + _ + X]addrC subrr addr0. +rewrite (_ : 'N__[g] = 'N_p%:E[-%R \o g]); last first. + by rewrite oppr_Lnorm. +apply: minkowski => //. + apply: measurable_funD => //. +apply: measurableT_comp => //. +Qed. + +Lemma minkowskie (f g : T -> R) (p : \bar R) : + measurable_fun setT f -> measurable_fun setT g -> 1 <= p -> + 'N_p[(f \+ g)%R] <= 'N_p[f] + 'N_p[g]. +Proof. +case: p => //[r|]; first exact: minkowski. +move=> mf mg _; rewrite unlock /Lnorm. +case: ifPn => mugt0; last by rewrite adde0 lexx. +exact: ess_sup_normD. +Qed. + End minkowski. diff --git a/theories/lebesgue_integral.v b/theories/lebesgue_integral.v index 5105187b21..d21d39f54d 100644 --- a/theories/lebesgue_integral.v +++ b/theories/lebesgue_integral.v @@ -273,6 +273,8 @@ Lemma mfunN f : - f = \- f :> (_ -> _). Proof. by []. Qed. Lemma mfunD f g : f + g = f \+ g :> (_ -> _). Proof. by []. Qed. Lemma mfunB f g : f - g = f \- g :> (_ -> _). Proof. by []. Qed. Lemma mfunM f g : f * g = f \* g :> (_ -> _). Proof. by []. Qed. +Lemma mfunMn f n : (f *+ n) = (fun x => f x *+ n) :> (_ -> _). +Proof. by apply/funext=> x; elim: n => //= n; rewrite !mulrS !mfunD /= => ->. Qed. Lemma mfun_sum I r (P : {pred I}) (f : I -> {mfun aT >-> rT}) (x : aT) : (\sum_(i <- r | P i) f i) x = \sum_(i <- r | P i) f i x. Proof. by elim/big_rec2: _ => //= i y ? Pi <-. Qed. @@ -286,6 +288,7 @@ HB.instance Definition _ f g := MeasurableFun.copy (f \+ g) (f + g). HB.instance Definition _ f g := MeasurableFun.copy (\- f) (- f). HB.instance Definition _ f g := MeasurableFun.copy (f \- g) (f - g). HB.instance Definition _ f g := MeasurableFun.copy (f \* g) (f * g). +(* TODO: fix this: HB.instance Definition _ f (n : nat) := MeasurableFun.copy (fun x => f x *+ n) (f *+ n). *) Definition mindic (D : set aT) of measurable D : aT -> rT := \1_D. @@ -3833,11 +3836,9 @@ Local Open Scope ereal_scope. Context d (T : measurableType d) (R : realType) (mu : {measure set T -> \bar R}). -Local Notation ae_eq := (ae_eq mu). - Let ae_eq_integral_abs_bounded (D : set T) (mD : measurable D) (f : T -> \bar R) M : measurable_fun D f -> (forall x, D x -> `|f x| <= M%:E) -> - ae_eq D f (cst 0) -> \int[mu]_(x in D) `|f x|%E = 0. + (\forall x \ae mu, D x -> f x = 0) -> \int[mu]_(x in D) `|f x|%E = 0. Proof. move=> mf fM [N [mA mN0 Df0N]]. pose Df_neq0 := D `&` [set x | f x != 0]. @@ -3866,7 +3867,8 @@ by rewrite mule0 -eq_le => /eqP. Qed. Lemma ae_eq_integral_abs (D : set T) (mD : measurable D) (f : T -> \bar R) : - measurable_fun D f -> \int[mu]_(x in D) `|f x| = 0 <-> ae_eq D f (cst 0). + measurable_fun D f -> + \int[mu]_(x in D) `|f x| = 0 <-> (\forall x \ae mu, D x -> f x = 0). Proof. move=> mf; split=> [iDf0|Df0]. exists (D `&` [set x | f x != 0]); split; @@ -3920,7 +3922,7 @@ transitivity (limn (fun n => \int[mu]_(x in D) (f_ n x) )). have [ftm|ftm] := leP `|f t|%E m%:R%:E. by rewrite lexx /= (le_trans ftm)// lee_fin ler_nat. by rewrite (ltW ftm) /= lee_fin ler_nat. -have ae_eq_f_ n : ae_eq D (f_ n) (cst 0). +have ae_eq_f_ n : (f_ n) = (cst 0) %[ae mu in D]. case: Df0 => N [mN muN0 DfN]. exists N; split => // t /= /not_implyP[Dt fnt0]. apply: DfN => /=; apply/not_implyP; split => //. @@ -4029,7 +4031,7 @@ Qed. Lemma ge0_ae_eq_integral (D : set T) (f g : T -> \bar R) : measurable D -> measurable_fun D f -> measurable_fun D g -> (forall x, D x -> 0 <= f x) -> (forall x, D x -> 0 <= g x) -> - ae_eq D f g -> \int[mu]_(x in D) (f x) = \int[mu]_(x in D) (g x). + f = g %[ae mu in D] -> \int[mu]_(x in D) (f x) = \int[mu]_(x in D) (g x). Proof. move=> mD mf mg f0 g0 [N [mN N0 subN]]. rewrite integralEpatch// [RHS]integralEpatch//. @@ -4047,7 +4049,7 @@ Qed. Lemma ae_eq_integral (D : set T) (g f : T -> \bar R) : measurable D -> measurable_fun D f -> measurable_fun D g -> - ae_eq D f g -> \int[mu]_(x in D) f x = \int[mu]_(x in D) g x. + f = g %[ae mu in D] -> \int[mu]_(x in D) f x = \int[mu]_(x in D) g x. Proof. move=> mD mf mg /ae_eq_funeposneg[Dfgp Dfgn]. rewrite integralE// [in RHS]integralE//; congr (_ - _). diff --git a/theories/lspace.v b/theories/lspace.v new file mode 100644 index 0000000000..36bfcd4282 --- /dev/null +++ b/theories/lspace.v @@ -0,0 +1,449 @@ +(* mathcomp analysis (c) 2022 Inria and AIST. License: CeCILL-C. *) +From HB Require Import structures. +From mathcomp Require Import all_ssreflect. +From mathcomp Require Import ssralg ssrnum ssrint interval finmap. +From mathcomp Require Import boolp classical_sets interval_inference reals. +From mathcomp Require Import functions cardinality topology normedtype ereal. +From mathcomp Require Import sequences esum exp measure numfun lebesgue_measure. +From mathcomp Require Import lebesgue_integral hoelder ess_sup_inf. + +(******************************************************************************) +(* *) +(* LfunType mu p == type of measurable functions f such that the *) +(* integral of |f| ^ p is finite *) +(* LType mu p == type of the elements of the Lp space *) +(* mu.-Lspace p == Lp space *) +(* *) +(******************************************************************************) + +Reserved Notation "mu .-Lspace p" (at level 4, format "mu .-Lspace p"). + +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. + +Definition finite_norm d (T : measurableType d) (R : realType) + (mu : {measure set T -> \bar R}) (p : \bar R) (f : T -> R) := + ('N[ mu ]_p [ EFin \o f ] < +oo)%E. + +HB.mixin Record isLfun d (T : measurableType d) (R : realType) + (mu : {measure set T -> \bar R}) (p : \bar R) (p1 : (1 <= p)%E) (f : T -> R) + of @MeasurableFun d _ T R f := { + lfuny : finite_norm mu p f +}. + +#[short(type=LfunType)] +HB.structure Definition Lfun d (T : measurableType d) (R : realType) + (mu : {measure set T -> \bar R}) (p : \bar R) (p1 : (1 <= p)%E) := + {f of @MeasurableFun d _ T R f & isLfun d T R mu p p1 f}. + +Arguments lfuny {d} {T} {R} {mu} {p} _. +#[global] Hint Resolve lfuny : core. +#[global] Hint Extern 0 (@LfunType _ _ _ _ _) => + solve [apply: lfuny] : core. + +Section Lfun_canonical. +Context d (T : measurableType d) (R : realType). +Variables (mu : {measure set T -> \bar R}) (p : \bar R) (p1 : (1 <= p)%E). + +HB.instance Definition _ := gen_eqMixin (LfunType mu p1). +HB.instance Definition _ := gen_choiceMixin (LfunType mu p1). + +End Lfun_canonical. + +Section Lequiv. +Context d (T : measurableType d) (R : realType). +Variables (mu : {measure set T -> \bar R}) (p : \bar R) (p1 : (1 <= p)%E). + +Definition Lequiv (f g : LfunType mu p1) := `[< f = g %[ae mu] >]. + +Let Lequiv_refl : reflexive Lequiv. +Proof. +by move=> f; exact/asboolP/(filterS _ (ae_eq_refl mu setT (EFin \o f))). +Qed. + +Let Lequiv_sym : symmetric Lequiv. +Proof. +by move=> f g; apply/idP/idP => /asboolP h; apply/asboolP/ae_eq_sym. +Qed. + +Let Lequiv_trans : transitive Lequiv. +Proof. +by move=> f g h /asboolP gf /asboolP fh; apply/asboolP/(ae_eq_trans gf fh). +Qed. + +Canonical Lequiv_canonical := + EquivRel Lequiv Lequiv_refl Lequiv_sym Lequiv_trans. + +Local Open Scope quotient_scope. + +Definition LspaceType := {eq_quot Lequiv}. +Canonical LspaceType_quotType := [the quotType _ of LspaceType]. +Canonical LspaceType_eqType := [the eqType of LspaceType]. +Canonical LspaceType_choiceType := [the choiceType of LspaceType]. +Canonical LspaceType_eqQuotType := [the eqQuotType Lequiv of LspaceType]. + +Lemma LequivP (f g : LfunType mu p1) : + reflect (f = g %[ae mu]) (f == g %[mod LspaceType]). +Proof. by apply/(iffP idP); rewrite eqmodE// => /asboolP. Qed. + +Record LType := MemLType { Lfun_class : LspaceType }. +Coercion LfunType_of_LType (f : LType) : LfunType mu p1 := + repr (Lfun_class f). + +End Lequiv. + +Section Lspace. +Context d (T : measurableType d) (R : realType). +Variable mu : {measure set T -> \bar R}. + +Definition Lspace p (p1 : (1 <= p)%E) := [set: LType mu p1]. +Arguments Lspace : clear implicits. + +Lemma LType1_integrable (f : LType mu (@lexx _ _ 1%E)) : + mu.-integrable setT (EFin \o f). +Proof. +apply/integrableP; split; first exact/measurable_EFinP. +have := lfuny _ f. +rewrite /finite_norm unlock /Lnorm invr1 poweRe1; last first. + by apply integral_ge0 => x _; rewrite lee_fin powRr1. +by under eq_integral => i _ do rewrite poweRe1//. +Qed. + +Let le12 : (1 <= 2%:E :> \bar R)%E. +Proof. +rewrite lee_fin. +rewrite (ler_nat _ 1 2). +by []. +Qed. + +Lemma LType2_integrable_sqr (f : LType mu le12) : + mu.-integrable [set: T] (EFin \o (fun x => f x ^+ 2)). +Proof. +apply/integrableP; split. + apply/measurable_EFinP. + exact/(@measurableT_comp _ _ _ _ _ _ (fun x : R => x ^+ 2)%R _ f). +rewrite (@lty_poweRy _ _ 2^-1)//. +rewrite (le_lt_trans _ (lfuny _ f))//. +rewrite unlock. +rewrite gt0_ler_poweR//. +- by rewrite in_itv/= leey integral_ge0// => x _. +- rewrite in_itv/= leey integral_ge0// => x _. + by rewrite lee_fin powR_ge0. +- rewrite ge0_le_integral//. + + apply: measurableT_comp => //; apply/measurable_EFinP. + exact/(@measurableT_comp _ _ _ _ _ _ (fun x : R => x ^+ 2)%R _ f). + + by move=> x _; rewrite lee_fin powR_ge0. + + apply/measurable_EFinP. + apply/(@measurableT_comp _ _ _ _ _ _ (fun x : R => x `^ 2)%R) => //. + exact/measurableT_comp. + + by move=> t _/=; rewrite lee_fin normrX powR_mulrn. +Qed. + +End Lspace. +Notation "mu .-Lspace p" := (@Lspace _ _ _ mu p) : type_scope. + +(* TODO: move to hoelder.v *) +Section conjugate. +Context d (T : measurableType d) (R : realType). +Variables (mu : {measure set T -> \bar R}) (p : \bar R). +Hypothesis (p1 : (1 <= p)%E). + +Local Open Scope classical_set_scope. +Local Open Scope ereal_scope. + +Definition conjugate := + match p with + | r%:E => [get q : R | r^-1 + q^-1 = 1]%:E + | +oo => 1 + | -oo => 0 + end. + +Lemma conjugateE : + conjugate = if p is r%:E then (r * (r-1)^-1)%:E + else if p == +oo then 1 else 0. +Proof. +rewrite /conjugate. +case: p p1 => [r|//=|//]. +rewrite lee_fin => r1. +have r0 : r != 0%R by rewrite gt_eqF// (lt_le_trans _ r1). +congr EFin; apply: get_unique. + by rewrite invf_div mulrBl divff// mul1r addrCA subrr addr0. +move=> /= y ry1. +suff -> : y = (1 - r^-1)^-1. + by rewrite -(mul1r r^-1) -{1}(divff r0) -mulrBl invf_div. +by rewrite -ry1 -addrAC subrr add0r invrK. +Qed. + +End conjugate. + +Section lfun_pred. +Context d (T : measurableType d) (R : realType). +Variables (mu : {measure set T -> \bar R}) (p : \bar R). + +Definition finlfun : {pred _ -> _} := mem [set f | finite_norm mu p f]. +Definition lfun : {pred _ -> _} := [predI @mfun _ _ T R & finlfun]. +Definition lfun_key : pred_key lfun. Proof. exact. Qed. +Canonical lfun_keyed := KeyedPred lfun_key. +Lemma sub_lfun_mfun : {subset lfun <= mfun}. Proof. by move=> x /andP[]. Qed. +Lemma sub_lfun_finlfun : {subset lfun <= finlfun}. Proof. by move=> x /andP[]. Qed. +End lfun_pred. + +Section lfun. +Context d (T : measurableType d) (R : realType). +Variables (mu : {measure set T -> \bar R}) (p : \bar R) (p1 : (1 <= p)%E). + +Notation lfun := (@lfun _ T R mu p). +Section Sub. +Context (f : T -> R) (fP : f \in lfun). +Definition lfun_Sub1_subproof := + @isMeasurableFun.Build d _ T R f (set_mem (sub_lfun_mfun fP)). +#[local] HB.instance Definition _ := lfun_Sub1_subproof. +Definition lfun_Sub2_subproof := + @isLfun.Build d T R mu p p1 f (set_mem (sub_lfun_finlfun fP)). + +Import HBSimple. + +#[local] HB.instance Definition _ := lfun_Sub2_subproof. +Definition lfun_Sub : LfunType mu p1 := f. +End Sub. + +Lemma lfun_rect (K : LfunType mu p1 -> Type) : + (forall f (Pf : f \in lfun), K (lfun_Sub Pf)) -> forall u, K u. +Proof. +move=> Ksub [f [[Pf1] [Pf2]]]. +have Pf : f \in lfun by apply/andP; rewrite ?inE. +have -> : Pf1 = set_mem (sub_lfun_mfun Pf) by []. +have -> : Pf2 = set_mem (sub_lfun_finlfun Pf) by []. +exact: Ksub. +Qed. + +Lemma lfun_valP f (Pf : f \in lfun) : lfun_Sub Pf = f :> (_ -> _). +Proof. by []. Qed. + +HB.instance Definition _ := isSub.Build _ _ (LfunType mu p1) lfun_rect lfun_valP. + +Lemma lfuneqP (f g : LfunType mu p1) : f = g <-> f =1 g. +Proof. by split=> [->//|fg]; apply/val_inj/funext. Qed. + +HB.instance Definition _ := [Choice of LfunType mu p1 by <:]. + +Import numFieldNormedType.Exports. + +Lemma lfuny0 : finite_norm mu p (cst 0). +Proof. by rewrite /finite_norm Lnorm0// ltry. Qed. + +HB.instance Definition _ := @isLfun.Build d T R mu p p1 (cst 0) lfuny0. + +Lemma mfunP (f : {mfun T >-> R}) : (f : T -> R) \in mfun. +Proof. exact: valP. Qed. + +Lemma lfunP (f : LfunType mu p1) : (f : T -> R) \in lfun. +Proof. exact: valP. Qed. + +Lemma mfun_scaler_closed : scaler_closed (@mfun _ _ T R). +Proof. move=> a/= f; rewrite !inE; exact: measurable_funM. Qed. + +HB.instance Definition _ := GRing.isScaleClosed.Build _ _ (@mfun _ _ T R) + mfun_scaler_closed. +HB.instance Definition _ := [SubZmodule_isSubLmodule of {mfun T >-> R} by <:]. + +Lemma LnormZ (f : LfunType mu p1) a : + ('N[mu]_p[EFin \o (a \*: f)] = `|a|%:E * 'N[mu]_p[EFin \o f])%E. +Proof. +rewrite unlock /Lnorm. +case: p p1 f => //[r r1 f|]. +- under eq_integral => x _/= do rewrite -mulr_algl scaler1 normrM powRM ?EFinM//. + rewrite integralZl//; last first. + apply /integrableP; split. + apply: measurableT_comp => //. + apply: (@measurableT_comp _ _ _ _ _ _ (@powR R ^~ r)) => //. + exact: measurableT_comp. + apply: (@lty_poweRy _ _ r^-1). + by rewrite gt_eqF// invr_gt0 ?(lt_le_trans ltr01). + have -> : ((\int[mu]_x `|(`|f x| `^ r)%:E|) `^ r^-1 = 'N[mu]_r%:E[EFin \o f])%E. + rewrite unlock /Lnorm. + by under eq_integral => x _ do rewrite gee0_abs ?lee_fin ?powR_ge0//. + exact: (lfuny r1 f). + rewrite poweRM ?integral_ge0=> //[||x _]; rewrite ?lee_fin ?powR_ge0//. + by rewrite poweR_EFin -powRrM mulfV ?gt_eqF ?(lt_le_trans ltr01)// powRr1. +- move=> p0 f; case: ifP => mu0; last by rewrite mule0. + rewrite -ess_supZl//; apply/eq_ess_sup/nearW => x /=. + by rewrite normrZ EFinM. +Qed. + +Lemma lfun_submod_closed : submod_closed (lfun). +Proof. +split. + rewrite -[0]/(cst 0). exact: lfunP. +move=> a/= f g fP gP. +rewrite -[f]lfun_valP -[g]lfun_valP. +move: (lfun_Sub _) (lfun_Sub _) => {fP} f {gP} g. +rewrite !inE rpredD ?rpredZ ?mfunP//=. +apply: mem_set => /=. +rewrite /finite_norm. +apply: le_lt_trans. + apply: minkowskie => //. + suff: a *: (g : T -> R) \in mfun by exact: set_mem. + by rewrite rpredZ//; exact: mfunP. +rewrite lte_add_pinfty//; last exact: lfuny. +rewrite LnormZ lte_mul_pinfty// ?lee_fin//. +exact: lfuny. +Qed. + +HB.instance Definition _ := GRing.isSubmodClosed.Build _ _ lfun + lfun_submod_closed. +HB.instance Definition _ := [SubChoice_isSubLmodule of LfunType mu p1 by <:]. + +End lfun. + +Section Lspace_norm. +Context d (T : measurableType d) (R : realType). +Variable mu : {measure set T -> \bar R}. +Variable (p : \bar R) (p1 : (1 <= p)%E). + +(* 0 - + should come with proofs that they are in LfunType mu p *) + +Notation ty := (LfunType mu p1). +Definition nm f := fine ('N[mu]_p[EFin \o f]). + +Lemma finite_norm_fine (f : ty) : (nm f)%:E = 'N[mu]_p[EFin \o f]. +Proof. +rewrite /nm fineK// fin_numElt (lt_le_trans ltNy0) ?Lnorm_ge0//=. +exact: lfuny. +Qed. + +Lemma ler_Lnorm_add (f g : ty) : + nm (f + g) <= nm f + nm g. +Proof. by rewrite -lee_fin EFinD !finite_norm_fine minkowskie. Qed. + +Lemma natmulfctE (U : pointedType) (K : ringType) (f : U -> K) n : + f *+ n = (fun x => f x *+ n). +Proof. by elim: n => [//|n h]; rewrite funeqE=> ?; rewrite !mulrSr h. Qed. + +Lemma LnormN (f : ty) : nm (\-f) = nm f. +Proof. by rewrite /nm oppr_Lnorm. Qed. + +Lemma enatmul_ninfty (n : nat) : + (-oo *+ n.+1 = -oo :> \bar R)%E \/ (-oo *+ n.+1 = +oo :> \bar R)%E. +Proof. by elim: n => //=[|n []->]; rewrite ?addNye; left. Qed. + +Lemma Lnorm_natmul (f : ty) k : nm (f *+ k) = nm f *+ k. +Proof. +apply/EFin_inj; rewrite finite_norm_fine -scaler_nat LnormZ normr_nat. +by rewrite -[in RHS]mulr_natl EFinM finite_norm_fine. +Qed. + +(* TODO : fix the definition *) +(* waiting for MathComp 2.4.0 +HB.instance Definition _ := + @Num.Zmodule_isSemiNormed.Build R (LfunType mu p1) + nm ler_Lnorm_add Lnorm_natmul LnormN. +*) + +(* TODO: add equivalent of mx_normZ and HB instance *) + +Lemma nm_eq0 (f : ty) : nm f = 0 -> f = 0 %[ae mu]. +Proof. +rewrite /nm=> /eqP; rewrite -eqe=> /eqP; rewrite finite_norm_fine=> /Lnorm_eq0_eq0. +by apply; rewrite ?(lt_le_trans _ p1). +Qed. + +End Lspace_norm. + +Section Lspace_inclusion. +Context d (T : measurableType d) (R : realType). +Variable mu : {measure set T -> \bar R}. + +(* the following lemma is not needed, but looks useful, should we include it anyways? *) +Lemma mul_lte_pinfty (x y : \bar R) : + (x \is a fin_num -> 0 < x -> x * y < +oo -> y < +oo)%E. +Proof. +rewrite fin_numE => /andP[/eqP xNoo /eqP xoo]. +move: x xNoo xoo. +case => // r _ _; rewrite lte_fin => r0. +rewrite /mule. +case: y => //[s|]. + by rewrite !ltry. +by rewrite eqe gt_eqF// lte_fin r0. +Qed. + +Local Open Scope ereal_scope. + +Lemma Lspace_inclusion (p q : \bar R) : + forall (p1 : 1 <= p) (q1 : 1 <= q), + mu [set: T] < +oo -> p < q -> + forall f : {mfun T >-> R}, finite_norm mu q f -> finite_norm mu p f. +Proof. +have := measure_ge0 mu [set: T]. +rewrite le_eqVlt => /predU1P[mu0 p1 q1 _ _ f _|mu_pos]. + rewrite /finite_norm unlock /Lnorm. + move: p p1; case=> //; last by rewrite -mu0 ltxx ltry. + move=> r r1. + under eq_integral do rewrite /= -[(_ `^ _)%R]ger0_norm ?powR_ge0//=. + rewrite (@integral_abs_eq0 _ _ _ _ setT setT (fun x => (`|f x| `^ r)%:E))//. + by rewrite poweR0r// invr_neq0// gt_eqF// -lte_fin (lt_le_trans _ r1). + apply/measurable_EFinP. + apply: (@measurableT_comp _ _ _ _ _ _ (@powR R ^~ r)) => //. + exact: measurableT_comp. +move: p q. +case=> //[p|]; case=> //[q|] p1 q1; last first. + have p0 : (0 < p)%R by rewrite ?(lt_le_trans ltr01). + move=> muoo _ f. + rewrite /finite_norm unlock /Lnorm mu_pos => supf_lty. + rewrite poweR_lty//; move: supf_lty => /ess_supr_bounded[M fM]. + rewrite (@le_lt_trans _ _ (\int[mu]_x (M `^ p)%:E)); [by []| |]; last first. + by rewrite integral_cst// lte_mul_pinfty// lee_fin powR_ge0. + apply: ae_ge0_le_integral => //. + - by move=> x _; rewrite lee_fin powR_ge0. + apply/measurable_EFinP. + apply: (@measurableT_comp _ _ _ _ _ _ (@powR R ^~ p)) => //. + exact: measurableT_comp. + - by move=> x _; rewrite lee_fin powR_ge0. + apply: filterS fM => t/= ftM _. + rewrite lee_fin ge0_ler_powR//; first exact: ltW. + by rewrite nnegrE (le_trans _ ftM). +move=> mu_fin pleq f ffin. +have:= ffin; rewrite /finite_norm. +have p0 : (0 < p)%R by rewrite ?(lt_le_trans ltr01). +have pN0 : p != 0%R by rewrite gt_eqF. +have q0 : (0 < q)%R by rewrite ?(lt_le_trans ltr01). +have qinv0 : q^-1 != 0%R by rewrite invr_neq0// gt_eqF. +pose r := q/p. +pose r' := (1 - r^-1)^-1. +have := (@hoelder _ _ _ mu (fun x => `|f x| `^ p) (cst 1)%R r r')%R. +rewrite (_ : (_ \* cst 1)%R = (fun x : T => `|f x| `^ p))%R -?fctM ?mulr1//. +rewrite Lnorm_cst1 unlock /Lnorm invr1. +have mfp : measurable_fun [set: T] (fun x : T => (`|f x| `^ p)%R). + apply: (@measurableT_comp _ _ _ _ _ _ (@powR R ^~ p)) => //. + exact: measurableT_comp. +have m1 : measurable_fun [set: T] (@cst _ R 1%R). + exact: measurable_cst. +have r0 : (0 < r)%R by rewrite/r divr_gt0. +have r'0 : (0 < r')%R. + by rewrite /r' invr_gt0 subr_gt0 invf_lt1 ?(lt_trans ltr01)//; + rewrite /r ltr_pdivlMr// mul1r. +have rr'1 : r^-1 + r'^-1 = 1%R. + by rewrite /r' /r invf_div invrK addrCA subrr addr0. +move=> /(_ mfp m1 r0 r'0 rr'1). +under [in leLHS] eq_integral do rewrite /= powRr1// norm_powR// normrE. +under [in leRHS] eq_integral do + rewrite /= norm_powR// normr_id -powRrM mulrCA divff// mulr1. +rewrite [X in X <= _]poweRe1; last + by apply: integral_ge0 => x _; rewrite lee_fin powR_ge0. +move=> h1 /lty_poweRy h2. +apply: poweR_lty. +apply: (le_lt_trans h1). +rewrite muleC lte_mul_pinfty ?fin_numElt?poweR_ge0//. + by rewrite (lt_le_trans _ (poweR_ge0 _ _)) ?ltNyr// ?poweR_lty. +rewrite poweR_lty// (lty_poweRy qinv0)//. +by have:= ffin; rewrite /finite_norm unlock /Lnorm. +Qed. + +End Lspace_inclusion. diff --git a/theories/measurable_realfun.v b/theories/measurable_realfun.v index a36e041a9b..e088d6a5b9 100644 --- a/theories/measurable_realfun.v +++ b/theories/measurable_realfun.v @@ -1564,6 +1564,50 @@ Notation emeasurable_fun_funeneg := measurable_funeneg (only parsing). #[deprecated(since="mathcomp-analysis 0.6.6", note="renamed `measurable_fun_limn_esup`")] Notation measurable_fun_lim_esup := measurable_fun_limn_esup (only parsing). +Section ereal_inf_sup_seq. +Context {R : realType}. +Implicit Types (S : set (\bar R)). +Local Open Scope ereal_scope. + +Lemma ereal_inf_seq S : S != set0 -> + {u : nat -> \bar R | forall i, S (u i) & u @ \oo --> ereal_inf S}. +Proof. +move=> SN0; apply/cid2; have [|Ninfy] := eqVneq (ereal_inf S) +oo. + move=> /[dup]/ereal_inf_pinfty/subset_set1/orW[/eqP/negPn/[!SN0]//|->] ->. + by exists (fun=> +oo) => //; apply: cvg_cst. +suff: exists2 v : (\bar R)^nat, v @ \oo --> ereal_inf S & + forall n, exists2 x : \bar R, x \in S & x < v n. + move=> [v vcvg] /(_ _)/sig2W-/all_sig/= [u /all_and2[/(_ _)/set_mem Su u_lt]]. + exists u => //; move: vcvg. + have: cst (ereal_inf S) @ \oo --> ereal_inf S by exact: cvg_cst. + apply: squeeze_cvge; apply: nearW => n; rewrite /cst/=. + by rewrite ereal_inf_le /= 1?ltW; last by exists (u n). +have [infNy|NinfNy] := eqVneq (ereal_inf S) -oo. + exists [sequence - (n%:R%:E)]_n => /=; last first. + by move=> n; setoid_rewrite set_mem_set; apply: lb_ereal_infNy_adherent. + rewrite infNy; apply/cvgNey; under eq_cvg do rewrite EFinN oppeK. + by apply/cvgeryP/cvgr_idn. +have inf_fin : ereal_inf S \is a fin_num by case: ereal_inf Ninfy NinfNy. +exists [sequence ereal_inf S + n.+1%:R^-1%:E]_n => /=; last first. + by move=> n; setoid_rewrite set_mem_set; apply: lb_ereal_inf_adherent. + apply/sube_cvg0 => //=; apply/cvg_abse0P. + rewrite (@eq_cvg _ _ _ _ (fun n => n.+1%:R^-1%:E)). + exact: cvge_harmonic. +by move=> n /=; rewrite /= addrAC subee// add0e gee0_abs//. +Unshelve. all: by end_near. Qed. + +Lemma ereal_sup_seq S : S != set0 -> + {u : nat -> \bar R | forall i, S (u i) & u @ \oo --> ereal_sup S}. +Proof. +move=> SN0; have NSN0 : [set - x | x in S] != set0. + by have /set0P[x Sx] := SN0; apply/set0P; exists (- x), x. +have [u /= Nxu] := ereal_inf_seq NSN0. +rewrite ereal_infN => /cvgeN; rewrite oppeK => Nu_to_sup. +by exists (fun n => - u n) => // i; have [? ? <-] := Nxu i; rewrite oppeK. +Qed. + +End ereal_inf_sup_seq. + Section open_itv_cover. Context {R : realType}. Implicit Types (A : set R). @@ -1575,7 +1619,7 @@ Lemma outer_measure_open_itv_cover A : (l^* A)%mu = ereal_inf [set \sum_(k _ /= [F [Fitv AF <-]]. + apply: le_ereal_inf => _ /= [F [Fitv AF <-]]. exists (fun i => `](sval (cid (Fitv i))).1, (sval (cid (Fitv i))).2]%classic). + split=> [i|]. * have [?|?] := ltP (sval (cid (Fitv i))).1 (sval (cid (Fitv i))).2. @@ -1587,56 +1631,113 @@ apply/eqP; rewrite eq_le; apply/andP; split. + apply: eq_eseriesr => k _; rewrite /l wlength_itv/=. case: (Fitv k) => /= -[a b]/= Fkab. by case: cid => /= -[x1 x2] ->; rewrite wlength_itv. -- have [/lb_ereal_inf_adherent lA|] := - boolP ((l^* A)%mu \is a fin_num); last first. - rewrite ge0_fin_numE ?outer_measure_ge0// -leNgt leye_eq => /eqP ->. - exact: leey. - apply/lee_addgt0Pr => /= e e0. - have : (0 < e / 2)%R by rewrite divr_gt0. - move=> /lA[_ [/= F [mF AF]] <-]; rewrite -/((l^* A)%mu) => lFe. - have Fcover n : exists2 B, F n `<=` B & - is_open_itv B /\ l B <= l (F n) + (e / 2 ^+ n.+2)%:E. - have [[a b] _ /= abFn] := mF n. - exists `]a, b + e / 2^+n.+2[%classic. - rewrite -abFn => x/= /[!in_itv] /andP[->/=] /le_lt_trans; apply. - by rewrite ltrDl divr_gt0. - split; first by exists (a, b + e / 2^+n.+2). - have [ab|ba] := ltP a b. - rewrite /l -abFn !wlength_itv//= !lte_fin ifT. - by rewrite ab -!EFinD lee_fin addrAC. - by rewrite ltr_wpDr// divr_ge0// ltW. - rewrite -abFn [in leRHS]set_itv_ge ?bnd_simp -?leNgt// /l wlength0 add0r. - rewrite wlength_itv//=; case: ifPn => [abe|_]; last first. - by rewrite lee_fin divr_ge0// ltW. - by rewrite -EFinD addrAC lee_fin -[leRHS]add0r lerD2r subr_le0. - pose G := fun n => sval (cid2 (Fcover n)). - have FG n : F n `<=` G n by rewrite /G; case: cid2. - have Gitv n : is_open_itv (G n) by rewrite /G; case: cid2 => ? ? []. - have lGFe n : l (G n) <= l (F n) + (e / 2 ^+ n.+2)%:E. - by rewrite /G; case: cid2 => ? ? []. - have AG : A `<=` \bigcup_k G k. - by apply: (subset_trans AF) => [/= r [n _ /FG Gnr]]; exists n. - apply: (@le_trans _ _ (\sum_(0 <= k /=; exists G. - exact: lee_nneseries. - rewrite nneseriesD//; last first. - by move=> i _; rewrite lee_fin// divr_ge0// ltW. - rewrite [in leRHS](splitr e) EFinD addeA leeD//; first exact/ltW. - have := @cvg_geometric_eseries_half R e 1; rewrite expr1. - rewrite [X in eseries X](_ : _ = (fun k => (e / (2 ^+ (k.+2))%:R)%:E)); last first. - by apply/funext => n; rewrite addn2 natrX. - move/cvg_lim => <-//; apply: lee_nneseries => //. - - by move=> n _; rewrite lee_fin divr_ge0// ltW. - - by move=> n _; rewrite lee_fin -natrX. +have [/lb_ereal_inf_adherent lA|] := + boolP ((l^* A)%mu \is a fin_num); last first. + rewrite ge0_fin_numE ?outer_measure_ge0// -leNgt leye_eq => /eqP ->. + exact: leey. +apply/lee_addgt0Pr => /= e e0. +have : (0 < e / 2)%R by rewrite divr_gt0. +move=> /lA[_ [/= F [mF AF]] <-]; rewrite -/((l^* A)%mu) => lFe. +have Fcover n : exists2 B, F n `<=` B & + is_open_itv B /\ l B <= l (F n) + (e / 2 ^+ n.+2)%:E. + have [[a b] _ /= abFn] := mF n. + exists `]a, b + e / 2^+n.+2[%classic. + rewrite -abFn => x/= /[!in_itv] /andP[->/=] /le_lt_trans; apply. + by rewrite ltrDl divr_gt0. + split; first by exists (a, b + e / 2^+n.+2). + have [ab|ba] := ltP a b. + rewrite /l -abFn !wlength_itv//= !lte_fin ifT. + by rewrite ab -!EFinD lee_fin addrAC. + by rewrite ltr_wpDr// divr_ge0// ltW. + rewrite -abFn [in leRHS]set_itv_ge ?bnd_simp -?leNgt// /l wlength0 add0r. + rewrite wlength_itv//=; case: ifPn => [abe|_]; last first. + by rewrite lee_fin divr_ge0// ltW. + by rewrite -EFinD addrAC lee_fin -[leRHS]add0r lerD2r subr_le0. +pose G := fun n => sval (cid2 (Fcover n)). +have FG n : F n `<=` G n by rewrite /G; case: cid2. +have Gitv n : is_open_itv (G n) by rewrite /G; case: cid2 => ? ? []. +have lGFe n : l (G n) <= l (F n) + (e / 2 ^+ n.+2)%:E. + by rewrite /G; case: cid2 => ? ? []. +have AG : A `<=` \bigcup_k G k. + by apply: (subset_trans AF) => [/= r [n _ /FG Gnr]]; exists n. +apply: (@le_trans _ _ (\sum_(0 <= k /=; exists G. + exact: lee_nneseries. +rewrite nneseriesD//; last first. + by move=> i _; rewrite lee_fin// divr_ge0// ltW. +rewrite [in leRHS](splitr e) EFinD addeA leeD//; first exact/ltW. +have := @cvg_geometric_eseries_half R e 1; rewrite expr1. +rewrite [X in eseries X](_ : _ = (fun k => (e / (2 ^+ (k.+2))%:R)%:E)); last first. + by apply/funext => n; rewrite addn2 natrX. +move/cvg_lim => <-//; apply: lee_nneseries => //. +- by move=> n _; rewrite lee_fin divr_ge0// ltW. +- by move=> n _; rewrite lee_fin -natrX. Qed. End open_itv_cover. + +Section ereal_supZ. +Context {R : realType}. +Implicit Types (r s : R) (A : set R) (X : set (\bar R)). +Local Open Scope ereal_scope. + +Lemma set_cst I T (x : T) (A : set I) : + [set x | _ in A] = if A == set0 then set0 else [set x]. +Proof. +apply/seteqP; split=> y /=. + by case=> i Ai ->; case: ifP => //= /eqP A0; rewrite A0 in Ai. +by case: ifPn => //= /set0P[i Ai ->]; exists i. +Qed. + +Lemma ereal_sup_cst T x (A : set T) : A != set0 -> + ereal_sup [set x | _ in A] = x :> \bar R. +Proof. by move=> AN0; rewrite set_cst ifN// ereal_sup1. Qed. + +Lemma ereal_inf_cst T x (A : set T) : A != set0 -> + ereal_inf [set x | _ in A] = x :> \bar R. +Proof. by move=> AN0; rewrite set_cst ifN// ereal_inf1. Qed. + +Lemma ereal_sup_pZl X r : (0 < r)%R -> + ereal_sup [set r%:E * x | x in X] = r%:E * ereal_sup X. +Proof. +move=> /[dup] r_gt0; rewrite lt0r => /andP[r_neq0 r_ge0]. + gen have gen : r r_gt0 {r_ge0 r_neq0} X / + ereal_sup [set r%:E * x | x in X] <= r%:E * ereal_sup X. + apply/ereal_supP => y/= [x Ax <-]; rewrite lee_pmul2l//=. + by apply/ereal_supP => //=; exists x. +apply/eqP; rewrite eq_le gen//= -lee_pdivlMl//. +rewrite (le_trans _ (gen _ _ _)) ?invr_gt0 ?image_comp//=. +by under eq_imagel do rewrite /= muleA -EFinM mulVf ?mul1e//=; rewrite image_id. +Qed. + +Lemma ereal_supZl X r : X != set0 -> (0 <= r)%R -> + ereal_sup [set r%:E * x | x in X] = r%:E * ereal_sup X. +Proof. +move=> AN0; have [r_gt0|//|<-] := ltgtP => _; first by rewrite ereal_sup_pZl. +by rewrite mul0e; under eq_imagel do rewrite mul0e/=; rewrite ereal_sup_cst. +Qed. + +Lemma ereal_inf_pZl X r : (0 < r)%R -> + ereal_inf [set r%:E * x | x in X] = r%:E * ereal_inf X. +Proof. +move=> r_gt0; rewrite !ereal_infEN muleN image_comp/=; congr (- _). +by under eq_imagel do rewrite /= -muleN; rewrite -image_comp ereal_sup_pZl. +Qed. + +Lemma ereal_infZl X r : X != set0 -> (0 < r)%R -> + ereal_sup [set r%:E * x | x in X] = r%:E * ereal_sup X. +Proof. +move=> XN0 r_gt0; rewrite !ereal_supEN muleN image_comp/=; congr (- _). +by under eq_imagel do rewrite /= -muleN; rewrite -image_comp ereal_inf_pZl. +Qed. + +End ereal_supZ. + Section egorov. Context d {R : realType} {T : measurableType d}. Context (mu : {measure set T -> \bar R}). - Local Open Scope ereal_scope. (*TODO : this generalizes to any metric space with a borel measure*) diff --git a/theories/measure.v b/theories/measure.v index 06338ce393..0b078e6b2b 100644 --- a/theories/measure.v +++ b/theories/measure.v @@ -272,8 +272,6 @@ From HB Require Import structures. (* ## More measure-theoretic definitions *) (* ``` *) (* m1 `<< m2 == m1 is absolutely continuous w.r.t. m2 or m2 dominates m1 *) -(* ess_sup f == essential supremum of the function f : T -> R where T is a *) -(* semiRingOfSetsType and R is a realType *) (* ``` *) (* *) (******************************************************************************) @@ -1305,6 +1303,10 @@ move=> A B mA mB; case: (semi_measurableD A B) => // [D [Dfin Dl -> _]]. by apply: fin_bigcup_measurable. Qed. +Lemma seqDU_measurable (F : sequence (set T)) : + (forall n, measurable (F n)) -> forall n, measurable (seqDU F n). +Proof. by move=> Fmeas n; apply/measurableD/bigsetU_measurable. Qed. + End ringofsets_lemmas. Section algebraofsets_lemmas. @@ -1978,6 +1980,10 @@ have /[!big_ord0] ->// := @measure_semi_additive _ _ _ mu (fun=> set0) 0%N. exact: trivIset_set0. Qed. +Lemma measure_gt0 x : (0%R < mu x) = (mu x != 0). +Proof. by rewrite lt_def measure_ge0 andbT. Qed. + + Hint Resolve measure0 : core. Hint Resolve measure_ge0 : core. @@ -4064,7 +4070,8 @@ Qed. Section ae. Definition almost_everywhere d (T : semiRingOfSetsType d) (R : realFieldType) - (mu : set T -> \bar R) (P : T -> Prop) := mu.-negligible (~` [set x | P x]). + (mu : set T -> \bar R) : set_system T := + fun P => mu.-negligible (~` [set x | P x]). Let almost_everywhereT d (T : semiRingOfSetsType d) (R : realFieldType) (mu : {content set T -> \bar R}) : almost_everywhere mu setT. @@ -4083,16 +4090,14 @@ Proof. by rewrite /almost_everywhere => mA mB; rewrite setCI; exact: negligibleU. Qed. -#[global] -Instance ae_filter_ringOfSetsType d {T : ringOfSetsType d} (R : realFieldType) +Definition ae_filter_ringOfSetsType d {T : ringOfSetsType d} (R : realFieldType) (mu : {measure set T -> \bar R}) : Filter (almost_everywhere mu). Proof. by split; [exact: almost_everywhereT|exact: almost_everywhereI| exact: almost_everywhereS]. Qed. -#[global] -Instance ae_properfilter_algebraOfSetsType d {T : algebraOfSetsType d} +Definition ae_properfilter_algebraOfSetsType d {T : algebraOfSetsType d} (R : realFieldType) (mu : {measure set T -> \bar R}) : mu [set: T] > 0 -> ProperFilter (almost_everywhere mu). Proof. @@ -4105,83 +4110,146 @@ End ae. #[global] Hint Extern 0 (Filter (almost_everywhere _)) => (apply: ae_filter_ringOfSetsType) : typeclass_instances. +#[global] Hint Extern 0 (Filter (nbhs (almost_everywhere _))) => + (apply: ae_filter_ringOfSetsType) : typeclass_instances. #[global] Hint Extern 0 (ProperFilter (almost_everywhere _)) => (apply: ae_properfilter_algebraOfSetsType) : typeclass_instances. +#[global] Hint Extern 0 (ProperFilter (nbhs (almost_everywhere _))) => + (apply: ae_properfilter_algebraOfSetsType) : typeclass_instances. -Definition almost_everywhere_notation d (T : semiRingOfSetsType d) - (R : realFieldType) (mu : set T -> \bar R) (P : T -> Prop) - & (phantom Prop (forall x, P x)) := almost_everywhere mu P. -Notation "{ 'ae' m , P }" := - (almost_everywhere_notation m (inPhantom P)) : type_scope. - -Lemma aeW {d} {T : semiRingOfSetsType d} {R : realFieldType} +Notation "{ 'ae' m , P }" := {near almost_everywhere m, P} : type_scope. +Notation "\forall x \ae mu , P" := (\forall x \near almost_everywhere mu, P) + (format "\forall x \ae mu , P", + x name, P at level 200, at level 200): type_scope. +Definition ae_eq d (T : semiRingOfSetsType d) (R : realType) (mu : {measure set T -> \bar R}) + (V : T -> Type) D (f g : forall x, V x) := (\forall x \ae mu, D x -> f x = g x). +Notation "f = g %[ae mu 'in' D ]" := (\forall x \ae mu, D x -> f x = g x) + (format "f = g '%[ae' mu 'in' D ]", g at next level, D at level 200, at level 70). +Notation "f = g %[ae mu ]" := (f = g %[ae mu in setT ]) + (format "f = g '%[ae' mu ]", g at next level, at level 70). + +Lemma aeW {d} {T : ringOfSetsType d} {R : realFieldType} (mu : {measure set _ -> \bar R}) (P : T -> Prop) : - (forall x, P x) -> {ae mu, forall x, P x}. + (forall x, P x) -> \forall x \ae mu, P x. Proof. move=> aP; have -> : P = setT by rewrite predeqE => t; split. by apply/negligibleP; [rewrite setCT|rewrite setCT measure0]. Qed. +Require Import -(notations) Setoid. + +Declare Scope signature_scope. +Delimit Scope signature_scope with signature. +Import -(notations) Morphisms. +Module ProperNotations. + + Notation " R ++> R' " := (@respectful _ _ (R%signature) (R'%signature)) + (right associativity, at level 55) : signature_scope. + + Notation " R ==> R' " := (@respectful _ _ (R%signature) (R'%signature)) + (right associativity, at level 55) : signature_scope. + + Notation " R ~~> R' " := (@respectful _ _ (Program.Basics.flip (R%signature)) (R'%signature)) + (right associativity, at level 55) : signature_scope. + +End ProperNotations. +Import ProperNotations. + +Arguments Proper {A}%_type R%_signature m. +Arguments respectful {A B}%_type (R R')%_signature _ _. + +Instance ae_eq_equiv d (T : ringOfSetsType d) R mu V D: Equivalence (@ae_eq d T R mu V D). +Proof. +split. +- by move=> f; near=> x. +- by move=> f g eqfg; near=> x => Dx; rewrite (near eqfg). +- by move=> f g h eqfg eqgh; near=> x => Dx; rewrite (near eqfg) ?(near eqgh). +Unshelve. all: by end_near. Qed. + Section ae_eq. -Local Open Scope ereal_scope. +Local Open Scope ring_scope. Context d (T : sigmaRingType d) (R : realType). +Implicit Types (U V : Type) (W : ringType). Variables (mu : {measure set T -> \bar R}) (D : set T). -Implicit Types f g h i : T -> \bar R. +Local Notation ae_eq := (ae_eq mu D). -Definition ae_eq f g := {ae mu, forall x, D x -> f x = g x}. - -Lemma ae_eq0 f g : measurable D -> mu D = 0 -> ae_eq f g. +Lemma ae_eq0 U (f g : T -> U) : measurable D -> mu D = 0 -> f = g %[ae mu in D]. Proof. by move=> mD D0; exists D; split => // t/= /not_implyP[]. Qed. -Lemma ae_eq_comp (j : \bar R -> \bar R) f g : +Instance comp_ae_eq U V (j : T -> U -> V) : Proper (ae_eq ==> ae_eq) (fun f x => j x (f x)). +Proof. by move=> f g; apply: filterS => x /[apply] /= ->. Qed. + +Instance comp_ae_eq2 U U' V (j : T -> U -> U' -> V) : Proper (ae_eq ==> ae_eq ==> ae_eq) (fun f g x => j x (f x) (g x)). +Proof. by move=> f f' + g g'; apply: filterS2 => x + + Dx => -> // ->. Qed. + +Instance comp_ae_eq2' U U' V (j : U -> U' -> V) : Proper (ae_eq ==> ae_eq ==> ae_eq) (fun f g x => j (f x) (g x)). +Proof. by move=> f f' + g g'; apply: filterS2 => x + + Dx => -> // ->. Qed. + +Instance sub_ae_eq2 : Proper (ae_eq ==> ae_eq ==> ae_eq) (@GRing.sub_fun T R). +Proof. exact: (@comp_ae_eq2' _ _ R (fun x y => x - y)). Qed. + +Lemma ae_eq_refl U (f : T -> U) : ae_eq f f. Proof. exact/aeW. Qed. +Hint Resolve ae_eq_refl : core. + +Lemma ae_eq_comp U V (j : U -> V) f g : ae_eq f g -> ae_eq (j \o f) (j \o g). -Proof. by apply: filterS => x /[apply] /= ->. Qed. +Proof. by move->. Qed. -Lemma ae_eq_funeposneg f g : ae_eq f g <-> ae_eq f^\+ g^\+ /\ ae_eq f^\- g^\-. -Proof. -split=> [fg|[]]. - split; apply: filterS fg => x /[apply]. - by rewrite !funeposE => ->. - by rewrite !funenegE => ->. -apply: filterS2 => x + + Dx => /(_ Dx) fg /(_ Dx) gf. -by rewrite (funeposneg f) (funeposneg g) fg gf. -Qed. +Lemma ae_eq_comp2 U V (j : T -> U -> V) f g : + ae_eq f g -> ae_eq (fun x => j x (f x)) (fun x => j x (g x)). +Proof. by apply: filterS => x /[swap] + ->. Qed. -Lemma ae_eq_refl f : ae_eq f f. Proof. exact/aeW. Qed. +Lemma ae_eq_funeposneg (f g : T -> \bar R) : + ae_eq f g <-> ae_eq f^\+ g^\+ /\ ae_eq f^\- g^\-. +Proof. +split=> [fg|[pfg nfg]]. + by split; near=> x => Dx; rewrite !(funeposE,funenegE) (near fg). +by near=> x => Dx; rewrite (funeposneg f) (funeposneg g) ?(near pfg, near nfg). +Unshelve. all: by end_near. Qed. -Lemma ae_eq_sym f g : ae_eq f g -> ae_eq g f. -Proof. by apply: filterS => x + Dx => /(_ Dx). Qed. +Lemma ae_eq_sym U (f g : T -> U) : ae_eq f g -> ae_eq g f. +Proof. by symmetry. Qed. -Lemma ae_eq_trans f g h : ae_eq f g -> ae_eq g h -> ae_eq f h. -Proof. by apply: filterS2 => x + + Dx => /(_ Dx) ->; exact. Qed. +Lemma ae_eq_trans U (f g h : T -> U) : ae_eq f g -> ae_eq g h -> ae_eq f h. +Proof. by apply transitivity. Qed. -Lemma ae_eq_sub f g h i : ae_eq f g -> ae_eq h i -> ae_eq (f \- h) (g \- i). -Proof. by apply: filterS2 => x + + Dx => /(_ Dx) -> /(_ Dx) ->. Qed. +Lemma ae_eq_sub W (f g h i : T -> W) : ae_eq f g -> ae_eq h i -> ae_eq (f \- h) (g \- i). +Proof. by apply: filterS2 => x + + Dx => /= /(_ Dx) -> /(_ Dx) ->. Qed. -Lemma ae_eq_mul2r f g h : ae_eq f g -> ae_eq (f \* h) (g \* h). -Proof. by apply: filterS => x /[apply] ->. Qed. +Lemma ae_eq_mul2r W (f g h : T -> W) : ae_eq f g -> ae_eq (f \* h) (g \* h). +Proof. by move=>/(ae_eq_comp2 (fun x y => y * h x)). Qed. -Lemma ae_eq_mul2l f g h : ae_eq f g -> ae_eq (h \* f) (h \* g). -Proof. by apply: filterS => x /[apply] ->. Qed. +Lemma ae_eq_mul2l W (f g h : T -> W) : ae_eq f g -> ae_eq (h \* f) (h \* g). +Proof. by move=>/(ae_eq_comp2 (fun x y => h x * y)). Qed. -Lemma ae_eq_mul1l f g : ae_eq f (cst 1) -> ae_eq g (g \* f). -Proof. by apply: filterS => x /[apply] ->; rewrite mule1. Qed. +Lemma ae_eq_mul1l W (f g : T -> W) : ae_eq f (cst 1) -> ae_eq g (g \* f). +Proof. by apply: filterS => x /= /[apply] ->; rewrite mulr1. Qed. -Lemma ae_eq_abse f g : ae_eq f g -> ae_eq (abse \o f) (abse \o g). +Lemma ae_eq_abse (f g : T -> \bar R) : ae_eq f g -> ae_eq (abse \o f) (abse \o g). Proof. by apply: filterS => x /[apply] /= ->. Qed. +Lemma ae_foralln (P : nat -> T -> Prop) : (forall n, \forall x \ae mu, P n x) -> \forall x \ae mu, forall n, P n x. +Proof. +move=> /(_ _)/cid - /all_sig[A /all_and3[Ameas muA0 NPA]]. +have seqDUAmeas := seqDU_measurable Ameas. +exists (\bigcup_n A n); split => //. +- exact/bigcup_measurable. +- rewrite seqDU_bigcup_eq measure_bigcup//. + rewrite eseries0// => i _ _. + rewrite (@subset_measure0 _ _ _ _ _ (A i))//=. + exact: subset_seqDU. +- by move=> x /=; rewrite -existsNP => -[n NPnx]; exists n => //; apply: NPA. +Qed. + End ae_eq. Section ae_eq_lemmas. -Context d (T : sigmaRingType d) (R : realType). -Implicit Types mu : {measure set T -> \bar R}. +Context d (T : sigmaRingType d) (R : realType) (U : Type). +Implicit Types (mu : {measure set T -> \bar R}) (A : set T) (f g : T -> U). Lemma ae_eq_subset mu A B f g : B `<=` A -> ae_eq mu A f g -> ae_eq mu B f g. -Proof. -move=> BA [N [mN N0 fg]]; exists N; split => //. -by apply: subset_trans fg; apply: subsetC => z /= /[swap] /BA ? ->. -Qed. +Proof. by move=> BA; apply: filterS => x + /BA; apply. Qed. End ae_eq_lemmas. @@ -5307,8 +5375,8 @@ End absolute_continuity. Notation "m1 `<< m2" := (measure_dominates m1 m2). Section absolute_continuity_lemmas. -Context d (T : measurableType d) (R : realType). -Implicit Types m : {measure set T -> \bar R}. +Context d (T : measurableType d) (R : realType) (U : Type). +Implicit Types (m : {measure set T -> \bar R}) (f g : T -> U). Lemma measure_dominates_ae_eq m1 m2 f g E : measurable E -> m2 `<< m1 -> ae_eq m1 E f g -> ae_eq m2 E f g. @@ -5316,20 +5384,3 @@ Proof. by move=> mE m21 [A [mA A0 ?]]; exists A; split => //; exact: m21. Qed. End absolute_continuity_lemmas. -Section essential_supremum. -Context d {T : semiRingOfSetsType d} {R : realType}. -Variable mu : {measure set T -> \bar R}. -Implicit Types f : T -> R. - -Definition ess_sup f := - ereal_inf (EFin @` [set r | mu (f @^-1` `]r, +oo[) = 0]). - -Lemma ess_sup_ge0 f : 0 < mu [set: T] -> (forall t, 0 <= f t)%R -> - 0 <= ess_sup f. -Proof. -move=> muT f0; apply: lb_ereal_inf => _ /= [r /eqP rf <-]; rewrite leNgt. -apply/negP => r0; apply/negP : rf; rewrite gt_eqF// (_ : _ @^-1` _ = setT)//. -by apply/seteqP; split => // x _ /=; rewrite in_itv/= (lt_le_trans _ (f0 x)). -Qed. - -End essential_supremum. diff --git a/theories/normedtype.v b/theories/normedtype.v index 171b7196d8..21a2424677 100644 --- a/theories/normedtype.v +++ b/theories/normedtype.v @@ -202,7 +202,7 @@ Lemma limf_esup_ge0 f F : ~ F set0 -> Proof. move=> F0 f0; rewrite limf_esupE; apply: lb_ereal_inf => /= x [A]. have [-> /F0//|/set0P[y Ay FA] <-{x}] := eqVneq A set0. -by apply: ereal_sup_le; exists (f y). +by apply: ereal_sup_ge; exists (f y). Qed. End limf_esup_einf_realType. diff --git a/theories/sequences.v b/theories/sequences.v index a94ac54f8d..8912ec0763 100644 --- a/theories/sequences.v +++ b/theories/sequences.v @@ -282,6 +282,9 @@ apply/funext => n; rewrite -setIDA; apply/seteqP; split; last first. by rewrite /seqDU -setIDA bigcup_mkord -big_distrr/= setDIr setIUr setDIK set0U. Qed. +Lemma subset_seqDU (A : (set T)^nat) (i : nat) : seqDU A i `<=` A i. +Proof. by move=> ?; apply: subDsetl. Qed. + End seqDU. Arguments trivIset_seqDU {T} F. #[global] Hint Resolve trivIset_seqDU : core. diff --git a/theories/topology_theory/nat_topology.v b/theories/topology_theory/nat_topology.v index 79bc3a1b39..82c92c7270 100644 --- a/theories/topology_theory/nat_topology.v +++ b/theories/topology_theory/nat_topology.v @@ -38,7 +38,7 @@ Qed. HB.instance Definition _ := Order_isNbhs.Build _ nat nat_nbhs_itv. HB.instance Definition _ := DiscreteUniform_ofNbhs.Build nat. -HB.instance Definition _ {R : numDomainType} := +HB.instance Definition _ {R : numDomainType} := @DiscretePseudoMetric_ofUniform.Build R nat. Lemma nbhs_infty_gt N : \forall n \near \oo, (N < n)%N. @@ -48,13 +48,16 @@ Proof. by exists N.+1. Qed. Lemma nbhs_infty_ge N : \forall n \near \oo, (N <= n)%N. Proof. by exists N. Qed. -Lemma nbhs_infty_ger {R : realType} (r : R) : - \forall n \near \oo, (r <= n%:R)%R. +Lemma nbhs_infty_gtr {R : realType} (r : R) : \forall n \near \oo, r < n%:R. Proof. -exists `|Num.ceil r|%N => // n /=; rewrite -(ler_nat R); apply: le_trans. -by rewrite (le_trans (ceil_ge _))// natr_absz ler_int ler_norm. +exists `|Num.ceil r|.+1%N => // n /=; rewrite -(ler_nat R); apply: lt_le_trans. +rewrite (le_lt_trans (ceil_ge _))// -natr1 natr_absz ltr_pwDr// ler_int. +exact: ler_norm. Qed. +Lemma nbhs_infty_ger {R : realType} (r : R) : \forall n \near \oo, r <= n%:R. +Proof. by apply: filterS (nbhs_infty_gtr r) => x /ltW. Qed. + Lemma cvg_addnl N : addn N @ \oo --> \oo. Proof. by move=> P [n _ Pn]; exists (n - N)%N => // m; rewrite /= leq_subLR => /Pn.