proposition: Lemma hoelder 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_1[(f \* g)%R] <= 'N_p%:E[f] * 'N_q%:E[g].
proof: Proof. move=> mf mg p0 q0 pq. have [f0|f0] := eqVneq 'N_p%:E[f] 0%E; first exact: hoelder0. have [g0|g0] := eqVneq 'N_q%:E[g] 0%E. rewrite muleC; apply: le_trans; last by apply: hoelder0 => //; rewrite addrC. by under eq_Lnorm do rewrite /= mulrC. have {f0}fpos : 0 < 'N_p%:E[f] by rewrite lt0e f0 Lnorm_ge0. have {g0}gpos : 0 < 'N_q%:E[g] by rewrite lt0e g0 Lnorm_ge0. have [foo|foo] := eqVneq 'N_p%:E[f] +oo%E; first by rewrite foo gt0_mulye ?leey. have [goo|goo] := eqVneq 'N_q%:E[g] +oo%E; first by rewrite goo gt0_muley ?leey. pose F := normalized p f; pose G := normalized q g. rewrite [leLHS](_ : _ = 'N_1[(F \* G)%R] * 'N_p%:E[f] * 'N_q%:E[g]); last first. rewrite !Lnorm1; under [in RHS]eq_integral. move=> x _; rewrite /F /G /normalized/=. rewrite ger0_norm; last by rewrite mulr_ge0 ?divr_ge0 ?fine_ge0 ?Lnorm_ge0. by rewrite mulrACA -normrM EFinM; over. rewrite ge0_integralZr//; last 2 first. - by do 2 apply: measurableT_comp => //; exact: measurable_funM. - by rewrite lee_fin mulr_ge0// invr_ge0 fine_ge0// Lnorm_ge0. rewrite -!muleA [X in _ * X](_ : _ = 1) ?mule1// EFinM muleACA. rewrite (_ : _ * 'N_p%:E[f] = 1) ?mul1e; last first. rewrite -[X in _ * X]fineK; last by rewrite ge0_fin_numE ?ltey// Lnorm_ge0. by rewrite -EFinM mulVr ?unitfE ?gt_eqF// fine_gt0// fpos/= ltey. rewrite -[X in _ * X]fineK; last by rewrite ge0_fin_numE ?ltey// Lnorm_ge0. by rewrite -EFinM mulVr ?unitfE ?gt_eqF// fine_gt0// gpos/= ltey. rewrite -(mul1e ('N_p%:E[f] * _)) -muleA lee_pmul ?mule_ge0 ?Lnorm_ge0//. rewrite [leRHS](_ : _ = \int[mu]_x (F x `^ p / p + G x `^ q / q)%:E). rewrite Lnorm1 ae_ge0_le_integral //. - do 2 apply: measurableT_comp => //. by apply: measurable_funM => //; exact: measurable_normalized. - by move=> x _; rewrite lee_fin addr_ge0// divr_ge0// ?powR_ge0// ltW. - by apply: measurableT_comp => //; apply: measurable_funD => //; apply: measurable_funM => //; apply: measurableT_comp_powR => //; exact: measurable_normalized. apply/aeW => x _; rewrite lee_fin ger0_norm ?conjugate_powR ?normalized_ge0//. by rewrite mulr_ge0// normalized_ge0. under eq_integral do rewrite EFinD. rewrite ge0_integralD//; last 4 first. - by move=> x _; rewrite lee_fin mulr_ge0// ?invr_ge0 ?powR_ge0// ltW. - apply: measurableT_comp => //; apply: measurable_funM => //. by apply: measurableT_comp_powR => //; exact: measurable_normalized. - by move=> x _; rewrite lee_fin mulr_ge0// ?invr_ge0 ?powR_ge0// ltW. - apply: measurableT_comp => //; apply: measurable_funM => //. by apply: measurableT_comp_powR => //; exact: measurable_normalized. under eq_integral do rewrite EFinM. rewrite [X in X + _]ge0_integralZr//; last 3 first. - apply: measurableT_comp => //. by apply: measurableT_comp_powR => //; exact: measurable_normalized. - by move=> x _; rewrite lee_fin powR_ge0. - by rewrite lee_fin invr_ge0 ltW. under [X in _ + X]eq_integral => x _ do rewrite EFinM. rewrite ge0_integralZr//; last 3 first. - apply: measurableT_comp => //. by apply: measurableT_comp_powR => //; exact: measurable_normalized. - by move=> x _; rewrite lee_fin powR_ge0. - by rewrite lee_fin invr_ge0 ltW. rewrite integral_normalized//; last exact: integrable_powR. rewrite integral_normalized//; last exact: integrable_powR. by rewrite 2!mul1e -EFinD pq. 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