Library mathcomp.analysis.realfun
(* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C. *)
From mathcomp Require Import all_ssreflect ssralg ssrint ssrnum finmap.
From mathcomp Require Import matrix interval zmodp vector fieldext falgebra.
Require Import boolp ereal reals mathcomp_extra functions.
Require Import classical_sets signed topology prodnormedzmodule.
Require Import cardinality normedtype derive.
From mathcomp Require Import all_ssreflect ssralg ssrint ssrnum finmap.
From mathcomp Require Import matrix interval zmodp vector fieldext falgebra.
Require Import boolp ereal reals mathcomp_extra functions.
Require Import classical_sets signed 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).
TODO: this is a workaround to weaken {in I, continuous f} to use IVT.
Updating this whole file to use {within [set` I], continuous f} is the
better, but more labor intensive approach
Lemma continuous_subspace_itv (I : interval R) (f : R → R) :
{in I, continuous f} → {within [set` I], continuous f}.
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}}.
{in I, continuous f} → {within [set` I], continuous f}.
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} → set_surj `[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} → set_surj `[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} → set_surj `[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}} →
set_surj `[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}} →
set_surj `[a, b] `[f b, f a] f →
{in `]a, b[, continuous f}.
Lemma segment_mono_surj_continuous a b f :
monotonous `[a, b] f → set_surj `[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 exprn_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.
#[global] 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} → set_surj `[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} → set_surj `[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} → set_surj `[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}} →
set_surj `[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}} →
set_surj `[a, b] `[f b, f a] f →
{in `]a, b[, continuous f}.
Lemma segment_mono_surj_continuous a b f :
monotonous `[a, b] f → set_surj `[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 exprn_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.
#[global] Hint Extern 0 (is_derive _ _ (fun _ ⇒ (_ _)^-1) _) ⇒
(eapply is_deriveV; first by []) : typeclass_instances.