proposition: Lemma minkowski f g p : 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: Proof. 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 rewrite minkowski_lty// ?ltW// ltey; [exact: Nfoo|exact: Ngoo]. suff : '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. have [-> _|Nfg0] := eqVneq 'N_p%:E[(f \+ g)%R] 0. by rewrite adde_ge0 ?Lnorm_ge0. rewrite lee_pdivl_mulr ?fine_gt0// ?lt0e ?Nfg0 ?Lnorm_ge0//. 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 lt0e Nfg0 Lnorm_ge0. rewrite fineK ?ge0_fin_numE ?Lnorm_ge0// => /le_trans; apply. rewrite lee_pdivr_mull; last first. by rewrite fine_gt0// poweR_lty// andbT poweR_gt0// lt0e Nfg0 Lnorm_ge0. 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//. apply: (@le_trans _ _ (\int[mu]_x ((`|f x| + `|g x|) * `|f x + g x| `^ (p - 1))%:E)). rewrite ge0_le_integral//. - by move=> ? _; rewrite lee_fin mulr_ge0// powR_ge0. - apply: measurableT_comp => //; apply: measurable_funM. exact/measurableT_comp/measurable_funD. exact/measurableT_comp_powR/measurableT_comp/measurable_funD. - by move=> ? _; rewrite lee_fin mulr_ge0// powR_ge0. - apply/measurableT_comp => //; apply: measurable_funM. by apply/measurable_funD => //; exact: measurableT_comp. exact/measurableT_comp_powR/measurableT_comp/measurable_funD. - by move=> ? _; rewrite lee_fin ler_wpM2r// ?powR_ge0// ler_normD. under eq_integral=> ? _ 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. 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. 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_num_poweR// -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 _. 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 onemV ?gt_eqF// invf_div; apply: congr2; last by []. apply: eq_integral => x _; congr EFin. rewrite norm_powR// normr_id -powRrM mulrCA divff ?mulr1//. by rewrite subr_eq0 gt_eqF. apply: (@hoelder _ _ _ _ _ _ p (p / (p - 1))) => //. + exact/measurableT_comp_powR/measurableT_comp/measurable_funD. + by rewrite divr_gt0// subr_gt0. + 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 _ . 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 []. 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. apply: (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 addrCA subrr addr0. rewrite -muleA; congr (_ * _). 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. Qed.
imports: HB(structures) mathcomp(all_ssreflect ssralg ssrnum ssrint interval finmap) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(cardinality fsbigop ) signed reals ereal topology normedtype sequences real_interval esum measure lebesgue_measure lebesgue_integral numfun exp convex itv