Plotting
Plotting a uniformly continuous function on a finite interval consists of producing the graph of a function as a compact set, approximating that graph, and finally rasterizing that approximation.A range for the plot must be provided. We choose to clamp the plotted function so that it lies inside the specified range. Thus we plot compose (clip b t) f rather than f.
Variable (l r:Q).
Hypothesis Hlr : l < r.
Variable (b t:Q).
Hypothesis Hbt : b < t.
Let clip := uc_compose (boundBelow b) (boundAbove t).
Variable f : Q_as_MetricSpace --> CR.
Lemma plFEQ : PrelengthSpace (FinEnum stableQ).
Definition graphQ f := CompactGraph_b f stableQ2 plFEQ (CompactIntervalQ (Qlt_le_weak _ _ Hlr)).
Lemma graphQ_bonus : forall e x y,
In (x, y) (approximate (graphQ (uc_compose clip f)) e) -> l <= x <= r /\ b <= y <= t.
Variable n m : N.
Hypothesis Hn : eq_nat n 0 = false.
Hypothesis Hm : eq_nat m 0 = false.
Let w := proj1_sigT _ _ (Qpos_lt_plus Hlr).
Let h := proj1_sigT _ _ (Qpos_lt_plus Hbt).
Let err := Qpos_max ((1 # 4 * P_of_succ_nat (pred n)) * w)
((1 # 4 * P_of_succ_nat (pred m)) * h).
Hypothesis Hlr : l < r.
Variable (b t:Q).
Hypothesis Hbt : b < t.
Let clip := uc_compose (boundBelow b) (boundAbove t).
Variable f : Q_as_MetricSpace --> CR.
Lemma plFEQ : PrelengthSpace (FinEnum stableQ).
Definition graphQ f := CompactGraph_b f stableQ2 plFEQ (CompactIntervalQ (Qlt_le_weak _ _ Hlr)).
Lemma graphQ_bonus : forall e x y,
In (x, y) (approximate (graphQ (uc_compose clip f)) e) -> l <= x <= r /\ b <= y <= t.
Variable n m : N.
Hypothesis Hn : eq_nat n 0 = false.
Hypothesis Hm : eq_nat m 0 = false.
Let w := proj1_sigT _ _ (Qpos_lt_plus Hlr).
Let h := proj1_sigT _ _ (Qpos_lt_plus Hbt).
Let err := Qpos_max ((1 # 4 * P_of_succ_nat (pred n)) * w)
((1 # 4 * P_of_succ_nat (pred m)) * h).
PlotQ is the function that does all the work.
The resulting plot is close to the graph of f
Theorem Plot_correct :
ball (err + Qpos_max ((1 # 2 * P_of_succ_nat (pred n)) * w)
((1 # 2 * P_of_succ_nat (pred m)) * h))
(graphQ (uc_compose clip f))
(Cunit (InterpRaster PlotQ (l,t) (r,b))).
End Plot.
ball (err + Qpos_max ((1 # 2 * P_of_succ_nat (pred n)) * w)
((1 # 2 * P_of_succ_nat (pred m)) * h))
(graphQ (uc_compose clip f))
(Cunit (InterpRaster PlotQ (l,t) (r,b))).
End Plot.
Some nice notation for the graph of f.