Module mathcomp.analysis.numfun

From HB Require Import structures.
From mathcomp Require Import boot order ssralg ssrnum ssrint interval.
From mathcomp Require Import interval_inference 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 reals ereal.
From mathcomp Require Import topology normedtype sequences.

# Numerical functions This file provides definitions and lemmas about numerical functions (e.g., the fact that numerical functions with a finite image from a (potentially zero) ring) and theorems such as Tietze's extension theorem. ``` itv_partition a b s == s is a partition of the interval `[a, b] itv_partitionL s c == the left side of splitting a partition at c itv_partitionR s c == the right side of splitting a partition at c variation a b f s == the sum of f at all points in the partition s variations a b f == the set of all variations of f between a and b bounded_variation a b f == all variations of f are bounded {nnfun T >-> R} == type of non-negative functions f ^\+ == the function formed by the non-negative outputs of f and 0 otherwise The codomain of f is the real numbers in scope ring_scope and the extended real numbers in scope ereal_scope. Rendered as f ⁺ with company-coq (U+207A). f ^\- == the function formed by the non-positive outputs of f and 0 o.w. Similar to ^\+. Rendered as f ⁻ with company-coq (U+207B). \1_ A == indicator function 1_A ```

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

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

Lemma { : numDomainType} ( : 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 { : numDomainType} ( : 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 {} { : porderType d}.
Implicit Type (a b : T) (s : seq T).

a :: s is a partition of the interval a, b

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

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

Proof.

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

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

Proof.

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

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

Proof.

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

Lemma :
(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_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 a b s -> (a <= b)%O.

Proof.

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

Lemma :
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 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 : (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 : (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 :
  {in `[a, b] &, nondecreasing_fun f} -> itv_partition a b s ->
  let : nat -> T := f \o nth b (a :: s) in
  forall , (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.

given a partition of a, b and c, returns a partition of a, c

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

given a partition of a, b and c, returns a partition of c, b

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

End interval_partition_porderType.

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

Lemma : (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 < c)%O]).
by rewrite /itv_partitionL last_rcons.
Qed.

Lemma : (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 : 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 : sorted <%O s -> c \notin s ->
s = [seq <- 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.
    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 { : numDomainType}.
Implicit Type (a b : R) (s : seq R).

Lemma :
  {in `[a, b] &, nonincreasing_fun f} -> itv_partition a b s ->
  let : nat -> R := f \o nth b (a :: s) in
  forall , (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 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)); first 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 { : numDomainType}.
Implicit Types (a b : R) (f g : R -> R).

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

Lemma : itv_partition a b s ->
variation a b f s = \sum_( <- 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 : itv_partition a b s ->
variation a b f s = \sum_( <- 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.
  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: (sorted_uniq lt_trans) => //; apply: path_sorted sa.
by apply: set_nth_default => /=; rewrite ltnS ltnW.
Qed.

Lemma : itv_partition a b s ->
variation a b f s =
\sum_( <- 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//; last exact: set_nth_default.
have /lt_sorted_uniq : sorted <%R (a :: s) by [].
by rewrite lastI rcons_uniq => /andP[].
Qed.

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

Proof.

by rewrite /variation/= big_nil. Qed.

Lemma : 0 <= variation a b f s.

Proof.

exact/sumr_ge0. Qed.

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

Proof.

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

Lemma :
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 : {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 <= < 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 : {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 : 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 : 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 : 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).
  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.
  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).
    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 : 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 := variation_cat (only parsing).

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

Lemma : 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)//.
  by apply: path_sorted; case: abs => + _; exact.
rewrite -notin_itv_partition//.
  by apply: path_sorted; case: abs => /= + _; exact.
rewrite !variation_zip//.
  by apply: itv_partition_cat;
    [exact: (itv_partitionLP _ bc)|exact: (itv_partitionRP ac)].
rewrite [in leLHS](notin_itv_partition _ cl).
  by apply: path_sorted; case: abs => + _; exact.
set L := [seq <- 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)//.
  by rewrite -!catA -cat_cons.
rewrite zip_cat; first by rewrite cats1 size_rcons.
rewrite (_ : a :: _ ++ _ ++ B = (a :: L0) ++ [:: L1] ++ [:: c] ++ B).
  by rewrite -!catA -cat_cons.
rewrite zip_cat; first 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).
  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 ( : 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) => //.
  exact: itv_partition1.
have [y [s' s'E]] : exists , 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: itv_partition1 | exact: le_variation].
Qed.

End variation_realDomainType.

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

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

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

Proof.

by move=> abs; exists s. Qed.

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

Proof.

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

Lemma : 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 : 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 := has_ubound (variations a b f).

Notation := bounded_variation.

Lemma : BV a a f.

Proof.

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

Lemma : 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 : BV a b f -> BV a b (\- f).

Proof.

by rewrite /bounded_variation variationsN. Qed.

Lemma : 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 ![in leRHS](set_nth_default c)//= ltnS ltnW.
Qed.

Lemma : 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 (- 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 :
{in `[a, b] &, {homo f : / 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.

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

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

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

Proof.

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

..

End fimfun_bin.

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

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

Lemma : f \_ set0 = cst 0.

Proof.

by rewrite patch_set0. Qed.

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

Proof.

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

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

Proof.

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

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

Proof.

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

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

Proof.

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

Lemma {} { : numFieldType} ( : set aT) ( : aT -> \bar rT) :
(forall , E x -> 0 <= f x)%E ->
D `<=` E -> forall , ((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 ( : Type) ( : realDomainType) ( : set T).
Implicit Types (f g : T -> \bar R) (r : R).

Lemma : f \_ set0 = cst 0.

Proof.

by rewrite patch_set0. Qed.

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

Proof.

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

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

Proof.

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

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

Proof.

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

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

Proof.

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

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

Proof.

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

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

Proof.

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

End erestrict_lemmas.

Section funrposneg.
Local Open Scope ring_scope.

Definition ( : realDomainType) ( : T -> R) :=
fun => Num.max (f x) 0.
Definition ( : realDomainType) ( : T -> R) :=
fun => Num.max (- f x) 0.

End funrposneg.

Notation := (funrpos f) : ring_scope.
Notation := (funrneg f) : ring_scope.

Section funrposneg_lemmas.
Local Open Scope ring_scope.
Variables ( : Type) ( : realDomainType) ( : set T).
Implicit Types (f g : T -> R) (r : R).

Lemma : 0 <= f^\+ x.

Proof.

by rewrite /funrpos /= le_max lexx orbT. Qed.

Lemma : 0 <= f^\- x.

Proof.

by rewrite /funrneg le_max lexx orbT. Qed.

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

Proof.

exact/funext. Qed.

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

Proof.

by apply/funext => x; rewrite /funrneg opprK. Qed.

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

Proof.

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

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

Proof.

by move=> f0 x; rewrite inE => Dx; apply/max_idPr; rewrite lerNl oppr0 f0.
Qed.

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

Proof.

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

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

Proof.

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

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

Proof.

by move=> ?; rewrite funeqE => x; rewrite /funrpos maxr_pMr// mulr0. Qed.

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

Proof.

by move=> r0; rewrite funeqE => x; rewrite /funrneg -mulrN maxr_pMr// mulr0.
Qed.

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

Proof.

move=> r0; rewrite -[in LHS](opprK r); under eq_fun do rewrite mulNr.
by rewrite funrposN ge0_funrnegM ?oppr_ge0.
Qed.

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

Proof.

move=> r0; rewrite -[in LHS](opprK r); under eq_fun do rewrite mulNr.
by rewrite funrnegN ge0_funrposM ?oppr_ge0.
Qed.

Lemma : f^\+ + f^\- = Num.norm \o f.

Proof.

rewrite funeqE => x /=; rewrite !fctE/=; have [fx0|/ltW fx0] := leP (f x) 0.
- rewrite ler0_norm// /funrpos /funrneg.
  move/max_idPr : (fx0) => ->; rewrite add0r.
  by move: fx0; rewrite -{1}oppr0 lerNr => /max_idPl ->.
- rewrite ger0_norm// /funrpos /funrneg; move/max_idPl : (fx0) => ->.
  by move: fx0; rewrite -{1}oppr0 lerNl => /max_idPr ->; rewrite addr0.
Qed.

Lemma : f^\+ - f^\- = f.

Proof.

apply/funext => x.
rewrite /funrpos /funrneg/= !fctE; have [|/ltW] := leP (f x) 0.
by rewrite -{1}oppr0 -lerNr => /max_idPl ->; rewrite opprK add0r.
by rewrite -{1}oppr0 -lerNl => /max_idPr ->; rewrite subr0.
Qed.

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

Proof.

by rewrite addBrfctE !funrposBneg. Qed.

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

Proof.

move=> fg x Dx; rewrite /funrpos /Num.max; 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 :
{in D, forall , f x <= g x} -> {in D, forall , g^\- x <= f^\- x}.

Proof.

move=> fg x Dx; rewrite /funrneg /Num.max; case: ifPn => gx; case: ifPn => fx//.
- by rewrite leNgt.
- by move: gx; rewrite -leNgt => /(lt_le_trans fx); rewrite ltrN2 ltNge fg.
- by rewrite lerN2; exact: fg.
Qed.

Lemma : f =1 g -> f^\+ =1 g^\+.

Proof.

by move=> eq_fg x; rewrite /funrpos eq_fg. Qed.

Lemma : f =1 g -> f^\- =1 g^\-.

Proof.

by move=> eq_fg x; rewrite /funrneg eq_fg. Qed.

Lemma : (fun _ : T => 0)^\+ x = 0 :> R.

Proof.

by rewrite /funrpos maxxx. Qed.

Lemma : (fun _ : T => 0)^\- x = 0 :> R.

Proof.

by rewrite /funrneg oppr0 maxxx. Qed.

Lemma : 0 <= c -> (c \*o f)^\+ =1 c \*o f^\+.

Proof.

by move=> ge0_c x; rewrite /= ge0_funrposM. Qed.

Lemma : 0 <= c -> (c \*o f)^\- =1 c \*o f^\-.

Proof.

move=> ge0_c x; rewrite /= -!funrposN; have /= <- := funrposZ (- f) ge0_c x.
by apply/eq_funrpos=> y /=; rewrite mulrN.
Qed.

Lemma ( : T -> nat) :
(fun => (n x)%:R * f x)^\+ x = (n x)%:R * f^\+ x.

Proof.

by rewrite /funrpos -[in RHS]normr_nat maxr_pMr// mulr0 ger0_norm.
Qed.

Lemma ( : T -> nat) :
(fun => (n x)%:R * f x)^\- x = (n x)%:R * f^\- x.

Proof.

rewrite -[in RHS]funrposN -funrpos_natrM -funrposN.
by apply/eq_funrpos=> y; rewrite mulrN.
Qed.

Lemma : f^\+ x <= `|f x|.

Proof.

by rewrite -/((Num.Def.normr \o f) x) -funrposDneg lerDl funrneg_ge0.
Qed.

End funrposneg_lemmas.
#[global]
Hint Extern 0 (is_true (0%R <= _ ^\+ _)%R) => solve [apply: funrpos_ge0] : core.
#[global]
Hint Extern 0 (is_true (0%R <= _ ^\- _)%R) => solve [apply: funrneg_ge0] : core.

.
( : realDomainType) ( : T -> \bar R) :=
fun => maxe (f x) 0.
.
( : realDomainType) ( : T -> \bar R) :=
fun => maxe (oppe (f x)) 0.

Notation := (funepos f) : ereal_scope.
Notation := (funeneg f) : ereal_scope.

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

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

Proof.

by rewrite unlock. Qed.

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

Proof.

by rewrite unlock. Qed.

Lemma : 0 <= f^\+ x.

Proof.

by rewrite funeposE le_max lexx orbT. Qed.

Lemma : 0 <= f^\- x.

Proof.

by rewrite funenegE le_max lexx orbT. Qed.

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

Proof.

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

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

Proof.

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

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

Proof.

by rewrite !unlock. Qed.

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

Proof.

by rewrite !unlock. Qed.

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

Proof.

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

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

Proof.

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

Lemma : (forall , 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 : (forall , 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 : (forall , 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 : (forall , 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 : (0 <= r)%R ->
(fun => r%:E * f x)^\+ = (fun => r%:E * (f^\+ x)).

Proof.

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

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

Proof.

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

Lemma : (r <= 0)%R ->
(fun => r%:E * f x)^\+ = (fun => - 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 : (r <= 0)%R ->
(fun => r%:E * f x)^\- = (fun => - 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 : f^\+ \+ f^\- = abse \o f.

Proof.

rewrite funeqE => x /=; have /orP[fx0|fx0] := le_total (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 : f^\+ \- f^\- = f.

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 : (f^\+ x +? - f^\- x).

Proof.

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

#[deprecated(since="mathcomp-analysis 1.15.0", note="use `funeposBneg` instead")]
Lemma : (f \+ g)^\+ \- (f \+ g)^\- = f \+ g.

Proof.

by rewrite funeposBneg. Qed.

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

Proof.

rewrite ge0_addBefctE//; [by move=> x; rewrite funeneg_ge0..|].
by rewrite -[in RHS](funeposBneg f) -[in RHS](funeposBneg g).
Qed.

Lemma :
{in D, forall , f x <= g x} -> {in D, forall , 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 :
{in D, forall , f x <= g x} -> {in D, forall , 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.

Lemma : (@cst T _ 0)^\+ t = 0 :> \bar R.

Proof.

by rewrite funeposE maxxx. Qed.

Lemma : (@cst T _ 0)^\- t = 0 :> \bar R.

Proof.

by rewrite funenegE oppe0 maxxx. Qed.

End funposneg_lemmas.
#[deprecated(since="mathcomp-analysis 1.15.0", note="use `-funeDB` instead")]
Notation := funeDB (only parsing).

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

Section funrpos_funepos_lemmas.
Context { : Type} { : realDomainType}.

Lemma ( : T -> R) : (EFin \o f)^\+%E = (EFin \o f^\+).

Proof.

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

Lemma ( : T -> R) : (EFin \o f)^\-%E = (EFin \o f^\-).

Proof.

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

End funrpos_funepos_lemmas.

Definition {} { : pzRingType} ( : set T) ( : T) : R := (x \in A)%:R.

Reserved Notation "'\1_' A" (at level 8, A at level 2, format "'\1_' A") .
Notation := (indic A) : ring_scope.

Lemma {} { : numDomainType} ( : set T) ( : 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 {} { : numDomainType} ( : set T) ( : T) :=
Itv.mk (@num_spec_indic T R A x).

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

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

Proof.

by []. Qed.

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

Proof.

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

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

Proof.

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

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

Proof.

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

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

Proof.

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

Lemma :
\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 ( : set T) ( : 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 : \1_D @` A `<=` ([set 0; 1] : set R).

Proof.

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

Lemma ( : {fimfun T >-> R}) :
f x = \sum_( \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 ( : {fimfun T >-> R})
( := fset_set (f @` setT)) :
forall , f x = \sum_( < #|`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 { : realType} ( : (set T)^nat) ( : T) :
trivIset [set: nat] A ->
(\1_(\bigcup_ A n) t)%:E = (\sum_(0 <= <oo) (\1_(A n) t)%:E)%E :> \bar R.

Proof.

move=> tA.
have [At|At] := eqVneq (\1_(\bigcup_ 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_ 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 { : numFieldType} ( : T -> R) ( : set T) :
f \_ D = (f \* \1_D)%R.

Proof.

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

Lemma ( : numDomainType) ( : T -> \bar R) ( : 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 ( : nzRingType) ( : set (T1 * T2)) :
xsection A x = (fun => (\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 ( : nzRingType) ( : set (T1 * T2)) :
ysection A y = (fun => (\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 { : numFieldType} ( : set T) :
[bounded \1_A x : R^o | in A].

Proof.

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

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

Proof.

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

Lemma ( : numFieldType) ( : 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 { : realFieldType} ( : R^o) :
x \in (ball 0 k : set R^o) ->
\1_(ball 0 k : set R^o) 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//=; last 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 ( : Type) ( : pzRingType).

Lemma : 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)).
Qed.

.
.isMulClosed.Build _ (@fimfun aT rT) fimfun_mulr_closed.
. of {fimfun aT >-> rT} by <:].

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

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

Proof.

by []. Qed.

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

Proof.

by []. Qed.

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

Proof.

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

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

Proof.

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

Lemma : @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.

. X.

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

..copy (k \o* f) (f * cst_fimfun k).

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

End ring.
Arguments indic_fimfun {aT rT} _.

Notation :=
  (GRing.SubPzRing_isSubComPzRing.Build _ _ U)
  (format "[ 'SubPzRing_isSubComPzRing' 'of' U 'by' <: ]")
  : form_scope.

Section comring.
Context ( : Type) ( : comPzRingType).
.
  [SubPzRing_isSubComPzRing of {fimfun aT >-> rT} by <:].

Implicit Types (f g : {fimfun aT >-> rT}).
..copy (f \* g) (f * g).
End comring.

. () () (f : T -> R) :=
  { fimfunE : exists ( : seq R) ( : R -> set T),
      forall , f x = \sum_( <- r) (y * \1_(A_ y) x) }.
. T R f.
  Lemma : @FiniteImage T R f.

Proof.

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

  ..
..

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

Hypothesis : normal_space X.

Lemma :
  closed A -> closed B -> A `&` B = set0 -> x < y ->
  exists : 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: cst_continuous.
    by apply: (@continuousB _ R^o) => //; exact: cst_continuous.
  by apply: continuousM => //; exact: cst_continuous.
- 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 ( : set X).
Hypothesis : closed A.

Local Lemma ( : X -> R) ( : R) :
  0 < M -> {within A, continuous f} ->
  (forall , A x -> `|f x| <= M) ->
  exists : X -> R, [/\ continuous g,
     (forall , A x -> `|f x - g x| <= 2/3 * M) &
     (forall , `|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: preimage_closed.
- by rewrite closed_setSI//; apply: preimage_closed => //; 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 | 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 | 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 ( : X -> R) :
  { : X -> R^o | {within A, continuous f} -> 0 < M ->
    (forall , A x -> `|f x| <= M) -> [/\ continuous g,
      forall , A x -> `|f x - g x| <= 2/3 * M :>R
      & forall , `|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 , 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 : 1 - 2/3 = 1/3 :> R.

Proof.

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

Tietze's theorem:

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

Proof.

move: M => _/posnumP[M] Af fbd; pose M2d3 := geometric M%:num (2/3) n.
have MN0 n : 0 < M2d3 n by rewrite /M2d3 /geometric /mk_sequence.
pose f_ := fix F :=
  if n is n.+1 then F n - projT1 (tietze_step (F n) (M2d3 n)) else f.
pose g_ := 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 , 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 , `|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 & \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 _ => 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; first 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: cst_continuous.
  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 _))//; first exact: Rhausdorff.
  by rewrite onem_twothirds mulrAC divff mul1r.
Unshelve. all: by end_near. Qed.

End Tietze.

Files

Module mathcomp.analysis.numfun