Strong IVT for partial functions
The IVT can be generalized to arbitrary partial functions; in the first part, we will simply do that, repeating the previous construction.
The same notations and conventions apply as before.
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).
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 and z [<] F y (incF _ Hy) ->
{xy0 : IR × IR | let x0 := fstT xy0 in let y0 := sndT xy0 in
{Hxy0 : (I x0) × (I y0) | let Hx0 := fstT Hxy0 in let Hy0 := sndT Hxy0 in
x0 [<] y0 and F x0 (incF _ Hx0) [<] z and z [<] F y0 (incF _ Hy0) |
y0[-]x0 [=] 2 [/]3[*] (y[-]x) /\ x [<=] x0 /\ y0 [<=] y}}.
Record IVT'_aux_seq_type : Type :=
{IVT'seq1 : IR;
IVT'seq2 : IR;
IVT'H1 : I IVT'seq1;
IVT'H2 : I IVT'seq2;
IVT'prf : IVT'seq1 [<] IVT'seq2;
IVT'z1 : F IVT'seq1 (incF _ IVT'H1) [<] z;
IVT'z2 : z [<] F IVT'seq2 (incF _ IVT'H2)}.
Definition IVT'_iter : IVT'_aux_seq_type -> IVT'_aux_seq_type.
Defined.
Definition IVT'_seq : N -> IVT'_aux_seq_type.
Defined.
Definition a'_seq n := IVT'seq1 (IVT'_seq n).
Definition b'_seq n := IVT'seq2 (IVT'_seq n).
Definition a'_seq_I n : I (a'_seq n) := IVT'H1 (IVT'_seq n).
Definition b'_seq_I n : I (b'_seq n) := IVT'H2 (IVT'_seq n).
Lemma a'_seq_less_b'_seq : forall n, a'_seq n [<] b'_seq n.
Lemma a'_seq_less_z : forall n, F _ (incF _ (a'_seq_I n)) [<] z.
Lemma z_less_b'_seq : forall 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'.
Other formulations
We now generalize the various statements of the intermediate value theorem to more widely applicable forms.
Lemma Weak_IVT : forall I F, Continuous I F -> forall a b Ha Hb (HFab : F a Ha [<] F b Hb),
I a -> I b -> forall e, 0 [<] e -> forall y, Compact (less_leEq _ _ _ HFab) y ->
{x : IR | Compact (Min_leEq_Max a b) x | forall Hx, AbsIR (F x Hx[-]y) [<=] e}.
Lemma IVT_inc : forall I F, Continuous I F -> forall a b Ha Hb, F a Ha [#] F b Hb ->
I a -> I b -> (forall x y, I x -> I y -> x [<] y -> forall Hx Hy, F x Hx [<] F y Hy) ->
forall y, Compact (Min_leEq_Max (F a Ha) (F b Hb)) y ->
{x : IR | Compact (Min_leEq_Max a b) x | forall Hx, F x Hx [=] y}.
Lemma IVT_dec : forall I F, Continuous I F -> forall a b Ha Hb, F a Ha [#] F b Hb ->
I a -> I b -> (forall x y, I x -> I y -> x [<] y -> forall Hx Hy, F y Hy [<] F x Hx) ->
forall y, Compact (Min_leEq_Max (F a Ha) (F b Hb)) y ->
{x : IR | Compact (Min_leEq_Max a b) x | forall Hx, F x Hx [=] y}.
Lemma IVT'_inc : forall I F, Continuous I F -> forall a b Ha Hb, F a Ha [#] F b Hb ->
I a -> I b -> (forall x y, I x -> I y -> x [<] y -> forall Hx Hy, F x Hx [<] F y Hy) ->
forall y, (⋅,⋅) (Min (F a Ha) (F b Hb)) (Max (F a Ha) (F b Hb)) y ->
{x : IR | (⋅,⋅) (Min a b) (Max a b) x | forall Hx, F x Hx [=] y}.
Lemma IVT'_dec : forall I F, Continuous I F -> forall a b Ha Hb, F a Ha [#] F b Hb ->
I a -> I b -> (forall x y, I x -> I y -> x [<] y -> forall Hx Hy, F y Hy [<] F x Hx) ->
forall y, (⋅,⋅) (Min (F a Ha) (F b Hb)) (Max (F a Ha) (F b Hb)) y ->
{x : IR | (⋅,⋅) (Min a b) (Max a b) x | forall Hx, F x Hx [=] y}.