Library mathcomp.analysis.realfun
(* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C. *)
From mathcomp Require Import ssreflect ssrfun ssrbool ssrnat eqtype choice.
From mathcomp Require Import seq fintype bigop order ssralg ssrint ssrnum finmap.
From mathcomp Require Import matrix interval zmodp vector fieldext falgebra.
Require Import boolp ereal reals.
Require Import classical_sets posnum nngnum topology prodnormedzmodule.
Require Import cardinality normedtype derive.
From mathcomp Require Import ssreflect ssrfun ssrbool ssrnat eqtype choice.
From mathcomp Require Import seq fintype bigop order ssralg ssrint ssrnum finmap.
From mathcomp Require Import matrix interval zmodp vector fieldext falgebra.
Require Import boolp ereal reals.
Require Import classical_sets posnum nngnum topology prodnormedzmodule.
Require Import cardinality normedtype derive.
This file provides properties of standard real-valued functions over real
numbers (e.g., the continuity of the inverse of a continuous function).
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.
Import numFieldNormedType.Exports.
Section real_inverse_functions.
Variable R : realType.
Implicit Types (a b : R) (f g : R → R).
Lemma itv_continuous_inj_le f (I : interval R) :
(∃ x y, [/\ x \in I, y \in I, x < y & f x ≤ f y]) →
{in I, continuous f} → {in I &, injective f} →
{in I &, {mono f : x y / x ≤ y}}.
Lemma itv_continuous_inj_ge f (I : interval R) :
(∃ x y, [/\ x \in I, y \in I, x < y & f y ≤ f x]) →
{in I, continuous f} → {in I &, injective f} →
{in I &, {mono f : x y /~ x ≤ y}}.
Lemma itv_continuous_inj_mono f (I : interval R) :
{in I, continuous f} → {in I &, injective f} → monotonous I f.
Lemma segment_continuous_inj_le f a b :
f a ≤ f b → {in `[a, b], continuous f} → {in `[a, b] &, injective f} →
{in `[a, b] &, {mono f : x y / x ≤ y}}.
Lemma segment_continuous_inj_ge f a b :
f a ≥ f b → {in `[a, b], continuous f} → {in `[a, b] &, injective f} →
{in `[a, b] &, {mono f : x y /~ x ≤ y}}.
The condition "f a <= f b" is unnecessary because the last
interval condition is vacuously true otherwise.
Lemma segment_can_le a b f g : a ≤ b →
{in `[a, b], continuous f} →
{in `[a, b], cancel f g} →
{in `[f a, f b] &, {mono g : x y / x ≤ y}}.
{in `[a, b], continuous f} →
{in `[a, b], cancel f g} →
{in `[f a, f b] &, {mono g : x y / x ≤ y}}.
The condition "f b <= f a" is unnecessary---see seg...increasing above
Lemma segment_can_ge a b f g : a ≤ b →
{in `[a, b], continuous f} →
{in `[a, b], cancel f g} →
{in `[f b, f a] &, {mono g : x y /~ x ≤ y}}.
Lemma segment_can_mono a b f g : a ≤ b →
{in `[a, b], continuous f} → {in `[a, b], cancel f g} →
monotonous (f @`[a, b]) g.
Lemma segment_continuous_surjective a b f : a ≤ b →
{in `[a, b], continuous f} → surjective `[a, b] (f @`[a, b]) f.
Lemma segment_continuous_le_surjective a b f : a ≤ b → f a ≤ f b →
{in `[a, b], continuous f} → surjective `[a, b] `[f a, f b] f.
Lemma segment_continuous_ge_surjective a b f : a ≤ b → f b ≤ f a →
{in `[a, b], continuous f} → surjective `[a, b] `[f b, f a] f.
Lemma continuous_inj_image_segment a b f : a ≤ b →
{in `[a, b], continuous f} → {in `[a, b] &, injective f} →
f @` `[a, b] = f @`[a, b]%classic.
Lemma continuous_inj_image_segmentP a b f : a ≤ b →
{in `[a, b], continuous f} → {in `[a, b] &, injective f} →
∀ y, reflect (exists2 x, x \in `[a, b] & f x = y) (y \in f @`[a, b]).
Lemma segment_continuous_can_sym a b f g : a ≤ b →
{in `[a, b], continuous f} → {in `[a, b], cancel f g} →
{in f @`[a, b], cancel g f}.
Lemma segment_continuous_le_can_sym a b f g : a ≤ b →
{in `[a, b], continuous f} → {in `[a, b], cancel f g} →
{in `[f a, f b], cancel g f}.
Lemma segment_continuous_ge_can_sym a b f g : a ≤ b →
{in `[a, b], continuous f} → {in `[a, b], cancel f g} →
{in `[f b, f a], cancel g f}.
Lemma segment_inc_surj_continuous a b f :
{in `[a, b] &, {mono f : x y / x ≤ y}} →
surjective `[a, b] `[f a, f b] f →
{in `]a, b[, continuous f}.
Lemma segment_dec_surj_continuous a b f :
{in `[a, b] &, {mono f : x y /~ x ≤ y}} →
surjective `[a, b] `[f b, f a] f →
{in `]a, b[, continuous f}.
Lemma segment_mono_surj_continuous a b f :
monotonous `[a, b] f → surjective `[a, b] (f @`[a, b]) f →
{in `]a, b[, continuous f}.
Lemma segment_can_le_continuous a b f g : a ≤ b →
{in `[a, b], continuous f} →
{in `[a, b], cancel f g} →
{in `](f a), (f b)[, continuous g}.
Lemma segment_can_ge_continuous a b f g : a ≤ b →
{in `[a, b], continuous f} →
{in `[a, b], cancel f g} →
{in `](f b), (f a)[, continuous g}.
Lemma segment_can_continuous a b f g : a ≤ b →
{in `[a, b], continuous f} →
{in `[a, b], cancel f g} →
{in f @`]a, b[, continuous g}.
Lemma near_can_continuousAcan_sym f g (x : R) :
{near x, cancel f g} → {near x, continuous f} →
{near (f x), continuous g} ∧ {near (f x), cancel g f}.
Lemma near_can_continuous f g (x : R) :
{near x, cancel f g} → {near x, continuous f} → {near (f x), continuous g}.
Lemma near_continuous_can_sym f g (x : R) :
{near x, continuous f} → {near x, cancel f g} → {near (f x), cancel g f}.
End real_inverse_functions.
Section real_inverse_function_instances.
Variable R : realType.
Lemma exp_continuous n : continuous (@GRing.exp R ^~ n).
Lemma sqr_continuous : continuous (@exprz R ^~ 2).
Lemma sqrt_continuous : continuous (@Num.sqrt R).
End real_inverse_function_instances.
Section is_derive_inverse.
Variable R : realType.
Lemma is_derive1_caratheodory (f : R → R) (x a : R) :
is_derive x 1 f a ↔
∃ g, [/\ ∀ z, f z - f x = g z × (z - x),
{for x, continuous g} & g x = a].
Lemma is_derive_0_is_cst (f : R → R) x y :
(∀ x, is_derive x 1 f 0) → f x = f y.
Global Instance is_derive1_comp (f g : R → R) (x a b : R) :
is_derive (g x) 1 f a → is_derive x 1 g b →
is_derive x 1 (f \o g) (a × b).
Lemma is_deriveV (f : R → R) (x t v : R) :
f x != 0 → is_derive x v f t →
is_derive x v (fun y ⇒ (f y)^-1) (- (f x) ^- 2 *: t).
Lemma is_derive_inverse (f g : R → R) l x :
{near x, cancel f g} →
{near x, continuous f} →
is_derive x 1 f l → l != 0 → is_derive (f x) 1 g l^-1.
End is_derive_inverse.
Hint Extern 0 (is_derive _ _ (fun _ ⇒ (_ _)^-1) _) ⇒
(eapply is_deriveV; first by []) : typeclass_instances.
{in `[a, b], continuous f} →
{in `[a, b], cancel f g} →
{in `[f b, f a] &, {mono g : x y /~ x ≤ y}}.
Lemma segment_can_mono a b f g : a ≤ b →
{in `[a, b], continuous f} → {in `[a, b], cancel f g} →
monotonous (f @`[a, b]) g.
Lemma segment_continuous_surjective a b f : a ≤ b →
{in `[a, b], continuous f} → surjective `[a, b] (f @`[a, b]) f.
Lemma segment_continuous_le_surjective a b f : a ≤ b → f a ≤ f b →
{in `[a, b], continuous f} → surjective `[a, b] `[f a, f b] f.
Lemma segment_continuous_ge_surjective a b f : a ≤ b → f b ≤ f a →
{in `[a, b], continuous f} → surjective `[a, b] `[f b, f a] f.
Lemma continuous_inj_image_segment a b f : a ≤ b →
{in `[a, b], continuous f} → {in `[a, b] &, injective f} →
f @` `[a, b] = f @`[a, b]%classic.
Lemma continuous_inj_image_segmentP a b f : a ≤ b →
{in `[a, b], continuous f} → {in `[a, b] &, injective f} →
∀ y, reflect (exists2 x, x \in `[a, b] & f x = y) (y \in f @`[a, b]).
Lemma segment_continuous_can_sym a b f g : a ≤ b →
{in `[a, b], continuous f} → {in `[a, b], cancel f g} →
{in f @`[a, b], cancel g f}.
Lemma segment_continuous_le_can_sym a b f g : a ≤ b →
{in `[a, b], continuous f} → {in `[a, b], cancel f g} →
{in `[f a, f b], cancel g f}.
Lemma segment_continuous_ge_can_sym a b f g : a ≤ b →
{in `[a, b], continuous f} → {in `[a, b], cancel f g} →
{in `[f b, f a], cancel g f}.
Lemma segment_inc_surj_continuous a b f :
{in `[a, b] &, {mono f : x y / x ≤ y}} →
surjective `[a, b] `[f a, f b] f →
{in `]a, b[, continuous f}.
Lemma segment_dec_surj_continuous a b f :
{in `[a, b] &, {mono f : x y /~ x ≤ y}} →
surjective `[a, b] `[f b, f a] f →
{in `]a, b[, continuous f}.
Lemma segment_mono_surj_continuous a b f :
monotonous `[a, b] f → surjective `[a, b] (f @`[a, b]) f →
{in `]a, b[, continuous f}.
Lemma segment_can_le_continuous a b f g : a ≤ b →
{in `[a, b], continuous f} →
{in `[a, b], cancel f g} →
{in `](f a), (f b)[, continuous g}.
Lemma segment_can_ge_continuous a b f g : a ≤ b →
{in `[a, b], continuous f} →
{in `[a, b], cancel f g} →
{in `](f b), (f a)[, continuous g}.
Lemma segment_can_continuous a b f g : a ≤ b →
{in `[a, b], continuous f} →
{in `[a, b], cancel f g} →
{in f @`]a, b[, continuous g}.
Lemma near_can_continuousAcan_sym f g (x : R) :
{near x, cancel f g} → {near x, continuous f} →
{near (f x), continuous g} ∧ {near (f x), cancel g f}.
Lemma near_can_continuous f g (x : R) :
{near x, cancel f g} → {near x, continuous f} → {near (f x), continuous g}.
Lemma near_continuous_can_sym f g (x : R) :
{near x, continuous f} → {near x, cancel f g} → {near (f x), cancel g f}.
End real_inverse_functions.
Section real_inverse_function_instances.
Variable R : realType.
Lemma exp_continuous n : continuous (@GRing.exp R ^~ n).
Lemma sqr_continuous : continuous (@exprz R ^~ 2).
Lemma sqrt_continuous : continuous (@Num.sqrt R).
End real_inverse_function_instances.
Section is_derive_inverse.
Variable R : realType.
Lemma is_derive1_caratheodory (f : R → R) (x a : R) :
is_derive x 1 f a ↔
∃ g, [/\ ∀ z, f z - f x = g z × (z - x),
{for x, continuous g} & g x = a].
Lemma is_derive_0_is_cst (f : R → R) x y :
(∀ x, is_derive x 1 f 0) → f x = f y.
Global Instance is_derive1_comp (f g : R → R) (x a b : R) :
is_derive (g x) 1 f a → is_derive x 1 g b →
is_derive x 1 (f \o g) (a × b).
Lemma is_deriveV (f : R → R) (x t v : R) :
f x != 0 → is_derive x v f t →
is_derive x v (fun y ⇒ (f y)^-1) (- (f x) ^- 2 *: t).
Lemma is_derive_inverse (f g : R → R) l x :
{near x, cancel f g} →
{near x, continuous f} →
is_derive x 1 f l → l != 0 → is_derive (f x) 1 g l^-1.
End is_derive_inverse.
Hint Extern 0 (is_derive _ _ (fun _ ⇒ (_ _)^-1) _) ⇒
(eapply is_deriveV; first by []) : typeclass_instances.