Module mathcomp.analysis.ess_sup_inf

From HB Require Import structures.
From mathcomp Require Import boot order algebra.
From mathcomp Require Import boolp classical_sets functions cardinality.
From mathcomp Require Import reals ereal topology normedtype sequences.
From mathcomp Require Import measure lebesgue_measure measurable_realfun.


Unset SsrOldRewriteGoalsOrder.  
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Import Order.TTheory GRing.Theory Num.Def Num.Theory.
Import numFieldNormedType.Exports.

Local Open Scope classical_set_scope.
Local Open Scope ring_scope.
Local Open Scope ereal_scope.

Section essential_supremum.
Context

dSource code

{

TSource code

: semiRingOfSetsType d} {

RSource code

: realType}.
Variable

muSource code

: {measure set T -> \bar R}.
Implicit Type f : T -> \bar R.

Definition

ess_sup

---

Used by

• mathcomp.analysis.hoelder

---

Source code

fSource code

:= ereal_inf [set

ySource code

| \forall

xSource code

\ae mu, f x <= y].

Lemma

ess_supEaeSource code

fSource code

: ess_sup f = ereal_inf [set

ySource code

| \forall

xSource code

\ae mu, f x <= y].

Proof.

by []. Qed.

End essential_supremum.

Section essential_supremum_lemmas.
Context

dSource code

{

TSource code

: measurableType d} {

RSource code

: realType}.
Variable

muSource code

: {measure set T -> \bar R}.
Implicit Types (f g : T -> \bar R) (h k : T -> R) (x y : \bar R) (r : R).

Lemma

ae_le_measurePSource code

fSource code

ySource code

: measurable_fun [set: T] f ->
  (\forall

xSource code

\ae mu, f x <= y) <-> mu (f @^-1` `]y, +oo[) = 0.

Proof.

move=> f_meas; have fVroo_meas : d.-measurable (f @^-1` `]y, +oo[).
  by rewrite -[_ @^-1` _]setTI; apply/f_meas=> //; exact/emeasurable_itv.
have setCfVroo : f @^-1` `]y, +oo[ = ~` [set

xSource code

| f x <= y].
  by apply: setC_inj; rewrite preimage_setC setCitv/= set_itvxx setU0 setCK.
split.
  move=> [N [dN muN0 inN]]; rewrite (subset_measure0 _ dN)// => x.
  by rewrite setCfVroo; apply: inN.
set N := (X in mu X) => muN0; exists N; rewrite -setCfVroo.
by split => //; exact: fVroo_meas.
Qed.

Local Notation

ess_supUsed by

• mathcomp.analysis.hoelder

---

Source code

:= (ess_sup mu).

Lemma

ess_supEmu0Source code

fSource code

: measurable_fun [set: T] f ->
   ess_sup f = ereal_inf [set

ySource code

| mu (f @^-1` `]y, +oo[) = 0].

Proof.

by move=> ?; congr (ereal_inf _); apply/predeqP => r; exact: ae_le_measureP.
Qed.

Lemma

ess_sup_geSource code

fSource code

: \forall

xSource code

\ae mu, f x <= ess_sup f.

Proof.

rewrite ess_supEae//; set I := (X in ereal_inf X).
have [->|IN0] := eqVneq I set0.
  by rewrite ereal_inf0; apply: nearW => ?; rewrite leey.
have [u uI uinf] := ereal_inf_seq IN0.
rewrite -(cvg_lim _ uinf)//; near=> x.
rewrite lime_ge//; first by apply/cvgP: uinf.
by apply: nearW; near: x; apply/ae_foralln => n; apply: uI.
Unshelve. all: by end_near. Qed.

Lemma

ess_supPSource code

fSource code

ySource code

: reflect (\forall

xSource code

\ae mu, f x <= y) (ess_sup f <= y).

Proof.

apply: (iffP (ereal_inf_leP _)) => /=; last 2 first.
- by move=> [z fz zy]; near do apply: le_trans zy.
- by move=> fy; exists y.
by rewrite -ess_supEae//; exact: ess_sup_ge.
Unshelve. all: by end_near. Qed.

Lemma

le_ess_supSource code

fSource code

gSource code

: (\forall

xSource code

\ae mu, f x <= g x) -> ess_sup f <= ess_sup g.

Proof.

move=> fg; apply/ess_supP => //.
near do rewrite (le_trans (near fg _ _))//=.
exact: ess_sup_ge.
Unshelve. all: by end_near. Qed.

Lemma

eq_ess_supUsed by

• mathcomp.analysis.hoelder

---

Source code

fSource code

gSource code

: (\forall

xSource code

\ae mu, f x = g x) -> ess_sup f = ess_sup g.

Proof.

move=> fg; apply/eqP; rewrite eq_le !le_ess_sup//=;
  by apply: filterS fg => x ->.
Qed.

Lemma

ess_sup_cstSource code

xSource code

: 0 < mu [set: T] -> ess_sup (cst x) = x.

Proof.

move=> muT_gt0; apply/eqP; rewrite eq_le; apply/andP; split.
  by apply/ess_supP => //; apply: nearW.
have ae_proper := ae_properfilter_algebraOfSetsType muT_gt0.
by near (almost_everywhere mu) => y; near: y; apply: ess_sup_ge.
Unshelve. all: by end_near. Qed.

Lemma

ess_sup_ae_cstUsed by

• mathcomp.analysis.hoelder

---

Source code

fSource code

ySource code

: 0 < mu [set: T] ->
  (\forall

xSource code

\ae mu, f x = y) -> ess_sup f = y.

Proof.

by move=> muT_gt0 /= /eq_ess_sup->; rewrite ess_sup_cst. Qed.

Lemma

ess_sup_geeUsed by

• mathcomp.analysis.hoelder

---

Source code

fSource code

aSource code

: 0 < mu [set: T] ->
  (\forall

xSource code

\ae mu, a <= f x) -> a <= ess_sup f.

Proof.

by move=> *; rewrite -(ess_sup_cst a)//; apply: le_ess_sup. Qed.

Lemma

abs_sup_eq0_ae_eqUsed by

• mathcomp.analysis.hoelder

---

Source code

fSource code

: ess_sup (abse \o f) = 0 -> f = \0 %[ae mu].

Proof.

move=> ess_sup_f_eq0; near=> x => _ /=; apply/eqP.
rewrite -abse_eq0 eq_le abse_ge0 andbT; near: x.
by apply/ess_supP; rewrite ess_sup_f_eq0.
Unshelve. all: by end_near. Qed.

Lemma

abs_ess_sup_eq0Source code

fSource code

: mu [set: T] > 0 ->
  f = \0 %[ae mu] -> ess_sup (abse \o f) = 0.

Proof.

move=> muT_gt0 f0; apply/eqP; rewrite eq_le; apply/andP; split.
  by apply/ess_supP => /=; near do rewrite (near f0 _ _)//= normr0//.
by rewrite -[0]ess_sup_cst// le_ess_sup//=; near=> x; rewrite abse_ge0.
Unshelve. all: by end_near. Qed.

Lemma

ess_sup_pZlSource code

fSource code

rSource code

: (0 < r)%R ->
  ess_sup (cst r%:E \* f) = r%:E * ess_sup f.

Proof.

move=> /[dup] /ltW r_ge0 r_gt0.
gen have esc_le : r f r_ge0 r_gt0 /
    ess_sup (cst r%:E \* f) <= r%:E * ess_sup f.
  by apply/ess_supP; near do rewrite /cst/= lee_pmul2l//; apply/ess_supP.
apply/eqP; rewrite eq_le esc_le// -lee_pdivlMl//=.
apply: le_trans (esc_le _ _ _ _); rewrite ?invr_gt0 ?invr_ge0//.
by under eq_fun do rewrite muleA -EFinM mulVf ?mul1e ?gt_eqF//.
Unshelve. all: by end_near. Qed.

Lemma

ess_supZlUsed by

• mathcomp.analysis.hoelder

---

Source code

fSource code

rSource code

: mu [set: T] > 0 -> (0 <= r)%R ->
  ess_sup (cst r%:E \* f) = r%:E * ess_sup f.

Proof.

move=> muTN0; case: ltgtP => // [r_gt0|<-] _; first exact: ess_sup_pZl.
by under eq_fun do rewrite mul0e; rewrite mul0e ess_sup_cst.
Qed.

Lemma

ess_sup_eqNyPSource code

fSource code

: ess_sup f = -oo <-> \forall

xSource code

\ae mu, f x = -oo.

Proof.

rewrite (rwP eqP) -leeNy_eq (eq_near (fun=> rwP eqP)).
by under eq_near do rewrite -leeNy_eq; apply/(rwP2 idP (ess_supP _ _)).
Qed.

Lemma

ess_supDSource code

fSource code

gSource code

: ess_sup (f \+ g) <= ess_sup f + ess_sup g.

Proof.

by apply/ess_supP; near do rewrite leeD//; apply/ess_supP.
Unshelve. all: by end_near. Qed.

Lemma

ess_sup_absDSource code

fSource code

gSource code

:
  ess_sup (abse \o (f \+ g)) <= ess_sup (abse \o f) + ess_sup (abse \o g).

Proof.

rewrite (le_trans _ (ess_supD _ _))// le_ess_sup//.
by apply/nearW => x; apply/lee_abs_add.
Qed.

End essential_supremum_lemmas.
Arguments ess_sup_ae_cst {d T R mu f}.
Arguments ess_supP {d T R mu f y}.

Section real_essential_supremum.
Context

dSource code

{

TSource code

: semiRingOfSetsType d} {

RSource code

: realType}.
Variable

muSource code

: {measure set T -> \bar R}.
Implicit Types f : T -> R.

Notation

ess_suprSource code

f := (ess_sup mu (EFin \o f)).

End real_essential_supremum.

Section real_essential_supremum_lemmas.
Context

dSource code

{

TSource code

: measurableType d} {

RSource code

: realType}.
Variable

muSource code

: {measure set T -> \bar R}.
Implicit Types (f : T -> R) (r : R).

Notation

ess_suprSource code

f := (ess_sup mu (EFin \o f)).

Lemma

ess_supr_boundedUsed by

• mathcomp.analysis.hoelder

---

Source code

fSource code

: ess_supr f < +oo ->
  exists

MSource code

, \forall

xSource code

\ae mu, (f x <= M)%R.

Proof.

set g := EFin \o f => ltfy; have [|supfNy] := eqVneq (ess_sup mu g) -oo.
  by move=> /ess_sup_eqNyP fNy; exists 0%:R; apply: filterS fNy.
have supf_fin : ess_supr f \is a fin_num by case: ess_sup ltfy supfNy.
by exists (fine (ess_supr f)); near do rewrite -lee_fin fineK//; apply/ess_supP.
Unshelve. all: by end_near. Qed.

Lemma

ess_sup_eqr0_ae_eqSource code

fSource code

: ess_supr (normr \o f) = 0 -> f = 0%R %[ae mu].

Proof.

under [X in ess_sup _ X]eq_fun do rewrite /= -abse_EFin.
move=> /abs_sup_eq0_ae_eq; apply: filterS => x /= /(_ _)/eqP.
by rewrite eqe => /(_ _)/eqP.
Qed.

Lemma

ess_suprZlSource code

fSource code

rSource code

: mu [set: T] > 0 -> (0 <= r)%R ->
  ess_supr (cst r \* f)%R = r%:E * ess_supr f.

Proof.

by move=> muT_gt0 r_ge0; rewrite -ess_supZl. Qed.

Lemma

ess_sup_gerSource code

fSource code

xSource code

: 0 < mu [set: T] -> (forall

tSource code

, x <= (f t)%:E) ->
  x <= ess_supr f.

Proof.

by move=> muT f0; apply/ess_sup_gee => //=; apply: nearW. Qed.

Lemma

ess_sup_lerSource code

fSource code

ySource code

: (forall

tSource code

, (f t)%:E <= y) -> ess_supr f <= y.

Proof.

by move=> ?; apply/ess_supP; apply: nearW. Qed.

Lemma

ess_sup_cstrSource code

ySource code

: 0 < mu [set: T] -> ess_supr (cst y) = y%:E.

Proof.

by move=> muN0; rewrite (ess_sup_ae_cst y%:E)//=; apply: nearW. Qed.

Lemma

ess_suprDSource code

fSource code

gSource code

: ess_supr (f \+ g)%R <= ess_supr f + ess_supr g.

Proof.

by rewrite (le_trans _ (ess_supD _ _ _)). Qed.

Lemma

ess_sup_normDUsed by

• mathcomp.analysis.hoelder

---

Source code

fSource code

gSource code

:
  ess_supr (normr \o (f \+ g)%R) <= ess_supr (normr \o f) + ess_supr (normr \o g).

Proof.

rewrite (le_trans _ (ess_suprD _ _))// le_ess_sup//.
by apply/nearW => x; apply/ler_normD.
Qed.

End real_essential_supremum_lemmas.
Notation

ess_suprSource code

mu f := (ess_sup mu (EFin \o f)).

Section essential_infimum.
Context

dSource code

{

TSource code

: semiRingOfSetsType d} {

RSource code

: realType}.
Variable

muSource code

: {measure set T -> \bar R}.
Implicit Types f : T -> \bar R.

Definition

ess_inf

---

Used by

• mathcomp.analysis.hoelder

---

Source code

fSource code

:= ereal_sup [set

ySource code

| \forall

xSource code

\ae mu, y <= f x].

Lemma

ess_infEaeSource code

fSource code

: ess_inf f = ereal_sup [set

ySource code

| \forall

xSource code

\ae mu, y <= f x].

Proof.

by []. Qed.

End essential_infimum.

Section essential_infimum_lemmas.
Context

dSource code

{

TSource code

: measurableType d} {

RSource code

: realType}.
Variable

muSource code

: {measure set T -> \bar R}.
Implicit Types (f : T -> \bar R) (x y : \bar R) (r : R).

Local Notation

ess_infUsed by

• mathcomp.analysis.hoelder

---

Source code

:= (ess_inf mu).
Local Notation

ess_supUsed by

• mathcomp.analysis.hoelder

---

Source code

:= (ess_sup mu).

Lemma

ess_infENSource code

fSource code

: ess_inf f = - ess_sup (\- f).

Proof.

rewrite ess_supEae ess_infEae ereal_infEN oppeK; congr (ereal_sup _).
apply/seteqP; split=> [y /= y_le|_ [/= y y_ge <-]].
  by exists (- y); rewrite ?oppeK//=; apply: filterS y_le => x; rewrite leeN2.
by apply: filterS y_ge => x; rewrite leeNl.
Qed.

Lemma

ess_supENSource code

fSource code

: ess_sup f = - ess_inf (\- f).

Proof.

by rewrite ess_infEN oppeK; apply/eq_ess_sup/nearW => ?; rewrite oppeK.
Qed.

Lemma

ess_infNSource code

fSource code

: ess_inf (\- f) = - ess_sup f.

Proof.

by rewrite ess_supEN oppeK. Qed.

Lemma

ess_supNSource code

fSource code

: ess_sup (\- f) = - ess_inf f.

Proof.

by rewrite ess_infEN oppeK. Qed.

Lemma

ess_infPUsed by

• mathcomp.analysis.hoelder

---

Source code

fSource code

ySource code

: reflect (\forall

xSource code

\ae mu, y <= f x) (y <= ess_inf f).

Proof.

by rewrite ess_infEN leeNr; apply: (iffP ess_supP);
   apply: filterS => x; rewrite leeN2.
Qed.

Lemma

ess_inf_leSource code

fSource code

: \forall

xSource code

\ae mu, ess_inf f <= f x.

Proof.

exact/ess_infP. Qed.

Lemma

le_ess_infSource code

fSource code

gSource code

: (\forall

xSource code

\ae mu, f x <= g x) -> ess_inf f <= ess_inf g.

Proof.

move=> fg; apply/ess_infP => //.
near do rewrite (le_trans _ (near fg _ _))//=.
exact: ess_inf_le.
Unshelve. all: by end_near. Qed.

Lemma

eq_ess_infSource code

fSource code

gSource code

: (\forall

xSource code

\ae mu, f x = g x) -> ess_inf f = ess_inf g.

Proof.

move=> fg; apply/eqP; rewrite eq_le !le_ess_inf//=;
  by apply: filterS fg => x ->.
Qed.

Lemma

ess_inf_cstSource code

xSource code

: 0 < mu [set: T] -> ess_inf (cst x) = x.

Proof.

by move=> ?; rewrite ess_infEN (ess_sup_ae_cst (- x)) ?oppeK//=; apply: nearW.
Qed.

Lemma

ess_inf_ae_cstUsed by

• mathcomp.analysis.hoelder

---

Source code

fSource code

ySource code

: 0 < mu [set: T] ->
  (\forall

xSource code

\ae mu, f x = y) -> ess_inf f = y.

Proof.

by move=> muT_gt0 /= /eq_ess_inf->; rewrite ess_inf_cst. Qed.

Lemma

ess_inf_geeSource code

fSource code

ySource code

: 0 < mu [set: T] ->
  (\forall

xSource code

\ae mu, y <= f x) -> y <= ess_inf f.

Proof.

by move=> *; rewrite -(ess_inf_cst y)//; apply: le_ess_inf. Qed.

Lemma

ess_inf_pZlSource code

fSource code

rSource code

: (0 < r)%R -> ess_inf (cst r%:E \* f) = r%:E * ess_inf f.

Proof.

move=> r_gt0; rewrite !ess_infEN muleN; congr (- _).
by under eq_fun do rewrite -muleN; rewrite ess_sup_pZl.
Qed.

Lemma

ess_infZlSource code

fSource code

rSource code

: mu [set: T] > 0 -> (0 <= r)%R ->
  ess_inf (cst r%:E \* f) = r%:E * ess_inf f.

Proof.

move=> muTN0; case: ltgtP => // [a_gt0|<-] _; first exact: ess_inf_pZl.
by under eq_fun do rewrite mul0e; rewrite mul0e ess_inf_cst.
Qed.

Lemma

ess_inf_eqyPSource code

fSource code

: ess_inf f = +oo <-> \forall

xSource code

\ae mu, f x = +oo.

Proof.

rewrite (rwP eqP) -leye_eq (eq_near (fun=> rwP eqP)).
by under eq_near do rewrite -leye_eq; apply/(rwP2 idP (ess_infP _ _)).
Qed.

Lemma

ess_infDSource code

fSource code

gSource code

: ess_inf (f \+ g) >= ess_inf f + ess_inf g.

Proof.

by apply/ess_infP; near do rewrite leeD//; apply/ess_infP.
Unshelve. all: by end_near. Qed.

End essential_infimum_lemmas.
Arguments ess_inf_ae_cst {d T R mu f}.
Arguments ess_infP {d T R mu f y}.

Section real_essential_infimum.
Context

dSource code

{

TSource code

: measurableType d} {

RSource code

: realType}.
Variable

muSource code

: {measure set T -> \bar R}.
Implicit Types (f : T -> R) (x : \bar R) (r : R).

Notation

ess_infrSource code

f := (ess_inf mu (EFin \o f)).

Lemma

ess_infr_boundedSource code

fSource code

: ess_infr f > -oo ->
  exists

MSource code

, \forall

xSource code

\ae mu, (f x >= M)%R.

Proof.

set g := EFin \o f => ltfy; have [|inffNy] := eqVneq (ess_inf mu g) +oo.
  by move=> /ess_inf_eqyP fNy; exists 0%:R; apply: filterS fNy.
have inff_fin : ess_infr f \is a fin_num by case: ess_inf ltfy inffNy.
by exists (fine (ess_infr f)); near do rewrite -lee_fin fineK//; apply/ess_infP.
Unshelve. all: by end_near. Qed.

Lemma

ess_infrZlSource code

fSource code

rSource code

: mu [set: T] > 0 -> (0 <= r)%R ->
  ess_infr (cst r \* f)%R = r%:E * ess_infr f.

Proof.

by move=> muT_gt0 r_ge0; rewrite -ess_infZl. Qed.

Lemma

ess_inf_gerSource code

fSource code

xSource code

: 0 < mu [set: T] -> (forall

tSource code

, x <= (f t)%:E) ->
  x <= ess_infr f.

Proof.

by move=> muT f0; apply/ess_inf_gee => //=; apply: nearW. Qed.

Lemma

ess_inf_lerSource code

fSource code

xSource code

: (forall

tSource code

, x <= (f t)%:E) -> x <= ess_infr f.

Proof.

by move=> ?; apply/ess_infP; apply: nearW. Qed.

Lemma

ess_inf_cstrSource code

rSource code

: 0 < mu [set: T] -> ess_infr (cst r) = r%:E.

Proof.

by move=> muN0; rewrite (ess_inf_ae_cst r%:E)//=; apply: nearW. Qed.

End real_essential_infimum.
Notation

ess_infrSource code

mu f := (ess_inf mu (EFin \o f)).