Library mathcomp.analysis.hoelder
(* 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.
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.
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.
Lemma Lnorm1 f : 'N_1[f] = \int[mu]_x `|f x|%:E.
Lemma Lnorm_ge0 p f : 0 ≤ 'N_p[f].
Lemma eq_Lnorm p f g : f =1 g → 'N_p[f] = 'N_p[g].
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).
End Lnorm.
#[global]
Hint Extern 0 (0 ≤ Lnorm _ _ _) ⇒ solve [apply: Lnorm_ge0] : core.
Notation "'N[ mu ]_ p [ f ]" := (Lnorm mu p f).
Section lnorm.
(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.
Lemma Lnorm1 f : 'N_1[f] = \int[mu]_x `|f x|%:E.
Lemma Lnorm_ge0 p f : 0 ≤ 'N_p[f].
Lemma eq_Lnorm p f g : f =1 g → 'N_p[f] = 'N_p[g].
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).
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}.
Lemma Lnorm_counting p (f : R^nat) : (0 < p)%R →
'N_p%:E [f] = (\sum_(k <oo) (`| f k | `^ p)%:E) `^ p^-1.
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.
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).
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].
Let normalized p f x := `|f x| / fine 'N_p%:E[f].
Let normalized_ge0 p f x : (0 ≤ normalized p f x)%R.
Let measurable_normalized p f : measurable_fun [set: T] f →
measurable_fun [set: T] (normalized p f).
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.
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].
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.
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).
End convex_powR.
Lemma Lnorm_counting p (f : R^nat) : (0 < p)%R →
'N_p%:E [f] = (\sum_(k <oo) (`| f k | `^ p)%:E) `^ p^-1.
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.
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).
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].
Let normalized p f x := `|f x| / fine 'N_p%:E[f].
Let normalized_ge0 p f x : (0 ≤ normalized p f x)%R.
Let measurable_normalized p f : measurable_fun [set: T] f →
measurable_fun [set: T] (normalized p f).
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.
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].
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.
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).
End convex_powR.