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.

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.
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.

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.