proposition: 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: 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 -> [the completeType of {uniform 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 _)) := !! pointwise_uniform_cvg _ cvgh. rewrite -fmap_comp /comp /h_ => <-; apply/esym/(@cvg_lim _ (@Rhausdorff R)). apply: (@cvg_zero R [the pseudoMetricNormedZmodType R of 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 //= addrCA subrr addr0. 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 _)) := !! 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 divrr ?mul1r// unitfE. Unshelve. all: by end_near. Qed.
imports: HB(structures) mathcomp(all_ssreflect ssralg ssrnum ssrint interval finmap) mathcomp(mathcomp_extra boolp classical_sets fsbigop) mathcomp(functions cardinality set_interval) signed reals ereal topology normedtype sequences