proposition: Lemma uniform_continuity_2d_1d : forall f a b c, (forall x, a <= x <= b -> continuity_2d_pt f x c) -> forall eps : posreal, exists delta : posreal, forall x y u v, a <= x <= b -> c - delta <= y <= c + delta -> a <= u <= b -> c - delta <= v <= c + delta -> Rabs (u - x) < delta -> Rabs (f u v - f x y) < eps.
proof: Proof. intros f a b c Cf eps. set (P x y u v := Rabs (f u v - f x y) < pos_div_2 eps). refine (_ (fun x Hx => locally_2d_ex_dec (P x c) x c _ (Cf x Hx _))). intros delta1. set (delta2 x := match Rle_dec a x, Rle_dec x b with left Ha, left Hb => pos_div_2 (proj1_sig (delta1 x (conj Ha Hb))) | _, _ => mkposreal _ Rlt_0_1 end). destruct (compactness_value_1d a b delta2) as (delta,Hdelta). exists (pos_div_2 delta) => x y u v Hx Hy Hu Hv Hux. specialize (Hdelta x Hx). apply Rnot_le_lt. apply: false_not_not Hdelta => Hdelta. apply Rlt_not_le. destruct Hdelta as (p&(Hap,Hpb)&Hxp&Hd). replace (f u v - f x y) with (f u v - f p c + (f p c - f x y)) by ring. apply Rle_lt_trans with (1 := Rabs_triang _ _). rewrite (double_var eps). revert Hxp Hd. unfold delta2. case Rle_dec => Hap' ; try easy. case Rle_dec => Hpb' ; try easy. clear delta2. case delta1 => /= r Hr Hxp Hd. apply Rplus_lt_compat. apply Hr. replace (u - p) with (u - x + (x - p)) by ring. apply Rle_lt_trans with (1 := Rabs_triang _ _). rewrite (double_var r). apply Rplus_lt_compat with (2 := Hxp). apply Rlt_le_trans with (2 := Hd). apply Rlt_trans with (1 := Hux). apply: Rlt_eps2_eps. apply cond_pos. apply Rle_lt_trans with (pos_div_2 delta). now apply Rabs_le_between'. apply Rlt_le_trans with(1 := Rlt_eps2_eps _ (cond_pos delta)). apply Rle_trans with (1 := Hd). apply Rlt_le. apply Rlt_eps2_eps. apply cond_pos. rewrite Rabs_minus_sym. apply Hr. apply Rlt_trans with (1 := Hxp). apply Rlt_eps2_eps. apply cond_pos. apply Rle_lt_trans with (pos_div_2 delta). now apply Rabs_le_between'. apply Rlt_le_trans with(1 := Rlt_eps2_eps _ (cond_pos delta)). apply Rle_trans with (1 := Hd). apply Rlt_le. apply Rlt_eps2_eps. apply cond_pos. intros u v. unfold P. destruct (Rlt_dec (Rabs (f u v - f x c)) (pos_div_2 eps)); [left|right] ; assumption. Qed.
imports: Coq(Reals ssreflect) Rcomplements Rbar Hierarchy Compactness Lim_seq