Library mathcomp.analysis.numfun
(* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C. *)
From HB Require Import structures.
From mathcomp Require Import all_ssreflect.
From mathcomp Require Import ssralg ssrnum ssrint interval finmap.
Require Import mathcomp_extra boolp classical_sets signed functions cardinality.
Require Import reals ereal topology normedtype sequences.
From HB Require Import structures.
From mathcomp Require Import all_ssreflect.
From mathcomp Require Import ssralg ssrnum ssrint interval finmap.
Require Import mathcomp_extra boolp classical_sets signed functions cardinality.
Require Import reals ereal topology normedtype sequences.
This file provides definitions and lemmas about numerical 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.
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 "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.
Lemma restrict_ge0 D f :
(∀ x, D x → 0 ≤ f x) → ∀ x, 0 ≤ (f \_ D) x.
Lemma ler_restrict D f g :
(∀ x, D x → f x ≤ g x) → ∀ x, (f \_ D) x ≤ (g \_ D) x.
End restrict_lemmas.
Lemma erestrict_ge0 {aT} {rT : numFieldType} (D : set aT) (f : aT → \bar rT) :
(∀ x, D x → (0 ≤ f x)%E) → ∀ x, (0 ≤ (f \_ D) x)%E.
Lemma lee_restrict {aT} {rT : numFieldType} (D : set aT) (f g : aT → \bar rT) :
(∀ x, D x → f x ≤ g x)%E → ∀ x, ((f \_ D) x ≤ (g \_ D) x)%E.
Lemma restrict_lee {aT} {rT : numFieldType} (D E : set aT) (f : aT → \bar rT) :
(∀ x, E x → 0 ≤ f x)%E →
D `<=` E → ∀ x, ((f \_ D) x ≤ (f \_ E) x)%E.
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.
Lemma erestrict0 : (cst 0 : T → \bar R) \_ D = cst 0.
Lemma erestrictD f g : (f \+ g) \_ D = f \_ D \+ g \_ D.
Lemma erestrictN f : (\- f) \_ D = \- f \_ D.
Lemma erestrictB f g : (f \- g) \_ D = f \_ D \- g \_ D.
Lemma erestrictM f g : (f \* g) \_ D = f \_ D \* g \_ D.
Lemma erestrict_scale k f :
(fun x ⇒ k%:E × f x) \_ D = (fun x ⇒ k%:E × (f \_ D) x).
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.
Lemma funeneg_ge0 f x : 0 ≤ f^\- x.
Lemma funeposN f : (\- f)^\+ = f^\-.
Lemma funenegN f : (\- f)^\- = f^\+.
Lemma funepos_restrict f : (f \_ D)^\+ = (f^\+) \_ D.
Lemma funeneg_restrict f : (f \_ D)^\- = (f^\-) \_ D.
Lemma ge0_funeposE f : (∀ x, D x → 0 ≤ f x) → {in D, f^\+ =1 f}.
Lemma ge0_funenegE f : (∀ x, D x → 0 ≤ f x) → {in D, f^\- =1 cst 0}.
Lemma le0_funeposE f : (∀ x, D x → f x ≤ 0) → {in D, f^\+ =1 cst 0}.
Lemma le0_funenegE f : (∀ x, D x → f x ≤ 0) → {in D, f^\- =1 \- f}.
Lemma gt0_funeposM r f : (0 < r)%R →
(fun x ⇒ r%:E × f x)^\+ = (fun x ⇒ r%:E × (f^\+ x)).
Lemma gt0_funenegM r f : (0 < r)%R →
(fun x ⇒ r%:E × f x)^\- = (fun x ⇒ r%:E × (f^\- x)).
Lemma lt0_funeposM r f : (r < 0)%R →
(fun x ⇒ r%:E × f x)^\+ = (fun x ⇒ - r%:E × (f^\- x)).
Lemma lt0_funenegM r f : (r < 0)%R →
(fun x ⇒ r%:E × f x)^\- = (fun x ⇒ - r%:E × (f^\+ x)).
Lemma fune_abse f : abse \o f = f^\+ \+ f^\-.
Lemma funeposneg f : f = (fun x ⇒ f^\+ x - f^\- x).
Lemma add_def_funeposneg f x : (f^\+ x +? - f^\- x).
Lemma funeD_Dpos f g : f \+ g = (f \+ g)^\+ \- (f \+ g)^\-.
Lemma funeD_posD f g : f \+ g = (f^\+ \+ g^\+) \- (f^\- \+ g^\-).
End funposneg_lemmas.
#[global]
Hint Extern 0 (is_true (0 ≤ _ ^\+ _)%E) ⇒ solve [apply: funepos_ge0] : core.
#[global]
Hint Extern 0 (is_true (0 ≤ _ ^\- _)%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.
Lemma indicE {T} {R : ringType} (A : set T) (x : T) :
indic A x = (x \in A)%:R :> R.
Lemma indicT {T} {R : ringType} : \1_[set: T] = cst (1 : R).
Lemma indic0 {T} {R : ringType} : \1_(@set0 T) = cst (0 : R).
Lemma indic_restrict {T : pointedType} {R : numFieldType} (A : set T) :
\1_A = 1 \_ A :> (T → R).
Lemma restrict_indic T (R : numFieldType) (E A : set T) :
(\1_E \_ A) = \1_(E `&` A) :> (T → R).
Lemma preimage_indic (T : Type) (R : ringType) (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).
Lemma image_indic T (R : ringType) (D A : set T) :
\1_D @` A = (if A `\` D != set0 then [set 0] else set0) `|`
(if A `&` D != set0 then [set 1 : R] else set0).
Lemma image_indic_sub T (R : ringType) (D A : set T) :
\1_D @` A `<=` [set (0 : R); 1].