going back to the N notation

CHANGELOG_UNRELEASED.md

@@ -35,6 +35,9 @@
   + lemmas `Lnorm1`, `Lnorm_ge0`, `eq_Lnorm`, `Lnorm_eq0_eq0`
   + lemma `hoelder`
 
+- new file `hoelder.v`:
+  + 
+
 ### Changed
 
 - `mnormalize` moved from `kernel.v` to `measure.v` and generalized

_CoqProject

@@ -37,6 +37,7 @@ theories/derive.v
 theories/measure.v
 theories/numfun.v
 theories/lebesgue_integral.v
+theories/hoelder.v
 theories/probability.v
 theories/summability.v
 theories/signed.v

theories/Make

@@ -28,6 +28,7 @@ derive.v
 measure.v
 numfun.v
 lebesgue_integral.v
+hoelder.v
 probability.v
 summability.v
 signed.v

theories/hoelder.v

@@ -4,17 +4,38 @@ 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 itv.
-
-Reserved Notation "'N[ mu ]_  p [ F ]"
+Require Import esum measure lebesgue_measure lebesgue_integral numfun exp.
+
+(******************************************************************************)
+(*                         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 "`|| F ||_ p"
-  (at level 0, F at level 99, format "'[' `|| F ||_ p ']'").
+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}.
@@ -23,21 +44,21 @@ Implicit Types (p : R) (f g : T -> R).
 
 Definition Lnorm p f := (\int[mu]_x (`|f x| `^ p)%:E) `^ p^-1.
 
-Local Notation "`|| f ||_ p" := (Lnorm p f).
+Local Notation "'N_ p [ f ]" := (Lnorm p f).
 
-Lemma Lnorm1 f : `|| f ||_1 = \int[mu]_x `|f x|%:E.
+Lemma Lnorm1 f : 'N_1[f] = \int[mu]_x `|f x|%:E.
 Proof.
 rewrite /Lnorm invr1// poweRe1//.
   by apply: eq_integral => t _; rewrite powRr1.
 by apply: integral_ge0 => t _; rewrite powRr1.
 Qed.
 
-Lemma Lnorm_ge0 p f : 0 <= `|| f ||_p. Proof. exact: poweR_ge0. Qed.
+Lemma Lnorm_ge0 p f : 0 <= 'N_p[f]. Proof. exact: poweR_ge0. Qed.
 
-Lemma eq_Lnorm p f g : f =1 g -> `|| f ||_p = `|| g ||_p.
+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 p f : measurable_fun setT f -> `|| f ||_p = 0 ->
+Lemma Lnorm_eq0_eq0 p f : measurable_fun setT f -> 'N_p[f] = 0 ->
   ae_eq mu [set: T] (fun t => (`|f t| `^ p)%:E) (cst 0).
 Proof.
 move=> mf /poweR_eq0_eq0 fp; apply/ae_eq_integral_abs => //=.
@@ -64,10 +85,10 @@ 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 "`|| f ||_ p" := (Lnorm mu p f).
+Local Notation "'N_ p [ f ]" := (Lnorm mu p f).
 
 Let integrable_powR f p : (0 < p)%R ->
-  measurable_fun [set: T] f -> `|| f ||_p != +oo ->
+  measurable_fun [set: T] f -> 'N_p[f] != +oo ->
   mu.-integrable [set: T] (fun x => (`|f x| `^ p)%:E).
 Proof.
 move=> p0 mf foo; apply/integrableP; split.
@@ -81,7 +102,7 @@ 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 ->
-  `|| f ||_ p = 0 -> `|| (f \* g)%R ||_1  <= `|| f ||_p * `|| g ||_q.
+  'N_p[f] = 0 -> 'N_1[(f \* g)%R]  <= 'N_p[f] * 'N_q[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.
@@ -92,7 +113,7 @@ rewrite (ae_eq_integral (cst 0)) => [|//||//|]; first by rewrite integral0.
   by rewrite normrM => ->; rewrite mul0r.
 Qed.
 
-Let normalized p f x := `|f x| / fine `|| f ||_p.
+Let normalized p f x := `|f x| / fine 'N_p[f].
 
 Let normalized_ge0 p f x : (0 <= normalized p f x)%R.
 Proof. by rewrite /normalized divr_ge0// fine_ge0// Lnorm_ge0. Qed.
@@ -101,12 +122,12 @@ 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 < `|| f ||_p ->
+Let integral_normalized f p : (0 < p)%R -> 0 < 'N_p[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 (`|| f ||_p `^ p))%:E).
+transitivity (\int[mu]_x (`|f x| `^ p / fine ('N_p[f] `^ p))%:E).
   apply: eq_integral => t _.
   rewrite powRM//; last by rewrite invr_ge0 fine_ge0// Lnorm_ge0.
   rewrite -powR_inv1; last by rewrite fine_ge0 // Lnorm_ge0.
@@ -126,19 +147,19 @@ 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 ->
- `|| (f \* g)%R ||_1 <= `|| f ||_p * `|| g ||_q.
+ 'N_1[(f \* g)%R] <= 'N_p[f] * 'N_q[g].
 Proof.
 move=> mf mg p0 q0 pq.
-have [f0|f0] := eqVneq `|| f ||_p 0%E; first exact: hoelder0.
-have [g0|g0] := eqVneq `|| g ||_q 0%E.
+have [f0|f0] := eqVneq 'N_p[f] 0%E; first exact: hoelder0.
+have [g0|g0] := eqVneq 'N_q[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 < `|| f ||_p by rewrite lt_neqAle eq_sym f0//= Lnorm_ge0.
-have {g0}gpos : 0 < `|| g ||_q by rewrite lt_neqAle eq_sym g0//= Lnorm_ge0.
-have [foo|foo] := eqVneq `|| f ||_p +oo%E; first by rewrite foo gt0_mulye ?leey.
-have [goo|goo] := eqVneq `|| g ||_q +oo%E; first by rewrite goo gt0_muley ?leey.
+have {f0}fpos : 0 < 'N_p[f] by rewrite lt_neqAle eq_sym f0//= Lnorm_ge0.
+have {g0}gpos : 0 < 'N_q[g] by rewrite lt_neqAle eq_sym g0//= Lnorm_ge0.
+have [foo|foo] := eqVneq 'N_p[f] +oo%E; first by rewrite foo gt0_mulye ?leey.
+have [goo|goo] := eqVneq 'N_q[g] +oo%E; first by rewrite goo gt0_muley ?leey.
 pose F := normalized p f; pose G := normalized q g.
-rewrite [leLHS](_ : _ = `|| (F \* G)%R ||_1 * `|| f ||_p * `|| g ||_q); last first.
+rewrite [leLHS](_ : _ = 'N_1[(F \* G)%R] * 'N_p[f] * 'N_q[g]); last first.
   rewrite !Lnorm1.
   under [in RHS]eq_integral.
     move=> x _.
@@ -151,13 +172,13 @@ rewrite [leLHS](_ : _ = `|| (F \* G)%R ||_1 * `|| f ||_p * `|| g ||_q); last fir
       exact: measurable_funM.
     - by rewrite lee_fin mulr_ge0// invr_ge0 fine_ge0// Lnorm_ge0.
   rewrite -muleA muleC muleA EFinM muleCA 2!muleA.
-  rewrite (_ : _ * `|| f ||_p = 1) ?mul1e; last first.
+  rewrite (_ : _ * 'N_p[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 (_ : `|| g ||_q * _ = 1) ?mul1e// muleC.
+  rewrite (_ : 'N_q[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 (`|| f ||_p * _)) -muleA lee_pmul ?mule_ge0 ?Lnorm_ge0//.
+rewrite -(mul1e ('N_p[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 => //.

theories/lebesgue_integral.v

@@ -4,7 +4,7 @@ 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 numfun exp itv.
+Require Import esum measure lebesgue_measure numfun.
 
 (******************************************************************************)
 (*                            Lebesgue Integral                               *)
@@ -45,8 +45,6 @@ Require Import esum measure lebesgue_measure numfun exp itv.
 (*              m1 \x^ m2 == product measure over T1 * T2, m2 is a measure    *)
 (*                           measure over T1, and m1 is a sigma finite        *)
 (*                           measure over T2                                  *)
-(*           'N[mu]_p[f] := (\int[mu]_x (`|f x| `^ p)%:E) `^ p^-1             *)
-(*                          The corresponding definition is Lnorm.            *)
 (*                                                                            *)
 (******************************************************************************)
 
@@ -5353,4 +5351,4 @@ by rewrite sfinite_measure_seqP.
 Qed.
 
 End sfinite_fubini.
-Arguments sfinite_Fubini {d d' X Y R} m1 m2 f.
+Arguments sfinite_Fubini {d d' X Y R} m1 m2 f.