Effective Integration
stepSample
The first step in defining integration is to define the unit function on [0,1] as a Bounded Function. This is defined to be the limit of step functions approximating the unit function.For efficenty reasons we want this approximation to be as good as we can muster because the number of steps this approximation returns will be the number of samples that we will take of the function we want to integrate. Furthermore, we want the tree structure defining the step function to be as balanced as possible.
First we create a step function with n steps that appoximates the identity function, stepSample.
Lemma oddGluePoint (p:positive) : 0 < Psucc p # xI p /\ Psucc p # xI p < 1.
Definition stepSample : positive -> StepQ := positive_rect2
(fun _ => StepQ)
(fun p rec1 rec2 => glue (Build_OpenUnit (oddGluePoint p)) (constStepF (Psucc p#xI p:QS) * rec1) ((constStepF (1#(xI p):QS))*(constStepF (Psucc p:QS) + constStepF (p:QS)*rec2)))
(fun p rec => glue (ou (1#2)) (constStepF (1#2:QS) * rec) (constStepF (1#2:QS) * (constStepF (1:QS) + rec)))
(constStepF (1#2:QS)).
We want to prove that stepSample n is within (1/(2*n)) of the
identity function, but the identity function doesn't exist yet.
Instead we define the SupDistanceToLinear which computes what would
the distance to a linear function on [0,1]. This distance function
is transitive in the sense that if a step function x is within e1 of
a linear function, and a step function y is within e2 of the same
linear function, then x and y are really within (e1+e2) of each other
(in Linf).
Section id01.
Lemma SupDistanceToLinearBase_pos : forall (l r:Q) (H:l<r) (x:Q), 0 < Qmax (x-l) (r-x).
Definition SupDistanceToLinear := StepFfold
(fun (x:QS) (l r:Q) (H:l < r) => mkQpos (SupDistanceToLinearBase_pos H x))
(fun b f g l r H =>
(Qpos_max (f _ _ (affineCombo_gt (OpenUnitDual b) H)) (g _ _ (affineCombo_lt (OpenUnitDual b) H)))).
Lemma SupDistanceToLinearBase_pos : forall (l r:Q) (H:l<r) (x:Q), 0 < Qmax (x-l) (r-x).
Definition SupDistanceToLinear := StepFfold
(fun (x:QS) (l r:Q) (H:l < r) => mkQpos (SupDistanceToLinearBase_pos H x))
(fun b f g l r H =>
(Qpos_max (f _ _ (affineCombo_gt (OpenUnitDual b) H)) (g _ _ (affineCombo_lt (OpenUnitDual b) H)))).
Various properties of SupDistanceToLinear
Lemma SupDistanceToLinear_glue : forall o l r a b (H:a < b),
(SupDistanceToLinear (glue o l r) H ==
Qmax (SupDistanceToLinear l (affineCombo_gt (OpenUnitDual o) H))
(SupDistanceToLinear r (affineCombo_lt (OpenUnitDual o) H)))%Q.
Lemma SupDistanceToLinear_wd1 : forall x l1 r1 (H1:l1 < r1) l2 r2 (H2:l2 < r2),
(l1 == l2 -> r1 == r2 ->
SupDistanceToLinear x H1 == SupDistanceToLinear x H2)%Q.
Lemma Qmax_affineCombo : forall x a b o, a < b -> (Qmax (Qmax (x - a) (affineCombo o a b - x))
(Qmax (x - affineCombo o a b) (b - x)) == Qmax (x - a) (b - x))%Q.
Lemma SupDistanceToLinear_split :
forall x o a b c (H0:a < c) (H1:c < b),
(c == affineCombo (OpenUnitDual o) a b)%Q ->
(Qmax (SupDistanceToLinear (SplitL x o) H0)
(SupDistanceToLinear (SplitR x o) H1) ==
SupDistanceToLinear x (Qlt_trans _ _ _ H0 H1))%Q.
Lemma SupDistanceToLinear_wd2 : forall x1 x2 a b (H: a < b), x1 == x2 ->
(SupDistanceToLinear x1 H == SupDistanceToLinear x2 H)%Q.
Lemma SupDistanceToLinear_translate :
forall x c a b (H:a < b) (H0:a+c < b + c),
(SupDistanceToLinear x H == SupDistanceToLinear (constStepF (c:QS) + x) H0)%Q.
Lemma SupDistanceToLinear_scale :
forall x c a b (H:a < b) (H0:c*a < c*b),
(c*SupDistanceToLinear x H == SupDistanceToLinear (constStepF (c:QS) * x) H0)%Q.
(SupDistanceToLinear (glue o l r) H ==
Qmax (SupDistanceToLinear l (affineCombo_gt (OpenUnitDual o) H))
(SupDistanceToLinear r (affineCombo_lt (OpenUnitDual o) H)))%Q.
Lemma SupDistanceToLinear_wd1 : forall x l1 r1 (H1:l1 < r1) l2 r2 (H2:l2 < r2),
(l1 == l2 -> r1 == r2 ->
SupDistanceToLinear x H1 == SupDistanceToLinear x H2)%Q.
Lemma Qmax_affineCombo : forall x a b o, a < b -> (Qmax (Qmax (x - a) (affineCombo o a b - x))
(Qmax (x - affineCombo o a b) (b - x)) == Qmax (x - a) (b - x))%Q.
Lemma SupDistanceToLinear_split :
forall x o a b c (H0:a < c) (H1:c < b),
(c == affineCombo (OpenUnitDual o) a b)%Q ->
(Qmax (SupDistanceToLinear (SplitL x o) H0)
(SupDistanceToLinear (SplitR x o) H1) ==
SupDistanceToLinear x (Qlt_trans _ _ _ H0 H1))%Q.
Lemma SupDistanceToLinear_wd2 : forall x1 x2 a b (H: a < b), x1 == x2 ->
(SupDistanceToLinear x1 H == SupDistanceToLinear x2 H)%Q.
Lemma SupDistanceToLinear_translate :
forall x c a b (H:a < b) (H0:a+c < b + c),
(SupDistanceToLinear x H == SupDistanceToLinear (constStepF (c:QS) + x) H0)%Q.
Lemma SupDistanceToLinear_scale :
forall x c a b (H:a < b) (H0:c*a < c*b),
(c*SupDistanceToLinear x H == SupDistanceToLinear (constStepF (c:QS) * x) H0)%Q.
This is the "transitivity" of the SupDistanceToLinear function.
Lemma SupDistanceToLinear_trans :
forall x y a b (H:a < b), StepFSupBall (SupDistanceToLinear x H + SupDistanceToLinear y H) x y.
forall x y a b (H:a < b), StepFSupBall (SupDistanceToLinear x H + SupDistanceToLinear y H) x y.
The stepSample p is as close to the virtual identity function as
we excpet.
Lemma stepSampleDistanceToId : (forall p, QposEq (@SupDistanceToLinear (stepSample p) 0 1 (@pos_one _)) (1#(2*p))).
Given a requested error of q, what is smallest n for stepFunction n
that will satifiy this error requirement.
Definition id01_raw_help (q:QposInf) : positive :=
match q with
|QposInfinity => 1%positive
|Qpos2Q+∞ q =>
match (Qceiling ((1#2)/q)%Qpos) with
| Zpos p => p
| _ => 1%positive
end
end.
Lemma id01_raw_help_le : forall (q:Qpos),
((1#2*id01_raw_help q) <= q)%Q.
match q with
|QposInfinity => 1%positive
|Qpos2Q+∞ q =>
match (Qceiling ((1#2)/q)%Qpos) with
| Zpos p => p
| _ => 1%positive
end
end.
Lemma id01_raw_help_le : forall (q:Qpos),
((1#2*id01_raw_help q) <= q)%Q.
Now define id01, the identity funciton on [0,1] as a bounded function,
to be the limit of these stepSample functions.
Definition id01_raw (q:QposInf) : StepQ := stepSample (id01_raw_help q).
Lemma id01_prf : is_RegularFunction (id01_raw:QposInf -> LinfStepQ).
Definition id01 : BoundedFunction :=
Build_RegularFunction id01_prf.
End id01.
Lemma id01_prf : is_RegularFunction (id01_raw:QposInf -> LinfStepQ).
Definition id01 : BoundedFunction :=
Build_RegularFunction id01_prf.
End id01.
StepFunctions distribute over Completion
The distribution function maps StepF (Complete X) to Complete (StepF X).
Definition distribComplete_raw (x:StepF CR) (e:QposInf) : LinfStepQ :=
StepFunction.Map (fun z => approximate z e) x.
Lemma distribComplete_prf : forall (x:StepF CR), is_RegularFunction (distribComplete_raw x).
Definition distribComplete (x:StepF CR) : BoundedFunction :=
Build_RegularFunction (distribComplete_prf x).
StepFunction.Map (fun z => approximate z e) x.
Lemma distribComplete_prf : forall (x:StepF CR), is_RegularFunction (distribComplete_raw x).
Definition distribComplete (x:StepF CR) : BoundedFunction :=
Build_RegularFunction (distribComplete_prf x).
Given a uniformly continuous function f, and a step function g,
the composition f o g is a bounded function. The map from g to f o g
is uniformly continuous with modulus mu f.
The same thing does not work for integrable functions becuase The map from g to f o g may not be uniformly continuous with modulus mu f. However, I have not found a counter example where f o g is not uniformly continuous. In fact, when f is lipschitz, then the map from g to f o g is Lipschitz. However Lipschitz functions haven't been formalzied yet.
The same thing does not work for integrable functions becuase The map from g to f o g may not be uniformly continuous with modulus mu f. However, I have not found a counter example where f o g is not uniformly continuous. In fact, when f is lipschitz, then the map from g to f o g is Lipschitz. However Lipschitz functions haven't been formalzied yet.
Definition ComposeContinuous_raw (f:Q_as_MetricSpace-->CR) (z:LinfStepQ) : BoundedFunction := dist (uc_stdFun f ^@> z).
Lemma ComposeContinuous_prf (f:Q_as_MetricSpace --> CR) :
is_UniformlyContinuousFunction (ComposeContinuous_raw f) (mu f).
Definition ComposeContinuous (f:Q_as_MetricSpace --> CR) : LinfStepQ --> BoundedFunction :=
Build_UniformlyContinuousFunction (ComposeContinuous_prf f).
Riemann-Stieltjes Integral
A measure on the reals is represented by the inverse of it's cumlative distribution function as a bounded function. So at the moment we can only integrate over bounded intervals. This effectively the Stieltjes integral ∫ f d(g^-1).
Definition IntegrateWithMeasure (f:Q_as_MetricSpace --> CR) : BoundedFunction --> CR :=
(uc_compose IntegrableFunction.Integral
(uc_compose BoundedAsIntegrable (Cbind (LinfStepQPrelengthSpace) (ComposeContinuous f)))).
(uc_compose IntegrableFunction.Integral
(uc_compose BoundedAsIntegrable (Cbind (LinfStepQPrelengthSpace) (ComposeContinuous f)))).
The Riemann Integral uses the uniform measure on [0,1]. The
inverse of it's cumlative distribution function is id01.
Definition Integrate01 f := IntegrateWithMeasure f id01.
Definition ContinuousSup01 f :=
(uc_compose sup (Cbind (LinfStepQPrelengthSpace) (ComposeContinuous f))) id01.
Definition ContinuousSup01 f :=
(uc_compose sup (Cbind (LinfStepQPrelengthSpace) (ComposeContinuous f))) id01.
Our integral on [0,1] is correct.