Top

Module mathcomp.analysis.numfun

From HB Require Import structures.
From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint interval finmap.
#[warning="-warn-library-file-internal-analysis"]
From mathcomp Require Import unstable.
From mathcomp Require Import mathcomp_extra boolp classical_sets fsbigop.
From mathcomp Require Import functions cardinality set_interval.
From mathcomp Require Import interval_inference reals ereal topology normedtype.
From mathcomp Require Import sequences function_spaces.


Reserved Notation "{ 'nnfun' aT >-> T }"
  (at level 0, format "{ 'nnfun' aT >-> T }").
Reserved Notation "[ 'nnfun' 'of' f ]"
  (at level 0, format "[ 'nnfun' 'of' f ]").

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Import Order.TTheory GRing.Theory Num.Theory.
Import numFieldTopology.Exports.

Local Open Scope classical_set_scope.
Local Open Scope ring_scope.

Notation "'nondecreasing_fun' f" := ({homo f : n m / (n <= m)%O >-> (n <= m)%O})
  (at level 10).
Notation "'nonincreasing_fun' f" := ({homo f : n m / (n <= m)%O >-> (n >= m)%O})
  (at level 10).
Notation "'increasing_fun' f" := ({mono f : n m / (n <= m)%O >-> (n <= m)%O})
  (at level 10).
Notation "'decreasing_fun' f" := ({mono f : n m / (n <= m)%O >-> (n >= m)%O})
  (at level 10).

Lemma nondecreasing_funN {R : numDomainType} a b (f : R -> R) :
  {in `[a, b] &, nondecreasing_fun f} <->
  {in `[a, b] &, nonincreasing_fun (\- f)}.

Proof.

split=> [h m n mab nab mn|h m n mab nab mn]; first by rewrite lerNr opprK h.
by rewrite -(opprK (f n)) -lerNr h.
Qed.

Lemma nonincreasing_funN {R : numDomainType} a b (f : R -> R) :
  {in `[a, b] &, nonincreasing_fun f} <->
  {in `[a, b] &, nondecreasing_fun (\- f)}.

Proof.

apply: iff_sym; apply: (iff_trans (nondecreasing_funN a b (\- f))).
rewrite [in X in _ <-> X](_ : f = \- (\- f))//.
by apply/funext => x /=; rewrite opprK.
Qed.

Section interval_partition_porderType.
Context {d} {T : porderType d}.
Implicit Type (a b : T) (s : seq T).

Definition itv_partition a b s := [/\ path <%O a s & last a s == b].

Lemma itv_partition_nil a b : itv_partition a b [::] -> a = b.

Proof.

by move=> [_ /eqP <-]. Qed.

Lemma itv_partition_cons a b x s :
  itv_partition a b (x :: s) -> itv_partition x b s.

Proof.

by rewrite /itv_partition/= => -[/andP[]]. Qed.

Lemma itv_partition1 a b : (a < b)%O -> itv_partition a b [:: b].

Proof.

by rewrite /itv_partition /= => ->. Qed.

Lemma itv_partition_size_neq0 a b s :
  (size s > 0)%N -> itv_partition a b s -> (a < b)%O.

Proof.

elim: s a => // x [_ a _|h t ih a _]; rewrite /itv_partition /=.
  by rewrite andbT => -[ax /eqP <-].
move=> [] /andP[ax /andP[xy] ht /eqP tb].
by rewrite (lt_trans ax)// ih// /itv_partition /= xy/= tb.
Qed.

Lemma itv_partitionxx a s : itv_partition a a s -> s = [::].

Proof.

case: s => //= h t [/= /andP[ah /lt_path_min/allP ht] /eqP hta].
suff : (h < a)%O by move/lt_trans => /(_ _ ah); rewrite ltxx.
apply/ht; rewrite -hta.
by have := mem_last h t; rewrite inE hta lt_eqF.
Qed.

Lemma itv_partition_le a b s : itv_partition a b s -> (a <= b)%O.

Proof.

case: s => [/itv_partition_nil ->//|h t /itv_partition_size_neq0 - /(_ _)/ltW].
exact.
Qed.

Lemma itv_partition_cat a b c s t :
  itv_partition a b s -> itv_partition b c t -> itv_partition a c (s ++ t).

Proof.

rewrite /itv_partition => -[sa /eqP asb] [bt btc].
by rewrite cat_path// sa /= last_cat asb.
Qed.

Lemma itv_partition_nth_size def a b s : itv_partition a b s ->
  nth def (a :: s) (size s) = b.

Proof.

by elim: s a => [a/= /itv_partition_nil//|y t ih a /= /itv_partition_cons/ih].
Qed.

Lemma itv_partition_nth_ge a b s m : (m < (size s).+1)%N ->
  itv_partition a b s -> (a <= nth b (a :: s) m)%O.

Proof.

elim: m s a b => [s a b _//|n ih [//|h t] a b].
rewrite ltnS => nh [/= /andP[ah ht] lb].
by rewrite (le_trans (ltW ah))// ih.
Qed.

Lemma itv_partition_nth_le a b s m : (m < (size s).+1)%N ->
  itv_partition a b s -> (nth b (a :: s) m <= b)%O.

Proof.

elim: m s a => [s a _|n ih]; first exact: itv_partition_le.
by move=> [//|a h t /= nt] H; rewrite ih//; exact: itv_partition_cons H.
Qed.

Lemma nondecreasing_fun_itv_partition a b f s :
  {in `[a, b] &, nondecreasing_fun f} -> itv_partition a b s ->
  let F : nat -> T := f \o nth b (a :: s) in
  forall k, (k < size s)%N -> (F k <= F k.+1)%O.

Proof.

move=> ndf abs F k ks.
have [_] := nondecreasing_seqP F; apply => m n mn; rewrite /F/=.
have [ms|ms] := ltnP m (size s).+1; last first.
  rewrite nth_default//.
  have [|ns] := ltnP n (size s).+1; last by rewrite nth_default.
  by move=> /(leq_ltn_trans mn); rewrite ltnS leqNgt ms.
have [ns|ns] := ltnP n (size s).+1; last first.
  rewrite [in leRHS]nth_default//=; apply/ndf/itv_partition_nth_le => //.
    by rewrite in_itv/= itv_partition_nth_le// andbT itv_partition_nth_ge.
  by rewrite in_itv/= lexx andbT; exact: (itv_partition_le abs).
move: abs; rewrite /itv_partition => -[] sa sab.
move: mn; rewrite leq_eqVlt => /predU1P[->//|mn].
apply/ndf/ltW/sorted_ltn_nth => //=; last exact: lt_trans.
  by rewrite in_itv/= itv_partition_nth_le// andbT itv_partition_nth_ge.
by rewrite in_itv/= itv_partition_nth_le// andbT itv_partition_nth_ge.
Qed.

Definition itv_partitionL s c := rcons [seq x <- s | (x < c)%O] c.

Definition itv_partitionR s c := [seq x <- s | (c < x)%O].

End interval_partition_porderType.

Section interval_partition_orderType.
Context {d} {T : orderType d}.
Implicit Type (a b : T) (s : seq T).

Lemma itv_partitionLP a b c s : (a < c)%O -> (c < b)%O -> itv_partition a b s ->
  itv_partition a c (itv_partitionL s c).

Proof.

move=> ac bc [] al /eqP htb; split.
  rewrite /itv_partitionL rcons_path/=; apply/andP; split.
    by apply: path_filter => //; exact: lt_trans.
  exact: (last_filterP [pred x | (x < c)%O]).
by rewrite /itv_partitionL last_rcons.
Qed.

Lemma itv_partitionRP a b c s : (a < c)%O -> (c < b)%O -> itv_partition a b s ->
  itv_partition c b (itv_partitionR s c).

Proof.

move=> ac cb [] sa /eqP alb; rewrite /itv_partition; split.
  move: sa; rewrite lt_path_sortedE => /andP[allas ss].
  rewrite lt_path_sortedE filter_all/=.
  by apply: sorted_filter => //; exact: lt_trans.
exact/eqP/(path_lt_last_filter ac).
Qed.

Lemma in_itv_partition c s : sorted <%O s -> c \in s ->
  s = itv_partitionL s c ++ itv_partitionR s c.

Proof.

elim: s c => // h t ih c /= ht.
rewrite inE => /predU1P[->{c}/=|ct].
  rewrite ltxx /itv_partitionL /= ltxx /itv_partitionR/= path_lt_filter0//=.
  by rewrite path_lt_filterT.
rewrite /itv_partitionL/=; case: ifPn => [hc|].
  by rewrite ltNge (ltW hc)/= /= [in LHS](ih _ _ ct)//; exact: path_sorted ht.
rewrite -leNgt le_eqVlt => /predU1P[ch|ch].
  by rewrite ch ltxx path_lt_filter0//= /itv_partitionR path_lt_filterT.
move: ht; rewrite lt_path_sortedE => /andP[/allP/(_ _ ct)].
by move=> /lt_trans-/(_ _ ch); rewrite ltxx.
Qed.

Lemma notin_itv_partition c s : sorted <%O s -> c \notin s ->
  s = [seq x <- s | (x < c)%O] ++ itv_partitionR s c.

Proof.

elim: s c => // h t ih c /= ht.
rewrite inE negb_or => /andP[]; rewrite neq_lt => /orP[ch|ch] ct.
  rewrite ch ltNge (ltW ch)/= path_lt_filter0/= /itv_partitionR; last first.
    exact: path_lt_head ht.
  by rewrite path_lt_filterT//; exact: path_lt_head ht.
by rewrite ch/= ltNge (ltW ch)/= -ih//; exact: path_sorted ht.
Qed.

End interval_partition_orderType.

Section interval_partition_numDomainType.
Context {R : numDomainType}.
Implicit Type (a b : R) (s : seq R).

Lemma nonincreasing_fun_itv_partition a b f s :
  {in `[a, b] &, nonincreasing_fun f} -> itv_partition a b s ->
  let F : nat -> R := f \o nth b (a :: s) in
  forall k, (k < size s)%N -> (F k.+1 <= F k)%O.

Proof.

move/nonincreasing_funN => ndNf abs F k ks; rewrite -(opprK (F k)) lerNr.
exact: (nondecreasing_fun_itv_partition ndNf abs).
Qed.

Lemma itv_partition_rev a b s : itv_partition a b s ->
  itv_partition (- b) (- a) (rev (belast (- a) (map -%R s))).

Proof.

move=> [sa /eqP alb]; split.
  rewrite (_ : - b = last (- a) (map -%R s)); last by rewrite last_map alb.
  rewrite rev_path// path_map.
  by apply: sub_path sa => x y xy/=; rewrite ltrNr opprK.
case: s sa alb => [_ <-//|h t] /= /andP[ah ht] <-{b}.
by rewrite rev_cons last_rcons.
Qed.

End interval_partition_numDomainType.

Section variation_numDomainType.
Context {R : numDomainType}.
Implicit Types (a b : R) (f g : R -> R).

Definition variation a b f s := let F := f \o nth b (a :: s) in
  \sum_(0 <= n < size s) `|F n.+1 - F n|%R.

Lemma variation_zip a b f s : itv_partition a b s ->
  variation a b f s = \sum_(x <- zip s (a :: s)) `|f x.1 - f x.2|.

Proof.

elim: s a b => // [a b|h t ih a b].
  by rewrite /itv_partition /= => -[_ /eqP <-]; rewrite /variation/= !big_nil.
rewrite /itv_partition /variation => -[]/= /andP[ah ht] /eqP htb.
rewrite big_nat_recl//= big_cons/=; congr +%R.
have /ih : itv_partition h b t by split => //; exact/eqP.
by rewrite /variation => ->; rewrite !big_seq; apply/eq_bigr => r rt.
Qed.

Lemma variation_prev a b f s : itv_partition a b s ->
  variation a b f s = \sum_(x <- s) `|f x - f (prev (locked (a :: s)) x)|.

Proof.

move=> [] sa /eqP asb; rewrite /variation [in LHS]/= (big_nth b) !big_nat.
apply: eq_bigr => i /andP[_ si]; congr (`| _ - f _ |).
rewrite -lock.
rewrite prev_nth inE gt_eqF; last first.
  rewrite -[a]/(nth b (a :: s) 0) -[ltRHS]/(nth b (a :: s) i.+1).
  exact: lt_sorted_ltn_nth.
rewrite orFb mem_nth// index_uniq//.
  by apply: set_nth_default => /=; rewrite ltnS ltnW.
by apply: (sorted_uniq lt_trans) => //; apply: path_sorted sa.
Qed.

Lemma variation_next a b f s : itv_partition a b s ->
  variation a b f s =
  \sum_(x <- belast a s) `|f (next (locked (a :: s)) x) - f x|.

Proof.

move=> [] sa /eqP asb; rewrite /variation [in LHS]/= (big_nth b) !big_nat.
rewrite size_belast; apply: eq_bigr => i /andP[_ si].
congr (`| f _ - f _ |); last first.
  by rewrite lastI -cats1 nth_cat size_belast// si.
rewrite -lock next_nth.
rewrite {1}lastI mem_rcons inE mem_nth ?size_belast// orbT.
rewrite lastI -cats1 index_cat mem_nth ?size_belast//.
rewrite index_uniq ?size_belast//.
  exact: set_nth_default.
have /lt_sorted_uniq : sorted <%R (a :: s) by [].
by rewrite lastI rcons_uniq => /andP[].
Qed.

Lemma variation_nil a b f : variation a b f [::] = 0.

Proof.

by rewrite /variation/= big_nil. Qed.

Lemma variation_ge0 a b f s : 0 <= variation a b f s.

Proof.

exact/sumr_ge0. Qed.

Lemma variationN a b f s : variation a b (\- f) s = variation a b f s.

Proof.

by rewrite /variation; apply: eq_bigr => k _ /=; rewrite -opprD normrN.
Qed.

Lemma variation_le a b f g s :
  variation a b (f \+ g)%R s <= variation a b f s + variation a b g s.

Proof.

rewrite [in leRHS]/variation -big_split/=.
apply: ler_sum => k _; apply: le_trans; last exact: ler_normD.
by rewrite /= addrACA -opprD.
Qed.

Lemma nondecreasing_variation a b f s : {in `[a, b] &, nondecreasing_fun f} ->
  itv_partition a b s -> variation a b f s = f b - f a.

Proof.

move=> ndf abs; rewrite /variation; set F : nat -> R := f \o nth _ (a :: s).
transitivity (\sum_(0 <= n < size s) (F n.+1 - F n)).
  rewrite !big_nat; apply: eq_bigr => k; rewrite leq0n/= => ks.
  by rewrite ger0_norm// subr_ge0; exact: nondecreasing_fun_itv_partition.
by rewrite telescope_sumr// /F/= (itv_partition_nth_size _ abs).
Qed.

Lemma nonincreasing_variation a b f s : {in `[a, b] &, nonincreasing_fun f} ->
  itv_partition a b s -> variation a b f s = f a - f b.

Proof.

move=> /nonincreasing_funN ndNf abs; have := nondecreasing_variation ndNf abs.
by rewrite opprK addrC => <-; rewrite variationN.
Qed.

Lemma variation_cat c a b f s t : a <= c -> c <= b ->
  itv_partition a c s -> itv_partition c b t ->
  variation a b f (s ++ t) = variation a c f s + variation c b f t.

Proof.

rewrite le_eqVlt => /predU1P[<-{c} cb|ac].
  by move=> /itv_partitionxx ->; rewrite variation_nil add0r.
rewrite le_eqVlt => /predU1P[<-{b}|cb].
  by move=> ? /itv_partitionxx ->; rewrite variation_nil addr0 cats0.
move=> acs cbt; rewrite /variation /= [in LHS]/index_iota subn0 size_cat.
rewrite iotaD add0n big_cat/= -[in X in X + _ = _](subn0 (size s)); congr +%R.
  rewrite -/(index_iota 0 (size s)) 2!big_nat.
  apply: eq_bigr => k /[!leq0n] /= ks.
  rewrite nth_cat ks -cat_cons nth_cat /= ltnS (ltnW ks).
  by rewrite !(set_nth_default b c)//= ltnS ltnW.
rewrite -[in LHS](addnK (size s) (size t)).
rewrite -/(index_iota (size s) (size t + size s)).
rewrite -{1}[in LHS](add0n (size s)) big_addn addnK 2!big_nat; apply: eq_bigr.
move=> k /[!leq0n]/= kt.
rewrite nth_cat {1}(addnC k) -ltn_subRL subnn ltn0 addnK.
case: k kt => [t0 /=|k kt].
  rewrite add0n -cat_cons nth_cat/= ltnS leqnn -last_nth.
  by case: acs => _ /eqP ->.
rewrite addSnnS (addnC k) -cat_cons nth_cat/= -ltn_subRL subnn ltn0.
by rewrite -(addnC k) addnK.
Qed.

Lemma le_variation a b f s x : variation a b f s <= variation a b f (x :: s).

Proof.

case: s => [|h t].
  by rewrite variation_nil /variation/= big_nat_recl//= big_nil addr0.
rewrite /variation/= !big_nat_recl//= addrA lerD2r.
by rewrite -(subrKA (f x)) addrC ler_normD.
Qed.

Lemma variation_opp_rev a b f s : itv_partition a b s ->
  variation a b f s =
  variation (- b) (- a) (f \o -%R) (rev (belast (- a) (map -%R s))).

Proof.

move=> abl; rewrite belast_map /variation /= [LHS]big_nat_rev/= add0n.
rewrite size_rev size_map size_belast 2!big_nat.
apply: eq_bigr => k; rewrite leq0n /= => ks.
rewrite nth_rev ?size_map ?size_belast// [in RHS]distrC.
rewrite (nth_map a); last first.
  by rewrite size_belast ltn_subLR// addSn ltnS leq_addl.
rewrite opprK -rev_rcons nth_rev ?size_rcons ?size_map ?size_belast 1?ltnW//.
rewrite subSn// -map_rcons (nth_map b) ?size_rcons ?size_belast; last first.
  by rewrite ltnS ltn_subLR// addSn ltnS leq_addl.
rewrite opprK nth_rcons size_belast -subSn// subSS.
rewrite (ltn_subLR _ (ltnW ks)) if_same.
case: k => [|k] in ks *.
  rewrite add0n ltnn subn1 (_ : nth b s _ = b); last first.
    case: abl ks => _.
    elim/last_ind : s => // h t _; rewrite last_rcons => /eqP -> _.
    by rewrite nth_rcons size_rcons ltnn eqxx.
  rewrite (_ : nth b (a :: s) _ = nth a (belast a s) (size s).-1)//.
  case: abl ks => _.
  elim/last_ind : s => // h t _; rewrite last_rcons => /eqP -> _.
  rewrite belast_rcons size_rcons/= -rcons_cons nth_rcons/= ltnS leqnn.
  exact: set_nth_default.
rewrite addSn ltnS leq_addl//; congr (`| f _ - f _ |).
  elim/last_ind : s ks {abl} => // h t _; rewrite size_rcons ltnS => kh.
  rewrite belast_rcons nth_rcons subSS ltn_subLR//.
  by rewrite addSn ltnS leq_addl// subSn.
elim/last_ind : s ks {abl} => // h t _; rewrite size_rcons ltnS => kh.
rewrite belast_rcons subSS -rcons_cons nth_rcons /= ltn_subLR//.
rewrite addnS ltnS leq_addl; apply: set_nth_default => //.
by rewrite /= ltnS leq_subLR leq_addl.
Qed.

Lemma variation_rev_opp a b f s : itv_partition (- b) (- a) s ->
  variation a b f (rev (belast b (map -%R s))) =
  variation (- b) (- a) (f \o -%R) s.

Proof.

move=> abs; rewrite [in RHS]variation_opp_rev ?opprK//.
suff: (f \o -%R) \o -%R = f by move=> ->.
by apply/funext=> ? /=; rewrite opprK.
Qed.

End variation_numDomainType.
#[deprecated(since="mathcomp-analysis 1.12.0", note="use `variation_cat` instead")]
Notation variationD := variation_cat (only parsing).

Section variation_realDomainType.
Context {R : realDomainType}.
Implicit Types (a b : R) (f g : R -> R).

Lemma variation_itv_partitionLR a b c f s : a < c -> c < b ->
  itv_partition a b s ->
  variation a b f s <= variation a b f (itv_partitionL s c ++ itv_partitionR s c).

Proof.

move=> ac bc abs; have [cl|cl] := boolP (c \in s).
  by rewrite -in_itv_partition//; case: abs => /path_sorted.
rewrite /itv_partitionL [in leLHS](notin_itv_partition _ cl)//; last first.
  by apply: path_sorted; case: abs => + _; exact.
rewrite -notin_itv_partition//; last first.
  by apply: path_sorted; case: abs => /= + _; exact.
rewrite !variation_zip//; last first.
  by apply: itv_partition_cat;
    [exact: (itv_partitionLP _ bc)|exact: (itv_partitionRP ac)].
rewrite [in leLHS](notin_itv_partition _ cl); last first.
  by apply: path_sorted; case: abs => + _; exact.
set L := [seq x <- s | x < c].
rewrite -cats1 -catA.
move: L => L.
set B := itv_partitionR s c.
move: B => B.
elim/last_ind : L => [|L0 L1 _].
  rewrite !cat0s /=; case: B => [|B0 B1].
    by rewrite big_nil big_cons/= big_nil addr0.
  by rewrite !big_cons/= addrA lerD// -(subrKA (f c)) [leRHS]addrC ler_normD.
rewrite -cats1.
rewrite (_ : a :: _ ++ B = (a :: L0) ++ [:: L1] ++ B)//; last first.
  by rewrite -!catA -cat_cons.
rewrite zip_cat; last by rewrite cats1 size_rcons.
rewrite (_ : a :: _ ++ _ ++ B = (a :: L0) ++ [:: L1] ++ [:: c] ++ B); last first.
  by rewrite -!catA -cat_cons.
rewrite zip_cat; last by rewrite cats1 size_rcons.
rewrite !big_cat lerD//.
case: B => [|B0 B1].
  by rewrite /= big_nil big_cons big_nil addr0.
rewrite -cat1s zip_cat// catA.
rewrite (_ : [:: L1] ++ _ ++ B1 = ([:: L1] ++ [:: c]) ++ [:: B0] ++ B1); last first.
  by rewrite catA.
rewrite zip_cat// !big_cat lerD//= !big_cons !big_nil !addr0/= [leRHS]addrC.
by rewrite (le_trans _ (ler_normD _ _))// subrKA.
Qed.

Lemma variation_subseq a b f (s t : list R) :
  itv_partition a b s -> itv_partition a b t ->
  subseq s t ->
  variation a b f s <= variation a b f t.

Proof.

elim: t s a => [? ? ? /= _ /eqP ->//|a s IH [|x t] w].
  by rewrite variation_nil // variation_ge0.
move=> /[dup] /itv_partition_cons itvxb /[dup] /itv_partition_le wb itvxt.
move=> /[dup] /itv_partition_cons itvas itvws /=.
have ab : a <= b by exact: (itv_partition_le itvas).
have wa : w < a by case: itvws => /= /andP[].
have waW : w <= a := ltW wa.
case: ifPn => [|] nXA.
  move/eqP : nXA itvxt itvxb => -> itvat itvt /= ta.
  rewrite -[_ :: t]cat1s -[_ :: s]cat1s.
  rewrite ?(@variation_cat _ a)//; [|exact: itv_partition1..].
  by rewrite lerD// IH.
move=> xts; rewrite -[_ :: s]cat1s (@variation_cat _ a) => //; last first.
  exact: itv_partition1.
have [y [s' s'E]] : exists y s', s = y :: s'.
  by case: {itvas itvws IH} s xts => // y s' ?; exists y, s'.
apply: (@le_trans _ _ (variation w b f s)).
  rewrite IH//.
  case: itvws => /= /andP[_]; rewrite s'E /= => /andP[ay ys' lyb].
  by split => //; rewrite (path_lt_head wa)//= ys' andbT.
by rewrite -variation_cat//; [exact: le_variation | exact: itv_partition1].
Qed.

End variation_realDomainType.

Section bounded_variation.
Context {R : numDomainType}.
Implicit Type (a b : R) (f : R -> R).

Definition variations a b f := [set variation a b f l | l in itv_partition a b].

Lemma variations_variation a b f s : itv_partition a b s ->
  variations a b f (variation a b f s).

Proof.

by move=> abs; exists s. Qed.

Lemma variations_neq0 a b f : a < b -> variations a b f !=set0.

Proof.

move=> ab; exists (variation a b f [:: b]); exists [:: b] => //.
exact: itv_partition1.
Qed.

Lemma variationsN a b f : variations a b (\- f) = variations a b f.

Proof.

apply/seteqP; split => [_ [s abs] <-|r [s abs]].
  by rewrite variationN; exact: variations_variation.
by rewrite -variationN => <-; exact: variations_variation.
Qed.

Lemma variationsxx a f : variations a a f = [set 0].

Proof.

apply/seteqP; split => [x [_ /itv_partitionxx ->]|x ->].
  by rewrite /variation big_nil => <-.
by exists [::] => //=; rewrite /variation /= big_nil.
Qed.

Definition bounded_variation a b f := has_ubound (variations a b f).

Notation BV := bounded_variation.

Lemma bounded_variationxx a f : BV a a f.

Proof.

by exists 0 => r; rewrite variationsxx => ->. Qed.

Lemma bounded_variationD a b f g : a < b ->
  BV a b f -> BV a b g -> BV a b (f \+ g).

Proof.

move=> ab [r abfr] [s abgs]; exists (r + s) => _ [l abl] <-.
apply: le_trans; first exact: variation_le.
rewrite lerD//.
- by apply: abfr; exact: variations_variation.
- by apply: abgs; exact: variations_variation.
Qed.

Lemma bounded_variationN a b f : BV a b f -> BV a b (\- f).

Proof.

by rewrite /bounded_variation variationsN. Qed.

Lemma bounded_variationl a c b f : a <= c -> c <= b -> BV a b f -> BV a c f.

Proof.

rewrite le_eqVlt => /predU1P[<-{c} ? ?|ac]; first exact: bounded_variationxx.
rewrite le_eqVlt => /predU1P[<-{b}//|cb].
move=> [x Hx]; exists x => _ [s acs] <-.
rewrite (@le_trans _ _ (variation a b f (rcons s b)))//; last first.
  apply/Hx/variations_variation; case: acs => sa /eqP asc.
  by rewrite /itv_partition rcons_path last_rcons sa/= asc.
rewrite {2}/variation size_rcons -[leLHS]addr0 big_nat_recr//= lerD//.
rewrite /variation !big_nat ler_sum// => k; rewrite leq0n /= => ks.
rewrite nth_rcons// ks -cats1 -cat_cons nth_cat /= ltnS (ltnW ks).
by rewrite //= ltnS ltnW.
Qed.

Lemma bounded_variationr a c b f : a <= c -> c <= b -> BV a b f -> BV c b f.

Proof.

rewrite le_eqVlt => /predU1P[<-{c}//|ac].
rewrite le_eqVlt => /predU1P[<-{b} ?|cb]; first exact: bounded_variationxx.
move=> [x Hx]; exists x => _ [s cbs] <-.
rewrite (@le_trans _ _ (variation a b f (c :: s)))//; last first.
  apply/Hx/variations_variation; case: cbs => cs csb.
  by rewrite /itv_partition/= ac/= cs.
by rewrite {2}/variation/= -[leLHS]add0r big_nat_recl//= lerD.
Qed.

Lemma variations_opp a b f :
  variations (- b) (- a) (f \o -%R) = variations a b f.

Proof.

rewrite eqEsubset; split=> [_ [s bas <-]| _ [s abs <-]].
  eexists; last exact: variation_rev_opp.
  by move/itv_partition_rev : bas; rewrite !opprK.
eexists; last by exact/esym/variation_opp_rev.
exact: itv_partition_rev abs.
Qed.

Lemma nondecreasing_bounded_variation a b f :
  {in `[a, b] &, {homo f : x y / x <= y}} -> BV a b f.

Proof.

move=> incf; exists (f b - f a) => ? [l pabl <-]; rewrite le_eqVlt.
by rewrite nondecreasing_variation// eqxx.
Qed.

End bounded_variation.

HB.mixin Record isNonNegFun (aT : Type) (rT : numDomainType) (f : aT -> rT) := {
  fun_ge0 : forall x, (0 <= f x)%R
}.
HB.structure Definition NonNegFun aT rT := {f of @isNonNegFun aT rT f}.
Notation "{ 'nnfun' aT >-> T }" := (@NonNegFun.type aT T) : form_scope.
Notation "[ 'nnfun' 'of' f ]" := [the {nnfun _ >-> _} of f] : form_scope.
#[global] Hint Extern 0 (is_true (0 <= _)) => solve [apply: fun_ge0] : core.

Section fimfun_bin.
Context (T : Type) (R : numDomainType).
Variables f g : {fimfun T >-> R}.

Lemma max_fimfun_subproof : @FiniteImage T R (f \max g).

Proof.

by split; apply: (finite_image11 Num.max). Qed.

HB.instance Definition _ := max_fimfun_subproof.

End fimfun_bin.

Reserved Notation "f ^\+" (at level 1, format "f ^\+").
Reserved Notation "f ^\-" (at level 1, format "f ^\-").

Section restrict_lemmas.
Context {aT : Type} {rT : numFieldType}.
Implicit Types (f g : aT -> rT) (D : set aT).

Lemma restrict_set0 f : f \_ set0 = cst 0.

Proof.

by rewrite patch_set0. Qed.

Lemma restrict_ge0 D f :
  (forall x, D x -> 0 <= f x) -> forall x, 0 <= (f \_ D) x.

Proof.

by move=> f0 x; rewrite /patch; case: ifP => // /set_mem/f0->. Qed.

Lemma ler_restrict D f g :
  (forall x, D x -> f x <= g x) -> forall x, (f \_ D) x <= (g \_ D) x.

Proof.

by move=> f0 x; rewrite /patch; case: ifP => // /set_mem/f0->. Qed.

Lemma restrict_normr D f : (Num.norm \o f) \_ D = Num.norm \o (f \_ D).

Proof.

by apply/funext => t; rewrite /= !patchE; case: ifPn =>// tD; rewrite ger0_norm.
Qed.

End restrict_lemmas.

Lemma erestrict_ge0 {aT} {rT : numFieldType} (D : set aT) (f : aT -> \bar rT) :
  (forall x, D x -> (0 <= f x)%E) -> forall x, (0 <= (f \_ D) x)%E.

Proof.

by move=> f0 x; rewrite /patch; case: ifP => // /set_mem/f0->. Qed.

Lemma lee_restrict {aT} {rT : numFieldType} (D : set aT) (f g : aT -> \bar rT) :
  (forall x, D x -> f x <= g x)%E -> forall x, ((f \_ D) x <= (g \_ D) x)%E.

Proof.

by move=> f0 x; rewrite /patch; case: ifP => // /set_mem/f0->. Qed.

Lemma restrict_lee {aT} {rT : numFieldType} (D E : set aT) (f : aT -> \bar rT) :
  (forall x, E x -> 0 <= f x)%E ->
  D `<=` E -> forall x, ((f \_ D) x <= (f \_ E) x)%E.

Proof.

move=> f0 ED x; rewrite /restrict; case: ifPn => [xD|xD].
  by rewrite mem_set//; apply: ED; rewrite in_setE in xD.
by case: ifPn => // xE; apply: f0; rewrite in_setE in xE.
Qed.

Section erestrict_lemmas.
Local Open Scope ereal_scope.
Variables (T : Type) (R : realDomainType) (D : set T).
Implicit Types (f g : T -> \bar R) (r : R).

Lemma erestrict_set0 f : f \_ set0 = cst 0.

Proof.

by rewrite patch_set0. Qed.

Lemma erestrict0 : (cst 0 : T -> \bar R) \_ D = cst 0.

Proof.

by apply/funext => x; rewrite /patch/=; case: ifP. Qed.

Lemma erestrictD f g : (f \+ g) \_ D = f \_ D \+ g \_ D.

Proof.

by apply/funext=> x; rewrite /patch/=; case: ifP; rewrite ?adde0. Qed.

Lemma erestrictN f : (\- f) \_ D = \- f \_ D.

Proof.

by apply/funext=> x; rewrite /patch/=; case: ifP; rewrite ?oppe0. Qed.

Lemma erestrictB f g : (f \- g) \_ D = f \_ D \- g \_ D.

Proof.

by apply/funext=> x; rewrite /patch/=; case: ifP; rewrite ?sube0. Qed.

Lemma erestrictM f g : (f \* g) \_ D = f \_ D \* g \_ D.

Proof.

by apply/funext=> x; rewrite /patch/=; case: ifP; rewrite ?mule0. Qed.

Lemma erestrict_scale k f :
  (fun x => k%:E * f x) \_ D = (fun x => k%:E * (f \_ D) x).

Proof.

by apply/funext=> x; rewrite /patch/=; case: ifP; rewrite ?mule0. Qed.

End erestrict_lemmas.

HB.lock
Definition funepos T (R : realDomainType) (f : T -> \bar R) :=
  fun x => maxe (f x) 0.
HB.lock
Definition funeneg T (R : realDomainType) (f : T -> \bar R) :=
  fun x => maxe (oppe (f x)) 0.

Notation "f ^\+" := (funepos f) : ereal_scope.
Notation "f ^\-" := (funeneg f) : ereal_scope.

Section funposneg_lemmas.
Local Open Scope ereal_scope.
Variables (T U : Type) (R : realDomainType) (D : set T).
Implicit Types (f g : T -> \bar R) (h : U -> T) (r : R).

Lemma funeposE f x : f^\+ x = maxe (f x) 0.

Proof.

by rewrite unlock. Qed.

Lemma funenegE f x : f^\- x = maxe (- f x) 0.

Proof.

by rewrite unlock. Qed.

Lemma funepos_ge0 f x : 0 <= f^\+ x.

Proof.

by rewrite funeposE le_max lexx orbT. Qed.

Lemma funeneg_ge0 f x : 0 <= f^\- x.

Proof.

by rewrite funenegE le_max lexx orbT. Qed.

Lemma funeposN f : (\- f)^\+ = f^\-.

Proof.

by apply/funext => x; rewrite funeposE funenegE. Qed.

Lemma funenegN f : (\- f)^\- = f^\+.

Proof.

by apply/funext => x; rewrite funeposE funenegE oppeK. Qed.

Lemma funepos_comp f h : (f \o h)^\+ = f^\+ \o h.

Proof.

by rewrite !unlock. Qed.

Lemma funeneg_comp f h : (f \o h)^\- = f^\- \o h.

Proof.

by rewrite !unlock. Qed.

Lemma funepos_restrict f : (f \_ D)^\+ = (f^\+) \_ D.

Proof.

by apply/funext => x; rewrite /patch !funeposE; case: ifP; rewrite //= maxxx.
Qed.

Lemma funeneg_restrict f : (f \_ D)^\- = (f^\-) \_ D.

Proof.

apply/funext => x; rewrite /patch !funenegE.
by case: ifP; rewrite //= oppr0 maxxx.
Qed.

Lemma ge0_funeposE f : (forall x, D x -> 0 <= f x) -> {in D, f^\+ =1 f}.

Proof.

by move=> f0 x; rewrite inE funeposE => Dx; apply/max_idPl/f0. Qed.

Lemma ge0_funenegE f : (forall x, D x -> 0 <= f x) -> {in D, f^\- =1 cst 0}.

Proof.

move=> f0 x; rewrite inE funenegE => Dx; apply/max_idPr.
by rewrite leeNl oppe0 f0.
Qed.

Lemma le0_funeposE f : (forall x, D x -> f x <= 0) -> {in D, f^\+ =1 cst 0}.

Proof.

by move=> f0 x; rewrite inE funeposE => Dx; exact/max_idPr/f0. Qed.

Lemma le0_funenegE f : (forall x, D x -> f x <= 0) -> {in D, f^\- =1 \- f}.

Proof.

move=> f0 x; rewrite inE funenegE => Dx; apply/max_idPl.
by rewrite leeNr oppe0 f0.
Qed.

Lemma ge0_funeposM r f : (0 <= r)%R ->
  (fun x => r%:E * f x)^\+ = (fun x => r%:E * (f^\+ x)).

Proof.

move=> ?; rewrite funeqE => x.
by rewrite !funeposE maxe_pMr// mule0.
Qed.

Lemma ge0_funenegM r f : (0 <= r)%R ->
  (fun x => r%:E * f x)^\- = (fun x => r%:E * (f^\- x)).

Proof.

by move=> r0; rewrite funeqE => x; rewrite !funenegE -muleN maxe_pMr// mule0.
Qed.

Lemma le0_funeposM r f : (r <= 0)%R ->
  (fun x => r%:E * f x)^\+ = (fun x => - r%:E * (f^\- x)).

Proof.

move=> r0; rewrite -[in LHS](opprK r); under eq_fun do rewrite EFinN mulNe.
by rewrite funeposN ge0_funenegM ?oppr_ge0.
Qed.

Lemma le0_funenegM r f : (r <= 0)%R ->
  (fun x => r%:E * f x)^\- = (fun x => - r%:E * (f^\+ x)).

Proof.

move=> r0; rewrite -[in LHS](opprK r); under eq_fun do rewrite EFinN mulNe.
by rewrite funenegN ge0_funeposM ?oppr_ge0.
Qed.

Lemma fune_abse f : abse \o f = f^\+ \+ f^\-.

Proof.

rewrite funeqE => x /=; have [fx0|/ltW fx0] := leP (f x) 0.
- rewrite lee0_abs// funeposE funenegE.
  move/max_idPr : (fx0) => ->; rewrite add0e.
  by move: fx0; rewrite -{1}oppe0 leeNr => /max_idPl ->.
- rewrite gee0_abs// funeposE funenegE; move/max_idPl : (fx0) => ->.
  by move: fx0; rewrite -{1}oppe0 leeNl => /max_idPr ->; rewrite adde0.
Qed.

Lemma funeposneg f : f = (fun x => f^\+ x - f^\- x).

Proof.

rewrite funeqE => x; rewrite funeposE funenegE; have [|/ltW] := leP (f x) 0.
  by rewrite -{1}oppe0 -leeNr => /max_idPl ->; rewrite oppeK add0e.
by rewrite -{1}oppe0 -leeNl => /max_idPr ->; rewrite sube0.
Qed.

Lemma add_def_funeposneg f x : (f^\+ x +? - f^\- x).

Proof.

by rewrite funenegE funeposE; case: (f x) => [r| |];
  [rewrite -fine_max/=|rewrite /maxe /= ltNyr|rewrite /maxe /= ltNyr].
Qed.

Lemma funeD_Dpos f g : f \+ g = (f \+ g)^\+ \- (f \+ g)^\-.

Proof.

apply/funext => x; rewrite funeposE funenegE; have [|/ltW] := leP 0 (f x + g x).
- by rewrite -{1}oppe0 -leeNl => /max_idPr ->; rewrite sube0.
- by rewrite -{1}oppe0 -leeNr => /max_idPl ->; rewrite oppeK add0e.
Qed.

Lemma funeD_posD f g : f \+ g = (f^\+ \+ g^\+) \- (f^\- \+ g^\-).

Proof.

apply/funext => x; rewrite !funeposE !funenegE.
have [|fx0] := leP 0 (f x); last rewrite add0e.
- rewrite -{1}oppe0 leeNl => /max_idPr ->; have [|/ltW] := leP 0 (g x).
    by rewrite -{1}oppe0 leeNl => /max_idPr ->; rewrite adde0 sube0.
  by rewrite -{1}oppe0 -leeNr => /max_idPl ->; rewrite adde0 sub0e oppeK.
- move/ltW : (fx0); rewrite -{1}oppe0 leeNr => /max_idPl ->.
  have [|] := leP 0 (g x); last rewrite add0e.
    by rewrite -{1}oppe0 leeNl => /max_idPr ->; rewrite adde0 oppeK addeC.
  move gg' : (g x) => g'; move: g' gg' => [g' gg' g'0|//|goo _].
  + move/ltW : (g'0); rewrite -{1}oppe0 -leeNr => /max_idPl => ->.
    by rewrite fin_num_oppeD// 2!oppeK.
  + by rewrite /maxe /=; case: (f x) fx0.
Qed.

Lemma funepos_le f g :
  {in D, forall x, f x <= g x} -> {in D, forall x, f^\+ x <= g^\+ x}.

Proof.

move=> fg x Dx; rewrite !funeposE /maxe; case: ifPn => fx; case: ifPn => gx //.
- by rewrite leNgt.
- by move: fx; rewrite -leNgt => /(lt_le_trans gx); rewrite ltNge fg.
- exact: fg.
Qed.

Lemma funeneg_le f g :
  {in D, forall x, f x <= g x} -> {in D, forall x, g^\- x <= f^\- x}.

Proof.

move=> fg x Dx; rewrite !funenegE /maxe; case: ifPn => gx; case: ifPn => fx //.
- by rewrite leNgt.
- by move: gx; rewrite -leNgt => /(lt_le_trans fx); rewrite lteN2 ltNge fg.
- by rewrite leeN2; exact: fg.
Qed.

End funposneg_lemmas.
#[global]
Hint Extern 0 (is_true (0%R <= _ ^\+ _)%E) => solve [apply: funepos_ge0] : core.
#[global]
Hint Extern 0 (is_true (0%R <= _ ^\- _)%E) => solve [apply: funeneg_ge0] : core.

Definition indic {T} {R : pzRingType} (A : set T) (x : T) : R := (x \in A)%:R.
Reserved Notation "'\1_' A" (at level 8, A at level 2, format "'\1_' A") .
Notation "'\1_' A" := (indic A) : ring_scope.

Lemma num_spec_indic {T} {R : numDomainType} (A : set T) (x : T) :
  Itv.spec (@Itv.num_sem R) (Itv.Real `[0, 1]%Z) (indic A x).

Proof.

apply/and3P; split; rewrite ?realn// bnd_simp ?mulrn_wge0//.
by rewrite -pmulrn ler_nat leq_b1.
Qed.

Canonical indic_inum {T} {R : numDomainType} (A : set T) (x : T) :=
  Itv.mk (@num_spec_indic T R A x).

Section indic_ringType.
Context (T : Type) (R : pzRingType).
Implicit Types A D : set T.

Lemma indicE A (x : T) : \1_A x = (x \in A)%:R :> R

Proof.

by []. Qed.

Lemma indicT : \1_[set: T] = cst (1 : R).

Proof.

by apply/funext=> x; rewrite indicE in_setT. Qed.

Lemma indic0 : \1_(@set0 T) = cst (0 : R).

Proof.

by apply/funext=> x; rewrite indicE in_set0. Qed.

Lemma indicI A B : \1_(A `&` B) = \1_A \* \1_B :> (_ -> R).

Proof.

by apply/funext=> u/=; rewrite !indicE in_setI -natrM mulnb. Qed.

Lemma indicC A : \1_(~` A) = (fun x => (~~ (x \in A))%:R) :> (_ -> R).

Proof.

by apply/funext=> u/=; rewrite indicE in_setC. Qed.

Lemma image_indic D A :
  \1_D @` A = (if A `\` D != set0 then [set 0] else set0) `|`
              (if A `&` D != set0 then [set 1 : R] else set0).

Proof.

rewrite /indic; apply/predeqP => x; split => [[t At /= <-]|].
  by rewrite /indic; case: (boolP (t \in D)); rewrite ?(inE, notin_setE) => Dt;
     [right|left]; rewrite ifT//=; apply/set0P; exists t.
by move=> []; case: ifPn; rewrite ?negbK// => /set0P[t [At Dt]] ->;
   exists t => //; case: (boolP (t \in D)); rewrite ?(inE, notin_setE).
Qed.

Lemma preimage_indic (D : set T) (B : set R) :
  \1_D @^-1` B = if 1 \in B then (if 0 \in B then setT else D)
                            else (if 0 \in B then ~` D else set0).

Proof.

rewrite /preimage/= /indic; apply/seteqP; split => x;
  case: ifPn => B1; case: ifPn => B0 //=.
- have [|] := boolP (x \in D); first by rewrite inE.
  by rewrite notin_setE in B0.
- have [|] := boolP (x \in D); last by rewrite notin_setE.
  by rewrite notin_setE in B1.
- by have [xD|xD] := boolP (x \in D);
    [rewrite notin_setE in B1|rewrite notin_setE in B0].
- by have [xD|xD] := boolP (x \in D); [rewrite inE in B1|rewrite inE in B0].
- have [xD|] := boolP (x \in D); last by rewrite notin_setE.
  by rewrite inE in B1.
- have [|xD] := boolP (x \in D); first by rewrite inE.
  by rewrite inE in B0.
Qed.

Lemma image_indic_sub D A : \1_D @` A `<=` ([set 0; 1] : set R).

Proof.

by rewrite image_indic; do ![case: ifP=> //= _] => // t []//= ->; [left|right].
Qed.

Lemma fimfunE (f : {fimfun T >-> R}) x :
  f x = \sum_(y \in range f) (y * \1_(f @^-1` [set y]) x).

Proof.

rewrite (fsbigD1 (f x))// /= indicE mem_set// mulr1 fsbig1 ?addr0//.
by move=> y [fy /= /nesym yfx]; rewrite indicE memNset ?mulr0.
Qed.

Lemma fimfunEord (f : {fimfun T >-> R})
    (s := fset_set (f @` setT)) :
  forall x, f x = \sum_(i < #|`s|) (s`_i * \1_(f @^-1` [set s`_i]) x).

Proof.

move=> x; rewrite fimfunE fsbig_finite//= (big_nth 0)/= big_mkord.
exact: eq_bigr.
Qed.

End indic_ringType.

Lemma indic_bigcup T {R : realType} (A : (set T)^nat) (t : T) :
  trivIset [set: nat] A ->
  (\1_(\bigcup_n A n) t)%:E = (\sum_(0 <= n <oo) (\1_(A n) t)%:E)%E :> \bar R.

Proof.

move=> tA.
have [At|At] := eqVneq (\1_(\bigcup_n A n) t) (1%R : R).
- move: (At) => /eqP; rewrite pnatr_eq1 eqb1 => /asboolP[i _] Ait.
  rewrite At (@nneseriesD1 _ _ i)//.
  rewrite indicE mem_set// eseries0 ?adde0// => j _/= ji.
  rewrite indicE memNset// => Ajt.
  move/trivIsetP : tA => /(_ j i Logic.I Logic.I ji).
  by apply/eqP/set0P; exists t.
- have {}At : \1_(\bigcup_n A n) t = 0%R :> R.
    by apply/eqP; move: At; rewrite pnatr_eq1 eqb1 pnatr_eq0 eqb0.
  move: (At) => /eqP; rewrite pnatr_eq0 eqb0 notin_setE => AtC.
  rewrite At eseries0// => j _ _.
  by rewrite indicE memNset// => Ajt; apply: AtC; exists j.
Qed.

Lemma patch_indic T {R : numFieldType} (f : T -> R) (D : set T) :
  f \_ D = (f \* \1_D)%R.

Proof.

apply/funext => x /=; rewrite patchE /= indicE.
by case: ifPn => _; rewrite ?(mulr1, mulr0).
Qed.

Lemma epatch_indic T (R : numDomainType) (f : T -> \bar R) (D : set T) :
  (f \_ D = f \* (EFin \o \1_D))%E.

Proof.

apply/funext => x; rewrite patchE/= indicE.
by case: ifPn => /=; rewrite ?mule1// mule0.
Qed.

Lemma xsection_indic (R : nzRingType) T1 T2 (A : set (T1 * T2)) x :
  xsection A x = (fun y => (\1_A (x, y) : R)) @^-1` [set 1].

Proof.

apply/seteqP; split => [y/mem_set/=|y/=]; rewrite indicE.
  by rewrite mem_xsection => ->.
by rewrite /xsection/=; case: (_ \in _) => //= /esym/eqP /[!oner_eq0].
Qed.

Lemma ysection_indic (R : nzRingType) T1 T2 (A : set (T1 * T2)) y :
  ysection A y = (fun x => (\1_A (x, y) : R)) @^-1` [set 1].

Proof.

apply/seteqP; split => [x/mem_set/=|x/=]; rewrite indicE.
  by rewrite mem_ysection => ->.
by rewrite /ysection/=; case: (_ \in _) => //= /esym/eqP /[!oner_eq0].
Qed.

Lemma bounded_indic T {R : numFieldType} (A : set T) :
  [bounded \1_A x : R^o | x in A].

Proof.

by exists 1; split => // r r1 t At/=; rewrite indicE mem_set//= normr1 ltW.
Qed.

Lemma indic_restrict {T : pointedType} {R : numFieldType} (A : set T) :
  \1_A = (1 : T -> R) \_ A.

Proof.

by apply/funext => x; rewrite indicE /patch; case: ifP. Qed.

Lemma restrict_indic T (R : numFieldType) (E A : set T) :
  ((\1_E : T -> R) \_ A) = \1_(E `&` A).

Proof.

apply/funext => x; rewrite /restrict 2!indicE.
case: ifPn => [|] xA; first by rewrite in_setI xA andbT.
by rewrite in_setI (negbTE xA) andbF.
Qed.

Lemma cvg_indic {R : realFieldType} (x : R^o) k :
  x \in (ball 0 k : set R^o) ->
  \1_(ball 0 k : set R^o) y @[y --> x] --> (\1_(ball 0 k) x : R).

Proof.

move=> xB; apply/(@cvgrPdist_le _ R^o) => /= e e0; near=> t.
rewrite !indicE xB/= mem_set//=; first by rewrite subrr normr0// ltW.
near: t.
rewrite inE /ball /= sub0r normrN in xB.
exists ((k - `|x|)/2) => /=; first by rewrite divr_gt0// subr_gt0.
rewrite /ball_/= => z /= h; rewrite /ball/= sub0r normrN.
rewrite -(subrK x z) (le_lt_trans (ler_normD _ _))//.
rewrite -ltrBrDr distrC (lt_le_trans h)//.
by rewrite ler_pdivrMr//= ler_pMr// ?subr_gt0// ler1n.
Unshelve. all: by end_near. Qed.

Section ring.
Context (aT : pointedType) (rT : nzRingType).

Lemma fimfun_mulr_closed : mulr_closed (@fimfun aT rT).

Proof.

split=> [|f g]; rewrite !inE/=; first exact: finite_image_cst.
by move=> fA gA; exact: (finite_image11 (fun x y => x * y)).
Qed.

HB.instance Definition _ :=
   @GRing.isMulClosed.Build _ (@fimfun aT rT) fimfun_mulr_closed.
HB.instance Definition _ := [SubZmodule_isSubNzRing of {fimfun aT >-> rT} by <:].

Implicit Types f g : {fimfun aT >-> rT}.

Lemma fimfunM f g : f * g = f \* g :> (_ -> _)

Proof.

by []. Qed.

Lemma fimfun1 : (1 : {fimfun aT >-> rT}) = cst 1 :> (_ -> _)

Proof.

by []. Qed.

Lemma fimfun_prod I r (P : {pred I}) (f : I -> {fimfun aT >-> rT}) (x : aT) :
  (\sum_(i <- r | P i) f i) x = \sum_(i <- r | P i) f i x.

Proof.

by elim/big_rec2: _ => //= i y ? Pi <-. Qed.

Lemma fimfunX f n : f ^+ n = (fun x => f x ^+ n) :> (_ -> _).

Proof.

by apply/funext => x; elim: n => [|n IHn]//; rewrite !exprS fimfunM/= IHn.
Qed.

Lemma indic_fimfun_subproof X : @FiniteImage aT rT \1_X.

Proof.

split; apply: (finite_subfset [fset 0; 1]%fset) => x [tt /=].
by rewrite !inE indicE; case: (_ \in _) => _ <-; rewrite ?eqxx ?orbT.
Qed.

HB.instance Definition _ X := indic_fimfun_subproof X.

Definition indic_fimfun (X : set aT) : {fimfun aT >-> rT} := \1_X.

HB.instance Definition _ k f := FImFun.copy (k \o* f) (f * cst_fimfun k).

Definition scale_fimfun k f : {fimfun aT >-> rT} := k \o* f.

End ring.
Arguments indic_fimfun {aT rT} _.

Section comring.
Context (aT : pointedType) (rT : comNzRingType).
HB.instance Definition _ :=
  [SubNzRing_isSubComNzRing of {fimfun aT >-> rT} by <:].

Implicit Types (f g : {fimfun aT >-> rT}).
HB.instance Definition _ f g := FImFun.copy (f \* g) (f * g).
End comring.

HB.factory Record FiniteDecomp (T : pointedType) (R : nzRingType) (f : T -> R) :=
  { fimfunE : exists (r : seq R) (A_ : R -> set T),
      forall x, f x = \sum_(y <- r) (y * \1_(A_ y) x) }.
HB.builders Context T R f of @FiniteDecomp T R f.
  Lemma finite_subproof: @FiniteImage T R f.

  

Proof.

  split; have [r [A_ fE]] := fimfunE.
  suff -> : f = \sum_(y <- r) cst_fimfun y * indic_fimfun (A_ y) by [].
  by apply/funext=> x; rewrite fE fimfun_sum.
  Qed.

  HB.instance Definition _ := finite_subproof.
HB.end.

Section Tietze.
Context {X : topologicalType} {R : realType}.

Hypothesis normalX : normal_space X.

Lemma urysohn_ext_itv A B x y :
  closed A -> closed B -> A `&` B = set0 -> x < y ->
  exists f : X -> R, [/\ continuous f,
    f @` A `<=` [set x], f @` B `<=` [set y] & range f `<=` `[x, y]].

Proof.

move=> cA cB A0 xy; move/normal_separatorP : normalX => urysohn_ext.
have /(@uniform_separatorP _ R)[f [cf f01 f0 f1]] := urysohn_ext R _ _ cA cB A0.
pose g : X -> R := line_path x y \o f; exists g; split; rewrite /g /=.
  move=> t; apply: continuous_comp; first exact: cf.
  apply: (@continuousD R R^o).
    apply: continuousM; last exact: cvg_cst.
    by apply: (@continuousB R R^o) => //; exact: cvg_cst.
  by apply: continuousM; [exact: cvg_id|exact: cvg_cst].
- by rewrite -image_comp => z /= [? /f0 -> <-]; rewrite line_path0.
- by rewrite -image_comp => z /= [? /f1 -> <-]; rewrite line_path1.
- rewrite -image_comp; apply: (subset_trans (image_subset _ f01)).
  by rewrite range_line_path.
Qed.

Context (A : set X).
Hypothesis clA : closed A.

Local Lemma tietze_step' (f : X -> R) (M : R) :
  0 < M -> {within A, continuous f} ->
  (forall x, A x -> `|f x| <= M) ->
  exists g : X -> R, [/\ continuous g,
     (forall x, A x -> `|f x - g x| <= 2/3 * M) &
     (forall x, `|g x| <= 1/3 * M)].

Proof.

move: M => _/posnumP[M] ctsf fA1.
have [] := @urysohn_ext_itv (A `&` f @^-1` `]-oo, -(1/3) * M%:num])
    (A `&` f @^-1` `[1/3 * M%:num,+oo[) (-(1/3) * M%:num) (1/3 * M%:num).
- by rewrite closed_setSI//; exact: closed_comp.
- by rewrite closed_setSI//; apply: closed_comp => //; exact: interval_closed.
- rewrite setIACA -preimage_setI eqEsubset; split => z // [_ []].
  rewrite !set_itvE/= => /[swap] /le_trans /[apply].
  by rewrite leNgt mulNr gtrN// mulr_gt0// divr_gt0.
- by rewrite mulNr gtrN// mulr_gt0//.
move=> g [ctsg gL3 gR3 grng]; exists g; split => //; first last.
  by move=> x; rewrite ler_norml -mulNr; apply: grng; exists x.
move=> x Ax; have := fA1 _ Ax; rewrite 2!ler_norml => /andP[Mfx fxM].
have [xL|xL] := leP (f x) (-(1/3) * M%:num).
  have: [set g x | x in A `&` f@^-1` `]-oo, -(1/3) * M%:num]] (g x) by exists x.
  move/gL3=> ->; rewrite !mulNr opprK; apply/andP; split.
    by rewrite -lerBlDr -opprD -2!mulrDl natr1 divff// mul1r.
  rewrite -lerBrDr -2!mulrBl -(@natrB _ 2 1)// (le_trans xL)//.
  by rewrite ler_pM2r// ltW// gtrN// divr_gt0.
have [xR|xR] := lerP (1/3 * M%:num) (f x).
  have : [set g x | x in A `&` f@^-1` `[1/3 * M%:num, +oo[] (g x).
    by exists x => //; split => //; rewrite /= in_itv //= xR.
  move/gR3 => ->; apply/andP; split.
    rewrite lerBrDl -2!mulrBl (le_trans _ xR)// ler_pM2r//.
    by rewrite ler_wpM2r ?invr_ge0 ?ler0n// lerBlDl natr1 ler1n.
  by rewrite lerBlDl -2!mulrDl nat1r divff ?mul1r.
have /andP[ng3 pg3] : -(1/3) * M%:num <= g x <= 1/3 * M%:num.
  by apply: grng; exists x.
rewrite ?(intrD _ 1 1) !mulrDl; apply/andP; split.
  by rewrite opprD lerB// -mulNr ltW.
by rewrite (lerD (ltW _))// lerNl -mulNr.
Qed.

Let tietze_step (f : X -> R) M :
  {g : X -> R^o | {within A, continuous f} -> 0 < M ->
    (forall x, A x -> `|f x| <= M) -> [/\ continuous g,
      forall x, A x -> `|f x - g x| <= 2/3 * M :>R
      & forall x, `|g x| <= 1/3 * M ]}.

Proof.

apply: cid.
have [|?] := pselect ({within A, continuous f}); last by exists point.
have [|?] := ltP 0 M; last by exists point.
have [|?] := pselect (forall x, A x -> `|f x| <= M); last by exists point.
by move=> bd pm cf; have [g ?] := tietze_step' pm cf bd; exists g.
Qed.

Let onem_twothirds : 1 - 2/3 = 1/3 :> R.

Proof.

by apply/eqP; rewrite subr_eq/= -mulrDl nat1r divff. Qed.

Lemma continuous_bounded_extension (f : X -> R^o) M :
  0 < M -> {within A, continuous f} -> (forall x, A x -> `|f x| <= M) ->
  exists g, [/\ {in A, f =1 g}, continuous g & forall x, `|g x| <= M].

Proof.

move: M => _/posnumP[M] Af fbd; pose M2d3 n := geometric M%:num (2/3) n.
have MN0 n : 0 < M2d3 n by rewrite /M2d3 /geometric /mk_sequence.
pose f_ := fix F n :=
  if n is n.+1 then F n - projT1 (tietze_step (F n) (M2d3 n)) else f.
pose g_ n := projT1 (tietze_step (f_ n) (M2d3 n)).
have fgE n : f_ n - f_ n.+1 = g_ n by rewrite /= opprB addrC subrK.
have twothirds1 : `|2/3| < 1 :> R.
  by rewrite gtr0_norm//= ltr_pdivrMr// mul1r ltr_nat.
have f_geo n : {within A, continuous f_ n} /\
    (forall x, A x -> `|f_ n x| <= geometric M%:num (2/3) n).
  elim: n => [|n [ctsN bdN]]; first by split=> //= x ?; rewrite expr0 mulr1 fbd.
  have [cg bdNS bd2] := projT2 (tietze_step (f_ n) _) ctsN (MN0 n) bdN.
  split=> [x|]; first by apply: cvgB; [exact:ctsN|exact/continuous_subspaceT/cg].
  by move=> x Ax; rewrite (le_trans (bdNS _ Ax))// /M2d3/= mulrCA -exprS.
have g_cts n : continuous (g_ n).
  by have [? ?] := f_geo n; case: (projT2 (tietze_step (f_ n) _) _ (MN0 n)).
have g_bd n : forall x, `|g_ n x| <= geometric ((1/3) * M%:num) (2/3) n.
  have [ctsN bdfN] := f_geo n; rewrite /geometric /= -[_ * M%:num * _]mulrA.
  by have [_ _] := projT2 (tietze_step (f_ n) _) ctsN (MN0 n) bdfN.
pose h_ : nat -> arrow_uniform_type X R^o := @series {uniform X -> _} g_.
have cvgh' : cvg (h_ @ \oo).
  apply/cauchy_cvgP/cauchy_ballP => eps epos; near_simpl.
  suff : \forall x & x' \near \oo, (x' <= x)%N -> ball (h_ x) eps (h_ x').
    move=>/[dup]; rewrite {1}near_swap; apply: filter_app2; near=> n m.
    by have /orP[mn /(_ mn)/ball_sym + _| ? _] := leq_total n m; apply.
  near=> n m; move=> /= MN; rewrite /ball /= /h_ => t; rewrite /ball /=.
  rewrite -[X in `|X|]/((series g_ n - series g_ m) t) sub_series MN fct_sumE.
  rewrite (le_lt_trans (ler_norm_sum _ _ _))//.
  rewrite (le_lt_trans (ler_sum _ (fun i _ => g_bd i t)))// -mulr_sumr.
  rewrite -(subnKC MN) geometric_partial_tail.
  pose L := (1/3) * M%:num * ((2/3) ^+ m / (1 - (2/3))).
  apply: (@le_lt_trans _ _ L); first by rewrite ler_pM2l // geometric_le_lim.
  rewrite /L onem_twothirds.
  rewrite [_ ^+ _ * _ ^-1]mulrC mulrA -[x in x < _]ger0_norm; last by [].
  near: m; near_simpl; move: eps epos.
  by apply: (cvgr0_norm_lt (fun _ => _ : R^o)); exact: cvg_geometric.
have cvgh : {uniform, h_ @ \oo --> lim (h_ @ \oo)}.
  by move=> ?; rewrite /= uniform_nbhsT; exact: cvgh'.
exists (lim (h_ @ \oo)); split.
- move=> t /set_mem At; have /pointwise_cvgP/(_ t)/(cvg_lim (@Rhausdorff _)) :=
    [elaborate pointwise_uniform_cvg _ cvgh].
  rewrite -fmap_comp /comp /h_ => <-; apply/esym/(@cvg_lim _ (@Rhausdorff R)).
  apply: (@cvg_zero R R^o); apply: norm_cvg0; under eq_fun => n.
    rewrite distrC /series /cst /= -mulN1r fct_sumE mulr_sumr.
    under [fun _ : nat => _]eq_fun => ? do rewrite mulN1r -fgE opprB.
    rewrite telescope_sumr //= subrKC.
    over.
  apply/norm_cvg0P/cvgr0Pnorm_lt => eps epos.
  have /(_ _ epos) := @cvgr0_norm_lt R _ _ _ eventually_filter (_ : nat -> R^o)
    (cvg_geometric M%:num twothirds1).
  apply: filter_app; near_simpl; apply: nearW => n /le_lt_trans; apply.
  by rewrite (le_trans ((f_geo n).2 _ _)) // ler_norm.
- apply: (@uniform_limit_continuous X _ (h_ @ \oo) (lim (h_ @ \oo))) =>//.
  near_simpl; apply: nearW; elim.
    by rewrite /h_ /series /= big_geq// => ?; exact: cvg_cst.
  move=> n; rewrite /h_ /series /= big_nat_recr /= // => IH t.
  by apply: continuousD; [exact: IH|exact: g_cts].
- move=> t.
  have /pointwise_cvgP/(_ t)/(cvg_lim (@Rhausdorff _)) :=
    [elaborate pointwise_uniform_cvg _ cvgh].
  rewrite -fmap_comp /comp /h_ => <-.
  under [fun _ : nat => _]eq_fun => ? do rewrite /series /= fct_sumE.
  have cvg_gt : cvgn [normed series (g_^~ t)].
    apply: (series_le_cvg _ _ (g_bd ^~ t) (is_cvg_geometric_series _)) => //.
    by move=> n; rewrite mulr_ge0.
  rewrite (le_trans (lim_series_norm _))//; apply: le_trans.
    exact/(lim_series_le cvg_gt _ (g_bd ^~ t))/is_cvg_geometric_series.
  rewrite (cvg_lim _ (cvg_geometric_series _))//; last exact: Rhausdorff.
  by rewrite onem_twothirds mulrAC divff mul1r.
Unshelve. all: by end_near. Qed.

End Tietze.