From 1e4ef3aea4e2a0c17003256a3970cf7bfc7d0106 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Thu, 15 May 2025 16:16:26 +0900 Subject: [PATCH 01/13] instead of lspace_master --- theories/hoelder.v | 757 ++++++++++++++++-- .../simple_functions.v | 3 + theories/probability.v | 393 ++++----- theories/topology_theory/nat_topology.v | 2 +- 4 files changed, 861 insertions(+), 294 deletions(-) diff --git a/theories/hoelder.v b/theories/hoelder.v index 5665424f93..b2aaaf2678 100644 --- a/theories/hoelder.v +++ b/theories/hoelder.v @@ -1,19 +1,43 @@ (* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C. *) From HB Require Import structures. From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint interval finmap. -From mathcomp Require Import mathcomp_extra unstable boolp classical_sets. -From mathcomp Require Import functions 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 ess_sup_inf. +From mathcomp Require Import mathcomp_extra unstable boolp interval_inference. +From mathcomp Require Import classical_sets functions cardinality fsbigop reals. +From mathcomp Require Import ereal topology normedtype sequences real_interval. +From mathcomp Require Import esum measure ess_sup_inf lebesgue_measure. +From mathcomp Require Import lebesgue_integral numfun exp convex. (**md**************************************************************************) (* # Hoelder's Inequality *) (* *) -(* This file provides Hoelder's inequality. *) +(* This file provides the Lp-norm, Hoelder's inequality and its consequences, *) +(* most notably Minkowski's inequality, the convexity of the power function, *) +(* and a definition of Lp-spaces. *) +(* *) +(* ``` *) +(* 'N[mu]_p[f] == the Lp-norm of f with measure mu *) +(* conjugate p == a real number q such that p^-1 + q^-1 = 1 when *) +(* p is real, otherwise conjugate +oo = 1 and *) +(* conjugate -oo = 0 *) +(* ``` *) +(* *) +(* Lp-spaces and properties of Lp-norms: *) +(* *) (* ``` *) -(* 'N[mu]_p[f] := (\int[mu]_x (`|f x| `^ p)%:E) `^ p^-1 *) -(* The corresponding definition is Lnorm. *) +(* finite_norm mu p f := the L-norm of real-valued function f is finite *) +(* The parameter p is an extended real. *) +(* LfunType mu p1 == type of measurable functions f with a finite *) +(* L-norm *) +(* p1 is a proof that the extended real number p is *) +(* greater or equal to 1. *) +(* The HB class is Lfun. *) +(* f \in lfun == holds for f : LfunType mu p1 *) +(* Lequiv f g == f is equal to g almost everywhere *) +(* The functions f and g have type LfunType mu p1. *) +(* Lequiv is made a canonical equivalence relation. *) +(* LspaceType mu p1 == type of the elements of the Lp space for the *) +(* measure mu *) +(* mu.-Lspace p == Lp space as a set *) (* ``` *) (* *) (******************************************************************************) @@ -33,85 +57,169 @@ Reserved Notation "'N[ mu ]_ p [ F ]" (* for use as a local notation when the measure is in context: *) Reserved Notation "'N_ p [ F ]" (at level 5, F at level 36, format "'[' ''N_' p '/ ' [ F ] ']'"). +Reserved Notation "mu .-Lspace p" (at level 4, format "mu .-Lspace p"). 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_supr 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}. Variable mu : {measure set T -> \bar R}. Local Open Scope ereal_scope. -Implicit Types (p : \bar R) (f g : T -> R) (r : R). +Implicit Types (p : \bar R) (f g : T -> \bar R) (r : R). Local Notation "'N_ p [ f ]" := (Lnorm mu p f). -Lemma Lnorm1 f : 'N_1[f] = \int[mu]_x `|f x|%:E. +Lemma Lnorm0 p : 1 <= p -> 'N_p[cst 0] = 0. Proof. -rewrite unlock oner_eq0 invr1// poweRe1//. - by apply: eq_integral => t _; rewrite powRr1. -by apply: integral_ge0 => t _; rewrite powRr1. +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 Lnorm_ge0 p f : 0 <= 'N_p[f]. +Lemma Lnorm1 f : 'N_1[f] = \int[mu]_x `|f x|. Proof. -rewrite unlock; move: p => [r/=|/=|//]. - by case: ifPn => // r0; exact: poweR_ge0. -by case: ifPn => // /ess_sup_ger; apply => t/=. +rewrite unlock invr1// poweRe1//; under eq_integral do [rewrite poweRe1//=] => //. +exact: integral_ge0. 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 poweR_Lnorm f r : r != 0%R -> + 'N_r%:E[f] `^ r = \int[mu]_x (`| f x | `^ r). 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. +move=> r0; rewrite unlock -poweRrM mulVf// poweRe1//. +by apply: integral_ge0 => x _; exact: poweR_ge0. Qed. -Lemma powR_Lnorm f r : r != 0%R -> - 'N_r%:E[f] `^ r = \int[mu]_x (`| f x | `^ r)%:E. +Lemma oppe_Lnorm f p : 'N_p[\- f]%E = 'N_p[f]. Proof. -move=> r0; rewrite unlock (negbTE r0) -poweRrM mulVf// poweRe1//. -by apply: integral_ge0 => x _; rewrite lee_fin// powR_ge0. +have NfE : abse \o (\- f) = abse \o f. + by apply/funext => x /=; rewrite abseN. +rewrite unlock /Lnorm NfE; case: p => /= [r|//|//]. +by under eq_integral => x _ do rewrite abseN. Qed. +Lemma Lnorm_cst1 r : 'N_r%:E[cst 1] = mu [set: T] `^ (r^-1). +Proof. +rewrite unlock /Lnorm; under eq_integral do rewrite /= normr1 powR1. +by rewrite integral_cst// mul1e. +Qed. + +Lemma Lnorm_ge0 p f : 0 <= 'N_p[f]. +Proof. +rewrite unlock; move: p => [r/=|/=|//]; first exact: poweR_ge0. +- by case: ifPn => // /ess_sup_gee; apply; apply/nearW => r/=. +- by case: ifPn => // muT0; apply/ess_infP/nearW => x /=. +Qed. + +Lemma Lnorm_eq0_eq0 f p : + measurable_fun setT f -> (0 < p)%E -> 'N_p[f] = 0 -> f = \0 %[ae mu]. +Proof. +rewrite unlock /Lnorm => mf. +case: p => [r||//]. +- rewrite lte_fin => r0 /poweR_eq0_eq0 => /(_ (integral_ge0 _ _)) h. + have : \int[mu]_x `|f x| `^ r = 0. + by apply: h => x _; rewrite poweR_ge0. + move=> H. + have {H} : \int[mu]_x `| `|f x| `^ r | = 0%R. + under eq_integral. + move=> x _. + rewrite gee0_abs; last by rewrite poweR_ge0. + over. + exact: H. + have mp : measurable_fun [set: T] (fun x : T => `|f x| `^ r). + apply: (@measurableT_comp _ _ _ _ _ _ (fun x => x `^ r)) => //=. + by apply (measurableT_comp (measurable_poweR _)) => //. + exact: measurableT_comp. + move/(ae_eq_integral_abs mu measurableT mp). + apply: filterS => x/= /[apply]. + move=> /poweR_eq0_eq0 /eqP => /(_ (abse_ge0 _)). + by rewrite abse_eq0 => /eqP. +- case: ifPn => [mu0 _|]. + move=> /abs_sup_eq0_ae_eq/=. + by apply: filterS => x/= /(_ I) /eqP + _ => /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. +Proof. by move=> r0; rewrite poweR_Lnorm. Qed. + End Lnorm_properties. #[global] Hint Extern 0 (0 <= Lnorm _ _ _) => solve [apply: Lnorm_ge0] : core. -Notation "'N[ mu ]_ p [ f ]" := (Lnorm mu p f). +Notation "'N[ mu ]_ p [ f ]" := (Lnorm mu p f) : ereal_scope. 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). +(** lp-norm is just Lp-norm applied to counting *) +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. Qed. +Proof. +by move=> p0; rewrite unlock ge0_integral_count// => k; rewrite poweR_ge0. +Qed. End lnorm. +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 hoelder. Context d {T : measurableType d} {R : realType}. Variable mu : {measure set T -> \bar R}. @@ -122,7 +230,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 -> @@ -133,7 +241,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. @@ -141,11 +249,13 @@ 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. +- move/measurable_EFinP in mf. + apply: filterS (Lnorm_eq0_eq0 mf p0 f0) => x /(_ I) + _. + by rewrite /= normrM EFinM -abse_EFin => ->; rewrite abse0 mul0e. Qed. Let normalized p f x := (`|f x| / fine 'N_p%:E[f])%R. @@ -168,10 +278,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 => -[_]. @@ -181,7 +291,8 @@ rewrite integralZl//; apply/eqP; rewrite eqe_pdivrMl ?mule1. - by rewrite gt_eqF// fine_gt0// foo andbT. Qed. -Lemma hoelder f g p q : measurable_fun setT f -> measurable_fun setT g -> +Lemma hoelder (f g : T -> R) p q : + measurable_fun [set: T] f -> measurable_fun [set: T] g -> (0 < p)%R -> (0 < q)%R -> (p^-1 + q^-1 = 1)%R -> 'N_1[(f \* g)%R] <= 'N_p%:E[f] * 'N_q%:E[g]. Proof. @@ -352,14 +463,14 @@ 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 -> +Let minkowski1 f g p : measurable_fun [set: T] f -> measurable_fun [set: T] g -> 'N_1[(f \+ g)%R] <= 'N_1[f] + 'N_1[g]. Proof. move=> mf mg. -rewrite !Lnorm1 -ge0_integralD//; [|by do 2 apply: measurableT_comp..]. +rewrite !Lnorm1 -ge0_integralD//=; [|by do 2 apply: measurableT_comp..]. rewrite ge0_le_integral//. - by do 2 apply: measurableT_comp => //; exact: measurable_funD. - by move=> x _; rewrite adde_ge0. @@ -368,7 +479,7 @@ rewrite ge0_le_integral//. Qed. Let minkowski_lty f g p : - measurable_fun setT f -> measurable_fun setT g -> (1 <= p)%R -> + measurable_fun [set: T] f -> measurable_fun [set: T] g -> (1 <= p)%R -> 'N_p%:E[f] < +oo -> 'N_p%:E[g] < +oo -> 'N_p%:E[(f \+ g)%R] < +oo. Proof. move=> mf mg p1 Nfoo Ngoo. @@ -379,7 +490,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//=. @@ -397,11 +508,13 @@ under eq_integral do rewrite EFinD. rewrite ge0_integralD//; last 2 first. - exact/measurable_EFinP/measurableT_comp_powR/measurableT_comp. - exact/measurable_EFinP/measurableT_comp_powR/measurableT_comp. -by rewrite lte_add_pinfty// -powR_Lnorm ?(gt_eqF (lt_trans _ p1))// poweR_lty. +by rewrite lte_add_pinfty//; + under eq_integral do rewrite -poweR_EFin -abse_EFin; + rewrite -powR_Lnorm// poweR_lty. Qed. -Lemma minkowski f g p : - measurable_fun setT f -> measurable_fun setT g -> (1 <= p)%R -> +Lemma minkowski_EFin f g p : + measurable_fun [set: T] f -> measurable_fun [set: T] g -> (1 <= p)%R -> 'N_p%:E[(f \+ g)%R] <= 'N_p%:E[f] + 'N_p%:E[g]. Proof. move=> mf mg; rewrite le_eqVlt => /predU1P[<-|p1]; first exact: minkowski1. @@ -427,7 +540,10 @@ suff : 'N_p%:E[(f \+ g)%R] `^ p <= ('N_p%:E[f] + 'N_p%:E[g]) * by rewrite fineK// 1?muleC// fin_num_poweR// ge0_fin_numE ?Lnorm_ge0. have p0 : (0 < p)%R by exact: (lt_trans _ p1). rewrite powR_Lnorm ?gt_eqF//. -under eq_integral => x _ do rewrite -mulr_powRB1//. +under eq_integral. + move=> x _. + rewrite abse_EFin poweR_EFin -mulr_powRB1//. + over. apply: (@le_trans _ _ (\int[mu]_x ((`|f x| + `|g x|) * `|f x + g x| `^ (p - 1))%:E)). rewrite ge0_le_integral//. @@ -449,16 +565,18 @@ rewrite ge0_integralD//; last 2 first. rewrite [leRHS](_ : _ = ('N_p%:E[f] + 'N_p%:E[g]) * (\int[mu]_x (`|f x + g x| `^ p)%:E) `^ `1-(p^-1)). rewrite muleDl; last 2 first. - - rewrite fin_num_poweR// -powR_Lnorm ?gt_eqF// fin_num_poweR//. + - rewrite fin_num_poweR//. + under eq_integral do rewrite -poweR_EFin -abse_EFin. + rewrite -powR_Lnorm ?gt_eqF// fin_num_poweR//. by rewrite ge0_fin_numE ?Lnorm_ge0. - by rewrite ge0_adde_def// inE Lnorm_ge0. apply: leeD. - pose h := (@powR R ^~ (p - 1) \o normr \o (f \+ g))%R; pose i := (f \* h)%R. rewrite [leLHS](_ : _ = 'N_1[i]%R); last first. - rewrite Lnorm1; apply: eq_integral => x _. + 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//. @@ -469,11 +587,11 @@ rewrite [leRHS](_ : _ = ('N_p%:E[f] + 'N_p%:E[g]) * + by rewrite invf_div -onemV ?gt_eqF// addrCA subrr addr0. - pose h := (fun x => `|f x + g x| `^ (p - 1))%R; pose i := (g \* h)%R. rewrite [leLHS](_ : _ = 'N_1[i]); last first. - rewrite Lnorm1; apply: eq_integral => x _ . + 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. @@ -486,8 +604,515 @@ 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 -powR_Lnorm ?gt_eqF// fin_num_poweR// ge0_fin_numE ?Lnorm_ge0. +- by rewrite unlock fine_poweR. +- under eq_integral do rewrite -poweR_EFin -abse_EFin. + by rewrite -powR_Lnorm ?gt_eqF// fin_num_poweR// ge0_fin_numE ?Lnorm_ge0. +Qed. + +Lemma lerB_DLnorm f g p : + measurable_fun [set: T] f -> measurable_fun [set: T] 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)%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 (_ : _ \o _ = \- (EFin \o g))// oppe_Lnorm. +by apply: minkowski_EFin => //; + [exact: measurable_funD|exact: measurableT_comp]. +Qed. + +Lemma lerB_LnormD f g p : + measurable_fun [set: T] f -> measurable_fun [set: T] g -> (1 <= p)%R -> + 'N_p%:E[f] - 'N_p%:E[g] <= 'N_p%:E[f \+ g]. +Proof. +move=> mf mg p1. +set rhs := (leRHS); have [?|] := boolP (rhs \is a fin_num). + by rewrite lee_subel_addr//; exact: lerB_DLnorm. +rewrite fin_numEn => /orP[|/eqP ->]; last by rewrite leey. +by rewrite gt_eqF// (lt_le_trans _ (Lnorm_ge0 _ _ _)). +Qed. + +(* TODO: rename to minkowski after version 1.12.0 *) +Lemma eminkowski f g (p : \bar R) : + measurable_fun [set: T] f -> measurable_fun [set: T] g -> 1 <= p -> + 'N_p[(f \+ g)%R] <= 'N_p[f] + 'N_p[g]. +Proof. +case: p => //[r|]; first exact: minkowski_EFin. +move=> mf mg _; rewrite unlock /Lnorm. +case: ifPn => mugt0; last by rewrite adde0 lexx. +exact: ess_sup_normD. Qed. End minkowski. +#[deprecated(since="mathcomp-analysis 1.10.0", + note="use `minkowski_EFin` or `eminkowski` instead")] +Notation minkowski := minkowski_EFin (only parsing). + +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}. +HB.instance Definition _ := Choice.on LspaceType. +HB.instance Definition _ := EqQuotient.on 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 mfun_extra. +Context d (T : measurableType d) (R : realType). +Variables (mu : {measure set T -> \bar R}). + +Lemma mfunP (f : {mfun T >-> R}) : (f : T -> R) \in mfun. +Proof. exact: valP. Qed. + +Import numFieldNormedType.Exports. + +Lemma mfun_scaler_closed : scaler_closed (@mfun _ _ T R). +Proof. by 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 <:]. + +End mfun_extra. + +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. + +Reserved Notation "[ 'lfun' 'of' f ]" + (at level 0, format "[ 'lfun' 'of' f ]"). +Notation "[ 'lfun' 'of' f ]" := [the LfunType _ _ of f] : form_scope. + +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)). +#[local] HB.instance Definition _ := lfun_Sub2_subproof. +Definition lfun_Sub := [lfun of 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 <:]. + +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 lfunP (f : LfunType mu p1) : (f : T -> R) \in lfun. +Proof. exact: valP. Qed. + +Lemma lfun_oppr_closed : oppr_closed lfun. +Proof. +move=> f /andP[mf /[!inE] lf]. +rewrite rpredN/= mf/= inE/= /finite_norm. +by rewrite (_ : _ \o _ = \- (EFin \o f))%E// oppe_Lnorm. +Qed. + +HB.instance Definition _ := GRing.isOppClosed.Build _ lfun + lfun_oppr_closed. + +(* NB: not used directly by HB.instance *) +Lemma lfun_addr_closed : addr_closed lfun. +Proof. +split. + by rewrite inE rpred0/= inE/= /finite_norm/= Lnorm0. +move=> f g /andP[mf /[!inE]/= lf] /andP[mg /[!inE]/= lg]. +rewrite rpredD//= inE/=. +rewrite /finite_norm. +rewrite (le_lt_trans (@eminkowski _ _ _ mu f g p _ _ _))//. +- by rewrite inE in mf. +- by rewrite inE in mg. +- by rewrite lte_add_pinfty. +Qed. + +Import numFieldNormedType.Exports. + +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|? f]. +- under eq_integral 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). + rewrite [ltLHS](_ : _ = 'N[mu]_r%:E[EFin \o f]%E); first exact: (lfuny r1 f). + rewrite unlock /Lnorm. + by under eq_integral do rewrite gee0_abs ?lee_fin ?powR_ge0//. + rewrite poweRM ?integral_ge0//. + by rewrite poweR_EFin -powRrM mulfV ?gt_eqF ?(lt_le_trans ltr01)// powRr1. +- case: ifPn => mu0; last by rewrite mule0. + rewrite -ess_supZl//; apply/eq_ess_sup/nearW => t /=. + by rewrite normrZ EFinM. +Qed. + +Lemma lfun_submod_closed : submod_closed lfun. +Proof. +split. + by 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 => /=; apply: (le_lt_trans (eminkowski _ _ _ _)) => //. +- suff: a *: (g : T -> R) \in mfun by exact: set_mem. + by rewrite rpredZ//; exact: mfunP. +- rewrite lte_add_pinfty//; last exact: lfuny. + by 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}. +Variables (p : \bar R) (p1 : (1 <= p)%E). + +(* TODO: 0 - + should come with proofs that they are in LfunType mu p *) + +Notation ty := (LfunType mu p1). +Let nm f := fine ('N[mu]_p[EFin \o f]). + +Lemma finite_norm_fine (f : ty) : (nm f)%:E = 'N[mu]_p[EFin \o f]%E. +Proof. +rewrite /nm fineK// fin_numElt (lt_le_trans ltNy0) ?Lnorm_ge0//=. +exact: lfuny. +Qed. + +Lemma ler_LnormD (f g : ty) : nm (f + g) <= nm f + nm g. +Proof. by rewrite -lee_fin EFinD !finite_norm_fine eminkowski. Qed. + +Lemma LnormrN (f : ty) : nm (\-f) = nm f. +Proof. by rewrite /nm (_ : _ \o _ = \- (EFin \o f))%E// oppe_Lnorm. Qed. + +Lemma Lnormr_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 fine_Lnormr_eq0 (f : ty) : nm f = 0 -> f = 0 %[ae mu]. +Proof. +move=> /eqP; rewrite -eqe => /eqP. +rewrite finite_norm_fine => /Lnorm_eq0_eq0. +have /measurable_EFinP : measurable_fun setT f by []. +move=> /[swap] /[apply] => /(_ (lt_le_trans lte01 p1)). +by apply: filterS => x /(_ I) []. +Qed. + +End Lspace_norm. + +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. + +Definition LType1 := LType mu (@lexx _ _ 1%E). + +Definition LType2 := LType mu (lee1n 2). + +Lemma lfun_integrable (f : T -> R) r : + 1 <= r -> f \in lfun mu r%:E -> + mu.-integrable setT (fun x => (`|f x| `^ r)%:E). +Proof. +rewrite inE => r0 /andP[/[!inE]/= mf] lpf. +apply/integrableP; split => //. + apply: measurableT_comp => //. + apply: (measurableT_comp (measurable_powR _)) => //. + exact: measurableT_comp. +move: lpf => /(poweR_lty r). +rewrite powR_Lnorm// ?gt_eqF// ?(lt_le_trans ltr01)//. +apply: le_lt_trans. +by under eq_integral => x _ do rewrite gee0_abs ?lee_fin ?powR_ge0//. +Qed. + +Lemma lfun1_integrable (f : T -> R) : + f \in lfun mu 1 -> mu.-integrable setT (EFin \o f). +Proof. +move=> /[dup] lf /lfun_integrable => /(_ (lexx _)). +under eq_fun => x do rewrite powRr1//. +move/integrableP => [mf fley]. +apply/integrableP; split. + move: lf; rewrite inE => /andP[/[!inE]/= {}mf _]. + exact: measurableT_comp. +rewrite (le_lt_trans _ fley)//=. +by under [leRHS]eq_integral => x _ do rewrite normr_id. +Qed. + +Lemma lfun2_integrable_sqr (f : T -> R) : f \in lfun mu 2%:E -> + mu.-integrable [set: T] (EFin \o (fun x => f x ^+ 2)). +Proof. +rewrite inE => /andP[mf]; rewrite inE/= => l2f. +move: mf; rewrite inE/= => mf. +apply/integrableP; split. + by apply/measurable_EFinP; exact: measurable_funX. +rewrite (@lty_poweRy _ _ 2^-1)//. +rewrite (le_lt_trans _ l2f)//. +rewrite unlock. +rewrite gt0_ler_poweR//. +- by rewrite in_itv/= leey integral_ge0. +- by rewrite in_itv/= leey integral_ge0. +- rewrite ge0_le_integral//. + + apply: measurableT_comp => //; apply/measurable_EFinP. + exact: measurable_funX. + + 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. + +Lemma lfun2M2_1 (f g : T -> R) : f \in lfun mu 2%:E -> g \in lfun mu 2%:E -> + f \* g \in lfun mu 1. +Proof. +move=> l2f l2g. +move: (l2f) (l2g) => /[!inE] /andP[/[!inE]/= mf _] /andP[/[!inE]/= mg _]. +apply/andP; split. + by rewrite inE/=; apply: measurable_funM. +rewrite !inE/= /finite_norm. +apply: le_lt_trans. + by apply: (@hoelder _ _ _ _ _ _ 2 2) => //; rewrite [RHS]splitr !div1r. +rewrite lte_mul_pinfty// ?ge0_fin_numE ?Lnorm_ge0//. +by move: l2f; rewrite inE => /andP[_]; rewrite inE/=. +by move: l2g; rewrite inE => /andP[_]; rewrite inE/=. +Qed. + +Lemma lfunp_scale (f : T -> R) a r : + 1 <= r -> f \in lfun mu r%:E -> a \o* f \in lfun mu r%:E. +Proof. +move=> r1 /[dup] lf lpf. +rewrite inE; apply/andP; split. + move: lf; rewrite inE => /andP[/[!inE]/= lf _]. + exact: measurable_funM. +rewrite !inE/= /finite_norm unlock /Lnorm. +rewrite poweR_lty//=. +under eq_integral => x _ do rewrite normrM powRM// EFinM. +rewrite integralZr// ?lfun_integrable//. +rewrite muleC lte_mul_pinfty// ?lee_fin ?powR_ge0//. +move: lpf => /(lfun_integrable r1) /integrableP[_]. +under eq_integral => x _ do rewrite gee0_abs ?lee_fin ?powR_ge0//. +by []. +Qed. + +End Lspace. +Notation "mu .-Lspace p" := (@Lspace _ _ _ mu p) : type_scope. + +Section Lspace_finite_measure. +Context d (T : measurableType d) (R : realType). +Variable mu : {finite_measure set T -> \bar R}. + +Lemma lfun_cst c r : cst c \in lfun mu r%:E. +Proof. +rewrite inE; apply/andP; split; rewrite inE//= /finite_norm unlock/Lnorm poweR_lty//. +under eq_integral => x _/= do rewrite (_ : `|c| `^ r = cst (`|c| `^ r) x)//. +have /integrableP[_/=] := finite_measure_integrable_cst mu (`|c| `^ r). +under eq_integral => x _ do rewrite ger0_norm ?powR_ge0//. +by []. +Qed. + +End Lspace_finite_measure. + +Section lfun_inclusion. +Context d (T : measurableType d) (R : realType). +Variable mu : {measure set T -> \bar R}. +Local Open Scope ereal_scope. + +Lemma lfun_inclusion (p q : \bar R) : forall (p1 : 1 <= p) (q1 : 1 <= q), + mu [set: T] \is a fin_num -> + p <= q -> {subset lfun mu q <= lfun mu p}. +Proof. +have := measure_ge0 mu [set: T]. +rewrite le_eqVlt => /predU1P[mu0 p1 q1 muTfin pq f +|mu_pos]. + rewrite inE => /andP[/[1!inE]/= mf _]. + rewrite inE; apply/andP; split; rewrite inE//=. + rewrite /finite_norm unlock /Lnorm. + move: p p1 {pq} => [r r1| |//]; last by rewrite -mu0 ltxx ltry. + 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/(@measurableT_comp _ _ _ _ _ _ (@powR R ^~ r)) => //. + exact: measurableT_comp. +move: p q => [p| |//] [q| |]// p1 q1. +- move=> mu_fin. + rewrite le_eqVlt => /predU1P[[->]//|]; rewrite lte_fin => pq f. + rewrite inE/= => /andP[/[!inE]/= mf] ffin. + apply/andP; split; rewrite inE//=. + move: (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)%R (cst 1)%R r r'. + rewrite (_ : (_ \* cst 1)%R = (fun x => `|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) by 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/(le_lt_trans h1). + rewrite muleC lte_mul_pinfty ?fin_numElt?poweR_ge0//. + by rewrite (lt_le_trans _ (poweR_ge0 _ _))//= ltey_eq fin_num_poweR. + rewrite poweR_lty// (lty_poweRy qinv0)//. + by have:= ffin; rewrite /finite_norm unlock /Lnorm. +- have p0 : (0 < p)%R by rewrite ?(lt_le_trans ltr01). + move=> muoo _ f. + rewrite !inE => /andP[/[1!inE]/= mf]. + rewrite !inE/= /finite_norm unlock /Lnorm mu_pos => supf_lty. + apply/andP; split; rewrite inE//= /finite_norm unlock /Lnorm. + 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// ltey_eq fin_numM. + 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). +- by move=> muTfin _. +Qed. + +Lemma lfun_inclusion12 : mu [set: T] \is a fin_num -> + {subset lfun mu 2%:E <= lfun mu 1}. +Proof. by move=> ?; apply: lfun_inclusion => //; rewrite lee1n. Qed. + +End lfun_inclusion. diff --git a/theories/lebesgue_integral_theory/simple_functions.v b/theories/lebesgue_integral_theory/simple_functions.v index 14cd93f104..08d726dbaf 100644 --- a/theories/lebesgue_integral_theory/simple_functions.v +++ b/theories/lebesgue_integral_theory/simple_functions.v @@ -32,6 +32,7 @@ From mathcomp Require Import function_spaces. (* {mfun aT >-> rT} == type of measurable functions *) (* aT and rT are sigmaRingType's. *) (* {sfun T >-> R} == type of simple functions *) +(* f \in mfun == holds for f : {mfun _ >-> _} *) (* {nnsfun T >-> R} == type of non-negative simple functions *) (* mindic mD := \1_D where mD is a proof that D is measurable *) (* indic_mfun mD := mindic mD *) @@ -218,6 +219,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. diff --git a/theories/probability.v b/theories/probability.v index 4670b343c4..b52c51e75f 100644 --- a/theories/probability.v +++ b/theories/probability.v @@ -8,7 +8,7 @@ From mathcomp Require Import exp numfun lebesgue_measure lebesgue_integral. From mathcomp Require Import reals interval_inference ereal topology normedtype. From mathcomp Require Import sequences derive esum measure exp trigo realfun. From mathcomp Require Import numfun lebesgue_measure lebesgue_integral kernel. -From mathcomp Require Import ftc gauss_integral. +From mathcomp Require Import ftc gauss_integral hoelder. (**md**************************************************************************) (* # Probability *) @@ -16,6 +16,10 @@ From mathcomp Require Import ftc gauss_integral. (* This file provides basic notions of probability theory. See measure.v for *) (* the type probability T R (a measure that sums to 1). *) (* *) +(* About integrability: as a rule of thumb, in this file, we favor the use *) +(* of `lfun P n` hypotheses instead of the `integrable` predicate from *) +(* `lebesgue_integral.v`. *) +(* *) (* ``` *) (* {RV P >-> T'} == random variable: a measurable function to the *) (* measurableType T' from the measured space *) @@ -256,9 +260,9 @@ Context d (T : measurableType d) (R : realType) (P : probability T R). Lemma expectation_def (X : {RV P >-> R}) : 'E_P[X] = (\int[P]_w (X w)%:E)%E. Proof. by rewrite unlock. Qed. -Lemma expectation_fin_num (X : {RV P >-> R}) : P.-integrable setT (EFin \o X) -> +Lemma expectation_fin_num (X : T -> R) : X \in lfun P 1 -> 'E_P[X] \is a fin_num. -Proof. by move=> ?; rewrite unlock integral_fune_fin_num. Qed. +Proof. by move=> ?; rewrite unlock integral_fune_fin_num ?lfun1_integrable. Qed. Lemma expectation_cst r : 'E_P[cst r] = r%:E. Proof. by rewrite unlock/= integral_cst//= probability_setT mule1. Qed. @@ -273,12 +277,12 @@ move: iX => /integrableP[? Xoo]; rewrite (le_lt_trans _ Xoo)// unlock. exact: le_trans (le_abse_integral _ _ _). Qed. -Lemma expectationZl (X : {RV P >-> R}) (iX : P.-integrable [set: T] (EFin \o X)) - (k : R) : 'E_P[k \o* X] = k%:E * 'E_P [X]. -Proof. by rewrite unlock muleC -integralZr. Qed. +Lemma expectationZl (X : T -> R) (k : R) : X \in lfun P 1 -> + 'E_P[k \o* X] = k%:E * 'E_P [X]. +Proof. by move=> ?; rewrite unlock muleC -integralZr ?lfun1_integrable. Qed. -Lemma expectation_ge0 (X : {RV P >-> R}) : - (forall x, 0 <= X x)%R -> 0 <= 'E_P[X]. +Lemma expectation_ge0 (X : T -> R) : (forall x, 0 <= X x)%R -> + 0 <= 'E_P[X]. Proof. by move=> ?; rewrite unlock integral_ge0// => x _; rewrite lee_fin. Qed. @@ -297,29 +301,23 @@ move=> mX mY X0 Y0 XY; rewrite unlock ae_ge0_le_integral => //. by apply: XYN => /=; apply: contra_not h; rewrite lee_fin. Qed. -Lemma expectationD (X Y : {RV P >-> R}) : - P.-integrable [set: T] (EFin \o X) -> P.-integrable [set: T] (EFin \o Y) -> +Lemma expectationD (X Y : T -> R) : X \in lfun P 1 -> Y \in lfun P 1 -> 'E_P[X \+ Y] = 'E_P[X] + 'E_P[Y]. -Proof. by move=> ? ?; rewrite unlock integralD_EFin. Qed. +Proof. by move=> ? ?; rewrite unlock integralD_EFin ?lfun1_integrable. Qed. -Lemma expectationB (X Y : {RV P >-> R}) : - P.-integrable [set: T] (EFin \o X) -> P.-integrable [set: T] (EFin \o Y) -> +Lemma expectationB (X Y : T -> R) : X \in lfun P 1 -> Y \in lfun P 1 -> 'E_P[X \- Y] = 'E_P[X] - 'E_P[Y]. -Proof. by move=> ? ?; rewrite unlock integralB_EFin. Qed. +Proof. by move=> ? ?; rewrite unlock integralB_EFin ?lfun1_integrable. Qed. -Lemma expectation_sum (X : seq {RV P >-> R}) : - (forall Xi, Xi \in X -> P.-integrable [set: T] (EFin \o Xi)) -> +Lemma expectation_sum (X : seq (T -> R)) : + (forall Xi, Xi \in X -> Xi \in lfun P 1) -> 'E_P[\sum_(Xi <- X) Xi] = \sum_(Xi <- X) 'E_P[Xi]. Proof. elim: X => [|X0 X IHX] intX; first by rewrite !big_nil expectation_cst. -have intX0 : P.-integrable [set: T] (EFin \o X0). - by apply: intX; rewrite in_cons eqxx. -have {}intX Xi : Xi \in X -> P.-integrable [set: T] (EFin \o Xi). - by move=> XiX; apply: intX; rewrite in_cons XiX orbT. -rewrite !big_cons expectationD ?IHX// (_ : _ \o _ = fun x => - \sum_(f <- map (fun x : {RV P >-> R} => EFin \o x) X) f x). - by apply: integrable_sum => // _ /mapP[h hX ->]; exact: intX. -by apply/funext => t/=; rewrite big_map sumEFin mfun_sum. +rewrite !big_cons expectationD; last 2 first. + by rewrite intX// mem_head. + by rewrite big_seq rpred_sum// => Y YX/=; rewrite intX// inE YX orbT. +by rewrite IHX//= => Xi XiX; rewrite intX// inE XiX orbT. Qed. End expectation_lemmas. @@ -332,31 +330,29 @@ HB.lock Definition covariance {d} {T : measurableType d} {R : realType} Canonical covariance_unlockable := Unlockable covariance.unlock. Arguments covariance {d T R} P _%_R _%_R. +Hint Extern 0 (fin_num_fun _) => + (apply: fin_num_measure) : core. + Section covariance_lemmas. Local Open Scope ereal_scope. Context d (T : measurableType d) (R : realType) (P : probability T R). -Lemma covarianceE (X Y : {RV P >-> R}) : - P.-integrable setT (EFin \o X) -> - P.-integrable setT (EFin \o Y) -> - P.-integrable setT (EFin \o (X * Y)%R) -> +Lemma covarianceE (X Y : T -> R) : + X \in lfun P 1 -> Y \in lfun P 1 -> + (X * Y)%R \in lfun P 1 -> covariance P X Y = 'E_P[X * Y] - 'E_P[X] * 'E_P[Y]. Proof. -move=> X1 Y1 XY1. -have ? : 'E_P[X] \is a fin_num by rewrite fin_num_abs// integrable_expectation. -have ? : 'E_P[Y] \is a fin_num by rewrite fin_num_abs// integrable_expectation. +move=> l1X l1Y l1XY. rewrite unlock [X in 'E_P[X]](_ : _ = (X \* Y \- fine 'E_P[X] \o* Y \- fine 'E_P[Y] \o* X \+ fine ('E_P[X] * 'E_P[Y]) \o* cst 1)%R); last first. - apply/funeqP => x /=; rewrite mulrDr !mulrDl/= mul1r fineM// mulrNN addrA. + apply/funeqP => x /=; rewrite mulrDr !mulrDl/= mul1r. + rewrite fineM ?expectation_fin_num// mulrNN addrA. by rewrite mulrN mulNr [Z in (X x * Y x - Z)%R]mulrC. -have ? : P.-integrable [set: T] (EFin \o (X \* Y \- fine 'E_P[X] \o* Y)%R). - by rewrite compreBr ?integrableB// compre_scale ?integrableZl. -rewrite expectationD/=; last 2 first. - - by rewrite compreBr// integrableB// compre_scale ?integrableZl. - - by rewrite compre_scale// integrableZl// finite_measure_integrable_cst. -rewrite 2?expectationB//= ?compre_scale// ?integrableZl//. -rewrite 3?expectationZl//= ?finite_measure_integrable_cst//. -by rewrite expectation_cst mule1 fineM// EFinM !fineK// muleC subeK ?fin_numM. +rewrite expectationD/= ?rpredB//= ?lfunp_scale ?lfun_cst//. +rewrite 2?expectationB//= ?rpredB ?lfunp_scale// 3?expectationZl//= ?lfun_cst//. +rewrite expectation_cst mule1 fineM ?expectation_fin_num// EFinM. +rewrite !fineK ?expectation_fin_num//. +by rewrite muleC subeK ?fin_numM ?expectation_fin_num. Qed. Lemma covarianceC (X Y : T -> R) : covariance P X Y = covariance P Y X. @@ -364,55 +360,50 @@ Proof. by rewrite unlock; congr expectation; apply/funeqP => x /=; rewrite mulrC. Qed. -Lemma covariance_fin_num (X Y : {RV P >-> R}) : - P.-integrable setT (EFin \o X) -> - P.-integrable setT (EFin \o Y) -> - P.-integrable setT (EFin \o (X * Y)%R) -> +Lemma covariance_fin_num (X Y : T -> R) : + X \in lfun P 1 -> Y \in lfun P 1 -> + (X * Y)%R \in lfun P 1 -> covariance P X Y \is a fin_num. Proof. -by move=> X1 Y1 XY1; rewrite covarianceE// fin_numB fin_numM expectation_fin_num. +by move=> ? ? ?; rewrite covarianceE// fin_numB fin_numM expectation_fin_num. Qed. -Lemma covariance_cst_l c (X : {RV P >-> R}) : covariance P (cst c) X = 0. +Lemma covariance_cst_l c (X : T -> R) : covariance P (cst c) X = 0. Proof. rewrite unlock expectation_cst/=. rewrite [X in 'E_P[X]](_ : _ = cst 0%R) ?expectation_cst//. by apply/funeqP => x; rewrite /GRing.mul/= subrr mul0r. Qed. -Lemma covariance_cst_r (X : {RV P >-> R}) c : covariance P X (cst c) = 0. +Lemma covariance_cst_r (X : T -> R) c : covariance P X (cst c) = 0. Proof. by rewrite covarianceC covariance_cst_l. Qed. -Lemma covarianceZl a (X Y : {RV P >-> R}) : - P.-integrable setT (EFin \o X) -> - P.-integrable setT (EFin \o Y) -> - P.-integrable setT (EFin \o (X * Y)%R) -> +Lemma covarianceZl a (X Y : T -> R) : + X \in lfun P 1 -> Y \in lfun P 1 -> + (X * Y)%R \in lfun P 1 -> covariance P (a \o* X)%R Y = a%:E * covariance P X Y. Proof. move=> X1 Y1 XY1. -have aXY : (a \o* X * Y = a \o* (X * Y))%R. - by apply/funeqP => x; rewrite mulrAC. -rewrite [LHS]covarianceE => [||//|] /=; last 2 first. -- by rewrite compre_scale ?integrableZl. -- by rewrite aXY compre_scale ?integrableZl. +have aXY : (a \o* X * Y = a \o* (X * Y))%R by apply/funeqP => x; rewrite mulrAC. +rewrite [LHS]covarianceE => [||//|] //=; last 2 first. +- by rewrite lfunp_scale. +- by rewrite aXY lfunp_scale. rewrite covarianceE// aXY !expectationZl//. by rewrite -muleA -muleBr// fin_num_adde_defr// expectation_fin_num. Qed. -Lemma covarianceZr a (X Y : {RV P >-> R}) : - P.-integrable setT (EFin \o X) -> - P.-integrable setT (EFin \o Y) -> - P.-integrable setT (EFin \o (X * Y)%R) -> +Lemma covarianceZr a (X Y : T -> R) : + X \in lfun P 1 -> Y \in lfun P 1 -> + (X * Y)%R \in lfun P 1 -> covariance P X (a \o* Y)%R = a%:E * covariance P X Y. Proof. move=> X1 Y1 XY1. by rewrite [in RHS]covarianceC covarianceC covarianceZl; last rewrite mulrC. Qed. -Lemma covarianceNl (X Y : {RV P >-> R}) : - P.-integrable setT (EFin \o X) -> - P.-integrable setT (EFin \o Y) -> - P.-integrable setT (EFin \o (X * Y)%R) -> +Lemma covarianceNl (X Y : T -> R) : + X \in lfun P 1 -> Y \in lfun P 1 -> + (X * Y)%R \in lfun P 1 -> covariance P (\- X)%R Y = - covariance P X Y. Proof. move=> X1 Y1 XY1. @@ -420,76 +411,66 @@ have -> : (\- X = -1 \o* X)%R by apply/funeqP => x /=; rewrite mulrN mulr1. by rewrite covarianceZl// EFinN mulNe mul1e. Qed. -Lemma covarianceNr (X Y : {RV P >-> R}) : - P.-integrable setT (EFin \o X) -> - P.-integrable setT (EFin \o Y) -> - P.-integrable setT (EFin \o (X * Y)%R) -> +Lemma covarianceNr (X Y : T -> R) : + X \in lfun P 1 -> Y \in lfun P 1 -> + (X * Y)%R \in lfun P 1 -> covariance P X (\- Y)%R = - covariance P X Y. Proof. by move=> X1 Y1 XY1; rewrite !(covarianceC X) covarianceNl 1?mulrC. Qed. -Lemma covarianceNN (X Y : {RV P >-> R}) : - P.-integrable setT (EFin \o X) -> - P.-integrable setT (EFin \o Y) -> - P.-integrable setT (EFin \o (X * Y)%R) -> +Lemma covarianceNN (X Y : T -> R) : + X \in lfun P 1 -> Y \in lfun P 1 -> + (X * Y)%R \in lfun P 1 -> covariance P (\- X)%R (\- Y)%R = covariance P X Y. Proof. -move=> X1 Y1 XY1. -have NY : P.-integrable setT (EFin \o (\- Y)%R) by rewrite compreN ?integrableN. -by rewrite covarianceNl ?covarianceNr ?oppeK//= mulrN compreN ?integrableN. +by move=> ? ? ?; rewrite covarianceNl//= ?covarianceNr ?oppeK ?mulrN//= ?rpredN. Qed. -Lemma covarianceDl (X Y Z : {RV P >-> R}) : - P.-integrable setT (EFin \o X) -> P.-integrable setT (EFin \o (X ^+ 2)%R) -> - P.-integrable setT (EFin \o Y) -> P.-integrable setT (EFin \o (Y ^+ 2)%R) -> - P.-integrable setT (EFin \o Z) -> P.-integrable setT (EFin \o (Z ^+ 2)%R) -> - P.-integrable setT (EFin \o (X * Z)%R) -> - P.-integrable setT (EFin \o (Y * Z)%R) -> +Lemma covarianceDl (X Y Z : T -> R) : + X \in lfun P 2%:E -> Y \in lfun P 2%:E -> Z \in lfun P 2%:E -> covariance P (X \+ Y)%R Z = covariance P X Z + covariance P Y Z. Proof. -move=> X1 X2 Y1 Y2 Z1 Z2 XZ1 YZ1. -rewrite [LHS]covarianceE//= ?mulrDl ?compreDr// ?integrableD//. -rewrite 2?expectationD//=. +move=> X2 Y2 Z2. +have Pfin : P setT \is a fin_num := fin_num_measure P _ measurableT. +have X1 := lfun_inclusion12 Pfin X2. +have Y1 := lfun_inclusion12 Pfin Y2. +have Z1 := lfun_inclusion12 Pfin Z2. +have XY1 := lfun2M2_1 X2 Y2. +have YZ1 := lfun2M2_1 Y2 Z2. +have XZ1 := lfun2M2_1 X2 Z2. +rewrite [LHS]covarianceE//= ?mulrDl ?compreDr ?rpredD//= 2?expectationD//=. rewrite muleDl ?fin_num_adde_defr ?expectation_fin_num//. rewrite oppeD ?fin_num_adde_defr ?fin_numM ?expectation_fin_num//. by rewrite addeACA 2?covarianceE. Qed. -Lemma covarianceDr (X Y Z : {RV P >-> R}) : - P.-integrable setT (EFin \o X) -> P.-integrable setT (EFin \o (X ^+ 2)%R) -> - P.-integrable setT (EFin \o Y) -> P.-integrable setT (EFin \o (Y ^+ 2)%R) -> - P.-integrable setT (EFin \o Z) -> P.-integrable setT (EFin \o (Z ^+ 2)%R) -> - P.-integrable setT (EFin \o (X * Y)%R) -> - P.-integrable setT (EFin \o (X * Z)%R) -> +Lemma covarianceDr (X Y Z : T -> R) : + X \in lfun P 2%:E -> Y \in lfun P 2%:E -> Z \in lfun P 2%:E -> covariance P X (Y \+ Z)%R = covariance P X Y + covariance P X Z. Proof. -move=> X1 X2 Y1 Y2 Z1 Z2 XY1 XZ1. -by rewrite covarianceC covarianceDl ?(covarianceC X) 1?mulrC. +by move=> X2 Y2 Z2; rewrite covarianceC covarianceDl ?(covarianceC X) 1?mulrC. Qed. -Lemma covarianceBl (X Y Z : {RV P >-> R}) : - P.-integrable setT (EFin \o X) -> P.-integrable setT (EFin \o (X ^+ 2)%R) -> - P.-integrable setT (EFin \o Y) -> P.-integrable setT (EFin \o (Y ^+ 2)%R) -> - P.-integrable setT (EFin \o Z) -> P.-integrable setT (EFin \o (Z ^+ 2)%R) -> - P.-integrable setT (EFin \o (X * Z)%R) -> - P.-integrable setT (EFin \o (Y * Z)%R) -> +Lemma covarianceBl (X Y Z : T -> R) : + X \in lfun P 2%:E -> Y \in lfun P 2%:E -> Z \in lfun P 2%:E -> covariance P (X \- Y)%R Z = covariance P X Z - covariance P Y Z. Proof. -move=> X1 X2 Y1 Y2 Z1 Z2 XZ1 YZ1. -rewrite -[(X \- Y)%R]/(X \+ (\- Y))%R covarianceDl ?covarianceNl//=. -- by rewrite compreN// integrableN. -- by rewrite mulrNN. -- by rewrite mulNr compreN// integrableN. +move=> X2 Y2 Z2. +have Pfin : P setT \is a fin_num := fin_num_measure P _ measurableT. +have Y1 := lfun_inclusion12 Pfin Y2. +have Z1 := lfun_inclusion12 Pfin Z2. +have YZ1 := lfun2M2_1 Y2 Z2. +by rewrite -[(X \- Y)%R]/(X \+ (\- Y))%R covarianceDl ?covarianceNl ?rpredN. Qed. -Lemma covarianceBr (X Y Z : {RV P >-> R}) : - P.-integrable setT (EFin \o X) -> P.-integrable setT (EFin \o (X ^+ 2)%R) -> - P.-integrable setT (EFin \o Y) -> P.-integrable setT (EFin \o (Y ^+ 2)%R) -> - P.-integrable setT (EFin \o Z) -> P.-integrable setT (EFin \o (Z ^+ 2)%R) -> - P.-integrable setT (EFin \o (X * Y)%R) -> - P.-integrable setT (EFin \o (X * Z)%R) -> +Lemma covarianceBr (X Y Z : T -> R) : + X \in lfun P 2%:E -> Y \in lfun P 2%:E -> Z \in lfun P 2%:E -> covariance P X (Y \- Z)%R = covariance P X Y - covariance P X Z. Proof. -move=> X1 X2 Y1 Y2 Z1 Z2 XY1 XZ1. +move=> X2 Y2 Z2. +have Pfin : P setT \is a fin_num := fin_num_measure P _ measurableT. +have Y1 := lfun_inclusion12 Pfin Y2. +have Z1 := lfun_inclusion12 Pfin Z2. +have YZ1 := lfun2M2_1 Y2 Z2. by rewrite !(covarianceC X) covarianceBl 1?(mulrC _ X). Qed. @@ -502,19 +483,23 @@ Context d (T : measurableType d) (R : realType) (P : probability T R). Definition variance (X : T -> R) := covariance P X X. Local Notation "''V_' P [ X ]" := (variance X). -Lemma varianceE (X : {RV P >-> R}) : - P.-integrable setT (EFin \o X) -> P.-integrable setT (EFin \o (X ^+ 2)%R) -> +Lemma varianceE (X : T -> R) : X \in lfun P 2%:E -> 'V_P[X] = 'E_P[X ^+ 2] - ('E_P[X]) ^+ 2. -Proof. by move=> X1 X2; rewrite /variance covarianceE. Qed. +Proof. +move=> X2. +by rewrite /variance covarianceE ?lfun2M2_1// lfun_inclusion12 ?fin_num_measure. +Qed. -Lemma variance_fin_num (X : {RV P >-> R}) : - P.-integrable setT (EFin \o X) -> P.-integrable setT (EFin \o X ^+ 2)%R -> +Lemma variance_fin_num (X : T -> R) : X \in lfun P 2%:E -> 'V_P[X] \is a fin_num. -Proof. by move=> /[dup]; apply: covariance_fin_num. Qed. +Proof. +move=> X2. +by rewrite covariance_fin_num ?lfun2M2_1// lfun_inclusion12 ?fin_num_measure. +Qed. -Lemma variance_ge0 (X : {RV P >-> R}) : (0 <= 'V_P[X])%E. +Lemma variance_ge0 (X : T -> R) : 0 <= 'V_P[X]. Proof. -by rewrite /variance unlock; apply: expectation_ge0 => x; apply: sqr_ge0. +by rewrite /variance unlock; apply: expectation_ge0 => x; exact: sqr_ge0. Qed. Lemma variance_cst r : 'V_P[cst r] = 0%E. @@ -524,107 +509,89 @@ rewrite [X in 'E_P[X]](_ : _ = cst 0%R) ?expectation_cst//. by apply/funext => x; rewrite /GRing.exp/GRing.mul/= subrr mulr0. Qed. -Lemma varianceZ a (X : {RV P >-> R}) : - P.-integrable setT (EFin \o X) -> P.-integrable setT (EFin \o (X ^+ 2)%R) -> +Lemma varianceZ a (X : T -> R) : X \in lfun P 2%:E -> 'V_P[(a \o* X)%R] = (a ^+ 2)%:E * 'V_P[X]. Proof. -move=> X1 X2; rewrite /variance covarianceZl//=. -- by rewrite covarianceZr// muleA. -- by rewrite compre_scale// integrableZl. -- rewrite [X in EFin \o X](_ : _ = (a \o* X ^+ 2)%R); last first. - by apply/funeqP => x; rewrite mulrA. - by rewrite compre_scale// integrableZl. +move=> X2. +have Pfin : P setT \is a fin_num := fin_num_measure P _ measurableT. +have X1 := lfun_inclusion12 Pfin X2. +rewrite /variance covarianceZl//=. +- by rewrite covarianceZr// ?muleA ?EFinM// lfun2M2_1. +- by rewrite lfunp_scale. +- by rewrite lfun2M2_1// lfunp_scale// ler1n. Qed. -Lemma varianceN (X : {RV P >-> R}) : - P.-integrable setT (EFin \o X) -> P.-integrable setT (EFin \o (X ^+ 2)%R) -> - 'V_P[(\- X)%R] = 'V_P[X]. -Proof. by move=> X1 X2; rewrite /variance covarianceNN. Qed. +Lemma varianceN (X : T -> R) : X \in lfun P 2%:E -> 'V_P[(\- X)%R] = 'V_P[X]. +Proof. +move=> X2. +by rewrite /variance covarianceNN ?lfun2M2_1 ?lfun_inclusion12 ?fin_num_measure. +Qed. -Lemma varianceD (X Y : {RV P >-> R}) : - P.-integrable setT (EFin \o X) -> P.-integrable setT (EFin \o (X ^+ 2)%R) -> - P.-integrable setT (EFin \o Y) -> P.-integrable setT (EFin \o (Y ^+ 2)%R) -> - P.-integrable setT (EFin \o (X * Y)%R) -> +Lemma varianceD (X Y : T -> R) : X \in lfun P 2%:E -> Y \in lfun P 2%:E -> 'V_P[X \+ Y]%R = 'V_P[X] + 'V_P[Y] + 2%:E * covariance P X Y. Proof. -move=> X1 X2 Y1 Y2 XY1. +move=> X2 Y2. +have Pfin : P setT \is a fin_num := fin_num_measure P _ measurableT. +have X1 := lfun_inclusion12 Pfin X2. +have Y1 := lfun_inclusion12 Pfin Y2. +have XY1 := lfun2M2_1 X2 Y2. rewrite -['V_P[_]]/(covariance P (X \+ Y)%R (X \+ Y)%R). -have XY : P.-integrable [set: T] (EFin \o (X \+ Y)%R). - by rewrite compreDr// integrableD. -rewrite covarianceDl//=; last 3 first. -- rewrite -expr2 sqrrD compreDr ?integrableD// compreDr// integrableD//. - rewrite -mulr_natr -[(_ * 2)%R]/(2 \o* (X * Y))%R compre_scale//. - exact: integrableZl. -- by rewrite mulrDr compreDr ?integrableD. -- by rewrite mulrDr mulrC compreDr ?integrableD. -rewrite covarianceDr// covarianceDr; [|by []..|by rewrite mulrC |exact: Y2]. +rewrite covarianceDl ?rpredD ?lee1n//= covarianceDr// covarianceDr//. rewrite (covarianceC P Y X) [LHS]addeA [LHS](ACl (1*4*(2*3)))/=. by rewrite -[2%R]/(1 + 1)%R EFinD muleDl ?mul1e// covariance_fin_num. Qed. -Lemma varianceB (X Y : {RV P >-> R}) : - P.-integrable setT (EFin \o X) -> P.-integrable setT (EFin \o (X ^+ 2)%R) -> - P.-integrable setT (EFin \o Y) -> P.-integrable setT (EFin \o (Y ^+ 2)%R) -> - P.-integrable setT (EFin \o (X * Y)%R) -> +Lemma varianceB (X Y : T -> R) : X \in lfun P 2%:E -> Y \in lfun P 2%:E -> 'V_P[(X \- Y)%R] = 'V_P[X] + 'V_P[Y] - 2%:E * covariance P X Y. Proof. -move=> X1 X2 Y1 Y2 XY1. +move=> X2 Y2. +have Pfin : P setT \is a fin_num := fin_num_measure P _ measurableT. +have X1 := lfun_inclusion12 Pfin X2. +have Y1 := lfun_inclusion12 Pfin Y2. +have XY1 := lfun2M2_1 X2 Y2. rewrite -[(X \- Y)%R]/(X \+ (\- Y))%R. -rewrite varianceD/= ?varianceN ?covarianceNr ?muleN//. -- by rewrite compreN ?integrableN. -- by rewrite mulrNN. -- by rewrite mulrN compreN ?integrableN. +by rewrite varianceD/= ?varianceN ?covarianceNr ?muleN ?rpredN. Qed. -Lemma varianceD_cst_l c (X : {RV P >-> R}) : - P.-integrable setT (EFin \o X) -> P.-integrable setT (EFin \o (X ^+ 2)%R) -> +Lemma varianceD_cst_l c (X : T -> R) : X \in lfun P 2%:E -> 'V_P[(cst c \+ X)%R] = 'V_P[X]. Proof. -move=> X1 X2. -rewrite varianceD//=; last 3 first. -- exact: finite_measure_integrable_cst. -- by rewrite compre_scale// integrableZl// finite_measure_integrable_cst. -- by rewrite mulrC compre_scale ?integrableZl. -by rewrite variance_cst add0e covariance_cst_l mule0 adde0. +move=> X2. +by rewrite varianceD ?lfun_cst// variance_cst add0e covariance_cst_l mule0 adde0. Qed. -Lemma varianceD_cst_r (X : {RV P >-> R}) c : - P.-integrable setT (EFin \o X) -> P.-integrable setT (EFin \o (X ^+ 2)%R) -> +Lemma varianceD_cst_r (X : T -> R) c : X \in lfun P 2%:E -> 'V_P[(X \+ cst c)%R] = 'V_P[X]. Proof. -move=> X1 X2. +move=> X2. have -> : (X \+ cst c = cst c \+ X)%R by apply/funeqP => x /=; rewrite addrC. exact: varianceD_cst_l. Qed. -Lemma varianceB_cst_l c (X : {RV P >-> R}) : - P.-integrable setT (EFin \o X) -> P.-integrable setT (EFin \o (X ^+ 2)%R) -> +Lemma varianceB_cst_l c (X : T -> R) : X \in lfun P 2%:E -> 'V_P[(cst c \- X)%R] = 'V_P[X]. Proof. -move=> X1 X2. -rewrite -[(cst c \- X)%R]/(cst c \+ (\- X))%R varianceD_cst_l/=; last 2 first. -- by rewrite compreN ?integrableN. -- by rewrite mulrNN; apply: X2. -by rewrite varianceN. +move=> X2; rewrite -[(cst c \- X)%R]/(cst c \+ (\- X))%R. +by rewrite varianceD_cst_l/= ?rpredN// varianceN. Qed. -Lemma varianceB_cst_r (X : {RV P >-> R}) c : - P.-integrable setT (EFin \o X) -> P.-integrable setT (EFin \o (X ^+ 2)%R) -> +Lemma varianceB_cst_r (X : T -> R) c : X \in lfun P 2%:E -> 'V_P[(X \- cst c)%R] = 'V_P[X]. Proof. -by move=> X1 X2; rewrite -[(X \- cst c)%R]/(X \+ (cst (- c)))%R varianceD_cst_r. +by move=> X2; rewrite -[(X \- cst c)%R]/(X \+ (cst (- c)))%R varianceD_cst_r. Qed. -Lemma covariance_le (X Y : {RV P >-> R}) : - P.-integrable setT (EFin \o X) -> P.-integrable setT (EFin \o (X ^+ 2)%R) -> - P.-integrable setT (EFin \o Y) -> P.-integrable setT (EFin \o (Y ^+ 2)%R) -> - P.-integrable setT (EFin \o (X * Y)%R) -> +Lemma covariance_le (X Y : T -> R) : X \in lfun P 2%:E -> Y \in lfun P 2%:E -> covariance P X Y <= sqrte 'V_P[X] * sqrte 'V_P[Y]. Proof. -move=> X1 X2 Y1 Y2 XY1. +move=> X2 Y2. +have Pfin : P setT \is a fin_num := fin_num_measure P _ measurableT. +have X1 := lfun_inclusion12 Pfin X2. +have Y1 := lfun_inclusion12 Pfin Y2. +have XY1 := lfun2M2_1 X2 Y2. rewrite -sqrteM ?variance_ge0//. rewrite lee_sqrE ?sqrte_ge0// sqr_sqrte ?mule_ge0 ?variance_ge0//. -rewrite -(fineK (variance_fin_num X1 X2)) -(fineK (variance_fin_num Y1 Y2)). +rewrite -(fineK (variance_fin_num X2)) -(fineK (variance_fin_num Y2)). rewrite -(fineK (covariance_fin_num X1 Y1 XY1)). rewrite -EFin_expe -EFinM lee_fin -(@ler_pM2l _ 4) ?ltr0n// [leRHS]mulrA. rewrite [in leLHS](_ : 4 = 2 * 2)%R -natrM// [in leLHS]natrM mulrACA -expr2. @@ -642,10 +609,7 @@ rewrite -lee_fin !EFinD EFinM fineK ?variance_fin_num// muleC -varianceZ//. rewrite 2!EFinM ?fineK ?variance_fin_num// ?covariance_fin_num//. rewrite -muleA [_ * r%:E]muleC -covarianceZl//. rewrite addeAC -varianceD ?variance_ge0//=. -- by rewrite compre_scale ?integrableZl. -- rewrite [X in EFin \o X](_ : _ = r ^+2 \o* X ^+ 2)%R 1?mulrACA//. - by rewrite compre_scale ?integrableZl. -- by rewrite -mulrAC compre_scale// integrableZl. +by rewrite lfunp_scale// ler1n. Qed. End variance. @@ -655,8 +619,7 @@ Section markov_chebyshev_cantelli. Local Open Scope ereal_scope. Context d (T : measurableType d) (R : realType) (P : probability T R). -Lemma markov (X : {RV P >-> R}) (f : R -> R) (eps : R) : - (0 < eps)%R -> +Lemma markov (X : {RV P >-> R}) (f : R -> R) (eps : R) : (0 < eps)%R -> measurable_fun [set: R] f -> (forall r, 0 <= r -> 0 <= f r)%R -> {in Num.nneg &, {homo f : x y / x <= y}}%R -> (f eps)%:E * P [set x | eps%:E <= `| (X x)%:E | ] <= @@ -673,7 +636,7 @@ apply: (le_trans (@le_integral_comp_abse _ _ _ P _ measurableT (EFin \o X) - by rewrite unlock. Qed. -Definition mmt_gen_fun (X : {RV P >-> R}) (t : R) := 'E_P[expR \o t \o* X]. +Definition mmt_gen_fun (X : T -> R) (t : R) := 'E_P[expR \o t \o* X]. Local Notation "'M_ X t" := (mmt_gen_fun X t). Lemma chernoff (X : {RV P >-> R}) (r a : R) : (0 < r)%R -> @@ -715,58 +678,34 @@ by move=> /le_trans; apply; rewrite /variance [in leRHS]unlock. Qed. Lemma cantelli (X : {RV P >-> R}) (lambda : R) : - P.-integrable setT (EFin \o X) -> P.-integrable setT (EFin \o (X ^+ 2)%R) -> - (0 < lambda)%R -> + (X : T -> R) \in lfun P 2%:E -> (0 < lambda)%R -> P [set x | lambda%:E <= (X x)%:E - 'E_P[X]] <= (fine 'V_P[X] / (fine 'V_P[X] + lambda^2))%:E. Proof. -move=> X1 X2 lambda_gt0. -have finEK : (fine 'E_P[X])%:E = 'E_P[X]. - by rewrite fineK ?unlock ?integral_fune_fin_num. +move=> /[dup] X2. +move=> /(lfun_inclusion12 (fin_num_measure P _ measurableT)) X1 lambda_gt0. +have finEK : (fine 'E_P[X])%:E = 'E_P[X] by rewrite fineK ?expectation_fin_num. have finVK : (fine 'V_P[X])%:E = 'V_P[X] by rewrite fineK ?variance_fin_num. pose Y := (X \- cst (fine 'E_P[X]))%R. -have Y1 : P.-integrable [set: T] (EFin \o Y). - rewrite compreBr => [|//]; apply: integrableB X1 _ => [//|]. - exact: finite_measure_integrable_cst. -have Y2 : P.-integrable [set: T] (EFin \o (Y ^+ 2)%R). - rewrite sqrrD/= compreDr => [|//]. - apply: integrableD => [//||]; last first. - rewrite -[(_ ^+ 2)%R]/(cst ((- fine 'E_P[X]) ^+ 2)%R). - exact: finite_measure_integrable_cst. - rewrite compreDr => [|//]; apply: integrableD X2 _ => [//|]. - rewrite [X in EFin \o X](_ : _ = (- fine 'E_P[X] * 2) \o* X)%R; last first. - by apply/funeqP => x /=; rewrite -mulr_natl mulrC mulrA. - by rewrite compre_scale => [|//]; apply: integrableZl X1. +have Y2 : (Y : T -> R) \in lfun P 2%:E. + by rewrite /Y rpredB ?lee1n//= => _; rewrite lfun_cst. have EY : 'E_P[Y] = 0. - rewrite expectationB/= ?finite_measure_integrable_cst//. - rewrite expectation_cst finEK subee//. - by rewrite unlock; apply: integral_fune_fin_num X1. + rewrite expectationB ?lfun_cst//= expectation_cst. + by rewrite finEK subee// expectation_fin_num. have VY : 'V_P[Y] = 'V_P[X] by rewrite varianceB_cst_r. have le (u : R) : (0 <= u)%R -> P [set x | lambda%:E <= (X x)%:E - 'E_P[X]] <= ((fine 'V_P[X] + u^2) / (lambda + u)^2)%:E. move=> uge0; rewrite EFinM. - have YU1 : P.-integrable [set: T] (EFin \o (Y \+ cst u)%R). - rewrite compreDr => [|//]; apply: integrableD Y1 _ => [//|]. - exact: finite_measure_integrable_cst. - have YU2 : P.-integrable [set: T] (EFin \o ((Y \+ cst u) ^+ 2)%R). - rewrite sqrrD/= compreDr => [|//]. - apply: integrableD => [//||]; last first. - rewrite -[(_ ^+ 2)%R]/(cst (u ^+ 2))%R. - exact: finite_measure_integrable_cst. - rewrite compreDr => [|//]; apply: integrableD Y2 _ => [//|]. - rewrite [X in EFin \o X](_ : _ = (2 * u) \o* Y)%R; last first. - by apply/funeqP => x /=; rewrite -mulr_natl mulrCA. - by rewrite compre_scale => [|//]; apply: integrableZl Y1. have -> : (fine 'V_P[X] + u^2)%:E = 'E_P[(Y \+ cst u)^+2]%R. rewrite -VY -[RHS](@subeK _ _ (('E_P[(Y \+ cst u)%R])^+2)); last first. - by rewrite fin_numX ?unlock ?integral_fune_fin_num. - rewrite -varianceE/= -/Y -?expe2//. - rewrite expectationD/= ?EY ?add0e ?expectation_cst -?EFinM; last 2 first. - - rewrite compreBr => [|//]; apply: integrableB X1 _ => [//|]. - exact: finite_measure_integrable_cst. - - exact: finite_measure_integrable_cst. - by rewrite (varianceD_cst_r _ Y1 Y2) EFinD fineK ?(variance_fin_num Y1 Y2). + rewrite fin_numX// expectation_fin_num//= rpredD ?lfun_cst//. + by rewrite rpredB// lfun_cst. + rewrite -varianceE/=; last first. + by rewrite rpredD ?lee1n//= => _; rewrite lfun_cst. + rewrite -expe2 expectationD/= ?lfun_cst//; last by rewrite rpredB ?lfun_cst. + rewrite EY// add0e expectation_cst -EFinM. + by rewrite (varianceD_cst_r _ Y2) EFinD fineK ?variance_fin_num. have le : [set x | lambda%:E <= (X x)%:E - 'E_P[X]] `<=` [set x | ((lambda + u)^2)%:E <= ((Y x + u)^+2)%:E]. move=> x /= le; rewrite lee_fin; apply: lerXn2r. @@ -776,7 +715,7 @@ have le (u : R) : (0 <= u)%R -> - by rewrite lerD2r -lee_fin EFinB finEK. apply: (le_trans (le_measure _ _ _ le)). - rewrite -[[set _ | _]]setTI inE; apply: emeasurable_fun_c_infty => [//|]. - by apply: emeasurable_funB => //; exact: measurable_int X1. + by apply: emeasurable_funB=> //; apply/measurable_int/(lfun1_integrable X1). - rewrite -[[set _ | _]]setTI inE; apply: emeasurable_fun_c_infty => [//|]. rewrite measurable_EFinP [X in measurable_fun _ X](_ : _ = (fun x => x ^+ 2) \o (fun x => Y x + u))%R//. diff --git a/theories/topology_theory/nat_topology.v b/theories/topology_theory/nat_topology.v index 79bc3a1b39..e542829ae1 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. From af695f8faef155e9ddf759f30ef30d9b7b6623b4 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Thu, 15 May 2025 16:35:40 +0900 Subject: [PATCH 02/13] changelog --- CHANGELOG_UNRELEASED.md | 52 +++++++++++++++++++++++++++++++++++++++++ 1 file changed, 52 insertions(+) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 699bb89453..590e60513a 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -88,6 +88,44 @@ + lemmas `ess_infr_bounded`, `ess_infrZl`, `ess_inf_ger`, `ess_inf_ler`, `ess_inf_cstr` +- in `simple_functions.v`: + + lemma `mfunMn` + +- in `hoelder.v` + + lemmas `Lnorm0`, `Lnorm_cst1` + + definition `conjugate` + + lemma `conjugateE` + + lemmas `lerB_DLnorm`, `lerB_LnormD`, `eminkowski` + + definition `finite_norm` + + mixin `isLfun` with field `lfuny` + + structure `Lfun` + + notation `LfunType` + + definition `Lequiv` + + canonical `Lequiv_canonical` + + definition `LspaceType` + + lemma `LequivP` + + record `LType` + + coercion `LfunType_of_LType` + + definition `Lspace` with notation `mu.-Lspace p` + + lemma `lfun_integrable`, `lfun1_integrable`, `lfun2_integrable_sqr`, `lfun2M2_1` + + lemma `lfunp_scale`, `lfun_cst`, + + definitions `finlfun`, `lfun`, `lfun_key` + + canonical `lfun_keyed` + + lemmas `sub_lfun_mfun`, `sub_lfun_finlfun` + + definition `lfun_Sub` + + lemmas `lfun_rect`, `lfun_valP`, `lfuneqP`, `lfuny0`, `mfunP`, `lfunP`, + `mfun_scaler_closed` + + lemmas `LnormZ`, `lfun_submod_closed` + + lemmas `finite_norm_fine`, `ler_LnormD`, + `LnormrN`, `fine_Lnormr_eq0` + + lemma `fine_Lnormr_eq0` + + lemma `lfun_inclusion`, `lfun_inclusion12` + + lemma `lfun_oppr_closed` + + lemma `lfun_addr_closed` + + lemmas `poweR_Lnorm`, `oppe_Lnorm` + +### Changed + - in `measure.v`: + notation `{ae mu, P}` (near use `{near _, _}` notation) + definition `ae_eq` @@ -126,6 +164,8 @@ + HB class `UniformZmodule` moved to `PreUniformZmodule` + HB class `UniformLmodule` moved to `PreUniformLmodule` +- in `hoelder.v`: + + `minkowski` -> `minkowski_EFin` ### Generalized @@ -133,6 +173,18 @@ + `derive_cst`, `derive1_cst` - in `convex.v` + parameter `R` of `convType` from `realDomainType` to `numDomainType` +- in `hoelder.v`: + + definition `Lnorm` generalized to functions with codomain `\bar R` + (this impacts the notation `'N_p[f]`) + + lemmas `Lnorm1`, `eq_Lnorm` (from `f : _ -> R` to `f : _ -> \bar R`) + +- in `probability.v` + + lemma `cantelli` + + lemmas `expectation_fin_num`, `expectationZl`, `expectationD`, `expectationB`, `expectation_sum`, + `covarianceE`, `covariance_fin_num`, `covarianceZl`, `covarianceZr`, `covarianceNl`, + `covarianceNr`, `covarianceNN`, `covarianceDl`, `covarianceDr`, `covarianceBl`, `covarianceBr`, + `varianceE`, `variance_fin_num`, `varianceZ`, `varianceN`, `varianceD`, `varianceB`, + `varianceD_cst_l`, `varianceD_cst_r`, `varianceB_cst_l`, `varianceB_cst_r`, `covariance_le` ### Deprecated From 9c4d726e7940563f5031e08041145c669d259e96 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Thu, 15 May 2025 17:33:38 +0900 Subject: [PATCH 03/13] minor generalization --- CHANGELOG_UNRELEASED.md | 1 + theories/hoelder.v | 3 +-- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 590e60513a..a4aac2d4ca 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -123,6 +123,7 @@ + lemma `lfun_oppr_closed` + lemma `lfun_addr_closed` + lemmas `poweR_Lnorm`, `oppe_Lnorm` + + lemma `integrable_poweR` ### Changed diff --git a/theories/hoelder.v b/theories/hoelder.v index b2aaaf2678..13aa9daa54 100644 --- a/theories/hoelder.v +++ b/theories/hoelder.v @@ -162,8 +162,7 @@ case: p => [r||//]. 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. +Lemma powR_Lnorm f r : r != 0%R -> 'N_r%:E[f] `^ r = \int[mu]_x `| f x | `^ r. Proof. by move=> r0; rewrite poweR_Lnorm. Qed. End Lnorm_properties. From 40dd22fa0c4049724bfd7ec0e619a6ff2a0812f5 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Sat, 17 May 2025 22:27:08 +0900 Subject: [PATCH 04/13] to please the CI --- theories/hoelder.v | 11 ++++++++--- 1 file changed, 8 insertions(+), 3 deletions(-) diff --git a/theories/hoelder.v b/theories/hoelder.v index 13aa9daa54..a2f538b3c2 100644 --- a/theories/hoelder.v +++ b/theories/hoelder.v @@ -618,7 +618,8 @@ rewrite (_ : f = ((f \+ g) \+ (-%R \o g))%R); last first. rewrite [X in _ <= 'N__[X] + _](_ : _ = (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 (_ : _ \o _ = \- (EFin \o g))// oppe_Lnorm. + rewrite (_ : _ \o _ = \- (EFin \o g))//. + exact/esym/oppe_Lnorm. by apply: minkowski_EFin => //; [exact: measurable_funD|exact: measurableT_comp]. Qed. @@ -806,7 +807,8 @@ Lemma lfun_oppr_closed : oppr_closed lfun. Proof. move=> f /andP[mf /[!inE] lf]. rewrite rpredN/= mf/= inE/= /finite_norm. -by rewrite (_ : _ \o _ = \- (EFin \o f))%E// oppe_Lnorm. +rewrite (_ : _ \o _ = \- (EFin \o f))%E//. +by rewrite (oppe_Lnorm _ (EFin \o f)). Qed. HB.instance Definition _ := GRing.isOppClosed.Build _ lfun @@ -893,7 +895,10 @@ Lemma ler_LnormD (f g : ty) : nm (f + g) <= nm f + nm g. Proof. by rewrite -lee_fin EFinD !finite_norm_fine eminkowski. Qed. Lemma LnormrN (f : ty) : nm (\-f) = nm f. -Proof. by rewrite /nm (_ : _ \o _ = \- (EFin \o f))%E// oppe_Lnorm. Qed. +Proof. +rewrite /nm (_ : _ \o _ = \- (EFin \o f))%E//; congr fine. +exact: oppe_Lnorm. +Qed. Lemma Lnormr_natmul (f : ty) k : nm (f *+ k) = nm f *+ k. Proof. From c06a6ab9970b9853aae5c5894c135a68a11f127b Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Thu, 29 May 2025 18:31:44 +0900 Subject: [PATCH 05/13] rename `lfun` pred into `Lfun` --- CHANGELOG_UNRELEASED.md | 26 +++--- theories/hoelder.v | 170 +++++++++++++++++++-------------------- theories/probability.v | 174 ++++++++++++++++++++-------------------- 3 files changed, 182 insertions(+), 188 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index a4aac2d4ca..e5134ad87f 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -97,8 +97,8 @@ + lemma `conjugateE` + lemmas `lerB_DLnorm`, `lerB_LnormD`, `eminkowski` + definition `finite_norm` - + mixin `isLfun` with field `lfuny` - + structure `Lfun` + + mixin `isLfunction` with field `Lfunction_finite` + + structure `Lfunction` + notation `LfunType` + definition `Lequiv` + canonical `Lequiv_canonical` @@ -107,21 +107,21 @@ + record `LType` + coercion `LfunType_of_LType` + definition `Lspace` with notation `mu.-Lspace p` - + lemma `lfun_integrable`, `lfun1_integrable`, `lfun2_integrable_sqr`, `lfun2M2_1` - + lemma `lfunp_scale`, `lfun_cst`, - + definitions `finlfun`, `lfun`, `lfun_key` - + canonical `lfun_keyed` - + lemmas `sub_lfun_mfun`, `sub_lfun_finlfun` - + definition `lfun_Sub` - + lemmas `lfun_rect`, `lfun_valP`, `lfuneqP`, `lfuny0`, `mfunP`, `lfunP`, + + lemma `Lfun_integrable`, `Lfun1_integrable`, `Lfun2_integrable_sqr`, `Lfun2_mul_Lfun1` + + lemma `Lfun_scale`, `Lfun_cst`, + + definitions `finLfun`, `Lfun`, `Lfun_key` + + canonical `Lfun_keyed` + + lemmas `sub_Lfun_mfun`, `sub_Lfun_finLfun` + + definition `Lfun_Sub` + + lemmas `Lfun_rect`, `Lfun_valP`, `LfuneqP`, `finite_norm_cst0`, `mfunP`, `LfunP`, `mfun_scaler_closed` - + lemmas `LnormZ`, `lfun_submod_closed` + + lemmas `LnormZ`, `Lfun_submod_closed` + lemmas `finite_norm_fine`, `ler_LnormD`, `LnormrN`, `fine_Lnormr_eq0` + lemma `fine_Lnormr_eq0` - + lemma `lfun_inclusion`, `lfun_inclusion12` - + lemma `lfun_oppr_closed` - + lemma `lfun_addr_closed` + + lemma `Lfun_subset`, `Lfun_subset12` + + lemma `Lfun_oppr_closed` + + lemma `Lfun_addr_closed` + lemmas `poweR_Lnorm`, `oppe_Lnorm` + lemma `integrable_poweR` diff --git a/theories/hoelder.v b/theories/hoelder.v index a2f538b3c2..7da1a99d3c 100644 --- a/theories/hoelder.v +++ b/theories/hoelder.v @@ -30,8 +30,8 @@ From mathcomp Require Import lebesgue_integral numfun exp convex. (* L-norm *) (* p1 is a proof that the extended real number p is *) (* greater or equal to 1. *) -(* The HB class is Lfun. *) -(* f \in lfun == holds for f : LfunType mu p1 *) +(* The HB class is Lfunction. *) +(* f \in Lfun == holds for f : LfunType mu p1 *) (* Lequiv f g == f is equal to g almost everywhere *) (* The functions f and g have type LfunType mu p1. *) (* Lequiv is made a canonical equivalence relation. *) @@ -619,7 +619,7 @@ rewrite [X in _ <= 'N__[X] + _](_ : _ = (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. rewrite (_ : _ \o _ = \- (EFin \o g))//. - exact/esym/oppe_Lnorm. + by have := oppe_Lnorm mu (EFin \o g) p%:E. by apply: minkowski_EFin => //; [exact: measurable_funD|exact: measurableT_comp]. Qed. @@ -655,29 +655,30 @@ 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) +HB.mixin Record isLfunction 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 + Lfunction_finite : finite_norm mu p f }. #[short(type=LfunType)] -HB.structure Definition Lfun d (T : measurableType d) (R : realType) +HB.structure Definition Lfunction 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}. + {f of @MeasurableFun d _ T R f & isLfunction 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. +Arguments Lfunction_finite {d} {T} {R} {mu} {p} _. +#[global] Hint Resolve Lfunction_finite : core. +#[global] Hint Extern 0 (@LfunType _ _ _ _ _) => + solve [apply: Lfunction_finite] : core. -Section Lfun_canonical. +Section LfunType_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. +End LfunType_canonical. Section Lequiv. Context d (T : measurableType d) (R : realType). @@ -738,90 +739,86 @@ HB.instance Definition _ := [SubZmodule_isSubLmodule of {mfun T >-> R} by <:]. End mfun_extra. -Section lfun_pred. +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}. +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}. +Lemma sub_Lfun_finLfun : {subset Lfun <= finLfun}. Proof. by move=> x /andP[]. Qed. -End lfun_pred. +End Lfun_pred. -Reserved Notation "[ 'lfun' 'of' f ]" - (at level 0, format "[ 'lfun' 'of' f ]"). -Notation "[ 'lfun' 'of' f ]" := [the LfunType _ _ of f] : form_scope. - -Section lfun. +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). +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)). -#[local] HB.instance Definition _ := lfun_Sub2_subproof. -Definition lfun_Sub := [lfun of f]. +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 := + @isLfunction.Build d T R mu p p1 f (set_mem (sub_Lfun_finLfun fP)). +#[local] HB.instance Definition _ := Lfun_Sub2_subproof. +Definition Lfun_Sub := [the LfunType _ _ of 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. +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 []. +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 :> (_ -> _). +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. + 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. +Lemma LfuneqP (f g : LfunType mu p1) : f = g <-> f =1 g. +Proof. by split=> [->//|fg]; exact/val_inj/funext. Qed. HB.instance Definition _ := [Choice of LfunType mu p1 by <:]. -Lemma lfuny0 : finite_norm mu p (cst 0). +Lemma finite_norm_cst0 : 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. +HB.instance Definition _ := + @isLfunction.Build d T R mu p p1 (cst 0) finite_norm_cst0. -Lemma lfunP (f : LfunType mu p1) : (f : T -> R) \in lfun. +Lemma LfunP (f : LfunType mu p1) : (f : T -> R) \in Lfun. Proof. exact: valP. Qed. -Lemma lfun_oppr_closed : oppr_closed lfun. +Lemma Lfun_oppr_closed : oppr_closed Lfun. Proof. move=> f /andP[mf /[!inE] lf]. rewrite rpredN/= mf/= inE/= /finite_norm. rewrite (_ : _ \o _ = \- (EFin \o f))%E//. -by rewrite (oppe_Lnorm _ (EFin \o f)). +by have -> := oppe_Lnorm mu (EFin \o f) p. Qed. -HB.instance Definition _ := GRing.isOppClosed.Build _ lfun - lfun_oppr_closed. +HB.instance Definition _ := GRing.isOppClosed.Build _ Lfun + Lfun_oppr_closed. (* NB: not used directly by HB.instance *) -Lemma lfun_addr_closed : addr_closed lfun. +Lemma Lfun_addr_closed : addr_closed Lfun. Proof. split. by rewrite inE rpred0/= inE/= /finite_norm/= Lnorm0. move=> f g /andP[mf /[!inE]/= lf] /andP[mg /[!inE]/= lg]. -rewrite rpredD//= inE/=. -rewrite /finite_norm. +rewrite rpredD//= inE/= /finite_norm. rewrite (le_lt_trans (@eminkowski _ _ _ mu f g p _ _ _))//. - by rewrite inE in mf. - by rewrite inE in mg. @@ -843,7 +840,8 @@ case: p p1 f => //[r r1 f|? f]. exact: measurableT_comp. apply: (@lty_poweRy _ _ r^-1). by rewrite gt_eqF// invr_gt0 ?(lt_le_trans ltr01). - rewrite [ltLHS](_ : _ = 'N[mu]_r%:E[EFin \o f]%E); first exact: (lfuny r1 f). + rewrite [ltLHS](_ : _ = 'N[mu]_r%:E[EFin \o f]%E). + exact: Lfunction_finite. rewrite unlock /Lnorm. by under eq_integral do rewrite gee0_abs ?lee_fin ?powR_ge0//. rewrite poweRM ?integral_ge0//. @@ -853,27 +851,27 @@ case: p p1 f => //[r r1 f|? f]. by rewrite normrZ EFinM. Qed. -Lemma lfun_submod_closed : submod_closed lfun. +Lemma Lfun_submod_closed : submod_closed Lfun. Proof. split. - by rewrite -[0]/(cst 0); exact: lfunP. + by 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 -[f]Lfun_valP -[g]Lfun_valP. +move: (Lfun_Sub _) (Lfun_Sub _) => {fP} f {gP} g. rewrite !inE rpredD ?rpredZ ?mfunP//=. apply: mem_set => /=; apply: (le_lt_trans (eminkowski _ _ _ _)) => //. - suff: a *: (g : T -> R) \in mfun by exact: set_mem. by rewrite rpredZ//; exact: mfunP. -- rewrite lte_add_pinfty//; last exact: lfuny. - by rewrite LnormZ lte_mul_pinfty// ?lee_fin//; exact: lfuny. +- rewrite lte_add_pinfty//; last exact: Lfunction_finite. + by rewrite LnormZ lte_mul_pinfty// ?lee_fin//; exact: Lfunction_finite. Qed. -HB.instance Definition _ := GRing.isSubmodClosed.Build _ _ lfun - lfun_submod_closed. +HB.instance Definition _ := GRing.isSubmodClosed.Build _ _ Lfun + Lfun_submod_closed. HB.instance Definition _ := [SubChoice_isSubLmodule of LfunType mu p1 by <:]. -End lfun. +End Lfun. Section Lspace_norm. Context d (T : measurableType d) (R : realType). @@ -888,7 +886,7 @@ Let nm f := fine ('N[mu]_p[EFin \o f]). Lemma finite_norm_fine (f : ty) : (nm f)%:E = 'N[mu]_p[EFin \o f]%E. Proof. rewrite /nm fineK// fin_numElt (lt_le_trans ltNy0) ?Lnorm_ge0//=. -exact: lfuny. +exact: Lfunction_finite. Qed. Lemma ler_LnormD (f g : ty) : nm (f + g) <= nm f + nm g. @@ -937,8 +935,8 @@ Definition LType1 := LType mu (@lexx _ _ 1%E). Definition LType2 := LType mu (lee1n 2). -Lemma lfun_integrable (f : T -> R) r : - 1 <= r -> f \in lfun mu r%:E -> +Lemma Lfun_integrable (f : T -> R) r : + 1 <= r -> f \in Lfun mu r%:E -> mu.-integrable setT (fun x => (`|f x| `^ r)%:E). Proof. rewrite inE => r0 /andP[/[!inE]/= mf] lpf. @@ -952,10 +950,10 @@ apply: le_lt_trans. by under eq_integral => x _ do rewrite gee0_abs ?lee_fin ?powR_ge0//. Qed. -Lemma lfun1_integrable (f : T -> R) : - f \in lfun mu 1 -> mu.-integrable setT (EFin \o f). +Lemma Lfun1_integrable (f : T -> R) : + f \in Lfun mu 1 -> mu.-integrable setT (EFin \o f). Proof. -move=> /[dup] lf /lfun_integrable => /(_ (lexx _)). +move=> /[dup] lf /Lfun_integrable => /(_ (lexx _)). under eq_fun => x do rewrite powRr1//. move/integrableP => [mf fley]. apply/integrableP; split. @@ -965,7 +963,7 @@ rewrite (le_lt_trans _ fley)//=. by under [leRHS]eq_integral => x _ do rewrite normr_id. Qed. -Lemma lfun2_integrable_sqr (f : T -> R) : f \in lfun mu 2%:E -> +Lemma Lfun2_integrable_sqr (f : T -> R) : f \in Lfun mu 2%:E -> mu.-integrable [set: T] (EFin \o (fun x => f x ^+ 2)). Proof. rewrite inE => /andP[mf]; rewrite inE/= => l2f. @@ -988,8 +986,8 @@ rewrite gt0_ler_poweR//. + by move=> t _/=; rewrite lee_fin normrX powR_mulrn. Qed. -Lemma lfun2M2_1 (f g : T -> R) : f \in lfun mu 2%:E -> g \in lfun mu 2%:E -> - f \* g \in lfun mu 1. +Lemma Lfun2_mul_Lfun1 (f g : T -> R) : f \in Lfun mu 2%:E -> g \in Lfun mu 2%:E -> + f \* g \in Lfun mu 1. Proof. move=> l2f l2g. move: (l2f) (l2g) => /[!inE] /andP[/[!inE]/= mf _] /andP[/[!inE]/= mg _]. @@ -1003,8 +1001,8 @@ by move: l2f; rewrite inE => /andP[_]; rewrite inE/=. by move: l2g; rewrite inE => /andP[_]; rewrite inE/=. Qed. -Lemma lfunp_scale (f : T -> R) a r : - 1 <= r -> f \in lfun mu r%:E -> a \o* f \in lfun mu r%:E. +Lemma Lfun_scale (f : T -> R) a r : + 1 <= r -> f \in Lfun mu r%:E -> a \o* f \in Lfun mu r%:E. Proof. move=> r1 /[dup] lf lpf. rewrite inE; apply/andP; split. @@ -1013,9 +1011,9 @@ rewrite inE; apply/andP; split. rewrite !inE/= /finite_norm unlock /Lnorm. rewrite poweR_lty//=. under eq_integral => x _ do rewrite normrM powRM// EFinM. -rewrite integralZr// ?lfun_integrable//. +rewrite integralZr// ?Lfun_integrable//. rewrite muleC lte_mul_pinfty// ?lee_fin ?powR_ge0//. -move: lpf => /(lfun_integrable r1) /integrableP[_]. +move: lpf => /(Lfun_integrable r1) /integrableP[_]. under eq_integral => x _ do rewrite gee0_abs ?lee_fin ?powR_ge0//. by []. Qed. @@ -1027,7 +1025,7 @@ Section Lspace_finite_measure. Context d (T : measurableType d) (R : realType). Variable mu : {finite_measure set T -> \bar R}. -Lemma lfun_cst c r : cst c \in lfun mu r%:E. +Lemma Lfun_cst c r : cst c \in Lfun mu r%:E. Proof. rewrite inE; apply/andP; split; rewrite inE//= /finite_norm unlock/Lnorm poweR_lty//. under eq_integral => x _/= do rewrite (_ : `|c| `^ r = cst (`|c| `^ r) x)//. @@ -1038,14 +1036,14 @@ Qed. End Lspace_finite_measure. -Section lfun_inclusion. +Section Lfun_subset. Context d (T : measurableType d) (R : realType). Variable mu : {measure set T -> \bar R}. Local Open Scope ereal_scope. -Lemma lfun_inclusion (p q : \bar R) : forall (p1 : 1 <= p) (q1 : 1 <= q), +Lemma Lfun_subset (p q : \bar R) : forall (p1 : 1 <= p) (q1 : 1 <= q), mu [set: T] \is a fin_num -> - p <= q -> {subset lfun mu q <= lfun mu p}. + p <= q -> {subset Lfun mu q <= Lfun mu p}. Proof. have := measure_ge0 mu [set: T]. rewrite le_eqVlt => /predU1P[mu0 p1 q1 muTfin pq f +|mu_pos]. @@ -1073,7 +1071,7 @@ move: p q => [p| |//] [q| |]// p1 q1. have := @hoelder _ _ _ mu (fun x => `|f x| `^ p)%R (cst 1)%R r r'. rewrite (_ : (_ \* cst 1)%R = (fun x => `|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). + have mfp : measurable_fun [set: T] (fun x => (`|f x| `^ p)%R). apply: (@measurableT_comp _ _ _ _ _ _ (@powR R ^~ p)) => //. exact: measurableT_comp. have m1 : measurable_fun [set: T] (@cst _ R 1%R) by exact: measurable_cst. @@ -1115,8 +1113,8 @@ move: p q => [p| |//] [q| |]// p1 q1. - by move=> muTfin _. Qed. -Lemma lfun_inclusion12 : mu [set: T] \is a fin_num -> - {subset lfun mu 2%:E <= lfun mu 1}. -Proof. by move=> ?; apply: lfun_inclusion => //; rewrite lee1n. Qed. +Lemma Lfun_subset12 : mu [set: T] \is a fin_num -> + {subset Lfun mu 2%:E <= Lfun mu 1}. +Proof. by move=> ?; apply: Lfun_subset => //; rewrite lee1n. Qed. -End lfun_inclusion. +End Lfun_subset. diff --git a/theories/probability.v b/theories/probability.v index b52c51e75f..9741f861d6 100644 --- a/theories/probability.v +++ b/theories/probability.v @@ -17,7 +17,7 @@ From mathcomp Require Import ftc gauss_integral hoelder. (* the type probability T R (a measure that sums to 1). *) (* *) (* About integrability: as a rule of thumb, in this file, we favor the use *) -(* of `lfun P n` hypotheses instead of the `integrable` predicate from *) +(* of `Lfun P n` hypotheses instead of the `integrable` predicate from *) (* `lebesgue_integral.v`. *) (* *) (* ``` *) @@ -260,9 +260,9 @@ Context d (T : measurableType d) (R : realType) (P : probability T R). Lemma expectation_def (X : {RV P >-> R}) : 'E_P[X] = (\int[P]_w (X w)%:E)%E. Proof. by rewrite unlock. Qed. -Lemma expectation_fin_num (X : T -> R) : X \in lfun P 1 -> +Lemma expectation_fin_num (X : T -> R) : X \in Lfun P 1 -> 'E_P[X] \is a fin_num. -Proof. by move=> ?; rewrite unlock integral_fune_fin_num ?lfun1_integrable. Qed. +Proof. by move=> ?; rewrite unlock integral_fune_fin_num ?Lfun1_integrable. Qed. Lemma expectation_cst r : 'E_P[cst r] = r%:E. Proof. by rewrite unlock/= integral_cst//= probability_setT mule1. Qed. @@ -277,9 +277,9 @@ move: iX => /integrableP[? Xoo]; rewrite (le_lt_trans _ Xoo)// unlock. exact: le_trans (le_abse_integral _ _ _). Qed. -Lemma expectationZl (X : T -> R) (k : R) : X \in lfun P 1 -> +Lemma expectationZl (X : T -> R) (k : R) : X \in Lfun P 1 -> 'E_P[k \o* X] = k%:E * 'E_P [X]. -Proof. by move=> ?; rewrite unlock muleC -integralZr ?lfun1_integrable. Qed. +Proof. by move=> ?; rewrite unlock muleC -integralZr ?Lfun1_integrable. Qed. Lemma expectation_ge0 (X : T -> R) : (forall x, 0 <= X x)%R -> 0 <= 'E_P[X]. @@ -301,16 +301,16 @@ move=> mX mY X0 Y0 XY; rewrite unlock ae_ge0_le_integral => //. by apply: XYN => /=; apply: contra_not h; rewrite lee_fin. Qed. -Lemma expectationD (X Y : T -> R) : X \in lfun P 1 -> Y \in lfun P 1 -> +Lemma expectationD (X Y : T -> R) : X \in Lfun P 1 -> Y \in Lfun P 1 -> 'E_P[X \+ Y] = 'E_P[X] + 'E_P[Y]. -Proof. by move=> ? ?; rewrite unlock integralD_EFin ?lfun1_integrable. Qed. +Proof. by move=> ? ?; rewrite unlock integralD_EFin ?Lfun1_integrable. Qed. -Lemma expectationB (X Y : T -> R) : X \in lfun P 1 -> Y \in lfun P 1 -> +Lemma expectationB (X Y : T -> R) : X \in Lfun P 1 -> Y \in Lfun P 1 -> 'E_P[X \- Y] = 'E_P[X] - 'E_P[Y]. -Proof. by move=> ? ?; rewrite unlock integralB_EFin ?lfun1_integrable. Qed. +Proof. by move=> ? ?; rewrite unlock integralB_EFin ?Lfun1_integrable. Qed. Lemma expectation_sum (X : seq (T -> R)) : - (forall Xi, Xi \in X -> Xi \in lfun P 1) -> + (forall Xi, Xi \in X -> Xi \in Lfun P 1) -> 'E_P[\sum_(Xi <- X) Xi] = \sum_(Xi <- X) 'E_P[Xi]. Proof. elim: X => [|X0 X IHX] intX; first by rewrite !big_nil expectation_cst. @@ -338,8 +338,8 @@ Local Open Scope ereal_scope. Context d (T : measurableType d) (R : realType) (P : probability T R). Lemma covarianceE (X Y : T -> R) : - X \in lfun P 1 -> Y \in lfun P 1 -> - (X * Y)%R \in lfun P 1 -> + X \in Lfun P 1 -> Y \in Lfun P 1 -> + (X * Y)%R \in Lfun P 1 -> covariance P X Y = 'E_P[X * Y] - 'E_P[X] * 'E_P[Y]. Proof. move=> l1X l1Y l1XY. @@ -348,8 +348,8 @@ rewrite unlock [X in 'E_P[X]](_ : _ = (X \* Y \- fine 'E_P[X] \o* Y apply/funeqP => x /=; rewrite mulrDr !mulrDl/= mul1r. rewrite fineM ?expectation_fin_num// mulrNN addrA. by rewrite mulrN mulNr [Z in (X x * Y x - Z)%R]mulrC. -rewrite expectationD/= ?rpredB//= ?lfunp_scale ?lfun_cst//. -rewrite 2?expectationB//= ?rpredB ?lfunp_scale// 3?expectationZl//= ?lfun_cst//. +rewrite expectationD/= ?rpredB//= ?Lfun_scale ?Lfun_cst//. +rewrite 2?expectationB//= ?rpredB ?Lfun_scale// 3?expectationZl//= ?Lfun_cst//. rewrite expectation_cst mule1 fineM ?expectation_fin_num// EFinM. rewrite !fineK ?expectation_fin_num//. by rewrite muleC subeK ?fin_numM ?expectation_fin_num. @@ -361,8 +361,8 @@ by rewrite unlock; congr expectation; apply/funeqP => x /=; rewrite mulrC. Qed. Lemma covariance_fin_num (X Y : T -> R) : - X \in lfun P 1 -> Y \in lfun P 1 -> - (X * Y)%R \in lfun P 1 -> + X \in Lfun P 1 -> Y \in Lfun P 1 -> + (X * Y)%R \in Lfun P 1 -> covariance P X Y \is a fin_num. Proof. by move=> ? ? ?; rewrite covarianceE// fin_numB fin_numM expectation_fin_num. @@ -379,31 +379,29 @@ Lemma covariance_cst_r (X : T -> R) c : covariance P X (cst c) = 0. Proof. by rewrite covarianceC covariance_cst_l. Qed. Lemma covarianceZl a (X Y : T -> R) : - X \in lfun P 1 -> Y \in lfun P 1 -> - (X * Y)%R \in lfun P 1 -> + X \in Lfun P 1 -> Y \in Lfun P 1 -> + (X * Y)%R \in Lfun P 1 -> covariance P (a \o* X)%R Y = a%:E * covariance P X Y. Proof. move=> X1 Y1 XY1. have aXY : (a \o* X * Y = a \o* (X * Y))%R by apply/funeqP => x; rewrite mulrAC. rewrite [LHS]covarianceE => [||//|] //=; last 2 first. -- by rewrite lfunp_scale. -- by rewrite aXY lfunp_scale. +- by rewrite Lfun_scale. +- by rewrite aXY Lfun_scale. rewrite covarianceE// aXY !expectationZl//. by rewrite -muleA -muleBr// fin_num_adde_defr// expectation_fin_num. Qed. -Lemma covarianceZr a (X Y : T -> R) : - X \in lfun P 1 -> Y \in lfun P 1 -> - (X * Y)%R \in lfun P 1 -> +Lemma covarianceZr a (X Y : T -> R) : X \in Lfun P 1 -> Y \in Lfun P 1 -> + (X * Y)%R \in Lfun P 1 -> covariance P X (a \o* Y)%R = a%:E * covariance P X Y. Proof. move=> X1 Y1 XY1. by rewrite [in RHS]covarianceC covarianceC covarianceZl; last rewrite mulrC. Qed. -Lemma covarianceNl (X Y : T -> R) : - X \in lfun P 1 -> Y \in lfun P 1 -> - (X * Y)%R \in lfun P 1 -> +Lemma covarianceNl (X Y : T -> R) : X \in Lfun P 1 -> Y \in Lfun P 1 -> + (X * Y)%R \in Lfun P 1 -> covariance P (\- X)%R Y = - covariance P X Y. Proof. move=> X1 Y1 XY1. @@ -411,32 +409,30 @@ have -> : (\- X = -1 \o* X)%R by apply/funeqP => x /=; rewrite mulrN mulr1. by rewrite covarianceZl// EFinN mulNe mul1e. Qed. -Lemma covarianceNr (X Y : T -> R) : - X \in lfun P 1 -> Y \in lfun P 1 -> - (X * Y)%R \in lfun P 1 -> +Lemma covarianceNr (X Y : T -> R) : X \in Lfun P 1 -> Y \in Lfun P 1 -> + (X * Y)%R \in Lfun P 1 -> covariance P X (\- Y)%R = - covariance P X Y. Proof. by move=> X1 Y1 XY1; rewrite !(covarianceC X) covarianceNl 1?mulrC. Qed. -Lemma covarianceNN (X Y : T -> R) : - X \in lfun P 1 -> Y \in lfun P 1 -> - (X * Y)%R \in lfun P 1 -> +Lemma covarianceNN (X Y : T -> R) : X \in Lfun P 1 -> Y \in Lfun P 1 -> + (X * Y)%R \in Lfun P 1 -> covariance P (\- X)%R (\- Y)%R = covariance P X Y. Proof. by move=> ? ? ?; rewrite covarianceNl//= ?covarianceNr ?oppeK ?mulrN//= ?rpredN. Qed. Lemma covarianceDl (X Y Z : T -> R) : - X \in lfun P 2%:E -> Y \in lfun P 2%:E -> Z \in lfun P 2%:E -> + X \in Lfun P 2%:E -> Y \in Lfun P 2%:E -> Z \in Lfun P 2%:E -> covariance P (X \+ Y)%R Z = covariance P X Z + covariance P Y Z. Proof. move=> X2 Y2 Z2. have Pfin : P setT \is a fin_num := fin_num_measure P _ measurableT. -have X1 := lfun_inclusion12 Pfin X2. -have Y1 := lfun_inclusion12 Pfin Y2. -have Z1 := lfun_inclusion12 Pfin Z2. -have XY1 := lfun2M2_1 X2 Y2. -have YZ1 := lfun2M2_1 Y2 Z2. -have XZ1 := lfun2M2_1 X2 Z2. +have X1 := Lfun_subset12 Pfin X2. +have Y1 := Lfun_subset12 Pfin Y2. +have Z1 := Lfun_subset12 Pfin Z2. +have XY1 := Lfun2_mul_Lfun1 X2 Y2. +have YZ1 := Lfun2_mul_Lfun1 Y2 Z2. +have XZ1 := Lfun2_mul_Lfun1 X2 Z2. rewrite [LHS]covarianceE//= ?mulrDl ?compreDr ?rpredD//= 2?expectationD//=. rewrite muleDl ?fin_num_adde_defr ?expectation_fin_num//. rewrite oppeD ?fin_num_adde_defr ?fin_numM ?expectation_fin_num//. @@ -444,33 +440,33 @@ by rewrite addeACA 2?covarianceE. Qed. Lemma covarianceDr (X Y Z : T -> R) : - X \in lfun P 2%:E -> Y \in lfun P 2%:E -> Z \in lfun P 2%:E -> + X \in Lfun P 2%:E -> Y \in Lfun P 2%:E -> Z \in Lfun P 2%:E -> covariance P X (Y \+ Z)%R = covariance P X Y + covariance P X Z. Proof. by move=> X2 Y2 Z2; rewrite covarianceC covarianceDl ?(covarianceC X) 1?mulrC. Qed. Lemma covarianceBl (X Y Z : T -> R) : - X \in lfun P 2%:E -> Y \in lfun P 2%:E -> Z \in lfun P 2%:E -> + X \in Lfun P 2%:E -> Y \in Lfun P 2%:E -> Z \in Lfun P 2%:E -> covariance P (X \- Y)%R Z = covariance P X Z - covariance P Y Z. Proof. move=> X2 Y2 Z2. have Pfin : P setT \is a fin_num := fin_num_measure P _ measurableT. -have Y1 := lfun_inclusion12 Pfin Y2. -have Z1 := lfun_inclusion12 Pfin Z2. -have YZ1 := lfun2M2_1 Y2 Z2. +have Y1 := Lfun_subset12 Pfin Y2. +have Z1 := Lfun_subset12 Pfin Z2. +have YZ1 := Lfun2_mul_Lfun1 Y2 Z2. by rewrite -[(X \- Y)%R]/(X \+ (\- Y))%R covarianceDl ?covarianceNl ?rpredN. Qed. Lemma covarianceBr (X Y Z : T -> R) : - X \in lfun P 2%:E -> Y \in lfun P 2%:E -> Z \in lfun P 2%:E -> + X \in Lfun P 2%:E -> Y \in Lfun P 2%:E -> Z \in Lfun P 2%:E -> covariance P X (Y \- Z)%R = covariance P X Y - covariance P X Z. Proof. move=> X2 Y2 Z2. have Pfin : P setT \is a fin_num := fin_num_measure P _ measurableT. -have Y1 := lfun_inclusion12 Pfin Y2. -have Z1 := lfun_inclusion12 Pfin Z2. -have YZ1 := lfun2M2_1 Y2 Z2. +have Y1 := Lfun_subset12 Pfin Y2. +have Z1 := Lfun_subset12 Pfin Z2. +have YZ1 := Lfun2_mul_Lfun1 Y2 Z2. by rewrite !(covarianceC X) covarianceBl 1?(mulrC _ X). Qed. @@ -483,18 +479,18 @@ Context d (T : measurableType d) (R : realType) (P : probability T R). Definition variance (X : T -> R) := covariance P X X. Local Notation "''V_' P [ X ]" := (variance X). -Lemma varianceE (X : T -> R) : X \in lfun P 2%:E -> +Lemma varianceE (X : T -> R) : X \in Lfun P 2%:E -> 'V_P[X] = 'E_P[X ^+ 2] - ('E_P[X]) ^+ 2. Proof. -move=> X2. -by rewrite /variance covarianceE ?lfun2M2_1// lfun_inclusion12 ?fin_num_measure. +move=> X2; rewrite /variance. +by rewrite covarianceE ?Lfun2_mul_Lfun1// Lfun_subset12 ?fin_num_measure. Qed. -Lemma variance_fin_num (X : T -> R) : X \in lfun P 2%:E -> +Lemma variance_fin_num (X : T -> R) : X \in Lfun P 2%:E -> 'V_P[X] \is a fin_num. Proof. move=> X2. -by rewrite covariance_fin_num ?lfun2M2_1// lfun_inclusion12 ?fin_num_measure. +by rewrite covariance_fin_num ?Lfun2_mul_Lfun1// Lfun_subset12 ?fin_num_measure. Qed. Lemma variance_ge0 (X : T -> R) : 0 <= 'V_P[X]. @@ -509,58 +505,58 @@ rewrite [X in 'E_P[X]](_ : _ = cst 0%R) ?expectation_cst//. by apply/funext => x; rewrite /GRing.exp/GRing.mul/= subrr mulr0. Qed. -Lemma varianceZ a (X : T -> R) : X \in lfun P 2%:E -> +Lemma varianceZ a (X : T -> R) : X \in Lfun P 2%:E -> 'V_P[(a \o* X)%R] = (a ^+ 2)%:E * 'V_P[X]. Proof. move=> X2. have Pfin : P setT \is a fin_num := fin_num_measure P _ measurableT. -have X1 := lfun_inclusion12 Pfin X2. +have X1 := Lfun_subset12 Pfin X2. rewrite /variance covarianceZl//=. -- by rewrite covarianceZr// ?muleA ?EFinM// lfun2M2_1. -- by rewrite lfunp_scale. -- by rewrite lfun2M2_1// lfunp_scale// ler1n. +- by rewrite covarianceZr// ?muleA ?EFinM// Lfun2_mul_Lfun1. +- by rewrite Lfun_scale. +- by rewrite Lfun2_mul_Lfun1// Lfun_scale// ler1n. Qed. -Lemma varianceN (X : T -> R) : X \in lfun P 2%:E -> 'V_P[(\- X)%R] = 'V_P[X]. +Lemma varianceN (X : T -> R) : X \in Lfun P 2%:E -> 'V_P[(\- X)%R] = 'V_P[X]. Proof. -move=> X2. -by rewrite /variance covarianceNN ?lfun2M2_1 ?lfun_inclusion12 ?fin_num_measure. +move=> X2; rewrite /variance. +by rewrite covarianceNN ?Lfun2_mul_Lfun1 ?Lfun_subset12 ?fin_num_measure. Qed. -Lemma varianceD (X Y : T -> R) : X \in lfun P 2%:E -> Y \in lfun P 2%:E -> +Lemma varianceD (X Y : T -> R) : X \in Lfun P 2%:E -> Y \in Lfun P 2%:E -> 'V_P[X \+ Y]%R = 'V_P[X] + 'V_P[Y] + 2%:E * covariance P X Y. Proof. move=> X2 Y2. have Pfin : P setT \is a fin_num := fin_num_measure P _ measurableT. -have X1 := lfun_inclusion12 Pfin X2. -have Y1 := lfun_inclusion12 Pfin Y2. -have XY1 := lfun2M2_1 X2 Y2. +have X1 := Lfun_subset12 Pfin X2. +have Y1 := Lfun_subset12 Pfin Y2. +have XY1 := Lfun2_mul_Lfun1 X2 Y2. rewrite -['V_P[_]]/(covariance P (X \+ Y)%R (X \+ Y)%R). rewrite covarianceDl ?rpredD ?lee1n//= covarianceDr// covarianceDr//. rewrite (covarianceC P Y X) [LHS]addeA [LHS](ACl (1*4*(2*3)))/=. by rewrite -[2%R]/(1 + 1)%R EFinD muleDl ?mul1e// covariance_fin_num. Qed. -Lemma varianceB (X Y : T -> R) : X \in lfun P 2%:E -> Y \in lfun P 2%:E -> +Lemma varianceB (X Y : T -> R) : X \in Lfun P 2%:E -> Y \in Lfun P 2%:E -> 'V_P[(X \- Y)%R] = 'V_P[X] + 'V_P[Y] - 2%:E * covariance P X Y. Proof. move=> X2 Y2. have Pfin : P setT \is a fin_num := fin_num_measure P _ measurableT. -have X1 := lfun_inclusion12 Pfin X2. -have Y1 := lfun_inclusion12 Pfin Y2. -have XY1 := lfun2M2_1 X2 Y2. +have X1 := Lfun_subset12 Pfin X2. +have Y1 := Lfun_subset12 Pfin Y2. +have XY1 := Lfun2_mul_Lfun1 X2 Y2. rewrite -[(X \- Y)%R]/(X \+ (\- Y))%R. by rewrite varianceD/= ?varianceN ?covarianceNr ?muleN ?rpredN. Qed. -Lemma varianceD_cst_l c (X : T -> R) : X \in lfun P 2%:E -> +Lemma varianceD_cst_l c (X : T -> R) : X \in Lfun P 2%:E -> 'V_P[(cst c \+ X)%R] = 'V_P[X]. Proof. move=> X2. -by rewrite varianceD ?lfun_cst// variance_cst add0e covariance_cst_l mule0 adde0. +by rewrite varianceD ?Lfun_cst// variance_cst add0e covariance_cst_l mule0 adde0. Qed. -Lemma varianceD_cst_r (X : T -> R) c : X \in lfun P 2%:E -> +Lemma varianceD_cst_r (X : T -> R) c : X \in Lfun P 2%:E -> 'V_P[(X \+ cst c)%R] = 'V_P[X]. Proof. move=> X2. @@ -568,27 +564,27 @@ have -> : (X \+ cst c = cst c \+ X)%R by apply/funeqP => x /=; rewrite addrC. exact: varianceD_cst_l. Qed. -Lemma varianceB_cst_l c (X : T -> R) : X \in lfun P 2%:E -> +Lemma varianceB_cst_l c (X : T -> R) : X \in Lfun P 2%:E -> 'V_P[(cst c \- X)%R] = 'V_P[X]. Proof. move=> X2; rewrite -[(cst c \- X)%R]/(cst c \+ (\- X))%R. by rewrite varianceD_cst_l/= ?rpredN// varianceN. Qed. -Lemma varianceB_cst_r (X : T -> R) c : X \in lfun P 2%:E -> +Lemma varianceB_cst_r (X : T -> R) c : X \in Lfun P 2%:E -> 'V_P[(X \- cst c)%R] = 'V_P[X]. Proof. by move=> X2; rewrite -[(X \- cst c)%R]/(X \+ (cst (- c)))%R varianceD_cst_r. Qed. -Lemma covariance_le (X Y : T -> R) : X \in lfun P 2%:E -> Y \in lfun P 2%:E -> +Lemma covariance_le (X Y : T -> R) : X \in Lfun P 2%:E -> Y \in Lfun P 2%:E -> covariance P X Y <= sqrte 'V_P[X] * sqrte 'V_P[Y]. Proof. move=> X2 Y2. have Pfin : P setT \is a fin_num := fin_num_measure P _ measurableT. -have X1 := lfun_inclusion12 Pfin X2. -have Y1 := lfun_inclusion12 Pfin Y2. -have XY1 := lfun2M2_1 X2 Y2. +have X1 := Lfun_subset12 Pfin X2. +have Y1 := Lfun_subset12 Pfin Y2. +have XY1 := Lfun2_mul_Lfun1 X2 Y2. rewrite -sqrteM ?variance_ge0//. rewrite lee_sqrE ?sqrte_ge0// sqr_sqrte ?mule_ge0 ?variance_ge0//. rewrite -(fineK (variance_fin_num X2)) -(fineK (variance_fin_num Y2)). @@ -609,7 +605,7 @@ rewrite -lee_fin !EFinD EFinM fineK ?variance_fin_num// muleC -varianceZ//. rewrite 2!EFinM ?fineK ?variance_fin_num// ?covariance_fin_num//. rewrite -muleA [_ * r%:E]muleC -covarianceZl//. rewrite addeAC -varianceD ?variance_ge0//=. -by rewrite lfunp_scale// ler1n. +by rewrite Lfun_scale// ler1n. Qed. End variance. @@ -678,19 +674,19 @@ by move=> /le_trans; apply; rewrite /variance [in leRHS]unlock. Qed. Lemma cantelli (X : {RV P >-> R}) (lambda : R) : - (X : T -> R) \in lfun P 2%:E -> (0 < lambda)%R -> + (X : T -> R) \in Lfun P 2%:E -> (0 < lambda)%R -> P [set x | lambda%:E <= (X x)%:E - 'E_P[X]] <= (fine 'V_P[X] / (fine 'V_P[X] + lambda^2))%:E. Proof. move=> /[dup] X2. -move=> /(lfun_inclusion12 (fin_num_measure P _ measurableT)) X1 lambda_gt0. +move=> /(Lfun_subset12 (fin_num_measure P _ measurableT)) X1 lambda_gt0. have finEK : (fine 'E_P[X])%:E = 'E_P[X] by rewrite fineK ?expectation_fin_num. have finVK : (fine 'V_P[X])%:E = 'V_P[X] by rewrite fineK ?variance_fin_num. pose Y := (X \- cst (fine 'E_P[X]))%R. -have Y2 : (Y : T -> R) \in lfun P 2%:E. - by rewrite /Y rpredB ?lee1n//= => _; rewrite lfun_cst. +have Y2 : (Y : T -> R) \in Lfun P 2%:E. + by rewrite /Y rpredB ?lee1n//= => _; rewrite Lfun_cst. have EY : 'E_P[Y] = 0. - rewrite expectationB ?lfun_cst//= expectation_cst. + rewrite expectationB ?Lfun_cst//= expectation_cst. by rewrite finEK subee// expectation_fin_num. have VY : 'V_P[Y] = 'V_P[X] by rewrite varianceB_cst_r. have le (u : R) : (0 <= u)%R -> @@ -699,11 +695,11 @@ have le (u : R) : (0 <= u)%R -> move=> uge0; rewrite EFinM. have -> : (fine 'V_P[X] + u^2)%:E = 'E_P[(Y \+ cst u)^+2]%R. rewrite -VY -[RHS](@subeK _ _ (('E_P[(Y \+ cst u)%R])^+2)); last first. - rewrite fin_numX// expectation_fin_num//= rpredD ?lfun_cst//. - by rewrite rpredB// lfun_cst. + rewrite fin_numX// expectation_fin_num//= rpredD ?Lfun_cst//. + by rewrite rpredB// Lfun_cst. rewrite -varianceE/=; last first. - by rewrite rpredD ?lee1n//= => _; rewrite lfun_cst. - rewrite -expe2 expectationD/= ?lfun_cst//; last by rewrite rpredB ?lfun_cst. + by rewrite rpredD ?lee1n//= => _; rewrite Lfun_cst. + rewrite -expe2 expectationD/= ?Lfun_cst//; last by rewrite rpredB ?Lfun_cst. rewrite EY// add0e expectation_cst -EFinM. by rewrite (varianceD_cst_r _ Y2) EFinD fineK ?variance_fin_num. have le : [set x | lambda%:E <= (X x)%:E - 'E_P[X]] @@ -715,7 +711,7 @@ have le (u : R) : (0 <= u)%R -> - by rewrite lerD2r -lee_fin EFinB finEK. apply: (le_trans (le_measure _ _ _ le)). - rewrite -[[set _ | _]]setTI inE; apply: emeasurable_fun_c_infty => [//|]. - by apply: emeasurable_funB=> //; apply/measurable_int/(lfun1_integrable X1). + by apply: emeasurable_funB=> //; apply/measurable_int/(Lfun1_integrable X1). - rewrite -[[set _ | _]]setTI inE; apply: emeasurable_fun_c_infty => [//|]. rewrite measurable_EFinP [X in measurable_fun _ X](_ : _ = (fun x => x ^+ 2) \o (fun x => Y x + u))%R//. From 3cab22eeb97de5e9b60f8dc6c704ad8668c4d23e Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Thu, 29 May 2025 23:21:57 +0900 Subject: [PATCH 06/13] minor gen --- CHANGELOG_UNRELEASED.md | 2 +- theories/hoelder.v | 8 ++++---- 2 files changed, 5 insertions(+), 5 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index e5134ad87f..8432fdfed5 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -177,7 +177,7 @@ - in `hoelder.v`: + definition `Lnorm` generalized to functions with codomain `\bar R` (this impacts the notation `'N_p[f]`) - + lemmas `Lnorm1`, `eq_Lnorm` (from `f : _ -> R` to `f : _ -> \bar R`) + + lemmas `Lnorm1`, `eq_Lnorm`, `Lnorm_counting` (from `f : _ -> R` to `f : _ -> \bar R`) - in `probability.v` + lemma `cantelli` diff --git a/theories/hoelder.v b/theories/hoelder.v index 7da1a99d3c..927b8c6e70 100644 --- a/theories/hoelder.v +++ b/theories/hoelder.v @@ -176,10 +176,10 @@ Section lnorm. Context d {T : measurableType d} {R : realType}. Local Open Scope ereal_scope. (** lp-norm is just Lp-norm applied to counting *) -Local Notation "'N_ p [ f ]" := (Lnorm counting p (EFin \o f)). +Local Notation "'N_ p [ f ]" := (Lnorm counting p f). -Lemma Lnorm_counting p (f : R^nat) : (0 < p)%R -> - 'N_p%:E [f] = (\sum_(k + 'N_p%:E [f] = (\sum_(k p0; rewrite unlock ge0_integral_count// => k; rewrite poweR_ge0. Qed. @@ -293,7 +293,7 @@ Qed. Lemma hoelder (f g : T -> R) p q : measurable_fun [set: T] f -> measurable_fun [set: T] g -> (0 < p)%R -> (0 < q)%R -> (p^-1 + q^-1 = 1)%R -> - 'N_1[(f \* g)%R] <= 'N_p%:E[f] * 'N_q%:E[g]. + 'N_1[(f \* g)%R] <= 'N_p%:E[f] * 'N_q%:E[g]. Proof. move=> mf mg p0 q0 pq. have [f0|f0] := eqVneq 'N_p%:E[f] 0%E; first exact: hoelder0. From 98900a9425c2fec8c878d58cce80413996664911 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Mon, 2 Jun 2025 19:39:57 +0900 Subject: [PATCH 07/13] fix hoelder_conjugate --- CHANGELOG_UNRELEASED.md | 5 +- theories/hoelder.v | 126 +++++++++++++++++++++++++++------------- 2 files changed, 89 insertions(+), 42 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 8432fdfed5..54e9ea505b 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -93,8 +93,9 @@ - in `hoelder.v` + lemmas `Lnorm0`, `Lnorm_cst1` - + definition `conjugate` - + lemma `conjugateE` + + definition `hoelder_conjugate` + + lemmas `hoelder_conjugate0`, `hoelder_conjugate1`, `hoelder_conjugate2`, + `hoelder_conjugatey`, `hoelder_conjugateK` + lemmas `lerB_DLnorm`, `lerB_LnormD`, `eminkowski` + definition `finite_norm` + mixin `isLfunction` with field `Lfunction_finite` diff --git a/theories/hoelder.v b/theories/hoelder.v index 927b8c6e70..de015337ef 100644 --- a/theories/hoelder.v +++ b/theories/hoelder.v @@ -16,9 +16,7 @@ From mathcomp Require Import lebesgue_integral numfun exp convex. (* *) (* ``` *) (* 'N[mu]_p[f] == the Lp-norm of f with measure mu *) -(* conjugate p == a real number q such that p^-1 + q^-1 = 1 when *) -(* p is real, otherwise conjugate +oo = 1 and *) -(* conjugate -oo = 0 *) +(* hoelder_conjugate p == an extended real number q s.t. p^-1 + q^-1 = 1 *) (* ``` *) (* *) (* Lp-spaces and properties of Lp-norms: *) @@ -82,16 +80,19 @@ Implicit Types (p : \bar R) (f g : T -> \bar R) (r : R). Local Notation "'N_ p [ f ]" := (Lnorm mu p f). -Lemma Lnorm0 p : 1 <= p -> 'N_p[cst 0] = 0. +(* TODO: true to remove conditions when we enable +(mu (f @^-1` (setT `\ 0%R))) when p = 0 +*) +Lemma Lnorm0 p : p != 0 -> 'N_p[cst 0] = 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). +rewrite unlock /Lnorm; case: p => [r|_|_]. +- rewrite eqe => r0. 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. +- case: ifPn => // mu0; apply: ess_sup_ae_cst => //. + by apply/nearW => x/=; rewrite normr0. +- case: ifPn => // mu0; apply: ess_inf_ae_cst => //. + by apply/nearW => x/=; rewrite normr0. Qed. Lemma Lnorm1 f : 'N_1[f] = \int[mu]_x `|f x|. @@ -186,38 +187,83 @@ Qed. End lnorm. -Section conjugate. +(* TODO: move *) +Lemma fine_eq1 {R : numDomainType} (x : \bar R) : + x \is a fin_num -> (fine x == 1%R) = (x == 1%E). +Proof. by move: x => [x| |]. Qed. + +Local Open Scope ereal_scope. +Lemma divee {R : realFieldType} (x : \bar R) : x != 0 -> x \is a fin_num -> + x / x = 1. +Proof. +move: x => [x|//|//]. +by rewrite eqe => x0; rewrite inver (negbTE x0) -EFinM divff. +Qed. +Local Close Scope ereal_scope. + +Section hoelder_conjugate. Context d (T : measurableType d) (R : realType). -Variables (mu : {measure set T -> \bar R}) (p : \bar R). -Hypothesis p1 : (1 <= p)%E. +Variables (mu : {measure set T -> \bar R}). 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. +Definition hoelder_conjugate (p : \bar R) : \bar R := + if p == +oo then 1 else + if p == -oo then 0 else + if p == 0 then -oo else + p / (p - 1). + +Local Notation "p ^*" := (hoelder_conjugate p) : ereal_scope. + +Lemma hoelder_conjugate0 : 0^* = -oo. +Proof. by rewrite /hoelder_conjugate/= eqxx. Qed. + +Lemma hoelder_conjugate1 : 1^* = +oo. +Proof. by rewrite /hoelder_conjugate/= onee_eq0 EFinN subee// inve0 mul1e. Qed. + +Lemma hoelder_conjugate2 : 2%:E^* = 2%:E. +Proof. +rewrite /hoelder_conjugate/= eqe/= pnatr_eq0/=. +by rewrite {2}(natrD _ 1 1) {2}EFinD EFinN addeK// inve1 mule1. +Qed. + +Lemma hoelder_conjugatey : +oo^* = 1. +Proof. by []. Qed. + +Lemma hoelder_conjugateNy : -oo^* = 0. +Proof. by []. Qed. + +Lemma hoelder_conjugate_eqy (p : \bar R) : +oo = p^* -> p = 1. +Proof. +move: p => [p| |]. +- rewrite /hoelder_conjugate/=; case: ifPn => [/eqP p0//|p0]. + rewrite -EFinD inver subr_eq0 -eqe. + by case: ifPn => // /eqP ->. +- by rewrite hoelder_conjugatey. +- by rewrite hoelder_conjugateNy. +Qed. -Lemma conjugateE : - conjugate = if p is r%:E then (r * (r-1)^-1)%:E - else if p == +oo then 1 else 0. +Lemma hoelder_conjugateK : involutive hoelder_conjugate. 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. +move=> [x| |]; last 2 first. + by rewrite hoelder_conjugatey hoelder_conjugate1. + by rewrite hoelder_conjugateNy hoelder_conjugate0. +rewrite /hoelder_conjugate/= !eqe. +have [x0/=|x0/=] := eqVneq x 0%R; first by rewrite x0. +rewrite -EFinD inver subr_eq0 -eqe. +have [x1/=|x1/=] := eqVneq x 1%R. + by rewrite x1 mul1e eqxx. +rewrite ifF; last first. + apply/negbTE; rewrite -EFinM eqe; apply/eqP. + move=> /(congr1 (fun z => z * (x - 1)))%R. + by rewrite mul0r -mulrA mulVf ?subr_eq0// mulr1 => /eqP; exact/negP. +rewrite -!(EFinM,EFinD) -[X in (_ / _ - X)%R](@divff _ (x - 1)) ?subr_eq0//. +rewrite -mulrBl opprB (addrC x (1 - _)%R) subrK div1r. +by rewrite EFinM -muleA divee ?mule1// eqe invr_eq0 subr_eq0. Qed. -End conjugate. +End hoelder_conjugate. Section hoelder. Context d {T : measurableType d} {R : realType}. @@ -793,7 +839,7 @@ Proof. by split=> [->//|fg]; exact/val_inj/funext. Qed. HB.instance Definition _ := [Choice of LfunType mu p1 by <:]. Lemma finite_norm_cst0 : finite_norm mu p (cst 0). -Proof. by rewrite /finite_norm Lnorm0// ltry. Qed. +Proof. by rewrite /finite_norm Lnorm0// gt_eqF// (lt_le_trans _ p1). Qed. HB.instance Definition _ := @isLfunction.Build d T R mu p p1 (cst 0) finite_norm_cst0. @@ -816,7 +862,7 @@ HB.instance Definition _ := GRing.isOppClosed.Build _ Lfun Lemma Lfun_addr_closed : addr_closed Lfun. Proof. split. - by rewrite inE rpred0/= inE/= /finite_norm/= Lnorm0. + by rewrite inE rpred0/= inE/=; exact: finite_norm_cst0. move=> f g /andP[mf /[!inE]/= lf] /andP[mg /[!inE]/= lg]. rewrite rpredD//= inE/= /finite_norm. rewrite (le_lt_trans (@eminkowski _ _ _ mu f g p _ _ _))//. @@ -1052,7 +1098,7 @@ rewrite le_eqVlt => /predU1P[mu0 p1 q1 muTfin pq f +|mu_pos]. rewrite /finite_norm unlock /Lnorm. move: p p1 {pq} => [r r1| |//]; last by rewrite -mu0 ltxx ltry. under eq_integral do rewrite /= -[(_ `^ _)%R]ger0_norm ?powR_ge0//=. - rewrite (@integral_abs_eq0 _ _ _ _ setT setT (fun x => (`|f x| `^ r)%:E))//. + rewrite (@integral_abs_eq0 _ _ _ _ _ (fun x => (`|f x| `^ r)%:E))//. by rewrite poweR0r// invr_neq0// gt_eqF// -lte_fin (lt_le_trans _ r1). apply/measurable_EFinP/(@measurableT_comp _ _ _ _ _ _ (@powR R ^~ r)) => //. exact: measurableT_comp. @@ -1065,9 +1111,9 @@ move: p q => [p| |//] [q| |]// p1 q1. 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 qinv0 : (q^-1 != 0)%R by rewrite invr_neq0// gt_eqF. + pose r := (q / p)%R. + pose r' := (1 - r^-1)^-1%R. have := @hoelder _ _ _ mu (fun x => `|f x| `^ p)%R (cst 1)%R r r'. rewrite (_ : (_ \* cst 1)%R = (fun x => `|f x| `^ p))%R -?fctM ?mulr1//. rewrite Lnorm_cst1 unlock /Lnorm invr1. @@ -1079,7 +1125,7 @@ move: p q => [p| |//] [q| |]// p1 q1. 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. + 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. From b482e6b1c3a96fe806adf264df500620f7a013c2 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Thu, 5 Jun 2025 12:27:02 +0900 Subject: [PATCH 08/13] properties of Hoelder's conjugate using ereal division --- theories/hoelder.v | 167 +++++++++++++++++++++++++++++++++++++++------ 1 file changed, 148 insertions(+), 19 deletions(-) diff --git a/theories/hoelder.v b/theories/hoelder.v index de015337ef..e6d77ca72c 100644 --- a/theories/hoelder.v +++ b/theories/hoelder.v @@ -15,8 +15,8 @@ From mathcomp Require Import lebesgue_integral numfun exp convex. (* and a definition of Lp-spaces. *) (* *) (* ``` *) -(* 'N[mu]_p[f] == the Lp-norm of f with measure mu *) -(* hoelder_conjugate p == an extended real number q s.t. p^-1 + q^-1 = 1 *) +(* 'N[mu]_p[f] == the Lp-norm of f with measure mu *) +(* hoelder_conjugate p == an extended real number q s.t. p^-1 + q^-1 = 1 *) (* ``` *) (* *) (* Lp-spaces and properties of Lp-norms: *) @@ -187,19 +187,66 @@ Qed. End lnorm. -(* TODO: move *) -Lemma fine_eq1 {R : numDomainType} (x : \bar R) : - x \is a fin_num -> (fine x == 1%R) = (x == 1%E). -Proof. by move: x => [x| |]. Qed. - +Section ereal. +Context {R : realFieldType}. +Implicit Type x y : \bar R. Local Open Scope ereal_scope. -Lemma divee {R : realFieldType} (x : \bar R) : x != 0 -> x \is a fin_num -> - x / x = 1. + +Lemma div1e x : 1 / x = x^-1. +Proof. +move: x => [x| |]/=. +- by rewrite mul1e. +- by rewrite invey mule0. +- by rewrite inveNy mul1e. +Qed. + +Lemma divee x : x != 0 -> x \is a fin_num -> x / x = 1. Proof. move: x => [x|//|//]. by rewrite eqe => x0; rewrite inver (negbTE x0) -EFinM divff. Qed. -Local Close Scope ereal_scope. + +Lemma inve_eq1 x : x^-1 = 1 <-> x = 1. +Proof. +move: x => [x| |]/=. +- split=> [|[->]]; last by rewrite inve1. + by move=> /(congr1 (fun x => x^-1)); rewrite inveK inve1 => ->. +- by rewrite invey; split => // /eqP; rewrite eq_sym onee_eq0. +- by rewrite inveNy. +Qed. + +Lemma inve_div x y : x \is a fin_num -> 0 < x -> (x / y)^-1 = y / x. +Proof. +move: x y => [x| |] [y| |]//=. +- rewrite !lte_fin => xfin x0. + rewrite inver//; case: ifPn => [/eqP->|y0]. + by rewrite mul0e gt0_muley ?lte_fin. + rewrite inver mulf_eq0 gt_eqF//= invr_eq0 (negbTE y0). + by rewrite invf_div// inver gt_eqF. +- rewrite lte_fin => _ x0. + by rewrite invey mule0 inve0 gt0_mulye// inve_gt0// eqe gt_eqF. +- rewrite !lte_fin => _ x0. + by rewrite gt0_mulNye ?inve_gt0// ?gt_eqF// inveNy gt0_muleNy. +Qed. + +(** NB: does not hold in general when x = +oo *) +Lemma ereal_conjugate x y : x \is a fin_num -> 1 < x -> + x^-1 + y^-1 = 1 -> y = x / (x - 1). +Proof. +move=> xfin x1 /eqP; rewrite eq_sym addeC -sube_eq//; last first. + by rewrite fin_num_adde_defl// fin_numV// ?gt_eqF ?(lt_trans _ x1)// ltNye. +move=> /eqP /(congr1 inve) /=; rewrite inveK => <-. +rewrite -[X in X - _](@divee x)//; last first. + by rewrite gt_eqF// (lt_trans _ x1). +rewrite -[X in _ - X]div1e -muleBl. +- rewrite inve_div//. + + by rewrite fin_numB// xfin. + + by rewrite sube_gt0. +- by rewrite fin_numV// ?gt_eqF// (lt_trans _ x1)// ltNyr. +- by rewrite fin_num_adde_defl. +Qed. + +End ereal. Section hoelder_conjugate. Context d (T : measurableType d) (R : realType). @@ -234,7 +281,7 @@ Proof. by []. Qed. Lemma hoelder_conjugateNy : -oo^* = 0. Proof. by []. Qed. -Lemma hoelder_conjugate_eqy (p : \bar R) : +oo = p^* -> p = 1. +Lemma hoelder_conjugate_eqy (p : \bar R) : p^* = +oo -> p = 1. Proof. move: p => [p| |]. - rewrite /hoelder_conjugate/=; case: ifPn => [/eqP p0//|p0]. @@ -244,25 +291,107 @@ move: p => [p| |]. - by rewrite hoelder_conjugateNy. Qed. +Lemma hoelder_conjugate_eqNy (p : \bar R) : p^* = -oo -> p = 0. +Proof. +move: p => [p| |]. +- rewrite /hoelder_conjugate/=; case: ifPn => [/eqP p0//|p0]. + rewrite -EFinD inver subr_eq0 -eqe. + by case: ifPn => //; rewrite eqe => /eqP ->; rewrite mul1e. +- by rewrite hoelder_conjugatey. +- by rewrite hoelder_conjugateNy. +Qed. + Lemma hoelder_conjugateK : involutive hoelder_conjugate. Proof. move=> [x| |]; last 2 first. by rewrite hoelder_conjugatey hoelder_conjugate1. by rewrite hoelder_conjugateNy hoelder_conjugate0. rewrite /hoelder_conjugate/= !eqe. -have [x0/=|x0/=] := eqVneq x 0%R; first by rewrite x0. +have [->//=|x0/=] := eqVneq x 0%R. rewrite -EFinD inver subr_eq0 -eqe. -have [x1/=|x1/=] := eqVneq x 1%R. - by rewrite x1 mul1e eqxx. -rewrite ifF; last first. - apply/negbTE; rewrite -EFinM eqe; apply/eqP. - move=> /(congr1 (fun z => z * (x - 1)))%R. - by rewrite mul0r -mulrA mulVf ?subr_eq0// mulr1 => /eqP; exact/negP. -rewrite -!(EFinM,EFinD) -[X in (_ / _ - X)%R](@divff _ (x - 1)) ?subr_eq0//. +have [->/=|x1/=] := eqVneq x 1%R; first by rewrite mul1e eqxx. +rewrite -EFinM eqe mulf_eq0 (negbTE x0)/= invr_eq0 subr_eq0 (negbTE x1). +rewrite -EFinD -[X in (_ / _ - X)%R](@divff _ (x - 1)) ?subr_eq0//. rewrite -mulrBl opprB (addrC x (1 - _)%R) subrK div1r. by rewrite EFinM -muleA divee ?mule1// eqe invr_eq0 subr_eq0. Qed. +(** NB: 0^-1 + 0^*^-1 = -oo *) +Lemma hoelder_conjugate_eq1 (p : \bar R) : p > -oo -> p != 0 -> + p^-1 + (p^*)^-1 = 1. +Proof. +move=> pNy p0; rewrite /hoelder_conjugate/=. +case: ifPn => [/eqP py|py]; first by rewrite py invey inve1 add0e. +rewrite gt_eqF// (negbTE p0). +move: p p0 py pNy => [p| |]//. +rewrite eqe => p0 _ _. +rewrite inver (negbTE p0) inver subr_eq0. +case: ifPn => [/eqP ->|p1]; first by rewrite invr1 mul1e invey adde0. +rewrite inveM; last first. + rewrite inveM_defE eqe (negbTE p0)/= andbT eqe. + rewrite invr_eq0 subr_eq0; apply/implyP => /eqP ->. + by rewrite lee01/= ltry. +rewrite inver (negbTE p0) inver invr_eq0 subr_eq0 (negbTE p1) invrK. +by rewrite EFinB muleBr// mule1 -EFinM mulVf// -EFinD addrC subrK. +Qed. + +Lemma hoelder_conjugateP p q : p >= 1 -> p^-1 + q^-1 = 1 <-> q = p^*. +Proof. +rewrite le_eqVlt => /predU1P[<-|]. + rewrite inve1 hoelder_conjugate1; split. + move=> /esym/eqP; rewrite addeC -sube_eq//; last first. + by rewrite fin_num_adde_defl. + by rewrite subee// => /eqP /(congr1 inve); rewrite inveK inve0. + by move=> ->; rewrite invey adde0. +have [->|] := eqVneq q -oo. + rewrite inveNy addeNy => p1; split => // /esym /hoelder_conjugate_eqNy /eqP. + by rewrite gt_eqF// (lt_trans _ p1). +rewrite -ltNye => qNy p1. +have {}p1' : (p \is a fin_num) \/ p == +oo by apply/orP; case: p p1. +case: p1' => [pfin|/eqP -> /=]; last first. + by rewrite hoelder_conjugatey invey add0r; exact: inve_eq1. +have {}q1' : (q \is a fin_num) \/ q == +oo by apply/orP; case: q qNy. +case: q1' => [qfin|/eqP -> /=]; last first. + rewrite invey addr0; split. + - by move/inve_eq1 => ->; rewrite hoelder_conjugate1. + - by move/esym/hoelder_conjugate_eqy => ->/=; rewrite inve1. +split => [pq1|pq]; last first. + rewrite pq hoelder_conjugate_eq1//. + by rewrite (lt_trans _ p1)// ltNyr. + by rewrite gt_eqF// (lt_trans _ p1). +rewrite /hoelder_conjugate ifF; last first. + by apply/negbTE; move/fin_numP : pfin => -[]. +rewrite gt_eqF; last first. + by move: pfin; rewrite fin_numE => /andP[pNy _]; rewrite ltNye. +rewrite gt_eqF// ?(lt_trans _ p1)//. +exact: ereal_conjugate. +Qed. + +(** NB: 0 / 0^* = 0 *) +Lemma hoelder_div_conjugate p : + (*p > -oo -> p != 0 -> *) p = -oo \/ p >= 1 -> p / p^* = p - 1. +Proof. +move=> [->|p1]. + by rewrite hoelder_conjugateNy inve0 mulNyy. +have [->|py] := eqVneq p +oo. + by rewrite hoelder_conjugatey inve1 mule1. +rewrite /hoelder_conjugate (negbTE py) ifF//; last first. + by apply/negbTE; rewrite -ltNye (lt_le_trans _ p1)// ltNye. +rewrite ifF; last by apply/negbTE; rewrite gt_eqF// (lt_le_trans _ p1). +have pfin : p \is a fin_num. + by rewrite fin_numE py andbT gt_eqF// (lt_le_trans _ p1)// ltNyr. +move: p1; rewrite le_eqVlt => /predU1P[<-|p1]. + by rewrite subee// inve0 !mul1e invey. +rewrite inveM//. + by rewrite inveK muleA divee// ?mul1e// gt_eqF// (lt_trans _ p1). +apply: fin_inveM_def => //. +- by rewrite gt_eqF// (lt_trans _ p1). +- by rewrite inve_eq0 sube_eq. +- rewrite fin_numV//. + + by rewrite sube_eq// add0e gt_eqF. + + by rewrite sube_eq// addNye -ltNye (le_lt_trans _ p1)// leNye. +Qed. + End hoelder_conjugate. Section hoelder. From 5f234c0d160966bd2b9bfd9dcca0802b21b96389 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Tue, 17 Jun 2025 12:14:08 +0900 Subject: [PATCH 09/13] complete hoelder conjugate lemmas --- CHANGELOG_UNRELEASED.md | 9 ++ reals/constructive_ereal.v | 51 ++++++++++ theories/hoelder.v | 198 +++++++++++++++---------------------- 3 files changed, 140 insertions(+), 118 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 54e9ea505b..402976ca15 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -126,6 +126,15 @@ + lemmas `poweR_Lnorm`, `oppe_Lnorm` + lemma `integrable_poweR` +- in `hoelder.v`: + + lemmas `hoelder_conjugate_div`, `hoelder_div_conjugate`, + `hoelder_Mconjugate`, `hoelder_conjugateP`, + `hoelder_conjugate_eq1`, `hoelder_conjugate_eqNy`, `hoelder_conjugate_eqy`, + `hoelder_conjugateNy` + +- in `constructive_ereal.v`: + + lemmas `div1e`, `divee`, `inve_eq1`, `Nyconjugate` + ### Changed - in `measure.v`: diff --git a/reals/constructive_ereal.v b/reals/constructive_ereal.v index 323de81333..a394bcd0bc 100644 --- a/reals/constructive_ereal.v +++ b/reals/constructive_ereal.v @@ -2418,6 +2418,15 @@ Qed. Lemma inve_eq0 x : (x^-1 == 0) = (x == +oo). Proof. by case: inveP; rewrite ?eqxx //= => r /negPf; rewrite eqe invr_eq0. Qed. +Lemma inve_eq1 x : (x^-1 == 1) = (x == 1). +Proof. +move: x => [x| |]/=. +- rewrite inver; case: ifPn => [/eqP ->|x0]; last by rewrite !eqe invr_eq1. + by rewrite eqe// [RHS]eq_sym oner_eq0; apply/negbTE. +- by rewrite invey eq_sym onee_eq0. +- by rewrite inveNy. +Qed. + Lemma inve_ge0 x : (0 <= x^-1) = (0 <= x). Proof. by case: inveP; rewrite ?le0y ?lexx //= => r; rewrite lee_fin invr_ge0. @@ -2452,6 +2461,13 @@ Proof. by move: x => [x| |]//; rewrite eqe => x0 _; rewrite inver (negbTE x0). Qed. +Lemma div1e x : 1 / x = x^-1. +Proof. +move: x => [x| |]/=; first by rewrite mul1e. +- by rewrite invey mule0. +- by rewrite inveNy mul1e. +Qed. + Lemma gee_pMl y x : y \is a fin_num -> 0 <= x -> y <= 1 -> y * x <= x. Proof. move=> yfin; rewrite le_eqVlt => /predU1P[<-|]; first by rewrite mule0. @@ -3478,6 +3494,41 @@ Proof. by move=> x0; rewrite inve_pgt ?inve1//= inE/= ?lee01. Qed. Lemma inve_ge1 x : 0 <= x -> (1 <= x^-1) = (x <= 1). Proof. by move=> x0; rewrite inve_pge ?inve1//= inE/= ?lee01. Qed. +Lemma divee x : x \is a fin_num -> x != 0 -> x / x = 1. +Proof. +move: x => [x|//|//] _. +by rewrite eqe => x0; rewrite inver (negbTE x0) -EFinM divff. +Qed. + +Lemma Nyconjugate x y : x \is a fin_num -> y != -oo -> + x^-1 + y^-1 = 1 -> y = x / (x - 1). +Proof. +move=> xfin yNy; have [->|x1] := eqVneq x 1. + rewrite subee// inve0 mul1e inve1 => /eqP. + rewrite -addeC eq_sym -sube_eq//; last by rewrite fin_num_adde_defl. + rewrite subee// => /eqP /esym; case: y yNy => // r _. + rewrite inver; case: ifPn => // r0 [] /(congr1 (fun z => z^-1)%R). + by rewrite invrK invr0 => /eqP; rewrite (negbTE r0). +have [->|x0] := eqVneq x 0. + rewrite inve0 mul0e => /eqP; rewrite addeC eq_sym -sube_eq//; last first. + rewrite /adde_def eqxx/= andbT negb_and/= orbT/=. + apply: contra yNy => /eqP /(congr1 inve). + by rewrite inveK inveNy => ->. + rewrite eq_sym/= addeC/= => /eqP /(congr1 inve). + by rewrite inveK// inveNy => /eqP; rewrite (negbTE yNy). +have xNy : x != -oo by move: xfin; rewrite fin_numE => /andP[]. +move=> /eqP; rewrite eq_sym addeC -sube_eq//; last first. + by rewrite fin_num_adde_defl// fin_numV. +move=> /eqP /(congr1 inve) /=; rewrite inveK => <-. +rewrite -[X in X - _](@divee x)// -[X in _ - X]div1e -muleBl. +- move: x xfin {xNy} x1 x0 => [x| |]// _; rewrite !eqe => x1 x0. + rewrite inver/= (negbTE x0)/= -EFinD -EFinM. + rewrite inver mulf_eq0 subr_eq0 (negbTE x1)/= invr_eq0. + by rewrite (negbTE x0) invfM// invrK mulrC EFinM inver/= subr_eq0 (negbTE x1). +- by rewrite fin_numV// ?gt_eqF// ltNye. +- by rewrite fin_num_adde_defl. +Qed. + Lemma lee_addgt0Pr x y : reflect (forall e, (0 < e)%R -> x <= y + e%:E) (x <= y). Proof. diff --git a/theories/hoelder.v b/theories/hoelder.v index e6d77ca72c..4fa8de45b9 100644 --- a/theories/hoelder.v +++ b/theories/hoelder.v @@ -192,59 +192,7 @@ Context {R : realFieldType}. Implicit Type x y : \bar R. Local Open Scope ereal_scope. -Lemma div1e x : 1 / x = x^-1. -Proof. -move: x => [x| |]/=. -- by rewrite mul1e. -- by rewrite invey mule0. -- by rewrite inveNy mul1e. -Qed. - -Lemma divee x : x != 0 -> x \is a fin_num -> x / x = 1. -Proof. -move: x => [x|//|//]. -by rewrite eqe => x0; rewrite inver (negbTE x0) -EFinM divff. -Qed. - -Lemma inve_eq1 x : x^-1 = 1 <-> x = 1. -Proof. -move: x => [x| |]/=. -- split=> [|[->]]; last by rewrite inve1. - by move=> /(congr1 (fun x => x^-1)); rewrite inveK inve1 => ->. -- by rewrite invey; split => // /eqP; rewrite eq_sym onee_eq0. -- by rewrite inveNy. -Qed. -Lemma inve_div x y : x \is a fin_num -> 0 < x -> (x / y)^-1 = y / x. -Proof. -move: x y => [x| |] [y| |]//=. -- rewrite !lte_fin => xfin x0. - rewrite inver//; case: ifPn => [/eqP->|y0]. - by rewrite mul0e gt0_muley ?lte_fin. - rewrite inver mulf_eq0 gt_eqF//= invr_eq0 (negbTE y0). - by rewrite invf_div// inver gt_eqF. -- rewrite lte_fin => _ x0. - by rewrite invey mule0 inve0 gt0_mulye// inve_gt0// eqe gt_eqF. -- rewrite !lte_fin => _ x0. - by rewrite gt0_mulNye ?inve_gt0// ?gt_eqF// inveNy gt0_muleNy. -Qed. - -(** NB: does not hold in general when x = +oo *) -Lemma ereal_conjugate x y : x \is a fin_num -> 1 < x -> - x^-1 + y^-1 = 1 -> y = x / (x - 1). -Proof. -move=> xfin x1 /eqP; rewrite eq_sym addeC -sube_eq//; last first. - by rewrite fin_num_adde_defl// fin_numV// ?gt_eqF ?(lt_trans _ x1)// ltNye. -move=> /eqP /(congr1 inve) /=; rewrite inveK => <-. -rewrite -[X in X - _](@divee x)//; last first. - by rewrite gt_eqF// (lt_trans _ x1). -rewrite -[X in _ - X]div1e -muleBl. -- rewrite inve_div//. - + by rewrite fin_numB// xfin. - + by rewrite sube_gt0. -- by rewrite fin_numV// ?gt_eqF// (lt_trans _ x1)// ltNyr. -- by rewrite fin_num_adde_defl. -Qed. End ereal. @@ -301,22 +249,6 @@ move: p => [p| |]. - by rewrite hoelder_conjugateNy. Qed. -Lemma hoelder_conjugateK : involutive hoelder_conjugate. -Proof. -move=> [x| |]; last 2 first. - by rewrite hoelder_conjugatey hoelder_conjugate1. - by rewrite hoelder_conjugateNy hoelder_conjugate0. -rewrite /hoelder_conjugate/= !eqe. -have [->//=|x0/=] := eqVneq x 0%R. -rewrite -EFinD inver subr_eq0 -eqe. -have [->/=|x1/=] := eqVneq x 1%R; first by rewrite mul1e eqxx. -rewrite -EFinM eqe mulf_eq0 (negbTE x0)/= invr_eq0 subr_eq0 (negbTE x1). -rewrite -EFinD -[X in (_ / _ - X)%R](@divff _ (x - 1)) ?subr_eq0//. -rewrite -mulrBl opprB (addrC x (1 - _)%R) subrK div1r. -by rewrite EFinM -muleA divee ?mule1// eqe invr_eq0 subr_eq0. -Qed. - -(** NB: 0^-1 + 0^*^-1 = -oo *) Lemma hoelder_conjugate_eq1 (p : \bar R) : p > -oo -> p != 0 -> p^-1 + (p^*)^-1 = 1. Proof. @@ -335,61 +267,91 @@ rewrite inver (negbTE p0) inver invr_eq0 subr_eq0 (negbTE p1) invrK. by rewrite EFinB muleBr// mule1 -EFinM mulVf// -EFinD addrC subrK. Qed. -Lemma hoelder_conjugateP p q : p >= 1 -> p^-1 + q^-1 = 1 <-> q = p^*. +Lemma hoelder_conjugateP p q : p > -oo -> p != 0 -> + p^-1 + q^-1 = 1 <-> q = p^*. Proof. -rewrite le_eqVlt => /predU1P[<-|]. - rewrite inve1 hoelder_conjugate1; split. - move=> /esym/eqP; rewrite addeC -sube_eq//; last first. - by rewrite fin_num_adde_defl. - by rewrite subee// => /eqP /(congr1 inve); rewrite inveK inve0. - by move=> ->; rewrite invey adde0. -have [->|] := eqVneq q -oo. - rewrite inveNy addeNy => p1; split => // /esym /hoelder_conjugate_eqNy /eqP. - by rewrite gt_eqF// (lt_trans _ p1). -rewrite -ltNye => qNy p1. -have {}p1' : (p \is a fin_num) \/ p == +oo by apply/orP; case: p p1. -case: p1' => [pfin|/eqP -> /=]; last first. - by rewrite hoelder_conjugatey invey add0r; exact: inve_eq1. -have {}q1' : (q \is a fin_num) \/ q == +oo by apply/orP; case: q qNy. -case: q1' => [qfin|/eqP -> /=]; last first. - rewrite invey addr0; split. - - by move/inve_eq1 => ->; rewrite hoelder_conjugate1. - - by move/esym/hoelder_conjugate_eqy => ->/=; rewrite inve1. -split => [pq1|pq]; last first. - rewrite pq hoelder_conjugate_eq1//. - by rewrite (lt_trans _ p1)// ltNyr. - by rewrite gt_eqF// (lt_trans _ p1). -rewrite /hoelder_conjugate ifF; last first. - by apply/negbTE; move/fin_numP : pfin => -[]. -rewrite gt_eqF; last first. - by move: pfin; rewrite fin_numE => /andP[pNy _]; rewrite ltNye. -rewrite gt_eqF// ?(lt_trans _ p1)//. -exact: ereal_conjugate. +move=> pNy p0. +have [->|py] := eqVneq p +oo. + rewrite hoelder_conjugatey invey add0e; split => /eqP. + by rewrite inve_eq1 => /eqP. + by rewrite -inve_eq1 => /eqP. +have pfin : p \is a fin_num by rewrite fin_numE py andbT -ltNye. +have [->|qNy] := eqVneq q -oo. + rewrite inveNy addeNy; split => // /esym /hoelder_conjugate_eqNy /eqP. + by rewrite (negbTE p0). +split => [pq1|pq]; last by rewrite pq hoelder_conjugate_eq1. +rewrite /hoelder_conjugate (negbTE py)//. +rewrite ifF//; last first. + by apply/negbTE; move: pfin; rewrite fin_numE => /andP[]. +by rewrite (negbTE p0); exact: Nyconjugate. Qed. -(** NB: 0 / 0^* = 0 *) -Lemma hoelder_div_conjugate p : - (*p > -oo -> p != 0 -> *) p = -oo \/ p >= 1 -> p / p^* = p - 1. +Lemma hoelder_conjugateK : involutive hoelder_conjugate. Proof. -move=> [->|p1]. - by rewrite hoelder_conjugateNy inve0 mulNyy. -have [->|py] := eqVneq p +oo. - by rewrite hoelder_conjugatey inve1 mule1. -rewrite /hoelder_conjugate (negbTE py) ifF//; last first. - by apply/negbTE; rewrite -ltNye (lt_le_trans _ p1)// ltNye. -rewrite ifF; last by apply/negbTE; rewrite gt_eqF// (lt_le_trans _ p1). -have pfin : p \is a fin_num. - by rewrite fin_numE py andbT gt_eqF// (lt_le_trans _ p1)// ltNyr. -move: p1; rewrite le_eqVlt => /predU1P[<-|p1]. - by rewrite subee// inve0 !mul1e invey. -rewrite inveM//. +move=> [x| |]; last 2 first. + by rewrite hoelder_conjugatey hoelder_conjugate1. + by rewrite hoelder_conjugateNy hoelder_conjugate0. +rewrite /hoelder_conjugate/= !eqe. +have [->//=|x0/=] := eqVneq x 0%R. +rewrite -EFinD inver subr_eq0 -eqe. +have [->/=|x1/=] := eqVneq x 1%R; first by rewrite mul1e eqxx. +rewrite -EFinM eqe mulf_eq0 (negbTE x0)/= invr_eq0 subr_eq0 (negbTE x1). +rewrite -EFinD -[X in (_ / _ - X)%R](@divff _ (x - 1)) ?subr_eq0//. +rewrite -mulrBl opprB (addrC x (1 - _)%R) subrK div1r. +by rewrite EFinM -muleA divee ?mule1// eqe invr_eq0 subr_eq0. +Qed. + +Lemma hoelder_Mconjugate p : p > -oo -> p != 0 -> p * p^* = p + p^*. +Proof. +move=> pNy p0. +rewrite /hoelder_conjugate. +case: ifPn => [/eqP ->|py]; first by rewrite mule1. +rewrite gt_eqF// (negbTE p0). +have [->|p1] := eqVneq p 1; first by rewrite subee// inve0 !mul1e. +rewrite -[X in _ = X + _]mule1. +have pfin : p \is a fin_num by rewrite fin_numE -ltNye pNy. +rewrite -[X in _ * X + _](@divee _ (p - 1)); last first. + by rewrite sube_eq ?add0e. + by rewrite fin_numB// pfin. +rewrite [in RHS]muleA -muleDl; last 2 first. + rewrite fin_numV//; first by rewrite sube_eq// add0e. + by rewrite sube_eq// -ltNye. + by rewrite fin_num_adde_defl. +by rewrite muleA muleBr ?fin_num_adde_defl// mule1 subeK. +Qed. + +Lemma hoelder_div_conjugate p : p > -oo -> p != 0 -> p / p^* = p - 1. +Proof. +move=> pNy p0. +rewrite /hoelder_conjugate; case: ifPn => [/eqP->|py]. + by rewrite inve1 mule1. +rewrite gt_eqF// (negbTE p0). +have ? : p \is a fin_num by rewrite fin_numE py andbT -ltNye. +have [->|p1] := eqVneq p 1; first by rewrite subee// inve0 !mul1e invey. +rewrite inveM. by rewrite inveK muleA divee// ?mul1e// gt_eqF// (lt_trans _ p1). -apply: fin_inveM_def => //. -- by rewrite gt_eqF// (lt_trans _ p1). -- by rewrite inve_eq0 sube_eq. -- rewrite fin_numV//. - + by rewrite sube_eq// add0e gt_eqF. - + by rewrite sube_eq// addNye -ltNye (le_lt_trans _ p1)// leNye. +apply: fin_inveM_def => //; first by rewrite inve_eq0 sube_eq. +rewrite fin_numV//; first by rewrite sube_eq// add0e. +by rewrite sube_eq// -ltNye. +Qed. + +Lemma hoelder_conjugate_div p : p > -oo -> p != 0 -> p^* / p = p^* - 1. +Proof. +move=> pNy p0. +rewrite /hoelder_conjugate; case: ifPn => [/eqP->|py]. + by rewrite invey mule0 subee. +rewrite gt_eqF// (negbTE p0). +have ? : p \is a fin_num by rewrite fin_numE py andbT -ltNye. +rewrite muleAC divee//. +have [->|p1] := eqVneq p 1; first by rewrite subee// inve0 mul1e. +rewrite -[X in _ = _ - X](@divee _ (p - 1)); last first. + by rewrite sube_eq// add0e. + by rewrite fin_numB//; apply/andP. +rewrite -muleBl//; last 2 first. + rewrite fin_numV//; first by rewrite sube_eq// add0e. + by rewrite sube_eq// -ltNye. + by rewrite fin_num_adde_defr. +by rewrite oppeB ?fin_num_adde_defl// addeA subee// add0e. Qed. End hoelder_conjugate. From 81a267f6cb8558e50bf033fd04b95b2e3ec4b914 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Tue, 17 Jun 2025 15:00:35 +0900 Subject: [PATCH 10/13] fix? --- theories/hoelder.v | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/theories/hoelder.v b/theories/hoelder.v index 4fa8de45b9..65e641b0f1 100644 --- a/theories/hoelder.v +++ b/theories/hoelder.v @@ -264,7 +264,8 @@ rewrite inveM; last first. rewrite invr_eq0 subr_eq0; apply/implyP => /eqP ->. by rewrite lee01/= ltry. rewrite inver (negbTE p0) inver invr_eq0 subr_eq0 (negbTE p1) invrK. -by rewrite EFinB muleBr// mule1 -EFinM mulVf// -EFinD addrC subrK. +rewrite EFinB muleBr// mule1 -EFinM mulVf// -EFinD addrC. +by rewrite (subrK p^-1%R). Qed. Lemma hoelder_conjugateP p q : p > -oo -> p != 0 -> From 4ecf4e6227878ddc056e87274d37b4d7c3112a11 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Tue, 17 Jun 2025 19:54:04 +0900 Subject: [PATCH 11/13] fix --- theories/hoelder.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/theories/hoelder.v b/theories/hoelder.v index 65e641b0f1..bc508548e7 100644 --- a/theories/hoelder.v +++ b/theories/hoelder.v @@ -264,8 +264,8 @@ rewrite inveM; last first. rewrite invr_eq0 subr_eq0; apply/implyP => /eqP ->. by rewrite lee01/= ltry. rewrite inver (negbTE p0) inver invr_eq0 subr_eq0 (negbTE p1) invrK. -rewrite EFinB muleBr// mule1 -EFinM mulVf// -EFinD addrC. -by rewrite (subrK p^-1%R). +rewrite EFinB muleBr// mule1 -EFinM mulVf// -EFinD. +by rewrite (addrC p^-1%R) (subrK p^-1%R). Qed. Lemma hoelder_conjugateP p q : p > -oo -> p != 0 -> From 3d85d06b22305f413c9a17175aefcd4747653031 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Tue, 17 Jun 2025 21:09:36 +0900 Subject: [PATCH 12/13] fix? --- theories/hoelder.v | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/theories/hoelder.v b/theories/hoelder.v index bc508548e7..8acf3ee731 100644 --- a/theories/hoelder.v +++ b/theories/hoelder.v @@ -756,8 +756,7 @@ rewrite (_ : f = ((f \+ g) \+ (-%R \o g))%R); last first. rewrite [X in _ <= 'N__[X] + _](_ : _ = (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. - rewrite (_ : _ \o _ = \- (EFin \o g))//. - by have := oppe_Lnorm mu (EFin \o g) p%:E. + by rewrite (_ : _ \o _ = \- (EFin \o g))//; exact/esym/oppe_Lnorm. by apply: minkowski_EFin => //; [exact: measurable_funD|exact: measurableT_comp]. Qed. From 475e03186d4878b25f90716cc6647b468335bde2 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Tue, 17 Jun 2025 22:22:22 +0900 Subject: [PATCH 13/13] fix? --- theories/hoelder.v | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/theories/hoelder.v b/theories/hoelder.v index 8acf3ee731..0b2375acca 100644 --- a/theories/hoelder.v +++ b/theories/hoelder.v @@ -756,7 +756,9 @@ rewrite (_ : f = ((f \+ g) \+ (-%R \o g))%R); last first. rewrite [X in _ <= 'N__[X] + _](_ : _ = (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 (_ : _ \o _ = \- (EFin \o g))//; exact/esym/oppe_Lnorm. + rewrite (_ : EFin \o (-%R \o g) = \- (EFin \o g))//. + apply: esym. + exact: oppe_Lnorm. by apply: minkowski_EFin => //; [exact: measurable_funD|exact: measurableT_comp]. Qed.