Graphing
Uniformly continuous functions over compact sets can be graph. A graph of a funciton f : X --> Y is the the subset of X*Y {(x,f x) | x in S} where S is the domain under consideration. This graph is compact when S is a compact subset of X.
graphPoint is the fundamental function of graphing. It will be lifted in
various ways to produce a graph
Definition graphPoint_raw (f:X -> Y) (x:X) : XY := (x,f x).
Variable f : X --> Y.
Definition graphPoint_modulus (e:Qpos) : Q+ :=
match (mu f e) with
| ∞ => e
| Qpos2QposInf d => Qpos_min e d
end.
Lemma graphPoint_uc : is_UniformlyContinuousFunction (graphPoint_raw f) graphPoint_modulus.
Definition graphPoint : X --> XY :=
Build_UniformlyContinuousFunction graphPoint_uc.
Hypothesis stableX : stableMetric X.
Hypothesis stableXY : stableMetric XY.
Variable f : X --> Y.
Definition graphPoint_modulus (e:Qpos) : Q+ :=
match (mu f e) with
| ∞ => e
| Qpos2QposInf d => Qpos_min e d
end.
Lemma graphPoint_uc : is_UniformlyContinuousFunction (graphPoint_raw f) graphPoint_modulus.
Definition graphPoint : X --> XY :=
Build_UniformlyContinuousFunction graphPoint_uc.
Hypothesis stableX : stableMetric X.
Hypothesis stableXY : stableMetric XY.
The compact image of graphFunction is the graph of Cmap f over any
compact set S
Definition CompactGraph (plFEX:PrelengthSpace (FinEnum stableX)) : Compact stableX --> Compact stableXY :=
CompactImage (1#1) _ plFEX graphPoint.
Lemma CompactGraph_correct1 : forall plX plFEX x s, (inCompact x s) ->
inCompact (Couple (x,(Cmap plX f x))) (CompactGraph plFEX s).
Lemma CompactGraph_correct2 : forall plFEX p s, inCompact p (CompactGraph plFEX s) ->
inCompact (Cfst p) s.
Lemma CompactGraph_correct3 : forall plX plFEX p s, inCompact p (CompactGraph plFEX s) ->
st_eq (Cmap plX f (Cfst p)) (Csnd p).
Lemma CompactGraph_graph : forall (plX : PrelengthSpace X) plFEX p q1 q2 s,
inCompact (Couple (p,q1)) (CompactGraph plFEX s) ->
inCompact (Couple (p,q2)) (CompactGraph plFEX s) ->
st_eq q1 q2.
Lemma CompactGraph_correct : forall plX plFEX x y s,
inCompact (Couple (x,y)) (CompactGraph plFEX s) <->
(inCompact x s /\ st_eq y (Cmap plX f x)).
End Graph.
Section GraphBind.
CompactImage (1#1) _ plFEX graphPoint.
Lemma CompactGraph_correct1 : forall plX plFEX x s, (inCompact x s) ->
inCompact (Couple (x,(Cmap plX f x))) (CompactGraph plFEX s).
Lemma CompactGraph_correct2 : forall plFEX p s, inCompact p (CompactGraph plFEX s) ->
inCompact (Cfst p) s.
Lemma CompactGraph_correct3 : forall plX plFEX p s, inCompact p (CompactGraph plFEX s) ->
st_eq (Cmap plX f (Cfst p)) (Csnd p).
Lemma CompactGraph_graph : forall (plX : PrelengthSpace X) plFEX p q1 q2 s,
inCompact (Couple (p,q1)) (CompactGraph plFEX s) ->
inCompact (Couple (p,q2)) (CompactGraph plFEX s) ->
st_eq q1 q2.
Lemma CompactGraph_correct : forall plX plFEX x y s,
inCompact (Couple (x,y)) (CompactGraph plFEX s) <->
(inCompact x s /\ st_eq y (Cmap plX f x)).
End Graph.
Section GraphBind.
Graph and Bind
The previous section used graphPoint to produce the graph of Cmap f over any compact set S. In this section we use graphPoint_b to produce the graph of Cbind f over any compact set S. It proceeds in largely the same way.Variable X Y:MetricSpace.
Let XY := ProductMS X Y.
Definition graphPoint_b_raw (f:X -> Complete Y) (x:X) : Complete XY := Couple (Cunit x,f x).
Variable f : X --> Complete Y.
Lemma graphPoint_b_uc : is_UniformlyContinuousFunction (graphPoint_b_raw f) (graphPoint_modulus f).
Definition graphPoint_b : X --> Complete XY :=
Build_UniformlyContinuousFunction graphPoint_b_uc.
Hypothesis stableX : stableMetric X.
Hypothesis stableXY : stableMetric XY.
Definition CompactGraph_b (plFEX:PrelengthSpace (FinEnum stableX)) : Compact stableX --> Compact stableXY :=
CompactImage_b (1#1) _ plFEX graphPoint_b.
Lemma CompactGraph_b_correct1 : forall plX plFEX x s, (inCompact x s) ->
inCompact (Couple (x,(Cbind plX f x))) (CompactGraph_b plFEX s).
Lemma CompactGraph_b_correct2 : forall plFEX p s, inCompact p (CompactGraph_b plFEX s) ->
inCompact (Cfst p) s.
Lemma CompactGraph_b_correct3 : forall plX plFEX p s, inCompact p (CompactGraph_b plFEX s) ->
st_eq (Cbind plX f (Cfst p)) (Csnd p).
Lemma CompactGraph_b_graph : forall (plX : PrelengthSpace X) plFEX p q1 q2 s,
inCompact (Couple (p,q1)) (CompactGraph_b plFEX s) ->
inCompact (Couple (p,q2)) (CompactGraph_b plFEX s) ->
st_eq q1 q2.
Lemma CompactGraph_b_correct : forall plX plFEX x y s,
inCompact (Couple (x,y)) (CompactGraph_b plFEX s) <->
(inCompact x s /\ st_eq y (Cbind plX f x)).
End GraphBind.