Module mathcomp.analysis.numfun
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 fsbigop.
From mathcomp Require Import functions cardinality set_interval.
Require Import signed reals ereal topology normedtype sequences function_spaces.
Numerical functions
This file provides definitions and lemmas about numerical functions.
{nnfun T >-> R} == type of non-negative functions
f ^\+ == the function formed by the non-negative outputs
of f (from a type to the type of extended real
numbers) and 0 otherwise
rendered as f ⁺ with company-coq (U+207A)
f ^\- == the function formed by the non-positive outputs
of f and 0 o.w.
rendered as f ⁻ with company-coq (U+207B)
\1_ A == indicator function 1_A
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.
HB.mixin Record isNonNegFun (aT : Type) (rT : numDomainType) (f : aT -> rT) := {
fun_ge0 : forall x, (0 <= f x)%R
}.
HB.structure Definition NonNegFun aT rT := {f of @isNonNegFun aT rT f}.
Reserved Notation "{ 'nnfun' aT >-> T }"
(at level 0, format "{ 'nnfun' aT >-> T }").
Reserved Notation "[ 'nnfun' 'of' f ]"
(at level 0, format "[ 'nnfun' 'of' f ]").
Notation "{ 'nnfun' aT >-> T }" := (@NonNegFun.type aT T) : form_scope.
Notation "[ 'nnfun' 'of' f ]" := [the {nnfun _ >-> _} of f] : form_scope.
#[global] Hint Extern 0 (is_true (0 <= _)) => solve [apply: fun_ge0] : core.
Section fimfun_bin.
Context (T : Type) (R : numDomainType).
Variables f g : {fimfun T >-> R}.
Lemma max_fimfun_subproof : @FiniteImage T R (f \max g).
Proof.
HB.instance Definition _ := max_fimfun_subproof.End fimfun_bin.
Reserved Notation "f ^\+" (at level 1, format "f ^\+").
Reserved Notation "f ^\-" (at level 1, format "f ^\-").
Section restrict_lemmas.
Context {aT : Type} {rT : numFieldType}.
Implicit Types (f g : aT -> rT) (D : set aT).
Lemma restrict_set0 f : f \_ set0 = cst 0.
Proof.
Lemma restrict_ge0 D f :
(forall x, D x -> 0 <= f x) -> forall x, 0 <= (f \_ D) x.
Proof.
Lemma ler_restrict D f g :
(forall x, D x -> f x <= g x) -> forall x, (f \_ D) x <= (g \_ D) x.
Proof.
Lemma restrict_normr D f : (normr \o f) \_ D = normr \o (f \_ D).
Proof.
End restrict_lemmas.
Lemma erestrict_ge0 {aT} {rT : numFieldType} (D : set aT) (f : aT -> \bar rT) :
(forall x, D x -> (0 <= f x)%E) -> forall x, (0 <= (f \_ D) x)%E.
Proof.
Lemma lee_restrict {aT} {rT : numFieldType} (D : set aT) (f g : aT -> \bar rT) :
(forall x, D x -> f x <= g x)%E -> forall x, ((f \_ D) x <= (g \_ D) x)%E.
Proof.
Lemma restrict_lee {aT} {rT : numFieldType} (D E : set aT) (f : aT -> \bar rT) :
(forall x, E x -> 0 <= f x)%E ->
D `<=` E -> forall x, ((f \_ D) x <= (f \_ E) x)%E.
Proof.
Section erestrict_lemmas.
Local Open Scope ereal_scope.
Variables (T : Type) (R : realDomainType) (D : set T).
Implicit Types (f g : T -> \bar R) (r : R).
Lemma erestrict_set0 f : f \_ set0 = cst 0.
Proof.
Lemma erestrict0 : (cst 0 : T -> \bar R) \_ D = cst 0.
Proof.
Lemma erestrictD f g : (f \+ g) \_ D = f \_ D \+ g \_ D.
Proof.
Lemma erestrictN f : (\- f) \_ D = \- f \_ D.
Proof.
Lemma erestrictB f g : (f \- g) \_ D = f \_ D \- g \_ D.
Proof.
Lemma erestrictM f g : (f \* g) \_ D = f \_ D \* g \_ D.
Proof.
Lemma erestrict_scale k f :
(fun x => k%:E * f x) \_ D = (fun x => k%:E * (f \_ D) x).
Proof.
End erestrict_lemmas.
Section funposneg.
Local Open Scope ereal_scope.
Definition funepos T (R : realDomainType) (f : T -> \bar R) :=
fun x => maxe (f x) 0.
Definition funeneg T (R : realDomainType) (f : T -> \bar R) :=
fun x => maxe (- f x) 0.
End funposneg.
Notation "f ^\+" := (funepos f) : ereal_scope.
Notation "f ^\-" := (funeneg f) : ereal_scope.
Section funposneg_lemmas.
Local Open Scope ereal_scope.
Variables (T : Type) (R : realDomainType) (D : set T).
Implicit Types (f g : T -> \bar R) (r : R).
Lemma funepos_ge0 f x : 0 <= f^\+ x.
Proof.
Lemma funeneg_ge0 f x : 0 <= f^\- x.
Proof.
Lemma funeposN f : (\- f)^\+ = f^\-. Proof. exact/funext.
Lemma funenegN f : (\- f)^\- = f^\+.
Proof.
Lemma funepos_restrict f : (f \_ D)^\+ = (f^\+) \_ D.
Proof.
Lemma funeneg_restrict f : (f \_ D)^\- = (f^\-) \_ D.
Proof.
Lemma ge0_funeposE f : (forall x, D x -> 0 <= f x) -> {in D, f^\+ =1 f}.
Proof.
Lemma ge0_funenegE f : (forall x, D x -> 0 <= f x) -> {in D, f^\- =1 cst 0}.
Proof.
Lemma le0_funeposE f : (forall x, D x -> f x <= 0) -> {in D, f^\+ =1 cst 0}.
Proof.
Lemma le0_funenegE f : (forall x, D x -> f x <= 0) -> {in D, f^\- =1 \- f}.
Proof.
Lemma gt0_funeposM r f : (0 < r)%R ->
(fun x => r%:E * f x)^\+ = (fun x => r%:E * (f^\+ x)).
Proof.
Lemma gt0_funenegM r f : (0 < r)%R ->
(fun x => r%:E * f x)^\- = (fun x => r%:E * (f^\- x)).
Proof.
Lemma lt0_funeposM r f : (r < 0)%R ->
(fun x => r%:E * f x)^\+ = (fun x => - r%:E * (f^\- x)).
Proof.
Lemma lt0_funenegM r f : (r < 0)%R ->
(fun x => r%:E * f x)^\- = (fun x => - r%:E * (f^\+ x)).
Proof.
Lemma fune_abse f : abse \o f = f^\+ \+ f^\-.
Proof.
Lemma funeposneg f : f = (fun x => f^\+ x - f^\- x).
Proof.
Lemma add_def_funeposneg f x : (f^\+ x +? - f^\- x).
Proof.
Lemma funeD_Dpos f g : f \+ g = (f \+ g)^\+ \- (f \+ g)^\-.
Proof.
Lemma funeD_posD f g : f \+ g = (f^\+ \+ g^\+) \- (f^\- \+ g^\-).
Proof.
Lemma funepos_le f g :
{in D, forall x, f x <= g x} -> {in D, forall x, f^\+ x <= g^\+ x}.
Proof.
Lemma funeneg_le f g :
{in D, forall x, f x <= g x} -> {in D, forall x, g^\- x <= f^\- x}.
Proof.
End funposneg_lemmas.
#[global]
Hint Extern 0 (is_true (0%R <= _ ^\+ _)%E) => solve [apply: funepos_ge0] : core.
#[global]
Hint Extern 0 (is_true (0%R <= _ ^\- _)%E) => solve [apply: funeneg_ge0] : core.
Definition indic {T} {R : ringType} (A : set T) (x : T) : R := (x \in A)%:R.
Reserved Notation "'\1_' A" (at level 8, A at level 2, format "'\1_' A") .
Notation "'\1_' A" := (indic A) : ring_scope.
Section indic_lemmas.
Context (T : Type) (R : ringType).
Implicit Types A D : set T.
Lemma indicE A (x : T) : \1_A x = (x \in A)%:R :> R. Proof. by [].
Lemma indicT : \1_[set: T] = cst (1 : R).
Proof.
Lemma indic0 : \1_(@set0 T) = cst (0 : R).
Proof.
Lemma image_indic D A :
\1_D @` A = (if A `\` D != set0 then [set 0] else set0) `|`
(if A `&` D != set0 then [set 1 : R] else set0).
Proof.
Lemma preimage_indic (D : set T) (B : set R) :
\1_D @^-1` B = if 1 \in B then (if 0 \in B then setT else D)
else (if 0 \in B then ~` D else set0).
Proof.
Lemma image_indic_sub D A : \1_D @` A `<=` ([set 0; 1] : set R).
Proof.
Lemma fimfunE (f : {fimfun T >-> R}) x :
f x = \sum_(y \in range f) (y * \1_(f @^-1` [set y]) x).
Proof.
Lemma fimfunEord (f : {fimfun T >-> R})
(s := fset_set (f @` setT)) :
forall x, f x = \sum_(i < #|`s|) (s`_i * \1_(f @^-1` [set s`_i]) x).
Proof.
End indic_lemmas.
Lemma patch_indic T {R : numFieldType} (f : T -> R) (D : set T) :
f \_ D = (f \* \1_D)%R.
Proof.
Lemma epatch_indic T (R : numDomainType) (f : T -> \bar R) (D : set T) :
(f \_ D = f \* (EFin \o \1_D))%E.
Proof.
Lemma xsection_indic (R : ringType) T1 T2 (A : set (T1 * T2)) x :
xsection A x = (fun y => (\1_A (x, y) : R)) @^-1` [set 1].
Proof.
Lemma ysection_indic (R : ringType) T1 T2 (A : set (T1 * T2)) y :
ysection A y = (fun x => (\1_A (x, y) : R)) @^-1` [set 1].
Proof.
Lemma indic_restrict {T : pointedType} {R : numFieldType} (A : set T) :
\1_A = (1 : T -> R) \_ A.
Proof.
Lemma restrict_indic T (R : numFieldType) (E A : set T) :
((\1_E : T -> R) \_ A) = \1_(E `&` A).
Proof.
Lemma cvg_indic {R : realFieldType} (x : R^o) k :
x \in (ball 0 k : set R^o) ->
\1_(ball 0 k : set R^o) y @[y --> x] --> (\1_(ball 0 k) x : R).
Proof.
Section ring.
Context (aT : pointedType) (rT : ringType).
Lemma fimfun_mulr_closed : mulr_closed (@fimfun aT rT).
Proof.
HB.instance Definition _ :=
@GRing.isMulClosed.Build _ (@fimfun aT rT) fimfun_mulr_closed.
HB.instance Definition _ := [SubZmodule_isSubRing of {fimfun aT >-> rT} by <:].
Implicit Types f g : {fimfun aT >-> rT}.
Lemma fimfunM f g : f * g = f \* g :> (_ -> _)
Proof.
Lemma fimfun1 : (1 : {fimfun aT >-> rT}) = cst 1 :> (_ -> _)
Proof.
Lemma fimfun_prod I r (P : {pred I}) (f : I -> {fimfun aT >-> rT}) (x : aT) :
(\sum_(i <- r | P i) f i) x = \sum_(i <- r | P i) f i x.
Proof.
Lemma fimfunX f n : f ^+ n = (fun x => f x ^+ n) :> (_ -> _).
Proof.
Lemma indic_fimfun_subproof X : @FiniteImage aT rT \1_X.
Proof.
HB.instance Definition _ X := indic_fimfun_subproof X.
Definition indic_fimfun (X : set aT) := [the {fimfun aT >-> rT} of \1_X].
HB.instance Definition _ k f := FImFun.copy (k \o* f) (f * cst_fimfun k).
Definition scale_fimfun k f := [the {fimfun aT >-> rT} of k \o* f].
End ring.
Arguments indic_fimfun {aT rT} _.
Section comring.
Context (aT : pointedType) (rT : comRingType).
HB.instance Definition _ := [SubRing_isSubComRing of {fimfun aT >-> rT} by <:].
Implicit Types (f g : {fimfun aT >-> rT}).
HB.instance Definition _ f g := FImFun.copy (f \* g) (f * g).
End comring.
HB.factory Record FiniteDecomp (T : pointedType) (R : ringType) (f : T -> R) :=
{ fimfunE : exists (r : seq R) (A_ : R -> set T),
forall x, f x = \sum_(y <- r) (y * \1_(A_ y) x) }.
HB.builders Context T R f of @FiniteDecomp T R f.
Lemma finite_subproof: @FiniteImage T R f.
Proof.
HB.instance Definition _ := finite_subproof.HB.end.
Lemma fset_set_comp (T1 : Type) (T2 T3 : choiceType) (D : set T1)
(f : {fimfun T1 >-> T2}) (g : T2 -> T3) :
fset_set [set (g \o f) x | x in D] =
[fset g x | x in fset_set [set f x | x in D]]%fset.
Proof.
Section Tietze.
Context {X : topologicalType} {R : realType}.
Local Notation "3" := 3%:R : ring_scope.
Hypothesis normalX : normal_space X.
Lemma urysohn_ext_itv A B x y :
closed A -> closed B -> A `&` B = set0 -> x < y ->
exists f : X -> R, [/\ continuous f,
f @` A `<=` [set x], f @` B `<=` [set y] & range f `<=` `[x, y]].
Proof.
Context (A : set X).
Hypothesis clA : closed A.
Local Notation "3" := 3%:R.
Local Lemma tietze_step' (f : X -> R) (M : R) :
0 < M -> {within A, continuous f} ->
(forall x, A x -> `|f x| <= M) ->
exists g : X -> R, [/\ continuous g,
(forall x, A x -> `|f x - g x| <= 2/3 * M) &
(forall x, `|g x| <= 1/3 * M)].
Proof.
Let tietze_step (f : X -> R) M :
{g : X -> R^o | {within A, continuous f} -> 0 < M ->
(forall x, A x -> `|f x| <= M) -> [/\ continuous g,
forall x, A x -> `|f x - g x| <= 2/3 * M :>R
& forall x, `|g x| <= 1/3 * M ]}.
Proof.
Let onem_twothirds : 1 - 2/3 = 1/3 :> R.
Proof.
Lemma continuous_bounded_extension (f : X -> R^o) M :
0 < M -> {within A, continuous f} -> (forall x, A x -> `|f x| <= M) ->
exists g, [/\ {in A, f =1 g}, continuous g & forall x, `|g x| <= M].
Proof.
End Tietze.