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.
Canonical locked_Lnorm := Unlockable Lnorm.unlock.
Arguments Lnorm {d T R} mu p f.
Section Lnorm_properties.
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).
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).
Lemma powR_Lnorm f r : r != 0%R →
'N_r%:E[f] `^ r = \int[mu]_x (`| f x | `^ r)%:E.
End Lnorm_properties.
#[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.
Canonical locked_Lnorm := Unlockable Lnorm.unlock.
Arguments Lnorm {d T R} mu p f.
Section Lnorm_properties.
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).
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).
Lemma powR_Lnorm f r : r != 0%R →
'N_r%:E[f] `^ r = \int[mu]_x (`| f x | `^ r)%:E.
End Lnorm_properties.
#[global]
Hint Extern 0 (0 ≤ Lnorm _ _ _) ⇒ solve [apply: Lnorm_ge0] : core.
Notation "'N[ mu ]_ p [ f ]" := (Lnorm mu p f).
Section lnorm.
l-norm is just L-norm applied to counting
Context d {T : measurableType d} {R : realType}.
Local Open Scope ereal_scope.
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.
Section minkowski.
Context d (T : measurableType d) (R : realType).
Variable mu : {measure set T → \bar R}.
Implicit Types (f g : T → R) (p : R).
Let convex_powR_abs_half f g p x : 1 ≤ p →
`| 2^-1 × f x + 2^-1 × g x | `^ p ≤
2^-1 × `| f x | `^ p + 2^-1 × `| g x | `^ p.
Let measurableT_comp_powR f p :
measurable_fun setT f → measurable_fun setT (fun x ⇒ f x `^ p)%R.
Local Open Scope ereal_scope.
Let minkowski1 f g p : measurable_fun setT f → measurable_fun setT g →
'N_1[(f \+ g)%R] ≤ 'N_1[f] + 'N_1[g].
Let minkowski_lty f g p :
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.
Lemma minkowski f g p :
measurable_fun setT f → measurable_fun setT g → (1 ≤ p)%R →
'N_p%:E[(f \+ g)%R] ≤ 'N_p%:E[f] + 'N_p%:E[g].
End minkowski.
Local Open Scope ereal_scope.
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.
Section minkowski.
Context d (T : measurableType d) (R : realType).
Variable mu : {measure set T → \bar R}.
Implicit Types (f g : T → R) (p : R).
Let convex_powR_abs_half f g p x : 1 ≤ p →
`| 2^-1 × f x + 2^-1 × g x | `^ p ≤
2^-1 × `| f x | `^ p + 2^-1 × `| g x | `^ p.
Let measurableT_comp_powR f p :
measurable_fun setT f → measurable_fun setT (fun x ⇒ f x `^ p)%R.
Local Open Scope ereal_scope.
Let minkowski1 f g p : measurable_fun setT f → measurable_fun setT g →
'N_1[(f \+ g)%R] ≤ 'N_1[f] + 'N_1[g].
Let minkowski_lty f g p :
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.
Lemma minkowski f g p :
measurable_fun setT f → measurable_fun setT g → (1 ≤ p)%R →
'N_p%:E[(f \+ g)%R] ≤ 'N_p%:E[f] + 'N_p%:E[g].
End minkowski.