proposition: Lemma regFunEq_e_small : forall (f g : RegularFunction (@ball X)) (E:Qpos), (forall (e:Qpos), proj1_sig e <= proj1_sig E -> ball (m:=X) (proj1_sig e+ proj1_sig e) (approximate f e) (approximate g e)) -> (regFunEq f g).
proof: Proof. intros f g E H. apply regFunEq_e. intros e. apply ball_closed. intros d dpos. assert (0 < (1#4)) as quarterPos. reflexivity. set (e':=Qpos_min (exist _ _ quarterPos*exist _ _ dpos) E). apply ball_weak_le with (proj1_sig ((e+e')+(e'+e')+(e'+e))%Qpos). apply (Qle_trans _ (proj1_sig ((e+exist _ _ quarterPos*exist _ _ dpos) +(exist _ _ quarterPos*exist _ _ dpos+exist _ _ quarterPos*exist _ _ dpos) +(exist _ _ quarterPos*exist _ _ dpos+e))%Qpos)). - simpl. ring_simplify. apply Qplus_le_r. apply (Qle_trans _ ((4#1) * ((1 # 4) * d))). 2: simpl; ring_simplify; apply Qle_refl. apply Qmult_le_l. reflexivity. apply Qpos_min_lb_l. - simpl. ring_simplify. apply Qle_refl. - apply ball_triangle with (approximate g e'). apply ball_triangle with (approximate f e'). apply regFun_prf. apply H. apply Qpos_min_lb_r. apply regFun_prf. Qed.
imports: CoRN.metric2.UniformContinuity CoRN.model.structures.QposInf CoRN.metric2.Classification CoRN.model.totalorder.QposMinMax CoRN.model.totalorder.QMinMax