-
Notifications
You must be signed in to change notification settings - Fork 49
/
Copy pathhoelder.v
332 lines (296 loc) · 13.9 KB
/
hoelder.v
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
(* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C. *)
From HB Require Import structures.
From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint interval finmap.
From mathcomp Require Import mathcomp_extra boolp classical_sets functions.
From mathcomp Require Import cardinality fsbigop .
Require Import signed reals ereal topology normedtype sequences real_interval.
Require Import esum measure lebesgue_measure lebesgue_integral numfun exp.
Require Import convex itv.
(******************************************************************************)
(* Hoelder's Inequality *)
(* *)
(* This file provides Hoelder's inequality. *)
(* *)
(* 'N[mu]_p[f] := (\int[mu]_x (`|f x| `^ p)%:E) `^ p^-1 *)
(* The corresponding definition is Lnorm. *)
(* *)
(******************************************************************************)
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Import Order.TTheory GRing.Theory Num.Def Num.Theory.
Import numFieldTopology.Exports.
Local Open Scope classical_set_scope.
Local Open Scope ring_scope.
Reserved Notation "'N[ mu ]_ p [ F ]"
(at level 5, F at level 36, mu at level 10,
format "'[' ''N[' mu ]_ p '/ ' [ F ] ']'").
(* for use as a local notation when the measure is in context: *)
Reserved Notation "'N_ p [ F ]"
(at level 5, F at level 36, format "'[' ''N_' p '/ ' [ F ] ']'").
Declare Scope Lnorm_scope.
Local Open Scope ereal_scope.
Section Lnorm.
Context d {T : measurableType d} {R : realType}.
Variable mu : {measure set T -> \bar R}.
Local Open Scope ereal_scope.
Implicit Types (p : \bar R) (f g : T -> R) (r : R).
Definition Lnorm p f :=
match p with
| 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
end.
Local Notation "'N_ p [ f ]" := (Lnorm p f).
Lemma Lnorm1 f : 'N_1[f] = \int[mu]_x `|f x|%:E.
Proof.
rewrite /Lnorm oner_eq0 invr1// poweRe1//.
by apply: eq_integral => t _; rewrite powRr1.
by apply: integral_ge0 => t _; rewrite powRr1.
Qed.
Lemma Lnorm_ge0 p f : 0 <= 'N_p[f].
Proof.
move: p => [r/=|/=|//].
by case: ifPn => // r0; exact: poweR_ge0.
by case: ifPn => // /ess_sup_ge0; apply => t/=.
Qed.
Lemma eq_Lnorm p f g : f =1 g -> 'N_p[f] = 'N_p[g].
Proof. by move=> fg; congr Lnorm; exact/funext. Qed.
Lemma Lnorm_eq0_eq0 r f : (0 < r)%R -> measurable_fun setT f ->
'N_r%:E[f] = 0 -> ae_eq mu [set: T] (fun t => (`|f t| `^ r)%:E) (cst 0).
Proof.
move=> r0 mf/=; rewrite (gt_eqF r0) => /poweR_eq0_eq0 fp.
apply/ae_eq_integral_abs => //=.
apply: measurableT_comp => //.
apply: (@measurableT_comp _ _ _ _ _ _ (@powR R ^~ r)) => //.
exact: measurableT_comp.
under eq_integral => x _ do rewrite ger0_norm ?powR_ge0//.
by rewrite fp//; apply: integral_ge0 => t _; rewrite lee_fin powR_ge0.
Qed.
End Lnorm.
#[global]
Hint Extern 0 (0 <= Lnorm _ _ _) => solve [apply: Lnorm_ge0] : core.
Notation "'N[ mu ]_ p [ f ]" := (Lnorm mu p f).
Section lnorm.
(* lnorm is just Lnorm applied to counting *)
Context d {T : measurableType d} {R : realType}.
Local Notation "'N_ p [ f ]" := (Lnorm [the measure _ _ of counting] p f).
Lemma Lnorm_counting p (f : R^nat) : (0 < p)%R ->
'N_p%:E [f] = (\sum_(k <oo) (`| f k | `^ p)%:E) `^ p^-1.
Proof.
move=> p0 /=; rewrite gt_eqF// ge0_integral_count// => k.
by rewrite lee_fin powR_ge0.
Qed.
End lnorm.
Section hoelder.
Context d {T : measurableType d} {R : realType}.
Variable mu : {measure set T -> \bar R}.
Local Open Scope ereal_scope.
Implicit Types (p q : R) (f g : T -> R).
Let measurableT_comp_powR f p :
measurable_fun [set: T] 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).
Let integrable_powR f p : (0 < p)%R ->
measurable_fun [set: T] f -> 'N_p%:E[f] != +oo ->
mu.-integrable [set: T] (fun x => (`|f x| `^ p)%:E).
Proof.
move=> p0 mf foo; apply/integrableP; split.
apply: measurableT_comp => //; apply: measurableT_comp_powR.
exact: measurableT_comp.
rewrite ltey; apply: contra foo.
move=> /eqP/(@eqy_poweR _ _ p^-1); rewrite invr_gt0 => /(_ p0) <-.
rewrite /= (gt_eqF p0); apply/eqP; congr (_ `^ _).
by apply/eq_integral => t _; rewrite ger0_norm// powR_ge0.
Qed.
Let hoelder0 f g p q : measurable_fun setT f -> measurable_fun setT g ->
(0 < p)%R -> (0 < q)%R -> (p^-1 + q^-1 = 1)%R ->
'N_p%:E[f] = 0 -> 'N_1[(f \* g)%R] <= 'N_p%:E[f] * 'N_q%:E[g].
Proof.
move=> mf mg p0 q0 pq f0; rewrite f0 mul0e Lnorm1 [leLHS](_ : _ = 0)//.
rewrite (ae_eq_integral (cst 0)) => [|//||//|]; first by rewrite integral0.
- apply: measurableT_comp => //; apply: measurableT_comp => //.
exact: measurable_funM.
- have := Lnorm_eq0_eq0 p0 mf f0.
apply: filterS => x /(_ I) /= [] /powR_eq0_eq0 + _.
by rewrite normrM => ->; rewrite mul0r.
Qed.
Let normalized p f x := `|f x| / fine 'N_p%:E[f].
Let normalized_ge0 p f x : (0 <= normalized p f x)%R.
Proof. by rewrite /normalized divr_ge0// fine_ge0// Lnorm_ge0. Qed.
Let measurable_normalized p f : measurable_fun [set: T] f ->
measurable_fun [set: T] (normalized p f).
Proof. by move=> mf; apply: measurable_funM => //; exact: measurableT_comp. Qed.
Let integral_normalized f p : (0 < p)%R -> 0 < 'N_p%:E[f] ->
mu.-integrable [set: T] (fun x => (`|f x| `^ p)%:E) ->
\int[mu]_x (normalized p f x `^ p)%:E = 1.
Proof.
move=> p0 fpos ifp.
transitivity (\int[mu]_x (`|f x| `^ p / fine ('N_p%:E[f] `^ p))%:E).
apply: eq_integral => t _.
rewrite powRM//; last by rewrite invr_ge0 fine_ge0// Lnorm_ge0.
rewrite -[in LHS]powR_inv1; last by rewrite fine_ge0 // Lnorm_ge0.
by rewrite fine_poweR powRAC -powR_inv1 // powR_ge0.
have fp0 : 0 < \int[mu]_x (`|f x| `^ p)%:E.
rewrite /= (gt_eqF p0) in fpos.
apply: gt0_poweR fpos; rewrite ?invr_gt0//.
by apply integral_ge0 => x _; rewrite lee_fin; exact: powR_ge0.
rewrite /Lnorm (gt_eqF p0) -poweRrM mulVf ?lt0r_neq0// poweRe1//; last exact: ltW.
under eq_integral do rewrite EFinM muleC.
have foo : \int[mu]_x (`|f x| `^ p)%:E < +oo.
move/integrableP: ifp => -[_].
by under eq_integral do rewrite gee0_abs// ?lee_fin ?powR_ge0//.
rewrite integralZl//; apply/eqP; rewrite eqe_pdivr_mull ?mule1.
- by rewrite fineK// ge0_fin_numE// ltW.
- by rewrite gt_eqF// fine_gt0// foo andbT.
Qed.
Lemma hoelder f g p q : measurable_fun setT f -> measurable_fun setT g ->
(0 < p)%R -> (0 < q)%R -> (p^-1 + q^-1 = 1)%R ->
'N_1[(f \* g)%R] <= 'N_p%:E[f] * 'N_q%:E[g].
Proof.
move=> mf mg p0 q0 pq.
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 [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.
rewrite [leLHS](_ : _ = 'N_1[(F \* G)%R] * 'N_p%:E[f] * 'N_q%:E[g]); last first.
rewrite !Lnorm1.
under [in RHS]eq_integral.
move=> x _.
rewrite /F /G /= /normalized (mulrC `|f x|)%R mulrA -(mulrA (_^-1)).
rewrite (mulrC (_^-1)) -mulrA ger0_norm; last first.
by rewrite mulr_ge0// divr_ge0 ?(fine_ge0, Lnorm_ge0, invr_ge0).
by rewrite mulrC -normrM EFinM; over.
rewrite ge0_integralZl//; last 2 first.
- apply: measurableT_comp => //; apply: measurableT_comp => //.
exact: measurable_funM.
- by rewrite lee_fin mulr_ge0// invr_ge0 fine_ge0//Lnorm_ge0.
rewrite -muleA muleC muleA EFinM muleCA 2!muleA.
rewrite (_ : _ * 'N_p%:E[f] = 1) ?mul1e; last first.
rewrite -[X in _ * X]fineK; last by rewrite ge0_fin_numE ?ltey// Lnorm_ge0.
by rewrite -EFinM mulVr ?unitfE ?gt_eqF// fine_gt0// fpos/= ltey.
rewrite (_ : 'N_q%:E[g] * _ = 1) ?mul1e// muleC.
rewrite -[X in _ * X]fineK; last by rewrite ge0_fin_numE ?ltey// Lnorm_ge0.
by rewrite -EFinM mulVr ?unitfE ?gt_eqF// fine_gt0// gpos/= ltey.
rewrite -(mul1e ('N_p%:E[f] * _)) -muleA lee_pmul ?mule_ge0 ?Lnorm_ge0//.
rewrite [leRHS](_ : _ = \int[mu]_x (F x `^ p / p + G x `^ q / q)%:E).
rewrite Lnorm1 ae_ge0_le_integral //.
- apply: measurableT_comp => //; apply: measurableT_comp => //.
by apply: measurable_funM => //; exact: measurable_normalized.
- by move=> x _; rewrite lee_fin addr_ge0// divr_ge0// ?powR_ge0// ltW.
- by apply: measurableT_comp => //; apply: measurable_funD => //;
apply: measurable_funM => //; apply: measurableT_comp_powR => //;
exact: measurable_normalized.
apply/aeW => x _; rewrite lee_fin ger0_norm ?conjugate_powR ?normalized_ge0//.
by rewrite mulr_ge0// normalized_ge0.
under eq_integral do rewrite EFinD mulrC (mulrC _ (_^-1)).
rewrite ge0_integralD//; last 4 first.
- by move=> x _; rewrite lee_fin mulr_ge0// ?invr_ge0 ?powR_ge0// ltW.
- apply: measurableT_comp => //; apply: measurableT_comp => //.
by apply: measurableT_comp_powR => //; exact: measurable_normalized.
- by move=> x _; rewrite lee_fin mulr_ge0// ?invr_ge0 ?powR_ge0// ltW.
- apply: measurableT_comp => //; apply: measurableT_comp => //.
by apply: measurableT_comp_powR => //; exact: measurable_normalized.
under eq_integral do rewrite EFinM.
rewrite {1}ge0_integralZl//; last 3 first.
- apply: measurableT_comp => //.
by apply: measurableT_comp_powR => //; exact: measurable_normalized.
- by move=> x _; rewrite lee_fin powR_ge0.
- by rewrite lee_fin invr_ge0 ltW.
under [X in (_ + X)%E]eq_integral => x _ do rewrite EFinM.
rewrite ge0_integralZl//; last 3 first.
- apply: measurableT_comp => //.
by apply: measurableT_comp_powR => //; exact: measurable_normalized.
- by move=> x _; rewrite lee_fin powR_ge0.
- by rewrite lee_fin invr_ge0 ltW.
rewrite integral_normalized//; last exact: integrable_powR.
rewrite integral_normalized//; last exact: integrable_powR.
by rewrite 2!mule1 -EFinD pq.
Qed.
End hoelder.
Section hoelder2.
Context {R : realType}.
Local Open Scope ring_scope.
Lemma hoelder2 (a1 a2 b1 b2 : R) (p q : R) :
0 <= a1 -> 0 <= a2 -> 0 <= b1 -> 0 <= b2 ->
0 < p -> 0 < q -> p^-1 + q^-1 = 1 ->
a1 * b1 + a2 * b2 <= (a1 `^ p + a2 `^ p) `^ p^-1 *
(b1 `^ q + b2 `^ q) `^ q^-1.
Proof.
move=> a10 a20 b10 b20 p0 q0 pq.
pose f a b n : R := match n with 0%nat => a | 1%nat => b | _ => 0 end.
have mf a b : measurable_fun setT (f a b) by [].
have := hoelder [the measure _ _ of counting] (mf a1 a2) (mf b1 b2) p0 q0 pq.
rewrite !Lnorm_counting//.
rewrite (nneseries_split 2); last by move=> k; rewrite lee_fin powR_ge0.
rewrite ereal_series_cond eseries0 ?adde0; last first.
by move=> [//|] [//|n _]; rewrite /f /= mulr0 normr0 powR0.
rewrite 2!big_ord_recr /= big_ord0 add0e powRr1 ?normr_ge0 ?powRr1 ?normr_ge0//.
rewrite (nneseries_split 2); last by move=> k; rewrite lee_fin powR_ge0.
rewrite ereal_series_cond eseries0 ?adde0; last first.
by move=> [//|] [//|n _]; rewrite /f /= normr0 powR0// gt_eqF.
rewrite 2!big_ord_recr /= big_ord0 add0e -EFinD poweR_EFin.
rewrite (nneseries_split 2); last by move=> k; rewrite lee_fin powR_ge0.
rewrite ereal_series_cond eseries0 ?adde0; last first.
by move=> [//|] [//|n _]; rewrite /f /= normr0 powR0// gt_eqF.
rewrite 2!big_ord_recr /= big_ord0 add0e -EFinD poweR_EFin.
rewrite -EFinM invr1 powRr1; last by rewrite addr_ge0.
do 2 (rewrite ger0_norm; last by rewrite mulr_ge0).
by do 4 (rewrite ger0_norm; last by []).
Qed.
End hoelder2.
Section convex_powR.
Context {R : realType}.
Local Open Scope ring_scope.
Lemma convex_powR p : 1 <= p ->
convex_function `[0, +oo[%classic (@powR R ^~ p).
Proof.
move=> p1 t x y /[!inE] /= /[!in_itv] /= /[!andbT] x_ge0 y_ge0.
have p0 : 0 < p by rewrite (lt_le_trans _ p1).
rewrite !convRE; set w1 := `1-(t%:inum); set w2 := t%:inum.
have [->|w10] := eqVneq w1 0.
rewrite !mul0r !add0r; have [->|w20] := eqVneq w2 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.
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.
pose q := p / (p - 1).
have q1 : 1 <= q by rewrite /q ler_pdivl_mulr// ?mul1r ?gerBl// subr_gt0.
have q0 : 0 < q by rewrite (lt_le_trans _ q1).
have pq1 : p^-1 + q^-1 = 1.
rewrite /q invf_div -{1}(div1r p) -mulrDl addrCA subrr addr0.
by rewrite mulfV// gt_eqF.
rewrite -(@powRr1 _ (w1 * x `^ p + w2 * y `^ p)); last first.
by rewrite addr_ge0// mulr_ge0// ?powR_ge0// /w2 ?onem_ge0// itv_ge0.
have -> : 1 = p^-1 * p by rewrite mulVf ?gt_eqF.
rewrite powRrM (ge0_ler_powR (le_trans _ (ltW p1)))//.
- by rewrite nnegrE addr_ge0// mulr_ge0 /w2 ?onem_ge0.
- by rewrite nnegrE powR_ge0.
have -> : w1 * x + w2 * y = w1 `^ (p^-1) * w1 `^ (q^-1) * x +
w2 `^ (p^-1) * w2 `^ (q^-1) * y.
rewrite -!powRD pq1; [|exact/implyP..].
by rewrite !powRr1// /w2 ?onem_ge0.
apply: (@le_trans _ _ ((w1 * x `^ p + w2 * y `^ p) `^ (p^-1) *
(w1 + w2) `^ q^-1)).
pose a1 := w1 `^ p^-1 * x. pose a2 := w2 `^ p^-1 * y.
pose b1 := w1 `^ q^-1. pose b2 := w2 `^ q^-1.
have : a1 * b1 + a2 * b2 <= (a1 `^ p + a2 `^ p) `^ p^-1 *
(b1 `^ q + b2 `^ q) `^ q^-1.
by apply: hoelder2 => //; rewrite ?mulr_ge0 ?powR_ge0.
rewrite ?powRM ?powR_ge0 -?powRrM ?mulVf ?powRr1 ?gt_eqF ?onem_ge0/w2//.
by rewrite mulrAC (mulrAC _ y) => /le_trans; exact.
by rewrite {2}/w1 {2}/w2 subrK powR1 mulr1.
Qed.
End convex_powR.