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.
From mathcomp Require Import mathcomp_extra boolp classical_sets functions.
From mathcomp Require Import cardinality.
Require Import ereal reals signed topology prodnormedzmodule normedtype derive.
Require Import real_interval.
From HB Require Import structures.
From mathcomp Require Import all_ssreflect ssralg ssrint ssrnum finmap.
From mathcomp Require Import matrix interval zmodp vector fieldext falgebra.
From mathcomp Require Import mathcomp_extra boolp classical_sets functions.
From mathcomp Require Import cardinality.
Require Import ereal reals signed topology prodnormedzmodule normedtype derive.
Require Import real_interval.
From HB Require Import structures.
This file provides properties of standard real-valued functions over real
numbers (e.g., the continuity of the inverse of a continuous function).
derivable_oo_continuous_bnd f x y == f is derivable on `]x, y[ and
continuous up to the boundary
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 derivable_oo_continuous_bnd.
Context {R : numFieldType} {V : normedModType R}.
Definition derivable_oo_continuous_bnd (f : R → V) (x y : R) :=
[/\ {in `]x, y[, ∀ x, derivable f x 1},
f @ x^'+ --> f x & f @ y^'- --> f y].
Lemma derivable_oo_continuous_bnd_within (f : R → V) (x y : R) :
derivable_oo_continuous_bnd f x y → {within `[x, y], continuous f}.
End derivable_oo_continuous_bnd.
Section real_inverse_functions.
Variable R : realType.
Implicit Types (a b : R) (f g : R → R).
This lemma should be used with caution. Generally `{within I, continuous f}`
is what one would intend. So having `{in I, continuous f}` as a condition
may indicate potential issues at the endpoints of the interval.
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]) →
{within [set` 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]) →
{within [set` I], continuous f} → {in I &, injective f} →
{in I &, {mono f : x y /~ x ≤ y}}.
Lemma itv_continuous_inj_mono f (I : interval R) :
{within [set` I], continuous f} → {in I &, injective f} → monotonous I f.
Lemma segment_continuous_inj_le f a b :
f a ≤ f b → {within `[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 → {within `[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]) →
{within [set` 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]) →
{within [set` I], continuous f} → {in I &, injective f} →
{in I &, {mono f : x y /~ x ≤ y}}.
Lemma itv_continuous_inj_mono f (I : interval R) :
{within [set` I], continuous f} → {in I &, injective f} → monotonous I f.
Lemma segment_continuous_inj_le f a b :
f a ≤ f b → {within `[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 → {within `[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 →
{within `[a, b], continuous f} →
{in `[a, b], cancel f g} →
{in `[f a, f b] &, {mono g : x y / x ≤ y}}.
Section negation_itv.
End negation_itv.
{within `[a, b], continuous f} →
{in `[a, b], cancel f g} →
{in `[f a, f b] &, {mono g : x y / x ≤ y}}.
Section negation_itv.
End negation_itv.
The condition "f b <= f a" is unnecessary---see seg...increasing above
Lemma segment_can_ge a b f g : a ≤ b →
{within `[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 →
{within `[a, b], continuous f} → {in `[a, b], cancel f g} →
monotonous (f @`[a, b]) g.
Lemma segment_continuous_surjective a b f : a ≤ b →
{within `[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 →
{within `[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 →
{within `[a, b], continuous f} → set_surj `[a, b] `[f b, f a] f.
Lemma continuous_inj_image_segment a b f : a ≤ b →
{within `[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 →
{within `[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 →
{within `[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 →
{within `[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 →
{within `[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 →
{within `[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 →
{within `[a, b], continuous f}.
Lemma segment_mono_surj_continuous a b f :
monotonous `[a, b] f → set_surj `[a, b] (f @`[a, b]) f →
{within `[a, b], continuous f}.
Lemma segment_can_le_continuous a b f g : a ≤ b →
{within `[a, b], continuous f} →
{in `[a, b], cancel f g} →
{within `[(f a), (f b)], continuous g}.
Lemma segment_can_ge_continuous a b f g : a ≤ b →
{within `[a, b], continuous f} →
{in `[a, b], cancel f g} →
{within `[(f b), (f a)], continuous g}.
Lemma segment_can_continuous a b f g : a ≤ b →
{within `[a, b], continuous f} →
{in `[a, b], cancel f g} →
{within 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.
{within `[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 →
{within `[a, b], continuous f} → {in `[a, b], cancel f g} →
monotonous (f @`[a, b]) g.
Lemma segment_continuous_surjective a b f : a ≤ b →
{within `[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 →
{within `[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 →
{within `[a, b], continuous f} → set_surj `[a, b] `[f b, f a] f.
Lemma continuous_inj_image_segment a b f : a ≤ b →
{within `[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 →
{within `[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 →
{within `[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 →
{within `[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 →
{within `[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 →
{within `[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 →
{within `[a, b], continuous f}.
Lemma segment_mono_surj_continuous a b f :
monotonous `[a, b] f → set_surj `[a, b] (f @`[a, b]) f →
{within `[a, b], continuous f}.
Lemma segment_can_le_continuous a b f g : a ≤ b →
{within `[a, b], continuous f} →
{in `[a, b], cancel f g} →
{within `[(f a), (f b)], continuous g}.
Lemma segment_can_ge_continuous a b f g : a ≤ b →
{within `[a, b], continuous f} →
{in `[a, b], cancel f g} →
{within `[(f b), (f a)], continuous g}.
Lemma segment_can_continuous a b f g : a ≤ b →
{within `[a, b], continuous f} →
{in `[a, b], cancel f g} →
{within 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.