IVT for Partial Functions

In general, we cannot prove the classically valid Intermediate Value Theorem for arbitrary partial functions, which states that in any interval [a,b], for any value z between f(a) and f(b) there exists x∈[a,b] such that f(x) = z.

However, as is usually the case, there are some good aproximation results. We will prove them here.

Section Lemma1.

Variables a b : IR.
Hypothesis Hab : a [<=] b.

Variable F : PartIR.
Hypothesis contF : Continuous_I Hab F.

First Lemmas

Let a, b : IR and Hab : a ≤ b and denote by I the interval [a,b]. Let F be a continuous function on I.

We begin by proving that, if f(a) < f(b), then for every y in [f(a),f(b)] there is an x∈[a,b] such that f(x) is close enough to z.

Lemma Weak_IVT_ap_lft : forall Ha Hb (HFab : F a Ha [<] F b Hb) e,
0 [<] e -> forall z, Compact (less_leEq _ _ _ HFab) z ->
{x : IR | Compact Hab x | forall Hx, AbsIR (F x Hx[-]z) [<=] e}.

End Lemma1.

Section Lemma2.

Variables a b : IR.
Hypothesis Hab : a [<=] b.

Variable F : PartIR.
Hypothesis contF : Continuous_I Hab F.

If f(b) < f(a), a similar result holds:

Lemma Weak_IVT_ap_rht : forall Ha Hb (HFab : F b Hb [<] F a Ha) e,
0 [<] e -> forall z, Compact (less_leEq _ _ _ HFab) z ->
{x : IR | Compact Hab x | forall Hx, AbsIR (F x Hx[-]z) [<=] e}.

End Lemma2.

Section IVT.

The IVT

We will now assume that a < b and that F is not only continuous, but also strictly increasing in I. Under these assumptions, we can build two sequences of values which converge to x0 such that f(x0) = z.

Variables a b : IR.
Hypothesis Hab' : a [<] b.
Hypothesis Hab : a [<=] b.

Variable F : PartIR.
Hypothesis contF : Continuous_I Hab F.

Hypothesis incrF : forall x y, I x -> I y -> x [<] y -> forall Hx Hy, F x Hx [<] F y Hy.

Variable z : IR.
Hypothesis Haz : F a (incF _ Ha) [<=] z.
Hypothesis Hzb : z [<=] F b (incF _ Hb).

Given any two points x < y in [a,b] such that x ≤ z ≤ y, we can find x' < y' such that |x'-y'|=2/3|x-y| and x' ≤ z ≤ y'.

Lemma IVT_seq_lemma : forall (xy : IR × IR) (x:=fstT xy) (y:=sndT xy)
(Hxy : (I x) × (I y)) (Hx := fstT Hxy) (Hy := sndT Hxy), x [<] y ->
F x (incF _ Hx) [<=] z /\ z [<=] F y (incF _ Hy) ->
{xy0 : IR × IR | let x0 := fstT xy0 in let y0 := sndT xy0 in
{Hxy0 : (I x0) × (I y0) | x0 [<] y0 | let Hx0 := fstT Hxy0 in let Hy0 := sndT Hxy0 in
F x0 (incF _ Hx0) [<=] z /\ z [<=] F y0 (incF _ Hy0) /\
y0[-]x0 [=] 2 [/]3[*] (y[-]x) /\ x [<=] x0 /\ y0 [<=] y}}.

We now iterate this construction.

Record IVT_aux_seq_type : Type :=
  {IVTseq1 : IR;
   IVTseq2 : IR;
   IVTH1 : I IVTseq1;
   IVTH2 : I IVTseq2;
   IVTprf : IVTseq1 [<] IVTseq2;
   IVTz1 : F IVTseq1 (incF _ IVTH1) [<=] z;
   IVTz2 : z [<=] F IVTseq2 (incF _ IVTH2)}.

Definition IVT_iter : IVT_aux_seq_type -> IVT_aux_seq_type.
Defined.

Definition IVT_seq : N -> IVT_aux_seq_type.
Defined.

We now define the sequences built from this iteration, starting with a and b.

Definition a_seq (n : N) := IVTseq1 (IVT_seq n).
Definition b_seq (n : N) := IVTseq2 (IVT_seq n).

Definition a_seq_I (n : N) : I (a_seq n) := IVTH1 (IVT_seq n).
Definition b_seq_I (n : N) : I (b_seq n) := IVTH2 (IVT_seq n).

Lemma a_seq_less_b_seq : forall n : N, a_seq n [<] b_seq n.

Lemma a_seq_leEq_z : forall n : N, F _ (incF _ (a_seq_I n)) [<=] z.

Lemma z_leEq_b_seq : forall n : N, z [<=] F _ (incF _ (b_seq_I n)).

Lemma a_seq_mon : forall i : N, a_seq i [<=] a_seq (S i).

Lemma b_seq_mon : forall i : N, b_seq (S i) [<=] b_seq i.

Lemma a_seq_b_seq_dist_n : forall n, b_seq (S n) [-]a_seq (S n) [=] 2 [/]3[*] (b_seq n[-]a_seq n).

Lemma a_seq_b_seq_dist : forall n, b_seq n[-]a_seq n [=] (2 [/]3) [^]n[*] (b[-]a).

Lemma a_seq_Cauchy : Cauchy_prop a_seq.

Lemma b_seq_Cauchy : Cauchy_prop b_seq.

Let xa := Lim (Build_CauchySeq _ _ a_seq_Cauchy).
Let xb := Lim (Build_CauchySeq _ _ b_seq_Cauchy).

Lemma a_seq_b_seq_lim : xa [=] xb.

Lemma xa_in_interval : I xa.

Lemma IVT_I : {x : IR | I x | forall Hx, F x Hx [=] z}.

End IVT.