Minkowski for p=1

math-comp · Sep 30, 2023 · 5211206 · 5211206
1 parent 048badf
commit 5211206
Showing 1 changed file with 12 additions and 3 deletions.
diff --git a/theories/hoelder.v b/theories/hoelder.v
@@ -440,10 +440,19 @@ Qed.
 
 Lemma minkowski (f g : T -> R) (p : R) :
   measurable_fun setT f -> measurable_fun setT g ->
-  (1 < p)%R ->
+  (1 <= p)%R ->
   'N_p%:E[(f \+ g)%R] <= 'N_p%:E[f] + 'N_p%:E[g].
 Proof.
-move=> mf mg p1.
+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_normD.
+  by rewrite le_eqVlt ge0_integralD ?eqxx//; repeat apply: measurableT_comp => //.  
 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.
@@ -548,4 +557,4 @@ rewrite -EFinM divff ?mule1; last by
 by rewrite ?fineK// fin_numElt (@lt_le_trans _ _ 0 -oo _ _ (Lnorm_ge0 _ _ _)).
 Qed.
 
-End minkowski.
+End minkowski.