Library mathcomp.analysis.mathcomp_extra

(* mathcomp analysis (c) 2022 Inria and AIST. License: CeCILL-C.              *)
From mathcomp Require choice.

Coercion choice.Choice.mixin : choice.Choice.class_of >-> choice.Choice.mixin_of.
From mathcomp Require Import all_ssreflect finmap ssralg ssrnum ssrint rat.
From mathcomp Require Import finset interval.

Set Implicit Arguments.

Reserved Notation "f \* g" (at level 40, left associativity).
Reserved Notation "f \- g" (at level 50, left associativity).
Reserved Notation "\- f" (at level 35, f at level 35).
Reserved Notation "f \max g" (at level 50, left associativity).

Lemma all_sig2_cond {I : Type} {T : Type} (D : pred I)
   (P Q : I → T → Prop) : T →
    (∀ x : I, D x → {y : T | P x y & Q x y}) →
  {f : ∀ x : I, T | ∀ x : I, D x → P x (f x) & ∀ x : I, D x → Q x (f x)}.

Lemma enum_ord0 : enum 'I_0 = [::].

Lemma enum_ordSr n : enum 'I_n.+1 =
  rcons (map (widen_ord (leqnSn _)) (enum 'I_n)) ord_max.

Definition olift aT rT (f : aT → rT) := Some \o f.

Lemma obindEapp {aT rT} (f : aT → option rT) : obind f = oapp f None.

Lemma omapEbind {aT rT} (f : aT → rT) : omap f = obind (olift f).

Lemma omapEapp {aT rT} (f : aT → rT) : omap f = oapp (olift f) None.

Lemma oappEmap {aT rT} (f : aT → rT) (y0 : rT) x :
  oapp f y0 x = odflt y0 (omap f x).

Lemma omap_comp aT rT sT (f : aT → rT) (g : rT → sT) :
  omap (g \o f) =1 omap g \o omap f.

Lemma oapp_comp aT rT sT (f : aT → rT) (g : rT → sT) x :
  oapp (g \o f) x =1 (@oapp _ _)^~ x g \o omap f.

Lemma oapp_comp_f {aT rT sT} (f : aT → rT) (g : rT → sT) (x : rT) :
  oapp (g \o f) (g x) =1 g \o oapp f x.

Lemma olift_comp aT rT sT (f : aT → rT) (g : rT → sT) :
  olift (g \o f) = olift g \o f.

Lemma compA {A B C D : Type} (f : B → A) (g : C → B) (h : D → C) :
  f \o (g \o h) = (f \o g) \o h.

Lemma can_in_pcan [rT aT : Type] (A : {pred aT}) [f : aT → rT] [g : rT → aT] :
  {in A, cancel f g} → {in A, pcancel f (fun y : rT ⇒ Some (g y))}.

Lemma pcan_in_inj [rT aT : Type] [A : {pred aT}] [f : aT → rT] [g : rT → option aT] :
  {in A, pcancel f g} → {in A &, injective f}.

Lemma can_in_comp [A B C : Type] (D : {pred B}) (D' : {pred C})
    [f : B → A] [h : C → B]
    [f' : A → B] [h' : B → C] :
  {homo h : x / x \in D' >-> x \in D} →
  {in D, cancel f f'} → {in D', cancel h h'} →
  {in D', cancel (f \o h) (h' \o f')}.

Lemma in_inj_comp A B C (f : B → A) (h : C → B) (P : pred B) (Q : pred C) :
  {in P &, injective f} → {in Q &, injective h} → {homo h : x / Q x >-> P x} →
  {in Q &, injective (f \o h)}.

Lemma pcan_in_comp [A B C : Type] (D : {pred B}) (D' : {pred C})
    [f : B → A] [h : C → B]
    [f' : A → option B] [h' : B → option C] :
  {homo h : x / x \in D' >-> x \in D} →
  {in D, pcancel f f'} → {in D', pcancel h h'} →
  {in D', pcancel (f \o h) (obind h' \o f')}.

Lemma ocan_comp [A B C : Type] [f : B → option A] [h : C → option B]
    [f' : A → B] [h' : B → C] :
  ocancel f f' → ocancel h h' → ocancel (obind f \o h) (h' \o f').

Definition pred_oapp T (D : {pred T}) : pred (option T) :=
  [pred x | oapp (mem D) false x].

Lemma ocan_in_comp [A B C : Type] (D : {pred B}) (D' : {pred C})
    [f : B → option A] [h : C → option B]
    [f' : A → B] [h' : B → C] :
  {homo h : x / x \in D' >-> x \in pred_oapp D} →
  {in D, ocancel f f'} → {in D', ocancel h h'} →
  {in D', ocancel (obind f \o h) (h' \o f')}.

Lemma eqbLR (b1 b2 : bool) : b1 = b2 → b1 → b2.

Lemma eqbRL (b1 b2 : bool) : b1 = b2 → b2 → b1.

Definition opp_fun T (R : zmodType) (f : T → R) x := (- f x)%R.
Notation "\- f" := (opp_fun f) : ring_scope.
Arguments opp_fun {T R} _ _ /.

Definition mul_fun T (R : ringType) (f g : T → R) x := (f x × g x)%R.
Notation "f \* g" := (mul_fun f g) : ring_scope.
Arguments mul_fun {T R} _ _ _ /.

Import Order.TTheory GRing.Theory Num.Theory.

Definition max_fun T (R : numDomainType) (f g : T → R) x := Num.max (f x) (g x).
Notation "f \max g" := (max_fun f g) : ring_scope.
Arguments max_fun {T R} _ _ _ /.

Lemma gtr_opp (R : numDomainType) (r : R) : (0 < r)%R → (- r < r)%R.

Lemma le_le_trans {disp : unit} {T : porderType disp} (x y z t : T) :
  (z ≤ x)%O → (y ≤ t)%O → (x ≤ y)%O → (z ≤ t)%O.

Notation eqLHS := (X in (X == _))%pattern.
Notation eqRHS := (X in (_ == X))%pattern.
Notation leLHS := (X in (X ≤ _)%O)%pattern.
Notation leRHS := (X in (_ ≤ X)%O)%pattern.
Notation ltLHS := (X in (X < _)%O)%pattern.
Notation ltRHS := (X in (_ < X)%O)%pattern.
Inductive boxed T := Box of T.

Lemma eq_bigl_supp [R : eqType] [idx : R] [op : Monoid.law idx] [I : Type]
  [r : seq I] [P1 : pred I] (P2 : pred I) (F : I → R) :
  {in [pred x | F x != idx], P1 =1 P2} →
  \big[op/idx]_(i <- r | P1 i) F i = \big[op/idx]_(i <- r | P2 i) F i.

Lemma perm_big_supp_cond [R : eqType] [idx : R] [op : Monoid.com_law idx] [I : eqType]
  [r s : seq I] [P : pred I] (F : I → R) :
  perm_eq [seq i <- r | P i && (F i != idx)] [seq i <- s | P i && (F i != idx)] →
  \big[op/idx]_(i <- r | P i) F i = \big[op/idx]_(i <- s| P i) F i.

Lemma perm_big_supp [R : eqType] [idx : R] [op : Monoid.com_law idx] [I : eqType]
  [r s : seq I] [P : pred I] (F : I → R) :
  perm_eq [seq i <- r | (F i != idx)] [seq i <- s | (F i != idx)] →
  \big[op/idx]_(i <- r | P i) F i = \big[op/idx]_(i <- s| P i) F i.

Local Open Scope order_scope.
Local Open Scope ring_scope.
Import GRing.Theory Order.TTheory.

Lemma mulr_ge0_gt0 (R : numDomainType) (x y : R) : 0 ≤ x → 0 ≤ y →
  (0 < x × y) = (0 < x) && (0 < y).

Section lt_le_gt_ge.
Variable (R : numFieldType).
Implicit Types x y z a b : R.

Lemma splitr x : x = x / 2%:R + x / 2%:R.

Lemma ler_addgt0Pr x y : reflect (∀ e, e > 0 → x ≤ y + e) (x ≤ y).

Lemma ler_addgt0Pl x y : reflect (∀ e, e > 0 → x ≤ e + y) (x ≤ y).

Lemma in_segment_addgt0Pr x y z :
  reflect (∀ e, e > 0 → y \in `[x - e, z + e]) (y \in `[x, z]).

Lemma in_segment_addgt0Pl x y z :
  reflect (∀ e, e > 0 → y \in `[(- e + x), (e + z)]) (y \in `[x, z]).

Lemma lt_le a b : (∀ x, x < a → x < b) → a ≤ b.

Lemma gt_ge a b : (∀ x, b < x → a < x) → a ≤ b.

End lt_le_gt_ge.

Coercion pair_of_interval T (I : interval T) : itv_bound T × itv_bound T :=
  let: Interval b1 b2 := I in (b1, b2).

Section itv_simp.
Variables (d : unit) (T : porderType d).
Implicit Types (x y : T) (b : bool).

Lemma ltBSide x y b b' :
  ((BSide b x < BSide b' y) = (x < y ?<= if b && ~~ b'))%O.

Lemma leBSide x y b b' :
  ((BSide b x ≤ BSide b' y) = (x < y ?<= if b' ==> b))%O.

Definition lteBSide := (ltBSide, leBSide).

Let BLeft_ltE x y b : (BSide b x < BLeft y)%O = (x < y)%O.
Let BRight_leE x y b : (BSide b x ≤ BRight y)%O = (x ≤ y)%O.
Let BRight_BLeft_leE x y : (BRight x ≤ BLeft y)%O = (x < y)%O.
Let BLeft_BRight_ltE x y : (BLeft x < BRight y)%O = (x ≤ y)%O.
Let BRight_BSide_ltE x y b : (BRight x < BSide b y)%O = (x < y)%O.
Let BLeft_BSide_leE x y b : (BLeft x ≤ BSide b y)%O = (x ≤ y)%O.
Let BSide_ltE x y b : (BSide b x < BSide b y)%O = (x < y)%O.
Let BSide_leE x y b : (BSide b x ≤ BSide b y)%O = (x ≤ y)%O.
Let BInfty_leE a : (a ≤ BInfty T false)%O.
Let BInfty_geE a : (BInfty T true ≤ a)%O.
Let BInfty_le_eqE a : (BInfty T false ≤ a)%O = (a == BInfty T false).
Let BInfty_ge_eqE a : (a ≤ BInfty T true)%O = (a == BInfty T true).
Let BInfty_ltE a : (a < BInfty T false)%O = (a != BInfty T false).
Let BInfty_gtE a : (BInfty T true < a)%O = (a != BInfty T true).
Let BInfty_ltF a : (BInfty T false < a)%O = false.
Let BInfty_gtF a : (a < BInfty T true)%O = false.
Let BInfty_BInfty_ltE : (BInfty T true < BInfty T false)%O.

Lemma ltBRight_leBLeft (a : itv_bound T) (r : T) :
  (a < BRight r)%O = (a ≤ BLeft r)%O.
Lemma leBRight_ltBLeft (a : itv_bound T) (r : T) :
  (BRight r ≤ a)%O = (BLeft r < a)%O.

Definition bnd_simp := (BLeft_ltE, BRight_leE,
  BRight_BLeft_leE, BLeft_BRight_ltE,
  BRight_BSide_ltE, BLeft_BSide_leE, BSide_ltE, BSide_leE,
  BInfty_leE, BInfty_geE, BInfty_BInfty_ltE,
  BInfty_le_eqE, BInfty_ge_eqE, BInfty_ltE, BInfty_gtE, BInfty_ltF, BInfty_gtF,
  @lexx _ T, @ltxx _ T, @eqxx T).

Lemma itv_splitU1 (a : itv_bound T) (x : T) : (a ≤ BLeft x)%O →
  Interval a (BRight x) =i [predU1 x & Interval a (BLeft x)].

Lemma itv_split1U (a : itv_bound T) (x : T) : (BRight x ≤ a)%O →
  Interval (BLeft x) a =i [predU1 x & Interval (BRight x) a].

End itv_simp.

Definition miditv (R : numDomainType) (i : interval R) : R :=
  match i with
  | Interval (BSide _ a) (BSide _ b) ⇒ (a + b) / 2%:R
  | Interval -oo%O (BSide _ b) ⇒ b - 1
  | Interval (BSide _ a) +oo%O ⇒ a + 1
  | Interval -oo%O +oo%O ⇒ 0
  | _ ⇒ 0
  end.

Section miditv_lemmas.
Variable R : numFieldType.
Implicit Types i : interval R.

Lemma mem_miditv i : (i.1 < i.2)%O → miditv i \in i.

Lemma miditv_le_left i b : (i.1 < i.2)%O → (BSide b (miditv i) ≤ i.2)%O.

Lemma miditv_ge_right i b : (i.1 < i.2)%O → (i.1 ≤ BSide b (miditv i))%O.

End miditv_lemmas.

Section itv_porderType.
Variables (d : unit) (T : orderType d).
Implicit Types (a : itv_bound T) (x y : T) (i j : interval T) (b : bool).

Lemma predC_itvl a : [predC Interval -oo%O a] =i Interval a +oo%O.

Lemma predC_itvr a : [predC Interval a +oo%O] =i Interval -oo%O a.

Lemma predC_itv i : [predC i] =i [predU Interval -oo%O i.1 & Interval i.2 +oo%O].

End itv_porderType.

Lemma fset_nat_maximum (X : choiceType) (A : {fset X})
    (f : X → nat) : A != fset0 →
  (∃ i, i \in A ∧ ∀ j, j \in A → f j ≤ f i)%nat.

Lemma image_nat_maximum n (f : nat → nat) :
  (∃ i, i ≤ n ∧ ∀ j, j ≤ n → f j ≤ f i)%N.

Lemma card_fset_sum1 (T : choiceType) (A : {fset T}) :
  #|` A| = (\sum_(i <- A) 1)%N.

Arguments big_rmcond {R idx op I r} P.
Arguments big_rmcond_in {R idx op I r} P.

Section bigminr_maxr.
Import Num.Def.

Lemma bigminr_maxr (R : realDomainType) I r (P : pred I) (F : I → R) x :
  \big[minr/x]_(i <- r | P i) F i = - \big[maxr/- x]_(i <- r | P i) - F i.
End bigminr_maxr.

Section SemiGroupProperties.
Variables (R : Type) (op : R → R → R).
Hypothesis opA : associative op.

Section Id.
Variable x : R.
Hypothesis opxx : op x x = x.

Lemma big_const_idem I (r : seq I) P : \big[op/x]_(i <- r | P i) x = x.

Lemma big_id_idem I (r : seq I) P F :
  op (\big[op/x]_(i <- r | P i) F i) x = \big[op/x]_(i <- r | P i) F i.

End Id.

Section Abelian.
Hypothesis opC : commutative op.

Let opCA : left_commutative op.

Variable x : R.

Lemma big_rem_AC (I : eqType) (r : seq I) z (P : pred I) F : z \in r →
  \big[op/x]_(y <- r | P y) F y =
    if P z then op (F z) (\big[op/x]_(y <- rem z r | P y) F y)
           else \big[op/x]_(y <- rem z r | P y) F y.

Lemma bigD1_AC (I : finType) j (P : pred I) F : P j →
  \big[op/x]_(i | P i) F i = op (F j) (\big[op/x]_(i | P i && (i != j)) F i).

Section Id.
Hypothesis opxx : op x x = x.

Lemma big_mkcond_idem I r (P : pred I) F :
  \big[op/x]_(i <- r | P i) F i = \big[op/x]_(i <- r) (if P i then F i else x).

Lemma big_split_idem I r (P : pred I) F1 F2 :
  \big[op/x]_(i <- r | P i) op (F1 i) (F2 i) =
    op (\big[op/x]_(i <- r | P i) F1 i) (\big[op/x]_(i <- r | P i) F2 i).

Lemma big_id_idem_AC I (r : seq I) P F :
  \big[op/x]_(i <- r | P i) op (F i) x = \big[op/x]_(i <- r | P i) F i.

Lemma bigID_idem I r (a P : pred I) F :
  \big[op/x]_(i <- r | P i) F i =
    op (\big[op/x]_(i <- r | P i && a i) F i)
       (\big[op/x]_(i <- r | P i && ~~ a i) F i).

End Id.

End Abelian.

End SemiGroupProperties.

Section bigmaxmin.
Local Open Scope order_scope.
Variables (d : _) (T : porderType d).
Variables (I : finType) (f : I → T) (x0 x : T) (P : pred I).

Lemma bigmax_le :
  x0 ≤ x → (∀ i, P i → f i ≤ x) → \big[max/x0]_(i | P i) f i ≤ x.

Lemma bigmax_lt :
  x0 < x → (∀ i, P i → f i < x) → \big[max/x0]_(i | P i) f i < x.

Lemma lt_bigmin :
  x < x0 → (∀ i, P i → x < f i) → x < \big[min/x0]_(i | P i) f i.

Lemma le_bigmin :
  x ≤ x0 → (∀ i, P i → x ≤ f i) → x ≤ \big[min/x0]_(i | P i) f i.

End bigmaxmin.

Section bigmax.
Local Open Scope order_scope.
Variables (d : unit) (T : orderType d).

Section bigmax_Type.
Variables (I : Type) (r : seq I) (x : T).
Implicit Types (P a : pred I) (F : I → T).

Lemma bigmax_mkcond P F : \big[max/x]_(i <- r | P i) F i =
  \big[max/x]_(i <- r) (if P i then F i else x).

Lemma bigmax_split P F1 F2 :
  \big[max/x]_(i <- r | P i) (max (F1 i) (F2 i)) =
  max (\big[max/x]_(i <- r | P i) F1 i) (\big[max/x]_(i <- r | P i) F2 i).

Lemma bigmax_idl P F :
  \big[max/x]_(i <- r | P i) F i = max x (\big[max/x]_(i <- r | P i) F i).

Lemma bigmax_idr P F :
  \big[max/x]_(i <- r | P i) F i = max (\big[max/x]_(i <- r | P i) F i) x.

Lemma bigmaxID a P F : \big[max/x]_(i <- r | P i) F i =
  max (\big[max/x]_(i <- r | P i && a i) F i)
      (\big[max/x]_(i <- r | P i && ~~ a i) F i).

End bigmax_Type.

Section bigmax_finType.
Variables (I : finType) (x : T).
Implicit Types (P : pred I) (F : I → T).

Lemma bigmaxD1 j P F : P j →
  \big[max/x]_(i | P i) F i = max (F j) (\big[max/x]_(i | P i && (i != j)) F i).

Lemma le_bigmax_cond j P F : P j → F j ≤ \big[max/x]_(i | P i) F i.

Lemma le_bigmax F j : F j ≤ \big[max/x]_i F i.

Lemma bigmax_sup j P m F : P j → m ≤ F j → m ≤ \big[max/x]_(i | P i) F i.

Lemma bigmax_leP m P F : reflect (x ≤ m ∧ ∀ i, P i → F i ≤ m)
                                 (\big[max/x]_(i | P i) F i ≤ m).

Lemma bigmax_ltP m P F :
  reflect (x < m ∧ ∀ i, P i → F i < m) (\big[max/x]_(i | P i) F i < m).

Lemma bigmax_eq_arg j P F : P j → (∀ i, P i → x ≤ F i) →
  \big[max/x]_(i | P i) F i = F [arg max_(i > j | P i) F i].

Lemma eq_bigmax j P F : P j → (∀ i, P i → x ≤ F i) →
  {i0 | i0 \in I & \big[max/x]_(i | P i) F i = F i0}.

Lemma homo_le_bigmax P F1 F2 : (∀ i, P i → F1 i ≤ F2 i) →
  \big[max/x]_(i | P i) F1 i ≤ \big[max/x]_(i | P i) F2 i.

End bigmax_finType.

End bigmax.
Arguments bigmax_mkcond {d T I r}.
Arguments bigmaxID {d T I r}.
Arguments bigmaxD1 {d T I x} j.
Arguments bigmax_sup {d T I x} j.
Arguments bigmax_eq_arg {d T I} x j.
Arguments eq_bigmax {d T I x} j.

Section bigmin.
Local Open Scope order_scope.
Variables (d : _) (T : orderType d).

Section bigmin_Type.
Variable (I : Type) (r : seq I) (x : T).
Implicit Types (P a : pred I) (F : I → T).

Lemma bigmin_mkcond P F : \big[min/x]_(i <- r | P i) F i =
   \big[min/x]_(i <- r) (if P i then F i else x).

Lemma bigmin_split P F1 F2 :
  \big[min/x]_(i <- r | P i) (min (F1 i) (F2 i)) =
  min (\big[min/x]_(i <- r | P i) F1 i) (\big[min/x]_(i <- r | P i) F2 i).

Lemma bigmin_idl P F :
  \big[min/x]_(i <- r | P i) F i = min x (\big[min/x]_(i <- r | P i) F i).

Lemma bigmin_idr P F :
  \big[min/x]_(i <- r | P i) F i = min (\big[min/x]_(i <- r | P i) F i) x.

Lemma bigminID a P F : \big[min/x]_(i <- r | P i) F i =
  min (\big[min/x]_(i <- r | P i && a i) F i)
      (\big[min/x]_(i <- r | P i && ~~ a i) F i).

End bigmin_Type.

Section bigmin_finType.
Variable (I : finType) (x : T).
Implicit Types (P : pred I) (F : I → T).

Lemma bigminD1 j P F : P j →
  \big[min/x]_(i | P i) F i = min (F j) (\big[min/x]_(i | P i && (i != j)) F i).

Lemma bigmin_le_cond j P F : P j → \big[min/x]_(i | P i) F i ≤ F j.

Lemma bigmin_le j F : \big[min/x]_i F i ≤ F j.

Lemma bigmin_inf j P m F : P j → F j ≤ m → \big[min/x]_(i | P i) F i ≤ m.

Lemma bigmin_geP m P F : reflect (m ≤ x ∧ ∀ i, P i → m ≤ F i)
                                 (m ≤ \big[min/x]_(i | P i) F i).

Lemma bigmin_gtP m P F :
  reflect (m < x ∧ ∀ i, P i → m < F i) (m < \big[min/x]_(i | P i) F i).

Lemma bigmin_eq_arg j P F : P j → (∀ i, P i → F i ≤ x) →
  \big[min/x]_(i | P i) F i = F [arg min_(i < j | P i) F i].

Lemma eq_bigmin j P F : P j → (∀ i, P i → F i ≤ x) →
  {i0 | i0 \in I & \big[min/x]_(i | P i) F i = F i0}.

End bigmin_finType.

End bigmin.
Arguments bigmin_mkcond {d T I r}.
Arguments bigminID {d T I r}.
Arguments bigminD1 {d T I x} j.
Arguments bigmin_inf {d T I x} j.
Arguments bigmin_eq_arg {d T I} x j.
Arguments eq_bigmin {d T I x} j.