diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 3686b4bdf..0dd21c212 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -33,86 +33,9 @@ `wlength_sigma_sub_additive`, `wlength_sigma_finite` + measure instance of `hlength` + definition `lebesgue_stieltjes_measure` -- in `kernel.v`: - + `kseries` is now an instance of `Kernel_isSFinite_subdef` -- in `classical_sets.v`: - + lemma `setU_id2r` -- in `lebesgue_measure.v`: - + lemma `compact_measurable` - -- in `measure.v`: - + lemmas `outer_measure_subadditive`, `outer_measureU2` - -- in `lebesgue_measure.v`: - + declare `lebesgue_measure` as a `SigmaFinite` instance - + lemma `lebesgue_regularity_inner_sup` -- in `convex.v`: - + lemmas `conv_gt0`, `convRE` - -- in `exp.v`: - + lemmas `concave_ln`, `conjugate_powR` - -- in file `lebesgue_integral.v`, - + new lemmas `integral_le_bound`, `continuous_compact_integrable`, and - `lebesgue_differentiation_continuous`. - -- in `normedtype.v`: - + lemmas `open_itvoo_subset`, `open_itvcc_subset` - -- in `lebesgue_measure.v`: - + lemma `measurable_ball` - -- in file `normedtype.v`, - + new lemmas `normal_openP`, `uniform_regular`, - `regular_openP`, and `pseudometric_normal`. -- in file `topology.v`, - + new definition `regular_space`. - + new lemma `ent_closure`. - -- in `lebesgue_measure.v`: - + lemma `measurable_mulrr` - -- in `constructive_ereal.v`: - + lemma `eqe_pdivr_mull` - -- new file `hoelder.v`: - + definition `Lnorm`, notations `'N[mu]_p[f]`, `'N_p[f]` - + lemmas `Lnorm1`, `Lnorm_ge0`, `eq_Lnorm`, `Lnorm_eq0_eq0` - + lemma `hoelder` - -- in file `lebesgue_integral.v`, - + new lemmas `simple_bounded`, `measurable_bounded_integrable`, - `compact_finite_measure`, `approximation_continuous_integrable` - -- in `sequences.v`: - + lemma `cvge_harmonic` - -- in `mathcomp_extra.v`: - + lemmas `le_bigmax_seq`, `bigmax_sup_seq` - -- in `constructive_ereal.v`: - + lemma `bigmaxe_fin_num` -- in `ereal.v`: - + lemmas `uboundT`, `supremumsT`, `supremumT`, `ereal_supT`, `range_oppe`, - `ereal_infT` - -- in `measure.v`: - + definition `ess_sup`, lemma `ess_sup_ge0` -- in `convex.v`: - + definition `convex_function` - -- in `exp.v`: - + lemmas `ln_le0`, `ger_powR`, `ler1_powR`, `le1r_powR`, `ger1_powR`, - `ge1r_powR`, `ge1r_powRZ`, `le1r_powRZ` - -- in `hoelder.v`: - + lemmas `lnormE`, `hoelder2`, `convex_powR` - -- in `lebesgue_integral.v`: - + lemma `ge0_integral_count` - in `exp.v`: - + lemmas `powRDm1`, `poweRN`, `poweR_lty`, `lty_powerRy`, `gt0_ler_poweR` + + lemmas `powRDm1`, `fin_num_poweR`, poweRN`, `poweR_lty`, `lty_powerRy`, `gt0_ler_poweR` - in `mathcomp_extra.v`: + lemma `oneminv` diff --git a/classical/mathcomp_extra.v b/classical/mathcomp_extra.v index 1ee160abb..b95dcfac6 100644 --- a/classical/mathcomp_extra.v +++ b/classical/mathcomp_extra.v @@ -1016,6 +1016,8 @@ Arguments max_fun {T R} _ _ _ /. (* End of mathComp > 1.16 additions *) (************************************) +Reserved Notation "`1- x" (format "`1- x", at level 2). + Section onem. Variable R : numDomainType. Implicit Types r : R. @@ -1065,7 +1067,7 @@ Qed. End onem. Notation "`1- r" := (onem r) : ring_scope. -Lemma oneminv (F : numFieldType) (x : F) : x != 0 -> `1- (x^-1) = (x-1)/x. +Lemma oneminv (F : numFieldType) (x : F) : x != 0 -> `1- (x^-1) = (x - 1) / x. Proof. by move=> ?; rewrite mulrDl divff// mulN1r. Qed. Lemma lez_abs2 (a b : int) : 0 <= a -> a <= b -> (`|a| <= `|b|)%N. diff --git a/theories/exp.v b/theories/exp.v index 965ea0997..44774beb2 100644 --- a/theories/exp.v +++ b/theories/exp.v @@ -769,12 +769,8 @@ Qed. Lemma powRDm1 (x p : R) : 0 <= x -> 0 < p -> x * x `^ (p - 1) = x `^ p. Proof. -move=> x0 p0. -have [->|xneq0] := eqVneq x 0. - by rewrite mul0r powR0// gt_eqF. -rewrite -{1}(@powRr1 x)// -powRD. - by rewrite addrCA subrr addr0. -by rewrite xneq0 implybT. +rewrite le_eqVlt => /predU1P[<- p0|x0 p0]; first by rewrite mul0r powR0 ?gt_eqF. +by rewrite -{1}(powRr1 (ltW x0))// -powRD addrCA subrr addr0// gt_eqF. Qed. Lemma powRN x r : x `^ (- r) = (x `^ r)^-1. @@ -892,8 +888,8 @@ Proof. by move: x => [x'| |]//= x0; rewrite ?powRr1// (negbTE (oner_neq0 _)). Qed. -Lemma poweRN (x : \bar R) r : x \is a fin_num -> x `^ (- r) = (((fine x) `^ r)^-1)%:E. -Proof. case: x => // x xf. by rewrite poweR_EFin powRN. Qed. +Lemma poweRN x r : x \is a fin_num -> x `^ (- r) = (fine x `^ r)^-1%:E. +Proof. by case: x => // x xf; rewrite poweR_EFin powRN. Qed. Lemma poweRNyr r : r != 0%R -> -oo `^ r = 0. Proof. by move=> r0 /=; rewrite (negbTE r0). Qed. @@ -904,14 +900,14 @@ Proof. by case: x => [x| |] //=; case: ifP. Qed. Lemma eqy_poweR x r : (0 < r)%R -> x = +oo -> x `^ r = +oo. Proof. by move: x => [| |]//= r0 _; rewrite gt_eqF. Qed. -Lemma poweR_lty (a : \bar R) (r : R) : a < +oo -> a `^ r < +oo. +Lemma poweR_lty x r : x < +oo -> x `^ r < +oo. Proof. -by move: a => [a| | _]//=; rewrite ?ltry//; case: ifPn => // _; rewrite ltry. +by move: x => [x| |]//=; rewrite ?ltry//; case: ifPn => // _; rewrite ltry. Qed. -Lemma lty_poweRy (a : \bar R) (r : R) : r != 0%R -> a `^ r < +oo -> a < +oo. +Lemma lty_poweRy x r : r != 0%R -> x `^ r < +oo -> x < +oo. Proof. -by move=> r0; move: a => [a| | _]//=; rewrite ?ltry// (negbTE r0). +by move=> r0; move: x => [x| | _]//=; rewrite ?ltry// (negbTE r0). Qed. Lemma poweR0r r : r != 0%R -> 0 `^ r = 0. @@ -950,14 +946,18 @@ Proof. by move=> + /eqP => /poweR_eq0-> /andP[/eqP]. Qed. Lemma gt0_ler_poweR (r : R) : (0 <= r)%R -> {in `[0, +oo] &, {homo poweR ^~ r : x y / x <= y >-> x <= y}}. Proof. -move=> r0 x y. -case: x => //= [x /[1!in_itv]/= /andP[xint _]| _ _]. +move=> r0 + y; case=> //= [x /[1!in_itv]/= /andP[xint _]| _ _]. - case: y => //= [y /[1!in_itv]/= /andP[yint _] xy| _ _]. - - rewrite !lee_fin ge0_ler_powR//. - - by case: eqP => [->|]; rewrite ?powRr0 ?leey. + + by rewrite !lee_fin ge0_ler_powR. + + by case: eqP => [->|]; rewrite ?powRr0 ?leey. - by rewrite leye_eq => /eqP ->. Qed. +Lemma fin_num_poweR x r : x \is a fin_num -> x `^ r \is a fin_num. +Proof. +by move=> xfin; rewrite ge0_fin_numE ?poweR_lty ?ltey_eq ?xfin// poweR_ge0. +Qed. + Lemma poweRM x y r : 0 <= x -> 0 <= y -> (x * y) `^ r = x `^ r * y `^ r. Proof. have [->|rN0] := eqVneq r 0%R; first by rewrite !poweRe0 mule1. diff --git a/theories/hoelder.v b/theories/hoelder.v index 573801f0d..2ee781606 100644 --- a/theories/hoelder.v +++ b/theories/hoelder.v @@ -340,11 +340,26 @@ End convex_powR. Section minkowski. Context d (T : measurableType d) (R : realType). Variable mu : {measure set T -> \bar R}. -Local Open Scope convex_scope. +Implicit Types f g : T -> R. Local Notation "'N_ p [ f ]" := (Lnorm mu p f). +Local Open Scope ereal_scope. + +Let minkowski1 f g (p : R) : + measurable_fun setT f -> measurable_fun setT 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 ge0_le_integral//. +- by do 2 apply: measurableT_comp => //; exact: measurable_funD. +- by apply: measurableT_comp => //; apply/measurable_funD; + exact/measurableT_comp. +- by move=> x _; rewrite lee_fin ler_norm_add. +Qed. -Let minkowski_half (f g : T -> R) (p : R) x : 1 <= p -> +Local Open Scope ring_scope. +Let convex_half f g (p : R) x : 1 <= p -> `| 2^-1 * f x + 2^-1 * g x | `^ p <= 2^-1 * `| f x | `^ p + 2^-1 * `| g x | `^ p. Proof. @@ -356,176 +371,149 @@ rewrite {1 3}(_ : 2^-1 = 1 - 2^-1); last by rewrite {2}(splitr 1) div1r addrK. rewrite (@convex_powR _ _ p1 (@Itv.mk _ _ _ _)) ?inE/= ?in_itv/= ?normr_ge0//. by rewrite /Itv.itv_cond/= in_itv/= invr_ge0 ler0n invf_le1 ?ler1n. Qed. +Local Close Scope ring_scope. -Local Open Scope ereal_scope. - -Let measurableT_comp_powR (f : T -> R) p : +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. -Let minkowski_lty (f g : T -> R) (p : R) : - measurable_fun setT f -> measurable_fun setT g -> - (1 <= p)%R -> 'N_p%:E[f] < +oo -> 'N_p%:E[g] < +oo -> 'N_p%:E[(f \+ g)%R] < +oo. +Let minkowski_lty f g (p : R) : + measurable_fun setT f -> measurable_fun setT 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. -have h x : (`| f x + g x | `^ p <= 2 `^ (p - 1) * (`| f x | `^ p + `| g x | `^ p))%R. - have := minkowski_half (fun x => 2 * f x)%R (fun x => 2 * g x)%R x p1. - rewrite mulrA mulVf// mul1r mulrA mulVf// mul1r !normrM (@ger0_norm _ 2)//. - move=> /le_trans; apply. - rewrite !powRM// !mulrA -powR_inv1//. - rewrite -powRD; last by apply /implyP => _. +have p0 : p != 0%R by rewrite gt_eqF// (lt_le_trans _ p1). +have h x : (`| f x + g x | `^ p <= + 2 `^ (p - 1) * (`| f x | `^ p + `| g x | `^ p))%R. + have := convex_half (fun x => 2 * f x)%R (fun x => 2 * g x)%R x p1. + rewrite !normrM (@ger0_norm _ 2)// !mulrA mulVf// !mul1r => /le_trans; apply. + rewrite !powRM// !mulrA -powR_inv1// -powRD; last first. + by rewrite pnatr_eq0; exact: implybT. by rewrite (addrC _ p) -mulrDr. -rewrite unlock gt_eqF ?(lt_le_trans _ p1)// poweR_lty//. -apply: (@le_lt_trans _ _ (\int[mu]_x (2 `^ (p - 1) * (`|f x| `^ p + `|g x| `^ p)%R)%:E)). - apply: ge0_le_integral => //=. - - by move=> t _; rewrite lee_fin powR_ge0. - - by apply/EFin_measurable_fun/measurableT_comp_powR; - apply: measurableT_comp => //; exact: measurable_funD. - - by move=> t _; rewrite lee_fin// mulr_ge0// ?addr_ge0 ?powR_ge0. - - by apply/EFin_measurable_fun/measurable_funM => //; apply/measurable_funD => //; - apply: measurableT_comp_powR => //; apply: measurableT_comp. - - by move=> x _; rewrite lee_fin. -under eq_integral do rewrite EFinM. -rewrite ge0_integralM_EFin//; last 3 first. +rewrite unlock (gt_eqF (lt_le_trans _ p1))// poweR_lty//. +pose x := \int[mu]_x (2 `^ (p - 1) * (`|f x| `^ p + `|g x| `^ p))%:E. +rewrite (@le_lt_trans _ _ x)//. + rewrite ge0_le_integral//=. + - by move=> t _; rewrite lee_fin// powR_ge0. + - apply/EFin_measurable_fun/measurableT_comp_powR/measurableT_comp => //. + exact: measurable_funD. + - by move=> t _; rewrite lee_fin mulr_ge0 ?addr_ge0 ?powR_ge0. + - by apply/EFin_measurable_fun/measurable_funM/measurable_funD => //; + exact/measurableT_comp_powR/measurableT_comp. + - by move=> ? _; rewrite lee_fin. +rewrite {}/x; under eq_integral do rewrite EFinM. +rewrite ge0_integralZl_EFin ?powR_ge0//; last 2 first. - by move=> x _; rewrite lee_fin addr_ge0// powR_ge0. - by apply/EFin_measurable_fun/measurable_funD => //; - apply: measurableT_comp_powR => //; apply: measurableT_comp. - - by rewrite powR_ge0. + exact/measurableT_comp_powR/measurableT_comp. rewrite lte_mul_pinfty ?lee_fin ?powR_ge0//. under eq_integral do rewrite EFinD. rewrite ge0_integralD//; last 4 first. - by move=> x _; rewrite lee_fin powR_ge0. - - by apply/EFin_measurable_fun; - apply: measurableT_comp_powR => //; apply: measurableT_comp. + - exact/EFin_measurable_fun/measurableT_comp_powR/measurableT_comp. - by move=> x _; rewrite lee_fin powR_ge0. - - by apply/EFin_measurable_fun; - apply: measurableT_comp_powR => //; apply: measurableT_comp. + - exact/EFin_measurable_fun/measurableT_comp_powR/measurableT_comp. rewrite lte_add_pinfty//. -- rewrite -Lnorm_powR_K ?(gt_eqF (lt_trans _ p1))//. - exact: poweR_lty. - by rewrite gt_eqF// (lt_le_trans _ p1). -- rewrite -Lnorm_powR_K ?(gt_eqF (lt_trans _ p1))//. - exact: poweR_lty. - by rewrite gt_eqF// (lt_le_trans _ p1). +- by rewrite -Lnorm_powR_K ?(gt_eqF (lt_trans _ p1))// poweR_lty. +- by rewrite -Lnorm_powR_K ?(gt_eqF (le_trans _ p1))// poweR_lty. Qed. -Lemma minkowski (f g : T -> R) (p : R) : - measurable_fun setT f -> measurable_fun setT g -> - (1 <= p)%R -> +Lemma minkowski f g (p : R) : + measurable_fun setT f -> measurable_fun setT 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 => /orP [/eqP <-|p1]. - rewrite !Lnorm1. - apply: (le_trans (y:=\int[mu]_x ((`|f x|)%:E + (`|g x|)%:E))). - apply: ge0_le_integral => //. - - by repeat apply: measurableT_comp => //; apply: measurable_funD. - - apply: measurableT_comp => //. - by apply: measurable_funD; apply: measurableT_comp. - - by move=> x _; rewrite lee_fin ler_norm_add. - by rewrite le_eqVlt ge0_integralD ?eqxx//; repeat apply: measurableT_comp => //. +move=> mf mg; rewrite le_eqVlt => /predU1P[<-|p1]; first exact: minkowski1. have [->|Nfoo] := eqVneq 'N_p%:E[f] +oo. by rewrite addye ?leey// -ltNye (lt_le_trans _ (Lnorm_ge0 _ _ _)). have [->|Ngoo] := eqVneq 'N_p%:E[g] +oo. by rewrite addey ?leey// -ltNye (lt_le_trans _ (Lnorm_ge0 _ _ _)). have Nfgoo : 'N_p%:E[(f \+ g)%R] < +oo. - by apply: minkowski_lty => //; rewrite ?ltW// ltey; [exact: Nfoo|exact: Ngoo]. -have pm10 : (p - 1 != 0)%R. - by rewrite gt_eqF// subr_gt0. -have p0 : (0 < p)%R. - by apply: (lt_trans _ p1). -have pneq0 : (p != 0)%R. - by rewrite neq_lt p0 orbT. -have : 'N_p%:E[(f \+ g)%R] `^ p <= - ('N_p%:E[f] + 'N_p%:E[g]) * 'N_p%:E[(f \+ g)%R] `^ p * ((fine 'N_p%:E[(f \+ g)%R])^-1)%:E. - rewrite Lnorm_powR_K//. + by rewrite minkowski_lty// ?ltW// ltey; [exact: Nfoo|exact: Ngoo]. +have p0 : (0 < p)%R by exact: (lt_trans _ p1). +have : 'N_p%:E[(f \+ g)%R] `^ p <= ('N_p%:E[f] + 'N_p%:E[g]) * + 'N_p%:E[(f \+ g)%R] `^ p * ((fine 'N_p%:E[(f \+ g)%R])^-1)%:E. + rewrite Lnorm_powR_K ?gt_eqF//. under eq_integral => x _ do rewrite -powRDm1//. - apply: (@le_trans _ _ (\int[mu]_x ((`|f x| + `|g x|) * `|f x + g x| `^ (p - 1))%:E)). - apply: ge0_le_integral => //. + apply: (@le_trans _ _ + (\int[mu]_x ((`|f x| + `|g x|) * `|f x + g x| `^ (p - 1))%:E)). + rewrite ge0_le_integral//. - by move=> x _; rewrite lee_fin mulr_ge0// powR_ge0. - apply: measurableT_comp => //; apply: measurable_funM. by apply: measurableT_comp => //; exact: measurable_funD. - apply: (measurableT_comp (f:=@powR R^~ (p-1)%R)) =>//. - by apply: measurableT_comp => //; exact: measurable_funD. + exact/measurableT_comp_powR/measurableT_comp/measurable_funD. - by move=> x _; rewrite lee_fin mulr_ge0// powR_ge0. - apply: measurableT_comp => //; apply: measurable_funM. by apply: measurable_funD => //; exact: measurableT_comp. - apply: (measurableT_comp (f:=@powR R^~ (p-1)%R)) => //. - by apply: measurableT_comp => //; exact: measurable_funD. + exact/measurableT_comp_powR/measurableT_comp/measurable_funD. - by move=> x _; rewrite lee_fin ler_wpmul2r// ?powR_ge0// ler_norm_add. under eq_integral=> x _ do rewrite mulrDl EFinD. rewrite ge0_integralD//; last 4 first. - by move=> x _; rewrite lee_fin mulr_ge0// powR_ge0. - apply: measurableT_comp => //; apply: measurable_funM. exact: measurableT_comp. - apply: (measurableT_comp (f:=@powR R^~ (p-1)%R)) => //. - by apply: measurableT_comp => //; exact: measurable_funD. + exact/measurableT_comp_powR/measurableT_comp/measurable_funD. - by move=> x _; rewrite lee_fin mulr_ge0// powR_ge0. - apply: measurableT_comp => //; apply: measurable_funM. exact: measurableT_comp. - apply: (measurableT_comp (f:=@powR R^~ (p-1)%R)) => //. - by apply: measurableT_comp => //; exact: measurable_funD. - apply: (@le_trans _ _ (('N_p%:E[f] + 'N_p%:E[g]) * - (\int[mu]_x (`|f x + g x| `^ p)%:E) `^ (`1- (p^-1)))). + exact/measurableT_comp_powR/measurableT_comp/measurable_funD. + 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_numElt (@lt_le_trans _ _ 0) ?poweR_ge0// andTb poweR_lty//. - rewrite /= gt_eqF// in Nfgoo. - by rewrite (@lty_poweRy _ _ (p^-1))// invr_neq0// eq_sym neq_lt (@lt_trans _ _ 1)%R. + - rewrite fin_num_poweR// -Lnorm_powR_K ?gt_eqF// fin_num_poweR//. + by rewrite ge0_fin_numE ?Lnorm_ge0. - by rewrite ge0_adde_def// inE Lnorm_ge0. rewrite lee_add//. - - apply: (@le_trans _ _ ('N_1[(f \* (@powR R ^~ (p - 1) \o normr \o (f \+ g)))%R])). - rewrite /Lnorm gt_eqF// invr1 [leRHS]poweRe1/=; last first. - by apply: integral_ge0 => x _; rewrite lee_fin powRr1. - rewrite le_eqVlt; apply/orP; left; apply/eqP. - apply: eq_integral => x _; congr EFin. - by rewrite powRr1// -{1}(ger0_norm (powR_ge0 _ _)) -normrM. - apply: le_trans. - apply: (@hoelder _ _ _ _ _ _ p (p / (p - 1))) => //. - - by apply: (measurableT_comp (measurableT_comp _ _) (measurable_funD _ _)). + - pose h0 := (@powR R ^~ (p - 1) \o normr \o (f \+ g))%R; pose h := (f \* h0)%R. + rewrite [leLHS](_ : _ = 'N_1[h]%R); last first. + rewrite Lnorm1; apply: eq_integral => x _. + by rewrite normrM (ger0_norm (powR_ge0 _ _)). + rewrite [leRHS](_ : _ = 'N_p%:E[f] * 'N_(p / (p - 1))%:E[h0]). + rewrite (@hoelder _ _ _ _ _ _ p (p / (p - 1)) _ _ _ _ _) //. + - exact/measurableT_comp_powR/measurableT_comp/measurable_funD. - by rewrite divr_gt0// subr_gt0. - - by rewrite invf_div -(oneminv pneq0) addrCA subrr addr0. - rewrite le_eqVlt; apply/orP; left; apply/eqP; apply: congr2=>[//|]. - rewrite (oneminv pneq0) -[in RHS]invf_div /Lnorm gt_eqF; last first. - rewrite divr_gt0// subr_gt0//. - apply: congr2 => [|//]. - by apply: eq_integral => x _; - rewrite norm_powR// normr_id -powRrM mulrC -mulrA (mulrC (_^-1)) divff ?mulr1. - - rewrite [leLHS](_ : _ = 'N_1[(g \* (fun x => `|f x + g x| `^ (p - 1)))%R]); last first. - under eq_integral=> x _ do rewrite -(normr_id (f x + g x))%R -norm_powR// -normrM. - by rewrite -(Lnorm1). - apply: le_trans. - apply: (@hoelder _ _ _ _ _ _ p ((`1-(p^-1))^-1)) => //. - - by apply: measurableT_comp_powR; apply: measurableT_comp => //; apply: measurable_funD => //. + - by rewrite invf_div -oneminv ?gt_eqF// addrCA subrr addr0. + congr (_ * _). + rewrite unlock mulf_eq0 gt_eqF//= invr_eq0 subr_eq0 (gt_eqF p1). + rewrite oneminv ?gt_eqF// invf_div; apply: congr2; last by []. + apply: eq_integral => x _; congr EFin. + by rewrite norm_powR// normr_id -powRrM mulrCA divff ?mulr1// subr_eq0 gt_eqF. + - pose h0 := (fun x => `|f x + g x| `^ (p - 1))%R; pose h := (g \* h0)%R. + rewrite [leLHS](_ : _ = 'N_1[h]); last first. + rewrite Lnorm1; apply: eq_integral => x _ . + by rewrite normrM norm_powR// normr_id. + rewrite [leRHS](_ : _ = 'N_p%:E[g] * 'N_((1 - p^-1)^-1)%:E[h0])//. + rewrite (le_trans (@hoelder _ _ _ _ _ _ p (1 - p^-1)^-1 _ _ _ _ _))//. + - exact/measurableT_comp_powR/measurableT_comp/measurable_funD. - by rewrite invr_gt0 onem_gt0// invf_lt1. - - by rewrite invrK /onem (addrC 1%R) addrA subrr add0r. - rewrite le_eqVlt; apply/orP; left; apply/eqP. - apply: congr1; rewrite /Lnorm gt_eqF; last first. - rewrite invr_gt0 onem_gt0// invf_lt1//. - rewrite invrK; apply: congr2=>[|//]. - by apply: eq_integral => x _; - rewrite ger0_norm ?powR_ge0// -powRrM oneminv// invf_div mulrCA divff ?mulr1. - rewrite le_eqVlt; apply/orP; left; apply/eqP; rewrite -muleA; congr (_ * _). + - by rewrite invrK addrCA subrr addr0. + congr (_ * _). + rewrite unlock invrK invr_eq0 subr_eq0 eq_sym invr_eq1 (gt_eqF p1). + apply: congr2; last by []. + apply: eq_integral => x _; congr EFin. + rewrite -/(onem p^-1) oneminv ?gt_eqF// norm_powR// normr_id -powRrM invf_div mulrCA. + by rewrite divff ?subr_eq0 ?gt_eqF// ?mulr1. + rewrite -muleA; congr (_ * _). under [X in X * _]eq_integral=> x _ do rewrite powRDm1 ?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; first - by rewrite /Lnorm gt_eqF// ?fine_poweR. - rewrite /= gt_eqF// in Nfgoo. - rewrite ge0_fin_numE ?(lty_poweRy (invr_neq0 _) Nfgoo)//. - by apply: integral_ge0=> x _; rewrite lee_fin powR_ge0. -have [-> _|Nfg0] := (eqVneq 'N_p%:E[(f \+ g)%R] 0). + congr (_ * _); rewrite poweRN; last first. + by rewrite -Lnorm_powR_K ?gt_eqF// fin_num_poweR// ge0_fin_numE ?Lnorm_ge0. + congr (_^-1%:E). + by rewrite unlock gt_eqF// fine_poweR. +have [-> _|Nfg0] := eqVneq 'N_p%:E[(f \+ g)%R] 0. by rewrite adde_ge0 ?Lnorm_ge0. -rewrite lee_pdivl_mulr ?fine_gt0// ?Nfgoo ?andbT; last by - rewrite lt_neqAle Lnorm_ge0 andbT eq_sym. -rewrite -{1}(@fineK _ ('N_p%:E[(f \+ g)%R] `^ p)); last by - rewrite fin_numElt (@lt_le_trans _ _ 0 -oo _ _ (poweR_ge0 _ _))// andTb poweR_lty. -rewrite -(invrK (fine _)) lee_pdivr_mull; last by - rewrite invr_gt0 fine_gt0// poweR_lty// lt_neqAle eq_sym poweR_eq0 ?Lnorm_ge0// pneq0 poweR_ge0 !andbT Nfg0. -rewrite muleC -muleA -{1}(@fineK _ ('N_p%:E[(f \+ g)%R] `^ p)); last by - rewrite fin_numElt (@lt_le_trans _ _ 0 -oo _ _ (poweR_ge0 _ _))// andTb poweR_lty. -rewrite -EFinM divff ?mule1; last by - rewrite neq_lt fine_gt0 ?orbT// lt_neqAle poweR_ge0 andbT eq_sym poweR_eq0 ?Lnorm_ge0// neq_lt (lt_trans _ p1)// orbT andbT Nfg0 andTb poweR_lty. -by rewrite ?fineK// fin_numElt (@lt_le_trans _ _ 0 -oo _ _ (Lnorm_ge0 _ _ _)). +rewrite lee_pdivl_mulr ?fine_gt0// ?Nfgoo ?andbT; last first. + by rewrite lt_neqAle Lnorm_ge0 andbT eq_sym. +rewrite -{1}(@fineK _ ('N_p%:E[(f \+ g)%R] `^ p)); last first. + by rewrite fin_num_poweR// ge0_fin_numE// Lnorm_ge0. +rewrite -(invrK (fine _)) lee_pdivr_mull; last first. + rewrite invr_gt0 fine_gt0// (poweR_lty _ Nfgoo) andbT poweR_gt0//. + by rewrite lt_neqAle eq_sym Lnorm_ge0 andbT. +rewrite fineK ?ge0_fin_numE ?Lnorm_ge0// => /le_trans; apply. +rewrite lee_pdivr_mull; last first. + rewrite fine_gt0// poweR_lty// andbT poweR_gt0// lt_neqAle eq_sym Nfg0/=. + by rewrite Lnorm_ge0. +by rewrite fineK// 1?muleC// fin_num_poweR// ge0_fin_numE ?Lnorm_ge0. Qed. End minkowski.