Modulus of continity and derivatives.
If two functions, one defined on IR and the other defined on CR, agree on rational valued inside a closed non-trival interval, and the function on IR is differentiable on that interval, then the function on CR is uniformly continuous with modulus fun e => e/M where M is some upper bound on the absolute value of the derivative.
Variable l r : option Q.
Hypothesis Hlr :
match l,r with
| None, _ => True
| _, None => True
| Some l', Some r' => (l'<r')%Q
end.
Let I :=
match l,r with
| None, None => (-∞,+∞)
| Some l', None => [⋅,+∞) (inj_Q _ l')
| None, Some r' => (-∞,⋅] (inj_Q _ r')
| Some l', Some r' => [⋅,⋅] (inj_Q _ l') (inj_Q _ r')
end.
Let properI : proper I.
Let clamp (q:Q) :=
match l,r with
| None, None => q
| Some l', None => QboundBelow_uc l' q
| None, Some r' => QboundAbove_uc r' q
| Some l', Some r' => (uc_compose (QboundBelow_uc l') (QboundAbove_uc r') q)
end.
Lemma ball_clamp : forall e a b, ball e a b -> ball e (clamp a) (clamp b).
Variable f f' : PartFunct IR.
Hypothesis Hf : Derivative I properI f f'.
Section GeneralCase.
Variable g : Q_as_MetricSpace -> CR.
Hypothesis Hg : forall (q:Q) Hq, I (inj_Q _ q) -> (g q == IRasCR (f (inj_Q _ q) Hq))%CR.
Variable c : Q.
Hypothesis Hc : forall x Hx, I x -> (AbsIR (f' x Hx)[<=](inj_Q _ (c:Q))).
Lemma is_UniformlyContinuousD : is_UniformlyContinuousFunction (fun x => g (clamp x)) (Qscale_modulus c).
End GeneralCase.
Lemma is_UniformlyContinuousD_Q
: forall g : Q_as_MetricSpace -> Q,
(forall (q : Q) (Hq : Dom f (inj_Q IR q)),
I (inj_Q IR q) -> (inj_Q IR (g q) [=] (f (inj_Q IR q) Hq))) ->
forall c : Q,
(forall (x : Q) (Hx : Dom f' (inj_Q IR x)), I (inj_Q IR x) -> AbsIR (f' (inj_Q IR x) Hx)[<=]inj_Q IR (c:Q)) ->
is_UniformlyContinuousFunction (fun x : Q_as_MetricSpace => g (clamp x)) (Qscale_modulus c).
End Modulus.
Hypothesis Hlr :
match l,r with
| None, _ => True
| _, None => True
| Some l', Some r' => (l'<r')%Q
end.
Let I :=
match l,r with
| None, None => (-∞,+∞)
| Some l', None => [⋅,+∞) (inj_Q _ l')
| None, Some r' => (-∞,⋅] (inj_Q _ r')
| Some l', Some r' => [⋅,⋅] (inj_Q _ l') (inj_Q _ r')
end.
Let properI : proper I.
Let clamp (q:Q) :=
match l,r with
| None, None => q
| Some l', None => QboundBelow_uc l' q
| None, Some r' => QboundAbove_uc r' q
| Some l', Some r' => (uc_compose (QboundBelow_uc l') (QboundAbove_uc r') q)
end.
Lemma ball_clamp : forall e a b, ball e a b -> ball e (clamp a) (clamp b).
Variable f f' : PartFunct IR.
Hypothesis Hf : Derivative I properI f f'.
Section GeneralCase.
Variable g : Q_as_MetricSpace -> CR.
Hypothesis Hg : forall (q:Q) Hq, I (inj_Q _ q) -> (g q == IRasCR (f (inj_Q _ q) Hq))%CR.
Variable c : Q.
Hypothesis Hc : forall x Hx, I x -> (AbsIR (f' x Hx)[<=](inj_Q _ (c:Q))).
Lemma is_UniformlyContinuousD : is_UniformlyContinuousFunction (fun x => g (clamp x)) (Qscale_modulus c).
End GeneralCase.
Lemma is_UniformlyContinuousD_Q
: forall g : Q_as_MetricSpace -> Q,
(forall (q : Q) (Hq : Dom f (inj_Q IR q)),
I (inj_Q IR q) -> (inj_Q IR (g q) [=] (f (inj_Q IR q) Hq))) ->
forall c : Q,
(forall (x : Q) (Hx : Dom f' (inj_Q IR x)), I (inj_Q IR x) -> AbsIR (f' (inj_Q IR x) Hx)[<=]inj_Q IR (c:Q)) ->
is_UniformlyContinuousFunction (fun x : Q_as_MetricSpace => g (clamp x)) (Qscale_modulus c).
End Modulus.