From cd4fa44146264fe36c58dcb7a909fbf5db383059 Mon Sep 17 00:00:00 2001 From: Alessandro Bruni Date: Thu, 15 Aug 2024 20:03:59 +0200 Subject: [PATCH] fix --- theories/lspace.v | 11 +++-------- 1 file changed, 3 insertions(+), 8 deletions(-) diff --git a/theories/lspace.v b/theories/lspace.v index 623ea6dad..aaed30615 100644 --- a/theories/lspace.v +++ b/theories/lspace.v @@ -115,17 +115,12 @@ Lemma LType2_integrable_sqr (f : LType mu 2) : mu.-integrable [set: T] (EFin \o (fun x => f x ^+ 2)). Proof. apply/integrableP; split. - -apply/EFin_measurable_fun. -exact: (@measurableT_comp _ _ _ _ _ _ (fun x : R => x ^+ 2)%R _ f) => //. + exact/EFin_measurable_fun/(@measurableT_comp _ _ _ _ _ _ (fun x : R => x ^+ 2)%R _ f)/measurable_lfun. rewrite (le_lt_trans _ (lfuny f))// ge0_le_integral//. - apply: measurableT_comp => //. - apply/EFin_measurable_fun. - exact: (@measurableT_comp _ _ _ _ _ _ (fun x : R => x ^+ 2)%R _ f) => //. + exact/EFin_measurable_fun/(@measurableT_comp _ _ _ _ _ _ (fun x : R => x ^+ 2)%R _ f)/measurable_lfun. - by move=> x _; rewrite lee_fin powR_ge0. -- apply/EFin_measurable_fun. - apply: (@measurableT_comp _ _ _ _ _ _ (fun x : R => x `^ 2)%R) => //. - exact: measurableT_comp. +- exact/EFin_measurable_fun/(@measurableT_comp _ _ _ _ _ _ (fun x : R => x `^ 2)%R)/measurableT_comp/measurable_lfun. - by move=> t _/=; rewrite lee_fin normrX powR_mulrn. Qed.