Library mathcomp.analysis.real_interval

(* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C.              *)
From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint interval.
From mathcomp Require Import finmap fingroup perm rat.
From mathcomp.classical Require Import boolp classical_sets functions.
From mathcomp.classical Require Import mathcomp_extra.
From mathcomp.classical Require Export set_interval.
From HB Require Import structures.
Require Import reals ereal signed topology normedtype sequences.

Set Implicit Arguments.
Import Order.TTheory GRing.Theory Num.Def Num.Theory.

Local Open Scope classical_set_scope.
Local Open Scope ring_scope.

Section interval_has.
Variable R : realType.
Implicit Types x : R.

Lemma has_sup_half x b (i : itv_bound R) : (i < BSide b x)%O →
  has_sup [set` Interval i (BSide b x)].

Lemma has_inf_half x b (i : itv_bound R) : (BSide b x < i)%O →
  has_inf [set` Interval (BSide b x) i].

End interval_has.

#[global]
Hint Extern 0 (has_sup _) ⇒ solve[apply: has_sup1 | exact: has_sup_half] : core.
#[global]
Hint Extern 0 (has_inf _) ⇒ solve[apply: has_inf1 | exact: has_inf_half]: core.

Section interval_sup_inf.
Variable R : realType.
Implicit Types x y : R.

Let sup_itv_infty_bnd x b : sup [set` Interval -oo%O (BSide b x)] = x.

Let inf_itv_bnd_infty x b : inf [set` Interval (BSide b x) +oo%O] = x.

Let sup_itv_o_bnd x y b : x < y →
  sup [set` Interval (BRight x) (BSide b y)] = y.

Let sup_itv_bounded x y a b : (BSide a x < BSide b y)%O →
  sup [set` Interval (BSide a x) (BSide b y)] = y.

Let inf_itv_bnd_o x y b : (BSide b x < BLeft y)%O →
  inf [set` Interval (BSide b x) (BLeft y)] = x.

Let inf_itv_bounded x y a b : (BSide a x < BSide b y)%O →
  inf [set` Interval (BSide a x) (BSide b y)] = x.

Lemma sup_itv a b x : (a < BSide b x)%O →
  sup [set` Interval a (BSide b x)] = x.

Lemma inf_itv a b x : (BSide b x < a)%O →
  inf [set` Interval (BSide b x) a] = x.

Lemma sup_itvcc x y : x ≤ y → sup `[x, y] = y.

Lemma inf_itvcc x y : x ≤ y → inf `[x, y] = x.

End interval_sup_inf.

Section set_itv_realType.
Variable R : realType.
Implicit Types x : R.

Lemma set_itvK : {in neitv, cancel pred_set (@Rhull R)}.

Lemma RhullT : Rhull setT = `]-oo, +oo[%R :> interval R.

Lemma RhullK : {in (@is_interval _ : set (set R)), cancel (@Rhull R) pred_set}.

Lemma itv_c_inftyEbigcap x :
  `[x, +oo[%classic = \bigcap_k `]x - k.+1%:R^-1, +oo[%classic.

Lemma itv_bnd_inftyEbigcup b x : [set` Interval (BSide b x) +oo%O] =
  \bigcup_k [set` Interval (BSide b x) (BLeft k%:R)].

Lemma itv_o_inftyEbigcup x :
  `]x, +oo[%classic = \bigcup_k `[x + k.+1%:R^-1, +oo[%classic.

Lemma set_itv_setT (i : interval R) : [set` i] = setT → i = `]-oo, +oo[.

End set_itv_realType.

Section Rhull_lemmas.
Variable R : realType.
Implicit Types (a b t r : R) (A : set R).

Lemma Rhull_smallest A : [set` Rhull A] = smallest (@is_interval R) A.

Lemma le_Rhull : {homo (@Rhull R) : A B / (A `<=` B) >-> {subset A ≤ B}}.

Lemma neitv_Rhull A : ~~ neitv (Rhull A) → A = set0.

Lemma Rhull_involutive A : Rhull [set` Rhull A] = Rhull A.

End Rhull_lemmas.

Coercion ereal_of_itv_bound T (b : itv_bound T) : \bar T :=
  match b with BSide _ y ⇒ y%:E | +oo%O ⇒ +oo%E | -oo%O ⇒ -oo%E end.
Arguments ereal_of_itv_bound T !b.

Section itv_realDomainType.
Context (R : realDomainType).

Lemma le_bnd_ereal (a b : itv_bound R) : (a ≤ b)%O → (a ≤ b)%E.

Lemma lt_ereal_bnd (a b : itv_bound R) : (a < b)%E → (a < b)%O.

Lemma Interval_ereal_mem (r : R) (a b : itv_bound R) :
  r \in Interval a b → (a ≤ r%:E ≤ b)%E.

Lemma ereal_mem_Interval (r : R) (a b : itv_bound R) :
  (a < r%:E < b)%E → r \in Interval a b.

Lemma itv_cyy : `[+oo%E, +oo[%classic = [set +oo%E] :> set (\bar R).

Lemma itv_oyy : `]+oo%E, +oo[%classic = set0 :> set (\bar R).

Lemma itv_cNyy : `[-oo%E, +oo[%classic = setT :> set (\bar R).

Lemma itv_oNyy : `]-oo%E, +oo[%classic = ~` [set -oo]%E :> set (\bar R).

End itv_realDomainType.

Section set_ereal.
Context (R : realType) T (f g : T → \bar R).
Local Open Scope ereal_scope.

Let E j := [set x | f x - g x ≥ j.+1%:R^-1%:E].

Lemma set_lte_bigcup : [set x | f x > g x] = \bigcup_j E j.

End set_ereal.

Lemma disj_itv_Rhull {R : realType} (A B : set R) : A `&` B = set0 →
  is_interval A → is_interval B → disjoint_itv (Rhull A) (Rhull B).