Skip to content

Commit

Permalink
introduced notation
Browse files Browse the repository at this point in the history
  • Loading branch information
@hoheinzollern
hoheinzollern committed Aug 10, 2023
1 parent d8156fa commit a9f7045
Showing 1 changed file with 90 additions and 67 deletions.
157 changes: 90 additions & 67 deletions theories/lebesgue_integral.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -5615,13 +5615,15 @@ Qed.

End hoelder.

Section hoelder_sums.
Section lnorm.
Context (R : realType).
Local Open Scope ereal_scope.

Definition C_norm (p : R) (f : R^nat) : \bar R :=
Definition lnorm (p : R) (f : R^nat) : \bar R :=
(\sum_(x <oo) (`|f x| `^ p)%:E) `^ p^-1.

Local Notation "`| f |_ p" := (lnorm p f).

Lemma ge0_integral_count (a : nat -> \bar R) : (forall k, 0 <= a k) ->
\int[counting]_t (a t) = \sum_(k <oo) (a k).
Proof.
Expand All @@ -5633,9 +5635,9 @@ rewrite (@ge0_integral_measure_series _ _ R (fun n => [the measure _ _ of \d_ n]
by apply: eq_eseriesr=> i _; rewrite integral_dirac//= indicE mem_set// mul1e.
Qed.

Lemma lc_norm p (f : R^nat) : L_norm counting p f = C_norm p f.
Lemma Lnorm_lnorm_eq p (f : R^nat) : 'N[counting]_p [f] = `| f |_p.
Proof.
rewrite /C_norm -ge0_integral_count// => k.
rewrite /lnorm -ge0_integral_count// => k.
by rewrite lee_fin powR_ge0.
Qed.

Expand All @@ -5644,10 +5646,10 @@ Proof.
rewrite /poweR. case:x => //. case: ifPn => //.
Qed.

Lemma not_summable_cnorm_ifty p (f : R^nat) : (0 < p)%R ->
~summable [set: nat] (fun t : nat => (`|f t| `^ p)%:E) -> C_norm p f = +oo%E.
Lemma not_summable_lnorm_ifty p (f : R^nat) : (0 < p)%R ->
~summable [set: nat] (fun t : nat => (`|f t| `^ p)%:E) -> `| f |_p = +oo%E.
Proof.
rewrite /summable /C_norm=>p0.
rewrite /summable /lnorm=>p0.
rewrite ltNge leye_eq => /negP /negPn /eqP.
rewrite nneseries_esum; last first.
move=> n _; rewrite lee_fin powR_ge0//.
Expand All @@ -5656,27 +5658,37 @@ under eq_esum => i _ do rewrite gee0_abs ?lee_fin ?powR_ge0//.
by move=> ->; rewrite poweRyr// gt_eqF// invr_gt0.
Qed.

Lemma cnorm_ifty_not_summable p (f : R^nat) : (0 < p)%R ->
C_norm p f = +oo%E -> ~summable [set: nat] (fun t : nat => (`|f t| `^ p)%:E).
Lemma lnorm_ifty_not_summable p (f : R^nat) : (0 < p)%R ->
lnorm p f = +oo%E -> ~summable [set: nat] (fun t : nat => (`|f t| `^ p)%:E).
Proof.
rewrite /summable /C_norm=>p0 /poweRyr_inv.
rewrite /summable /lnorm=>p0 /poweRyr_inv.
under eq_esum => i _ do rewrite gee0_abs ?lee_fin ?powR_ge0//.
rewrite nneseries_esum; last first.
move=> n _; rewrite lee_fin powR_ge0//.
rewrite -fun_true => ->//.
Qed.

Lemma C_norm_ge0 (p : R) (f : R^nat) : (0 <= C_norm p f)%E.
Lemma lnorm_ge0 (p : R) (f : R^nat) : (0 <= `| f |_p)%E.
Proof.
rewrite /C_norm poweR_ge0//.
rewrite /lnorm poweR_ge0//.
Qed.

End lnorm.

Declare Scope lnorm_scope.
Notation "`| f |_ p" := (lnorm p f) : lnorm_scope.

Section hoelder_sums.
Context (R : realType).
Local Open Scope ereal_scope.
Local Open Scope lnorm_scope.

Lemma hoelder_sums (f g : R^nat) (p q : R) :
measurable_fun setT f -> measurable_fun setT g ->
(0 < p)%R -> (0 < q)%R -> (p^-1 + q^-1 = 1)%R ->
C_norm 1 (f \* g)%R <= C_norm p f * C_norm q g.
`| (f \* g)%R |_(1) <= `| f |_p * `| g |_q.
Proof.
move=> mf mg p0 q0 pq; rewrite -!lc_norm hoelder//.
move=> mf mg p0 q0 pq; rewrite -!Lnorm_lnorm_eq hoelder//.
Qed.

Lemma hoelder_sum2 (a1 a2 b1 b2 : R) (p q : R) : (0 <= a1)%R -> (0 <= a2)%R -> (0 <= b1)%R -> (0 <= b2)%R ->
Expand All @@ -5687,7 +5699,7 @@ move=> a10 a20 b10 b20 p0 q0 pq.
pose f := fun a b n => match n with 0%nat => a | 1%nat => b | _ => 0%R:R end.
have mf a b : measurable_fun setT (f a b). done.
have := @hoelder_sums (f a1 a2) (f b1 b2) p q (mf a1 a2) (mf b1 b2) p0 q0 pq.
rewrite /C_norm.
rewrite /lnorm.
rewrite (nneseries_split 2); last by move=> k; rewrite lee_fin powR_ge0.
rewrite ereal_series_cond eseries0 ?adde0; last first.
case=>//; case=>// n n2; rewrite /f /= mulr0 normr0 powR0//.
Expand Down Expand Up @@ -5719,7 +5731,7 @@ Variable mu : {measure set T -> \bar R}.
Local Open Scope ereal_scope.
Local Open Scope convex_scope.

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

Lemma ln_le0 (x : R) : (x <= 1 -> ln x <= 0)%R.
Proof.
Expand Down Expand Up @@ -5819,7 +5831,7 @@ rewrite {2}/w1 {2}/w2 -addrA (addrC (- _)%R) subrr addr0 powR1 mulr1//.
Qed.
(* follows https://math.stackexchange.com/questions/2200155/elementary-proof-that-xp-is-convex *)

Let minkowski00 (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.
Expand All @@ -5839,28 +5851,31 @@ Qed.

Lemma poweR_lty (a : \bar R) (r : R) : a < +oo -> a `^ r < +oo.
Proof.
by move: a => [a| |_]//=; rewrite ?ltry//; case: ifPn => // _; rewrite ltry.
by move: a => [a| | _]//=; rewrite ?ltry//; case: ifPn => // _; rewrite ltry.
Qed.

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

Let minkowski0 (f g : T -> R) (p : R) :
Let measurableT_comp_powR (f : T -> R) p :
measurable_fun setT f -> measurable_fun setT (fun x => f x `^ p)%R.
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 [f] < +oo -> 'N_p [g] < +oo -> 'N_p [(f \+ g)%R] < +oo.
(1 < p)%R -> `| f |_p < +oo -> `| g |_p < +oo -> `| (f \+ g)%R |_p < +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.
have := minkowski00 (fun x => 2 * f x)%R (fun x => 2 * g x)%R x p1.
have := minkowski_half (fun x => 2 * f x)%R (fun x => 2 * g x)%R x p1.
rewrite mulrA mulVf// mul1r mulrA mulVf// mul1r !normrM (@ger0_norm _ 2)//.
move=> /le_trans; apply.
rewrite !powRM// !mulrA -powR_inv1//.
rewrite -powRD; last by apply /implyP => _.
by rewrite (addrC _ p) -mulrDr.
rewrite /L_norm poweR_lty//.
rewrite /Lnorm 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.
Expand Down Expand Up @@ -5901,45 +5916,54 @@ Lemma gt0_ler_poweR (r : R) : (0 <= r)%R ->
{in `[0, +oo] &, {homo poweR ^~ r : x y / x <= y >-> x <= y}}.
Proof.
move=> r0 x y.
case: x => //= [x xint|_ _].
- case: y => //= [y yint xy|_ _].
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 case: eqP => [->|]; rewrite ?powRr0 ?leey.
- by rewrite leye_eq => /eqP ->.
Qed.

Lemma Lnorm_powR_K f p : (p != 0%R) -> `| f |_(p) `^ p = \int[mu]_x (`| f x | `^ p)%:E.
Proof.
move=>p0.
rewrite /Lnorm -poweRrM mulVf//.
by rewrite poweRe1// integral_ge0// => x _; rewrite lee_fin// powR_ge0.
Qed.

Lemma powRDm1 (x p : R) : (0 <= x -> 0 < p -> x `^ p = x * x `^ (p - 1))%R.
Proof.
move=> x0 p0.
have [->|x0'] := eqVneq x 0%R.
by rewrite mul0r powR0// gt_eqF.
rewrite -{2}(@powRr1 _ x)// -powRD.
by rewrite addrCA subrr addr0.
by rewrite x0' implybT.
Qed.

Lemma minkowski (f g : T -> R) (p : R) :
measurable_fun setT f -> measurable_fun setT g ->
(1 < p)%R ->
'N_p [(f \+ g)%R] <= 'N_p [f] + 'N_p [g].
`|(f \+ g)%R|_p <= `|f|_p + `|g|_p.
Proof.
move=> mf mg p1.
have [->|Nfoo] := eqVneq 'N_p[f] +oo.
by rewrite addye ?leey// -ltNye (lt_le_trans _ (L_norm_ge0 _ _ _)).
have [->|Ngoo] := eqVneq 'N_p[g] +oo.
by rewrite addey ?leey// -ltNye (lt_le_trans _ (L_norm_ge0 _ _ _)).
have Nfgoo : 'N_p[(f \+ g)%R] < +oo.
by apply: minkowski0 => //; rewrite ltey; [exact: Nfoo|exact: Ngoo].
have [->|Nfoo] := eqVneq `|f|_p +oo.
by rewrite addye ?leey// -ltNye (lt_le_trans _ (Lnorm_ge0 _ _ _)).
have [->|Ngoo] := eqVneq `|g|_p +oo.
by rewrite addey ?leey// -ltNye (lt_le_trans _ (Lnorm_ge0 _ _ _)).
have Nfgoo : `|(f \+ g)%R|_p < +oo.
by apply: minkowski_lty => //; rewrite ltey; [exact: Nfoo|exact: Ngoo].
have pm10 : (p - 1 != 0)%R.
by rewrite gt_eqF// subr_gt0.
have p0 : (0 < p)%R.
by apply: (lt_trans _ p1).
have pneq0 : (p != 0)%R.
by rewrite neq_lt p0 orbT.
have : 'N_p [(f \+ g)%R] `^ p <=
('N_p [f] + 'N_p [g]) * 'N_p [(f \+ g)%R] `^ p * ((fine 'N_p [(f \+ g)%R])^-1)%:E.
rewrite [leLHS](_ : _ = \int[mu]_x (`| f x + g x | `^ p)%:E); last first.
rewrite /L_norm -poweRrM mulVf; last by rewrite gt_eqF// (le_lt_trans _ p1).
by rewrite poweRe1 ?integral_ge0// => x _; rewrite lee_fin// powR_ge0.
rewrite [leLHS](_ : _ = \int[mu]_x (`|f x + g x| * `|f x + g x| `^ (p - 1))%:E); last first.
apply: eq_integral => x _; congr EFin.
have [->|fxgx0]:= eqVneq `|f x + g x|%R 0%R.
by rewrite mul0r powR0// gt_eqF//.
rewrite -[X in (X * _)%R]powRr1//.
rewrite -powRD; last by apply /implyP=> _.
by rewrite addrCA subrr addr0.
have : `|(f \+ g)%R|_p `^ p <=
(`|f|_p + `|g|_p) * `|(f \+ g)%R|_p `^ p * ((fine `|(f \+ g)%R|_p)^-1)%:E.
rewrite Lnorm_powR_K//.
under eq_integral => x _ do rewrite powRDm1//.
apply: (@le_trans _ _ (\int[mu]_x ((`|f x| + `|g x|) * `|f x + g x| `^ (p - 1))%:E)).
apply: ge0_le_integral => //.
- by move=> x _; rewrite lee_fin mulr_ge0// powR_ge0.
Expand All @@ -5965,15 +5989,15 @@ have : 'N_p [(f \+ g)%R] `^ p <=
exact: measurableT_comp.
apply: (measurableT_comp (f:=@powR R^~ (p-1)%R)) => //.
by apply: measurableT_comp => //; exact: measurable_funD.
apply: (@le_trans _ _ (('N_p[f] + 'N_p[g]) *
apply: (@le_trans _ _ ((`|f|_p + `|g|_p) *
(\int[mu]_x (`|f x + g x| `^ p)%:E) `^ (1 - p^-1))).
rewrite muleDl; last 2 first.
- rewrite fin_numElt (@lt_le_trans _ _ 0) ?poweR_ge0// andTb poweR_lty//.
by rewrite (@lty_poweRy _ (p^-1))// invr_neq0// eq_sym neq_lt (@lt_trans _ _ 1)%R.
- by rewrite ge0_adde_def//= inE L_norm_ge0.
- by rewrite ge0_adde_def//= inE Lnorm_ge0.
rewrite lee_add//.
- apply: (@le_trans _ _ ('N_1 [(f \* (@powR R ^~ (p - 1) \o normr \o (f \+ g)))%R])).
rewrite /L_norm invr1 [leRHS]poweRe1/=; last first.
- apply: (@le_trans _ _ (`|(f \* (@powR R ^~ (p - 1) \o normr \o (f \+ g)))%R|_1)).
rewrite /Lnorm invr1 [leRHS]poweRe1/=; last first.
by apply: integral_ge0 => x _; rewrite lee_fin powRr1.
rewrite le_eqVlt; apply/orP; left; apply/eqP.
apply: eq_integral => x _; congr EFin.
Expand All @@ -5984,33 +6008,31 @@ have : 'N_p [(f \+ g)%R] `^ p <=
- by rewrite divr_gt0// subr_gt0.
- by rewrite invf_div -(oneminvp pneq0) addrCA subrr addr0.
rewrite le_eqVlt; apply/orP; left; apply/eqP; apply: congr2=>[//|].
rewrite /L_norm/= invf_div -(oneminvp pneq0); apply: congr2=>[|//].
rewrite (oneminvp pneq0) -[in RHS]invf_div /Lnorm; apply: congr2 => [|//].
by apply: eq_integral => x _;
rewrite norm_powR// normr_id -powRrM mulrC -mulrA (mulrC (_^-1)) divff ?mulr1.
- rewrite [leLHS](_ : _ = 'N_1[(g \* (fun x => `|f x + g x| `^ (p - 1)))%R]); last first.
rewrite /L_norm invr1 poweRe1//; last first.
by apply: integral_ge0 => x _; rewrite lee_fin powRr1.
- rewrite [leLHS](_ : _ = `|(g \* (fun x => `|f x + g x| `^ (p - 1)))%R|_1); last first.
rewrite Lnorm1.
apply: eq_integral => x _ /=; congr (_%:E).
rewrite normrM norm_powR// normr_id//.
by rewrite powRr1// mulr_ge0// powR_ge0.
by exact: 0%R.
apply: le_trans.
apply: (@hoelder _ _ _ _ _ _ p ((1-p^-1)^-1)) => //.
- by apply: measurableT_comp_powR; apply: measurableT_comp => //; apply: measurable_funD => //.
- by rewrite invr_gt0 onem_gt0// invf_lt1.
- by rewrite invrK (addrC 1%R) addrA subrr add0r.
rewrite le_eqVlt; apply/orP; left; apply/eqP.
apply: congr1; rewrite /L_norm invrK; apply: congr2=>[|//].
apply: congr1; rewrite /Lnorm invrK; apply: congr2=>[|//].
by apply: eq_integral => x _;
rewrite ger0_norm ?powR_ge0// -powRrM oneminvp// invf_div mulrCA divff ?mulr1.
rewrite -muleA lee_wpmul2l// ?adde_ge0 ?L_norm_ge0//.
rewrite -muleA lee_wpmul2l// ?adde_ge0 ?Lnorm_ge0//.
rewrite le_eqVlt; apply/orP; left; apply/eqP.
rewrite oneminvp ?gt_eqF ?(lt_trans _ p1)//.
transitivity ('N_(p/(p -1)) [(@powR R ^~ (p - 1)%R \o normr \o (f \+ g)%R)]).
rewrite /L_norm/= -oneminvp ?gt_eqF ?(lt_trans _ p1)//.
apply congr2; last by rewrite oneminvp ?invf_div.
transitivity (`|(@powR R ^~ (p - 1)%R \o normr \o (f \+ g)%R)|_(p/(p -1))).
rewrite /Lnorm invf_div; apply: congr2 => [|//].
apply: eq_integral => x _;
by rewrite norm_powR ?normr_id ?oneminvp// -powRrM -mulrCA divff// mulr1.
rewrite /L_norm/=.
rewrite /Lnorm/=.
rewrite -poweRrM (mulrC (_^-1)) divff; last by rewrite neq_lt (@lt_trans _ _ 1 0)%R ?orbT.
rewrite [X in X * _]poweRe1; last by apply integral_ge0 => x _; rewrite lee_fin powR_ge0.
under eq_integral => x _ do
Expand All @@ -6024,19 +6046,20 @@ have : 'N_p [(f \+ g)%R] `^ p <=
rewrite fin_numE !neq_lt (@lt_le_trans _ _ 0 (-oo) _ _ (poweR_ge0 _ _)) ?orbT// andTb.
rewrite poweR_lty//; apply: (@lty_poweRy _ _ _ Nfgoo).
by rewrite invr_neq0// neq_lt (lt_trans _ p1) ?orbT.
have [-> _|Nfg0] := (eqVneq 'N_p[(f \+ g)%R] 0).
by rewrite adde_ge0 ?L_norm_ge0.
have [-> _|Nfg0] := (eqVneq `|(f \+ g)%R|_p 0).
by rewrite adde_ge0 ?Lnorm_ge0.
rewrite lee_pdivl_mulr ?fine_gt0// ?Nfgoo ?andbT; last by
rewrite lt_neqAle L_norm_ge0 andbT eq_sym.
rewrite -{1}(@fineK _ ('N_p[(f \+ g)%R] `^ p)); last by
rewrite lt_neqAle Lnorm_ge0 andbT eq_sym.
rewrite -{1}(@fineK _ (`|(f \+ g)%R|_p `^ p)); last by
rewrite fin_numElt (@lt_le_trans _ _ 0 -oo _ _ (poweR_ge0 _ _))// andTb poweR_lty.
rewrite -(invrK (fine _)) lee_pdivr_mull; last by
rewrite invr_gt0 fine_gt0// poweR_lty// andbT lt_neqAle eq_sym poweR_eq0 poweR_ge0// andbT;
rewrite neq_lt (lt_trans _ p1)// orbT andbT.
rewrite muleC -muleA -{1}(@fineK _ ('N_p[(f \+ g)%R] `^ p)); last by
rewrite muleC -muleA -{1}(@fineK _ (`|(f \+ g)%R|_p `^ p)); last by
rewrite fin_numElt (@lt_le_trans _ _ 0 -oo _ _ (poweR_ge0 _ _))// andTb poweR_lty.
rewrite -EFinM divff ?mule1; last by
rewrite neq_lt fine_gt0 ?orbT// lt_neqAle poweR_ge0 andbT eq_sym poweR_eq0 ?L_norm_ge0// neq_lt (lt_trans _ p1)// orbT andbT Nfg0 andTb poweR_lty.
rewrite ?fineK// fin_numElt (@lt_le_trans _ _ 0 -oo _ _ (L_norm_ge0 _ _ _))//.
rewrite neq_lt fine_gt0 ?orbT// lt_neqAle poweR_ge0 andbT eq_sym poweR_eq0 ?Lnorm_ge0// neq_lt (lt_trans _ p1)// orbT andbT Nfg0 andTb poweR_lty.
by rewrite ?fineK// fin_numElt (@lt_le_trans _ _ 0 -oo _ _ (Lnorm_ge0 _ _ _)).
Qed.

End minkowski.

0 comments on commit a9f7045

Please sign in to comment.