src/probability/real_topologyScript.sml

646 val linear = new_definition ("linear",
647   ``linear (f:real->real) <=>
652  ``!c. linear(\x:real. c * x)``,
653  SIMP_TAC std_ss [linear] THEN REAL_ARITH_TAC);
656  ``!f c. linear f ==> linear (\x. c * f(x))``,
657   SIMP_TAC std_ss [linear] THEN REPEAT STRIP_TAC THEN REAL_ARITH_TAC);
660  ``!f. linear f ==> linear (\x. -(f(x)))``,
661   SIMP_TAC std_ss [linear] THEN REPEAT STRIP_TAC THEN REAL_ARITH_TAC);
664  ``!f g. linear f /\ linear g ==> linear (\x. f(x) + g(x))``,
665   SIMP_TAC std_ss [linear] THEN REPEAT STRIP_TAC THEN REAL_ARITH_TAC);
668  ``!f g. linear f /\ linear g ==> linear (\x. f(x) - g(x))``,
669   SIMP_TAC std_ss [linear] THEN REPEAT STRIP_TAC THEN REAL_ARITH_TAC);
672  ``!f g. linear f /\ linear g ==> linear (g o f)``,
673   SIMP_TAC std_ss [linear, o_THM]);
676  ``linear (\x. x)``,
677   SIMP_TAC std_ss [linear]);
680  ``linear (\x. 0)``,
681   SIMP_TAC std_ss [linear] THEN CONJ_TAC THEN REAL_ARITH_TAC);
684  ``linear (\x. -x)``,
685   SIMP_TAC std_ss [linear] THEN REAL_ARITH_TAC);
688  ``!f s. FINITE s /\ (!a. a IN s ==> linear(f a))
689          ==> linear(\x. sum s (\a. f a x))``,
691   KNOW_TAC ``((!a. a IN s ==> linear (f a)) ==> linear (\x. sum s (\a. f a x))) =
692          (\s. (!a. a IN s ==> linear (f a)) ==> linear (\x. sum s (\a. f a x))) s`` THENL
696   KNOW_TAC ``(linear (\x. f e x + sum s (\a. f a x))) =
697               linear (\x. (\x. f e x) x + (\x. sum s (\a. f a x)) x)`` THENL
703      linear f ==> linear (\x. f(x) * v)``,
704   SIMP_TAC std_ss [linear] THEN REPEAT STRIP_TAC THEN REAL_ARITH_TAC);
707  ``!f. linear f ==> (f(0) = 0)``,
708   METIS_TAC [REAL_MUL_LZERO, linear]);
711  ``!f c x. linear f ==> (f(c * x) = c * f(x))``,
712   SIMP_TAC std_ss [linear]);
715  ``!f x. linear f ==> (f(-x) = -(f x))``,
719  ``!f x y. linear f ==> (f(x + y) = f(x) + f(y))``,
720   SIMP_TAC std_ss [linear]);
723  ``!f x y. linear f ==> (f(x - y) = f(x) - f(y))``,
727  ``!f g s. linear f /\ FINITE s ==> (f(sum s g) = sum s (f o g))``,
739         linear f /\ FINITE s
748  ``!f:real->real. linear f ==> ?B. !x. abs(f x) <= B * abs(x)``,
761  ``!f:real->real. linear f ==> ?B. &0 < B /\ !x. abs(f x) <= B * abs(x)``,
771  ``!f s. (!x. x IN s ==> -x IN s) /\ linear f
781   ``bilinear f <=> (!x. linear(\y. f x y)) /\ (!y. linear(\x. f x y))``);
790   SIMP_TAC std_ss [bilinear, linear]);
794   SIMP_TAC std_ss [bilinear, linear]);
798   SIMP_TAC std_ss [bilinear, linear]);
802   SIMP_TAC std_ss [bilinear, linear]);
840   KNOW_TAC ``(!x. linear (\y. h:real->real->real x y)) = (!x. linear (h x))`` THENL
844   KNOW_TAC ``((!y. linear (\x. h:real->real->real x y)) /\ FINITE s) =
845              ((!y. linear (\x. h x y) /\ FINITE s))`` THENL
900       FULL_SIMP_TAC std_ss [bilinear, linear]], FULL_SIMP_TAC std_ss [bilinear, linear],
926 (* A bit of linear algebra.                                                  *)
987  ``!f s. linear f /\ subspace s ==> subspace(IMAGE f s)``,
990   METIS_TAC [linear, LINEAR_0]);
993  ``!f s. linear f /\ subspace s ==> subspace {x | f(x) IN s}``,
995   METIS_TAC [linear, LINEAR_0]);
1011         linear f /\ subspace s
1615  ``!f a b. linear f ==> (midpoint(f a,f b) = f(midpoint(a,b)))``,
2018  ``!f b. independent b ==> ?g:real->real. linear g /\ (!x. x IN b ==> (g x = f x))``,
2027   ASM_SIMP_TAC std_ss [INDEPENDENT_BOUND, linear] THEN
2031  ``!f. linear f ==> subspace {x | f(x) = 0}``,
2037  ``!f:real->real b. linear f /\ (!x. x IN b ==> (f(x) = 0))
2047  ``!f b s. linear f /\ s SUBSET (span b) /\
2052  ``!f g b s. linear f /\ linear g /\ s SUBSET (span b) /\
2059  ``!f:real->real g. linear f /\ linear g /\
2076  ``!f:real->real. linear f /\ (!x y. (f x = f y) ==> (x = y))
2077                   ==> ?g. linear g /\ (g o f = (\x. x))``,
2079   SUBGOAL_THEN ``?h. linear(h:real->real) /\
2087    FULL_SIMP_TAC std_ss [linear] THEN KNOW_TAC ``0 = (f:real->real) 0`` THENL
2200  ``!f:real->real s. independent s /\ linear f /\
2231  ``!f:real->real s. independent s /\ linear f /\
2237  ``!f:real->real s. linear f ==> (span(IMAGE f s) = IMAGE f (span s))``,
2261  ``!f:real->real. linear f /\ (!x y. (f(x) = f(y)) ==> (x = y))
2275 (* Left-invertible linear transformation has a lower bound.                  *)
2279  ``!f:real->real g. linear f /\ linear g /\ (g o f = I)
2294  ``!f:real->real g. linear f /\ linear g /\ (g o f = I) ==>
2299  ``!f:real->real. linear f /\ (!x y. (f x = f y) ==> (x = y))
2853         linear f /\ (!y. ?x. f x = y) /\ (!x. abs(f x) = abs x)
2856   SIMP_TAC std_ss [linear, IN_IMAGE, dist, EXTENSION, GSPECIFICATION] THEN
2879         linear f /\ (!y. ?x. f x = y) /\ (!x. abs(f x) = abs x)
2882   SIMP_TAC std_ss [linear, IN_IMAGE, dist, EXTENSION, GSPECIFICATION] THEN
2905         linear f /\ (!y. ?x. f x = y) /\ (!x. abs(f x) = abs x)
2908   SIMP_TAC std_ss [linear, IN_IMAGE, dist, EXTENSION, GSPECIFICATION] THEN
3424  ``!f a b. linear f
3433         linear f /\ (!x y. (f x = f y) ==> (x = y))
3436   SIMP_TAC std_ss [linear, IN_IMAGE, dist, EXTENSION, GSPECIFICATION, IN_DIFF] THEN
6228         (f --> l) net /\ linear h ==> ((\x. h(f x)) --> h l) net``,
6249   REWRITE_TAC [linear] THEN REAL_ARITH_TAC);
7380  ``!f:real->real s. bounded s /\ linear f ==> bounded(IMAGE f s)``,
9483  ``!f:real->real s. linear f ==> f uniformly_continuous_on s``,
9650   REWRITE_TAC[bilinear, linear] THEN BETA_TAC THEN REAL_ARITH_TAC);
9672   REWRITE_TAC [linear] THEN BETA_TAC THEN REAL_ARITH_TAC);
9980  ``!f. linear f ==> (f --> 0) (at (0))``,
9989  ``!f:real->real a. linear f ==> f continuous (at a)``,
9992   KNOW_TAC ``linear (\x. f (a + x) - f a)`` THENL
9993   [POP_ASSUM MP_TAC THEN SIMP_TAC std_ss [linear] THEN
10000  ``!f:real->real s x. linear f ==> f continuous (at x within s)``,
10004  ``!f:real->real s. linear f ==> f continuous_on s``,
10009    f continuous net /\ linear g ==> (\x. g(f x)) continuous net``,
10014     f continuous_on s /\ linear g ==> (\x. g(f x)) continuous_on s``,
10021   SUBGOAL_THEN ``linear(\x:real. x)`` MP_TAC THENL
10049 SIMP_TAC std_ss [bilinear, linear] THEN REAL_ARITH_TAC);
10121  ``!f:real->real s. compact s /\ linear f ==> compact(IMAGE f s)``,
10160  ``!f:real->real s. connected s /\ linear f ==> connected(IMAGE f s)``,
13508   REWRITE_TAC[bilinear, linear] THEN BETA_TAC THEN
13663   REWRITE_TAC[linear] THEN CONJ_TAC THEN SIMP_TAC std_ss [] THEN REAL_ARITH_TAC);
13671   REWRITE_TAC[linear] THEN CONJ_TAC THEN SIMP_TAC std_ss [] THEN REAL_ARITH_TAC);
13679   REWRITE_TAC[linear] THEN CONJ_TAC THEN SIMP_TAC std_ss [] THEN REAL_ARITH_TAC);
13687   REWRITE_TAC[linear] THEN CONJ_TAC THEN SIMP_TAC std_ss [] THEN REAL_ARITH_TAC);
13741         linear f /\ (!x. abs(f x) = abs x)
16212         linear f /\ (!x y. (f x = f y) ==> (x = y))
16233         linear f /\ (!x y. (f x = f y) ==> (x = y))
16244         linear f /\ (!x y. (f x = f y) ==> (x = y))
17546 (* "Isometry" (up to constant bounds) of injective linear map etc.           *)
17552         linear f /\ (!x. x IN s ==> abs(f x) >= e * abs(x)) /\
17567         linear f /\ (!x. x IN s ==> abs(f x) >= e * abs(x)) /\
17586         linear f /\ (!x. x IN s /\ (f x = 0) ==> (x = 0))
17640   UNDISCH_TAC ``linear f`` THEN DISCH_TAC THEN
17651          linear f /\
17662 (* Relating linear images to open/closed/interior/closure.                   *)
17667         linear f /\ (!y. ?x. f x = y)
17707         linear f /\ (!x y. (f x = f y) ==> (x = y)) /\ (!y. ?x. f x = y)
17718         linear f /\ (!x y. (f x = f y) ==> (x = y))
17746         linear f /\ (!x y. (f x = f y) ==> (x = y))
17757         linear f ==> IMAGE f (closure s) SUBSET closure(IMAGE f s)``,
17764         linear f /\ (!x y. (f x = f y) ==> (x = y))
17774         linear f /\ bounded s
17786         linear f /\ (!x y. (f x = f y) ==> (x = y))
17792         linear f /\ (!y. ?x. f x = y)
17800         linear f /\ (!x y. (f x = f y) ==> (x = y)) /\ (!y. ?x. f x = y)
17843         linear f /\ linear g /\ (f o g = I) /\ x IN interior s
17853         linear f /\ linear g /\ (f o g = I)
17861         linear f /\ (!x y. (f x = f y) ==> (x = y))
17868         linear f /\ (!x y. (f x = f y) ==> (x = y))
17874         linear f /\ (!x y. (f x = f y) ==> (x = y))
17880         linear f /\ (!x y. (f x = f y) ==> (x = y))
17918   SIMP_TAC std_ss [linear] THEN REPEAT CONJ_TAC THEN REAL_ARITH_TAC);
17933   SIMP_TAC std_ss [linear] THEN REPEAT CONJ_TAC THEN REAL_ARITH_TAC);
18146  ``!f h l s. (f sums l) s /\ linear h ==> ((\n. h(f n)) sums h l) s``,
18281  ``!f h s. summable s f /\ linear h ==> summable s (\n. h(f n))``,
18471  ``!f h s. summable s f /\ linear h
19121    [SIMP_TAC std_ss [bilinear, linear] THEN
19935         linear f /\ (!x. abs(f x) = abs x)
20567            linear f /\ (!x. abs(f x) = abs x)
21595         (!f s. linear f /\ (!x y. (f x = f y) ==> (x = y))
21597         ==>  (!f s. linear f /\ (!x y. (f x = f y) ==> (x = y))
21601   ASM_CASES_TAC ``linear(f:real->real) /\ (!x y. (f x = f y) ==> (x = y))`` THEN