Intermediate Value Theorem
Nested intervals
Let a,b:nat->IR be sequences such that:
- a is increasing;
- b is decreasing;
- forall (i:nat), (a i) < (b i);
- for every positive real number ε, there is an i such that (b i) < (a i) +ε.
Variables a b : N -> IR.
Hypothesis a_mon : forall i : N, a i [<=] a (S i).
Hypothesis b_mon : forall i : N, b (S i) [<=] b i.
Hypothesis a_b : forall i : N, a i [<] b i.
Hypothesis b_a : forall ε : IR, 0 [<] ε -> {i : N | b i [<=] a i[+]ε}.
Lemma a_mon' : forall i j : N, i <= j -> a i [<=] a j.
Lemma b_mon' : forall i j : N, i <= j -> b j [<=] b i.
Lemma a_b' : forall i j : N, a i [<] b j.
Lemma intervals_cauchy : Cauchy_prop a.
Lemma Cnested_intervals_limit : {z : IR | forall i, a i [<=] z | forall i, z [<=] b i}.
Let f be a continuous real function.
Variable f : CSetoid_un_op IR.
Hypothesis f_contin : contin f.
Lemma f_contin_pos : forall z : IR, 0 [<] f z ->
{ε : IR | 0 [<] ε | forall x, x [<=] z[+]ε -> z [<=] x[+]ε -> 0 [<] f x}.
Lemma f_contin_neg : forall z : IR, f z [<] 0 ->
{ε : IR | 0 [<] ε | forall x, x [<=] z[+]ε -> z [<=] x[+]ε -> f x [<] 0}.
Assume also that forall i, f (a i) ≤ 0 ≤ f (b i).
Hypothesis f_a : forall i, f (a i) [<=] 0.
Hypothesis f_b : forall i, 0 [<=] f (b i).
Lemma Cnested_intervals_zero : {z : IR | a 0 [<=] z /\ z [<=] b 0 /\ f z [=] 0}.
End Nested_Intervals.
Section Bisection.
Variable f : CSetoid_un_op IR.
Hypothesis f_apzero_interval :
forall a b, a [<] b -> {c : IR | a [<=] c /\ c [<=] b | f c [#] 0}.
Variables a b : IR.
Hypothesis a_b : a [<] b.
Hypothesis f_a : f a [<=] 0.
Hypothesis f_b : 0 [<=] f b.
Let Small denote 2/3, lft be (2×a+b) /3 and rht be (a+2×b) /3.
Lemma a_lft : a [<] lft.
Lemma rht_b : rht [<] b.
Lemma lft_rht : lft [<] rht.
Lemma smaller_lft : rht[-]a [=] Small[*] (b[-]a).
Lemma smaller_rht : b[-]lft [=] Small[*] (b[-]a).
Lemma Cbisect' : {a' : IR | {b' : IR |
a' [<] b' | a [<=] a' /\ b' [<=] b /\ b'[-]a' [<=] Small[*] (b[-]a) /\ f a' [<=] 0 /\ 0 [<=] f b'}}.
End Bisection.
Section Bisect_Interval.
Variable f : CSetoid_un_op IR.
Hypothesis C_f_apzero_interval :
forall a b, a [<] b -> {c : IR | a [<=] c /\ c [<=] b | f c [#] 0}.
Record bisect_interval : Type :=
{interval_lft : IR;
interval_rht : IR;
interval_lft_rht : interval_lft [<] interval_rht;
interval_f_lft : f interval_lft [<=] 0;
interval_f_rht : 0 [<=] f interval_rht}.
Lemma Cbisect_exists : forall I : bisect_interval, {I' : bisect_interval |
interval_rht I'[-]interval_lft I' [<=] Small[*] (interval_rht I[-]interval_lft I) /\
interval_lft I [<=] interval_lft I' /\ interval_rht I' [<=] interval_rht I}.
Definition bisect I : bisect_interval := ProjT1 (Cbisect_exists I).
Lemma bisect_prop : forall I : bisect_interval,
interval_rht (bisect I) [-]interval_lft (bisect I) [<=] Small[*] (interval_rht I[-]interval_lft I)
/\ interval_lft I [<=] interval_lft (bisect I) /\ interval_rht (bisect I) [<=] interval_rht I.
End Bisect_Interval.
Section IVT_Op.
Variable f : CSetoid_un_op IR.
Hypothesis f_contin : contin f.
Hypothesis f_apzero_interval :
forall a b, a [<] b -> {c : IR | a [<=] c /\ c [<=] b | f c [#] 0}.
Variables a b : IR.
Hypothesis a_b : a [<] b.
Hypothesis f_a : f a [<=] 0.
Hypothesis f_b : 0 [<=] f b.
Fixpoint interval_sequence (n : N) : bisect_interval f :=
match n with
| O => Build_bisect_interval f a b a_b f_a f_b
| S m => bisect f f_apzero_interval (interval_sequence m)
end.
Let a_ (i : N) := interval_lft _ (interval_sequence i).
Let b_ (i : N) := interval_rht _ (interval_sequence i).
Lemma intervals_smaller : forall i, b_ i[-]a_ i [<=] Small[^]i[*] (b[-]a).
Lemma intervals_small'' : forall i : N, Small[^]i[*]nring i [<=] 1.
Lemma intervals_small' : forall ε, 0 [<] ε -> {i : N | Small[^]i[*] (b[-]a) [<=] ε}.
Lemma intervals_small : forall ε, 0 [<] ε -> {i : N | b_ i [<=] a_ i[+]ε}.
Lemma Civt_op : {z : IR | a [<=] z /\ z [<=] b /\ f z [=] 0}.
End IVT_Op.
Section IVT_Poly.
Lemma Civt_poly : forall f : cpoly_cring IR, f [#] 0 ->
forall a b, a [<] b -> f ! a [<=] 0 -> 0 [<=] f ! b -> {x : IR | a [<=] x /\ x [<=] b /\ f ! x [=] 0}.
End IVT_Poly.