Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Minkowski #1000

Merged
merged 8 commits into from
Nov 13, 2023
Merged

Minkowski #1000

Show file tree
Hide file tree
Changes from 7 commits
Commits
Show all changes
8 commits
Select commit Hold shift + click to select a range
5222d08
Convexity of power function
affeldt-aist Jun 3, 2023
891b922
Minkowski's inequality and accessory lemmas
hoheinzollern Aug 23, 2023
bb1700d
Moved `oneminv` to `mathcomp_extra.v`
hoheinzollern Aug 24, 2023
5f80dae
updated lemmas with new Lp_norm definition
hoheinzollern Sep 7, 2023
384c3be
Minkowski for p=1
hoheinzollern Sep 30, 2023
5756c76
rebase, minor simplifications
affeldt-aist Oct 27, 2023
b52ba3c
last fixes
affeldt-aist Oct 28, 2023
2aa2ea2
fix
affeldt-aist Oct 28, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
9 changes: 9 additions & 0 deletions CHANGELOG_UNRELEASED.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -34,6 +34,15 @@
+ measure instance of `hlength`
+ definition `lebesgue_stieltjes_measure`

- in `exp.v`:
+ lemmas `mulr_powRB1`, `fin_num_poweR`, poweRN`, `poweR_lty`, `lty_poweRy`, `gt0_ler_poweR`

- in `mathcomp_extra.v`:
+ lemma `onemV`

- in `hoelder.v`:
+ lemmas `powR_Lnorm`, `minkowski`

### Changed

- in `hoelder.v`:
Expand Down
5 changes: 5 additions & 0 deletions classical/mathcomp_extra.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down Expand Up @@ -1065,6 +1067,9 @@ Qed.
End onem.
Notation "`1- r" := (onem r) : ring_scope.

Lemma onemV (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.
Proof. by case: a => //= n _; case: b. Qed.

Expand Down
42 changes: 38 additions & 4 deletions theories/exp.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -620,7 +620,7 @@ End Ln.

Section PowR.
Variable R : realType.
Implicit Types a x : R.
Implicit Types a x y z r : R.

Definition powR a x := if a == 0 then (x == 0)%:R else expR (x * ln a).

Expand Down Expand Up @@ -707,7 +707,7 @@ move=> /andP[a0 a1] r1.
by rewrite (le_trans (ger_powR _ r1)) ?powRr1 ?a0// ltW.
Qed.

Lemma ge0_ler_powR (r : R) : 0 <= r ->
Lemma ge0_ler_powR r : 0 <= r ->
{in Num.nneg &, {homo powR ^~ r : x y / x <= y >-> x <= y}}.
Proof.
rewrite le_eqVlt => /predU1P[<- x y _ _ _|]; first by rewrite !powRr0.
Expand All @@ -719,7 +719,7 @@ move=> /predU1P[->//|xy]; first by rewrite eqxx.
by apply/orP; right; rewrite /powR !gt_eqF// ltr_expR ltr_pmul2l// ltr_ln.
Qed.

Lemma gt0_ltr_powR (r : R) : 0 < r ->
Lemma gt0_ltr_powR r : 0 < r ->
{in Num.nneg &, {homo powR ^~ r : x y / x < y >-> x < y}}.
Proof.
move=> r0 x y x0 y0 xy; have := ge0_ler_powR (ltW r0) x0 y0 (ltW xy).
Expand Down Expand Up @@ -749,7 +749,7 @@ move=> x1 y0 r1.
by rewrite (powRM _ (le_trans _ x1))// ler_wpmul2r ?powR_ge0// le1r_powR// x0.
Qed.

Lemma powRrM (x y z : R) : x `^ (y * z) = (x `^ y) `^ z.
Lemma powRrM x y z : x `^ (y * z) = (x `^ y) `^ z.
Proof.
rewrite /powR mulf_eq0; have [_|xN0] := eqVneq x 0.
by case: (y == 0); rewrite ?eqxx//= oner_eq0 ln1 mulr0 expR0.
Expand All @@ -767,6 +767,12 @@ have [->|] := eqVneq r 0; first by rewrite mul1r add0r.
by rewrite implybF mul0r => _ /negPf ->.
Qed.

Lemma mulr_powRB1 x p : 0 <= x -> 0 < p -> x * x `^ (p - 1) = x `^ p.
Proof.
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.
Proof.
have [r0|r0] := eqVneq r 0%R; first by rewrite r0 oppr0 powRr0 invr1.
Expand Down Expand Up @@ -882,6 +888,9 @@ Proof.
by move: x => [x'| |]//= x0; rewrite ?powRr1// (negbTE (oner_neq0 _)).
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.

Expand All @@ -891,6 +900,16 @@ 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 x r : x < +oo -> x `^ r < +oo.
Proof.
by move: x => [x| |]//=; rewrite ?ltry//; case: ifPn => // _; rewrite ltry.
Qed.

Lemma lty_poweRy x r : r != 0%R -> x `^ r < +oo -> x < +oo.
Proof.
by move=> r0; move: x => [x| | _]//=; rewrite ?ltry// (negbTE r0).
Qed.

Lemma poweR0r r : r != 0%R -> 0 `^ r = 0.
Proof. by move=> r0; rewrite poweR_EFin powR0. Qed.

Expand Down Expand Up @@ -924,6 +943,21 @@ Qed.
Lemma poweR_eq0_eq0 x r : 0 <= x -> x `^ r = 0 -> x = 0.
Proof. by move=> + /eqP => /poweR_eq0-> /andP[/eqP]. Qed.

Lemma gt0_ler_poweR r : (0 <= r)%R ->
{in `[0, +oo] &, {homo poweR ^~ r : x y / x <= y >-> x <= y}}.
Copy link
Member

@affeldt-aist affeldt-aist Oct 27, 2023 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Maybe we should use Rpos.nneg here? I misread.

Proof.
move=> r0 + y; case=> //= [x /[1!in_itv]/= /andP[xint _]| _ _].
- case: y => //= [y /[1!in_itv]/= /andP[yint _] xy| _ _].
+ 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.
Expand Down
196 changes: 185 additions & 11 deletions theories/hoelder.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -35,17 +35,15 @@ Reserved Notation "'N_ p [ F ]"

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) :=
match p with
| p%:E => if p == 0%R then
| p%:E => (if p == 0%R then
mu (f @^-1` (setT `\ 0%R))
else
(\int[mu]_x (`|f x| `^ p)%:E) `^ p^-1
| +oo => if mu [set: T] > 0 then ess_sup mu (normr \o f) else 0
| -oo => 0
(\int[mu]_x (`|f x| `^ p)%:E) `^ p^-1)%E
| +oo%E => (if mu [set: T] > 0 then ess_sup mu (normr \o f) else 0)%E
| -oo%E => 0%E
end.
Canonical locked_Lnorm := Unlockable Lnorm.unlock.
Arguments Lnorm {d T R} mu p f.
Expand Down Expand Up @@ -87,7 +85,15 @@ under eq_integral => x _ do rewrite ger0_norm ?powR_ge0//.
by rewrite fp//; apply: integral_ge0 => t _; rewrite lee_fin powR_ge0.
Qed.

Lemma powR_Lnorm f r : r != 0%R ->
'N_r%:E[f] `^ r = \int[mu]_x (`| f x | `^ r)%:E.
Proof.
move=> r0; rewrite unlock (negbTE r0) -poweRrM mulVf// poweRe1//.
by apply: integral_ge0 => x _; rewrite lee_fin// powR_ge0.
Qed.

End Lnorm_properties.

#[global]
Hint Extern 0 (0 <= Lnorm _ _ _) => solve [apply: Lnorm_ge0] : core.

Expand All @@ -96,7 +102,7 @@ Notation "'N[ mu ]_ p [ f ]" := (Lnorm mu p f).
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 [the measure _ _ of counting] p f).

Lemma Lnorm_counting p (f : R^nat) : (0 < p)%R ->
Expand Down Expand Up @@ -186,8 +192,8 @@ 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 lt_neqAle eq_sym f0// Lnorm_ge0.
have {g0}gpos : 0 < 'N_q%:E[g] by rewrite lt_neqAle eq_sym g0// Lnorm_ge0.
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.
Expand Down Expand Up @@ -296,8 +302,7 @@ have [->|w10] := eqVneq w1 0.
by rewrite !mul0r powR0// gt_eqF.
by rewrite ge1r_powRZ// /w2 lt_neqAle eq_sym w20/=; apply/andP.
have [->|w20] := eqVneq w2 0.
rewrite !mul0r !addr0 ge1r_powRZ// onem_le1// andbT.
by rewrite lt_neqAle eq_sym onem_ge0// andbT.
by rewrite !mul0r !addr0 ge1r_powRZ// onem_le1// andbT lt0r w10 onem_ge0.
have [->|p_neq1] := eqVneq p 1.
by rewrite !powRr1// addr_ge0// mulr_ge0// /w2 ?onem_ge0.
have {p_neq1} {}p1 : 1 < p by rewrite lt_neqAle eq_sym p_neq1.
Expand Down Expand Up @@ -330,3 +335,172 @@ by rewrite {2}/w1 {2}/w2 subrK powR1 mulr1.
Qed.

End convex_powR.

Section minkowski.
Context d (T : measurableType d) (R : realType).
Variable mu : {measure set T -> \bar R}.
Implicit Types (f g : T -> R) (p : R).

Let convex_powR_abs_half f g p x : 1 <= p ->
`| 2^-1 * f x + 2^-1 * g x | `^ p <=
2^-1 * `| f x | `^ p + 2^-1 * `| g x | `^ p.
Proof.
move=> p1; rewrite (@le_trans _ _ ((2^-1 * `| f x | + 2^-1 * `| g x |) `^ p))//.
rewrite ge0_ler_powR ?nnegrE ?(le_trans _ p1)//.
by rewrite (le_trans (ler_norm_add _ _))// 2!normrM ger0_norm.
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.

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 Open Scope ereal_scope.

Let minkowski1 f g p : 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/measurable_funD; exact/measurableT_comp.
- by move=> x _; rewrite lee_fin ler_norm_add.
Qed.

Let minkowski_lty f g p :
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 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_powR_abs_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 ?pnatr_eq0 ?implybT//.
by rewrite (addrC _ p) -mulrDr.
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.
apply: (@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 => //;
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.
- exact/EFin_measurable_fun/measurableT_comp_powR/measurableT_comp.
- by move=> x _; rewrite lee_fin powR_ge0.
- exact/EFin_measurable_fun/measurableT_comp_powR/measurableT_comp.
by rewrite lte_add_pinfty// -powR_Lnorm ?(gt_eqF (lt_trans _ p1))// poweR_lty.
Qed.

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.
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_wpmul2r// ?powR_ge0// ler_norm_add.
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: lee_add.
- 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.

End minkowski.
Loading