Skip to content

Commit

Permalink
Minkowski for p=1
Browse files Browse the repository at this point in the history
  • Loading branch information
@hoheinzollern
hoheinzollern committed Oct 3, 2023
1 parent 33ff679 commit 7995997
Show file tree
Hide file tree
Showing 2 changed files with 27 additions and 23 deletions.
4 changes: 2 additions & 2 deletions theories/exp.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -954,8 +954,8 @@ move=> r0 x y.
case: x => //= [x xint| _ _].
- case: y => //= [y yint xy| _ _].
- rewrite !lee_fin gt0_ler_powR//.
by move: xint; rewrite !in_itv /= andbT lee_fin => /andP [x0 _].
by move: yint; rewrite !in_itv /= andbT lee_fin => /andP [y0 _].
by move: xint; rewrite !in_itv /= leey andbT lee_fin.
by move: yint; rewrite !in_itv /= leey andbT lee_fin.
- by case: eqP => [->|]; rewrite ?powRr0 ?leey.
- by rewrite leye_eq => /eqP ->.
Qed.
Expand Down
46 changes: 25 additions & 21 deletions theories/hoelder.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -346,22 +346,17 @@ Local Open Scope convex_scope.

Local Notation "'N_ p [ f ]" := (Lnorm mu p f).

Let minkowski_half (f g : T -> R) (p : R) x : (1 < p)%R ->
Let minkowski_half (f g : T -> R) (p : R) x : (1 <= p)%R ->
(`| 2^-1 * f x + 2^-1 * g x | `^ p <= 2^-1 * `| f x | `^ p + 2^-1 * `| g x | `^ p)%R.
Proof.
move=> p1.
apply: (@le_trans _ _ ((2^-1 * `| f x | + 2^-1 * `| g x |) `^ p))%R.
apply: gt0_ler_powR.
- by rewrite le_eqVlt; apply/orP; right; apply: (@lt_trans _ _ 1%R) => //.
- by rewrite in_itv/= andbT.
- by rewrite in_itv/= andbT.
- have -> : (2^-1 * `|f x| + 2^-1 * `|g x| = `|2^-1 * f x| + `|2^-1 * g x|)%R.
by rewrite !normrM !(@ger0_norm _ (2^-1)).
exact: ler_norm_add.
apply: ge0_ler_powR; rewrite ?nnegrE ?(le_trans _ p1)//.
by rewrite -[in leRHS](@ger0_norm _ (2^-1))// -!normrM; exact: ler_norm_add.
rewrite {1 3}(_ : 2^-1 = 1 - 2^-1 :> R)%R; last by rewrite {2}(splitr 1) div1r addrK.
have K : ((2^-1 : R) \in `[0, 1])%R.
by rewrite in_itv//= invr_ge0 ler0n/= invf_le1// ler1n.
apply (@convex_powR _ _ (ltW p1) (@Itv.mk _ `[0, 1] 2^-1 K)%R (`|f x|)%R (`|g x|)%R);
apply (@convex_powR _ _ p1 (@Itv.mk _ `[0, 1] 2^-1 K)%R (`|f x|)%R (`|g x|)%R);
by rewrite inE /= in_itv /= normr_ge0.
Qed.

Expand All @@ -371,7 +366,7 @@ Proof. exact: (@measurableT_comp _ _ _ _ _ _ (@powR R ^~ p)). Qed.

Let minkowski_lty (f g : T -> R) (p : R) :
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.
(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 h x : (`| f x + g x | `^ p <= 2 `^ (p - 1) * (`| f x | `^ p + `| g x | `^ p))%R.
Expand All @@ -381,12 +376,12 @@ have h x : (`| f x + g x | `^ p <= 2 `^ (p - 1) * (`| f x | `^ p + `| g x | `^
rewrite !powRM// !mulrA -powR_inv1//.
rewrite -powRD; last by apply /implyP => _.
by rewrite (addrC _ p) -mulrDr.
rewrite /Lnorm gt_eqF ?(lt_trans _ p1)// poweR_lty//.
rewrite /Lnorm gt_eqF ?(lt_le_trans _ p1)// poweR_lty//.
apply: (@le_lt_trans _ _ (\int[mu]_x (2 `^ (p - 1) * (`|f x| `^ p + `|g x| `^ p)%R)%:E)).
apply: ge0_le_integral => //=.
- by move=> t _; rewrite lee_fin// powR_ge0.
- apply/EFin_measurable_fun/measurableT_comp_powR.
by apply: measurableT_comp => //; exact: measurable_funD.
- by move=> t _; rewrite lee_fin powR_ge0.
- by apply/EFin_measurable_fun/measurableT_comp_powR;
apply: measurableT_comp => //; exact: measurable_funD.
- by move=> t _; rewrite lee_fin// mulr_ge0// ?addr_ge0 ?powR_ge0.
- by apply/EFin_measurable_fun/measurable_funM => //; apply/measurable_funD => //;
apply: measurableT_comp_powR => //; apply: measurableT_comp.
Expand All @@ -407,26 +402,35 @@ rewrite ge0_integralD//; last 4 first.
- by apply/EFin_measurable_fun;
apply: measurableT_comp_powR => //; apply: measurableT_comp.
rewrite lte_add_pinfty//.
- rewrite /= gt_eqF ?(lt_trans _ p1)// in Nfoo.
- rewrite /= gt_eqF ?(lt_le_trans _ p1)// in Nfoo.
apply: lty_poweRy Nfoo.
by rewrite invr_neq0// gt_eqF// (le_lt_trans _ p1).
- rewrite /= gt_eqF ?(lt_trans _ p1)// in Ngoo.
by rewrite invr_neq0// gt_eqF// (lt_le_trans _ p1).
- rewrite /= gt_eqF ?(lt_le_trans _ p1)// in Ngoo.
apply: lty_poweRy Ngoo.
by rewrite invr_neq0// gt_eqF// (le_lt_trans _ p1).
by rewrite invr_neq0// gt_eqF// (lt_le_trans _ p1).
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_norm_add.
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.
by rewrite addey ?leey// -ltNye (lt_le_trans _ (Lnorm_ge0 _ _ _)).
have Nfgoo : 'N_p%:E[(f \+ g)%R] < +oo.
by apply: minkowski_lty => //; rewrite ltey; [exact: Nfoo|exact: Ngoo].
by apply: minkowski_lty => //; rewrite ?ltW// ltey; [exact: Nfoo|exact: Ngoo].
have pm10 : (p - 1 != 0)%R.
by rewrite gt_eqF// subr_gt0.
have p0 : (0 < p)%R.
Expand Down

0 comments on commit 7995997

Please sign in to comment.