19.2 A trivial part of Sarkovskii’s theorem
今回は，連続関数の性質です．まず，f:real->realがx:realにおいて連続であることは，中置き演算子 cont(locally continuous) により，f contl xと表され，thmとしては
# REWRITE_CONV[contl]`f contl x`;;
val it : thm = |- f contl x <=> ( (\h. f (x + h) ) tends_real_real f x) (&0)
のように参照できます．これを所謂イプシロンデルタ流に表すと
# REWRITE_CONV[contl;LIM; REAL_SUB_RZERO]`f contl x`;;
val it : thm =
|- f contl x <=>
(!e. &0 < e
==> (?d. &0 < d /\
(!x'. &0 < abs x' /\ abs x' < d
==> abs (f (x + x') - f x) < e)))
或いは，REWRITE_RULEにより，thmとして書き換えて
# REWRITE_RULE[LIM; REAL_SUB_RZERO] contl;;
val it : thm =
|- !f x.
f contl x <=>
(!e. &0 < e
==> (?d. &0 < d /\
(!x'. &0 < abs x' /\ abs x' < d
==> abs (f (x + x') - f x) < e)))
となります．
連続関数の性質のうち，最も基本的なものの一つが中間値定理(intermediate
value theorem)
# IVT;;
val it : thm =
|- !f a b y.
a <= b /\
(f a <= y /\ y <= f b) /\
(!x. a <= x /\ x <= b ==> f contl x)
==> (?x. a <= x /\ x <= b /\ f x = y)
# IVT2;;
val it : thm =
|- !f a b y.
a <= b /\
(f b <= y /\ y <= f a) /\
(!x. a <= x /\ x <= b ==> f contl x)
==> (?x. a <= x /\ x <= b /\ f x = y)
です．これと
# REAL_LE_TOTAL;;
val it : thm = |- !x y. x <= y \/ y <= x
を参照すると，y=0の場合の
# MESON[IVT;IVT2;REAL_LE_TOTAL]`a<=b /\ f a<= &0 /\ &0<=f b /\ (!t. (a<=t /\ t<=
b)==>(f contl t)) ==> ?x. ( a<=x /\ x<=b /\ &0=f x)`;;
0..0..0..0..2..5..8..24..42..64..92..122..152..224..297..390..561..738..931..156
0..2260..3125..4239..5504..6828..8609..10513..12597..15938..19409..23486..29174.
.solved at 32460
val it : thm =
|- a <= b /\ f a <= &0 /\ &0 <= f b /\ (!t. a <= t /\ t <= b ==> f contl t)
==> (?x. a <= x /\ x <= b /\ &0 = f x)
や全空間における
# let IVT_LEMMA1 =MESON[IVT;IVT2;REAL_LE_TOTAL]`(!t. f contl t) /\ (?a. f a <= &
0 ) /\ (?b. &0<=f b) ==> ?c. f c= &0`;;
0..0..1..2..5..9..33..72..111..240..419..solved at 561
val ( IVT_LEMMA1 ) : thm =
|- (!t. f contl t) /\ (?a. f a <= &0) /\ (?b. &0 <= f b) ==> (?c. f c = &0)
が得られ，更に不動点に関連してf(x)-xに適用した形を証明するなら
# g(`(!t. f contl t) /\ (?a. f a <= a ) /\ (?b. b <= f b) ==> ?c. f c=c`);;
Warning: Free variables in goal: f
val it : goalstack = 1 subgoal (1 total)`(!t. f contl t) /\ (?a. f a <= a) /\ (?b. b <= f b) ==> (?c. f c = c)`
# e(REPEAT STRIP_TAC);;
val it : goalstack = 1 subgoal (1 total)0 [`!t. f contl t`]
1 [`f a <= a`]
2 [`b <= f b`]`?c. f c = c`
# e(MP_TAC (INST[`(\x:real. f(x)-x)`,`f:real->real`]IVT_LEMMA1) );;
val it : goalstack = 1 subgoal (1 total)0 [`!t. f contl t`]
1 [`f a <= a`]
2 [`b <= f b`]`*1
==> (?c. f c = c)`# e(ASM_SIMP_TAC[CONT_X;CONT_SUB;REAL_ARITH`f a - a <= &0 <=> f a<=a`;REAL_ARITH
`&0<= f b - b <=> b <= f b`;REAL_ARITH`f c - c = &0<=> f c=c`;]);;
val it : goalstack = 1 subgoal (1 total)0 [`!t. f contl t`]
1 [`f a <= a`]
2 [`b <= f b`]`( (?a. f a <= a) /\ (?b. b <= f b) ==> (?c. f c = c)) ==> (?c. f c = c)`
# e(ASM_MESON_TAC[]);;
0..0..solved at 2
0..0..solved at 2
0..0..solved at 2
val it : goalstack = No subgoals# let IVT_LEMMA2=top_thm();;
val ( IVT_LEMMA2 ) : thm =
|- (!t. f contl t) /\ (?a. f a <= a) /\ (?b. b <= f b) ==> (?c. f c = c)
となります．
これを用いて，f:R->Rが連続関数のとき
∃x.f(f(f(x)))=x ==> ∃x.f(x)=x
を証明すると
# g(`(!t. f contl t) ==> (?x. f( f( f(x)))=x)==>(?x. f(x)=x)`);;
Warning: Free variables in goal: f
val it : goalstack = 1 subgoal (1 total)`(!t. f contl t) ==> (?x. f (f (f x)) = x) ==> (?x. f x = x)`
# e(STRIP_TAC);;
val it : goalstack = 1 subgoal (1 total)0 [`!t. f contl t`]
`(?x. f (f (f x)) = x) ==> (?x. f x = x)`
# e(ONCE_REWRITE_TAC[GSYM(CONTRAPOS_THM)]);;
val it : goalstack = 1 subgoal (1 total)0 [`!t. f contl t`]
`~(?x. f x = x) ==> ~(?x. f (f (f x)) = x)`
# e(MP_TAC(ONCE_REWRITE_RULE[MESON[]`(p/\q==>r)<=>(p/\(~r)==>(~q))`]IVT_LEMMA2))
;;
val it : goalstack = 1 subgoal (1 total)0 [`!t. f contl t`]
`( (!t. f contl t) /\ ~(?c. f c = c) ==> ~*2 = x)`
# e (ASM_REWRITE_TAC[DE_MORGAN_THM;NOT_EXISTS_THM;REAL_NOT_LE;]);;
val it : goalstack = 1 subgoal (1 total)0 [`!t. f contl t`]
`( (!c. ~(f c = c)) ==> (!a. a < f a) \/ (!b. f b < b))
==> (!x. ~(f x = x))
==> (!x. ~(f (f (f x)) = x))`# e(MESON_TAC[REAL_LT_TRANS;REAL_NOT_EQ;]);;
0..0..solved at 2
0..0..1..9..25..74..211..solved at 301
0..0..1..9..25..73..210..solved at 424
val it : goalstack = No subgoals# let SARKOVSKII_TRIVIAL=top_thm();;
val ( SARKOVSKII_TRIVIAL ) : thm =
|- (!t. f contl t) ==> (?x. f (f (f x)) = x) ==> (?x. f x = x)
のようになります．
また，MESONは対偶を知っているので，ある程度の指針を与え，不等式についてのthmを参照させれば
# let SARKOVSKII_TRIVIAL = prove(
`(!t. f contl t) /\ (?x. f(f(f(x)))=x) ==> (?x. f(x)=x)` ,
MP_TAC(ONCE_REWRITE_RULE[MESON[]`(p/\q==>r)<=>(p/\(~r)==>(~q))`]IVT_LEMMA2) T
HEN
MESON_TAC[IVT_LEMMA2;REAL_NOT_LE;REAL_LT_TRANS;REAL_NOT_EQ;] );;
0..0..solved at 2
0..0..solved at 2
0..0..2..12..33..76..193..421..1047..2751..6346..solved at 6580
0..0..2..12..33..75..188..406..1000..2632..6049..solved at 6280
val ( SARKOVSKII_TRIVIAL ) : thm =
|- (!t. f contl t) /\ (?x. f (f (f x)) = x) ==> (?x. f x = x)
のように証明してくれます．
なお，チュートリアルでは，(?x. f (f (f x)) = x)のとき，
`x <= f x \/ f x <= f (f x) \/ f (f x) <= f (f (f x))`および`f x <= x \/ f (f x) <= f x \/ f (f (f x)) <= f (f x)`が成り立つことから，x,f(x),f( f( x ) )に対してIVT_LEMMA2を適用して
# let SARKOVSKII_TRIVIAL = prove
(`!f:real->real. (!x. f contl x) /\ (?x. f(f(f(x))) = x) ==> ?x. f(x) = x`,
REPEAT STRIP_TAC THEN MATCH_MP_TAC IVT_LEMMA2 THEN ASM_REWRITE_TAC THEN
CONJ_TAC THEN MATCH_MP_TAC
(MESON `P x \/ P (f x) \/ P (f(f x)) ==> ?x:real. P x`) THEN
FIRST_ASSUM(UNDISCH_TAC o check is_eq o concl) THEN REAL_ARITH_TAC);;
0..0..solved at 2
0..0..solved at 2
0..0..solved at 2
val ( SARKOVSKII_TRIVIAL ) : thm =
|- !f. (!x. f contl x) /\ (?x. f (f (f x)) = x) ==> (?x. f x = x)
のように証明しています．
