|
linear_transformations_2D: THEORY
%----------------------------------------------------------------------------
%------------linear transformations over vect2-------------------------------
%------------Original Date: Dec 15, 2009-------------------------------------
%----------------------------------------------------------------------------
%------------Authors: Anthony Narkawicz, NASA--------------------------------
%----------------------------------------------------------------------------
%----------------------------------------------------------------------------
%----------------------------------------------------------------------------
BEGIN
IMPORTING vectors_2D, det_2D, basis_2D
u,v,w : VAR Vector
a,b,c : VAR real
nza : VAR nzreal
L,J : VAR [Vector -> Vector] % Linear Transformations
F,G : VAR [Vector -> real] % Linear Functionals
% LINEAR TRANSFORMATIONS
linear_transform?(L): bool =
FORALL (u,v: Vector): FORALL (a,b: real): L(a*u+b*v) = a*L(u) + b*L(v)
% Basic Properties
linear_transform_zero: LEMMA
linear_transform?(L) IMPLIES L(zero) = zero
linear_transform_scal: LEMMA
linear_transform?(L) IMPLIES
FORALL (u: Vector, a: real): L(a*u) = a*L(u)
linear_transform_add: LEMMA
linear_transform?(L) IMPLIES
FORALL (u,v: Vector): L(u+v) = L(u) + L(v)
linear_transform_sub: LEMMA
linear_transform?(L) IMPLIES
FORALL (u,v: Vector): L(u-v) = L(u) - L(v)
% Equivalent Characterizations
linear_transform_rew: LEMMA linear_transform?(L) IFF
(FORALL (u,v: Vector): L(u+v) = L(u) + L(v)) AND
(FORALL (u: Vector, a: real): L(a*u) = a*L(u))
linear_transform_alt_left: LEMMA linear_transform?(L) IFF
FORALL (u,v: Vector): FORALL (a: real): L(a*u + v) = a*L(u) + L(v)
linear_transform_alt_right: LEMMA linear_transform?(L) IFF
FORALL (u,v: Vector): FORALL (a: real): L(u+a*v) = L(u) + a*L(v)
% Other Theorems
linear_transform_perp_unique: LEMMA u /= zero AND v /= zero AND
linear_transform?(L) AND
linear_transform?(J) AND
orthogonal?(u,v) AND
L(u) = J(u) AND
L(v) = J(v)
IMPLIES
L = J
% Auto rewrites for linear transformations Vect2 -> Vect2
AUTO_REWRITE+ linear_transform_zero % L(zero) = zero
% LINEAR FUNCTIONALS
linear_functional?(F): bool =
FORALL (u,v: Vector): FORALL (a,b: real): F(a*u+b*v) = a*F(u) + b*F(v)
% Basic Properties
linear_functional_zero: LEMMA
linear_functional?(F) IMPLIES F(zero) = 0
linear_functional_scal: LEMMA
linear_functional?(F) IMPLIES
FORALL (u: Vector, a: real): F(a*u) = a*F(u)
linear_functional_add: LEMMA
linear_functional?(F) IMPLIES
FORALL (u,v: Vector): F(u+v) = F(u) + F(v)
linear_functional_sub: LEMMA
linear_functional?(F) IMPLIES
FORALL (u,v: Vector): F(u-v) = F(u) - F(v)
kernel_functional_nonempty: LEMMA
linear_functional?(F) IMPLIES
EXISTS (v: Vector): v /= zero AND F(v) = 0
linear_functional_is_dot: LEMMA
linear_functional?(F) IMPLIES
EXISTS (w: Vector): F = (LAMBDA (v: Vector): w*v)
% Equivalent Characterizations
linear_functional_rew: LEMMA linear_functional?(F) IFF
(FORALL (u,v: Vector): F(u+v) = F(u) + F(v)) AND
(FORALL (u: Vector, a: real): F(a*u) = a*F(u))
linear_functional_alt_left: LEMMA linear_functional?(F) IFF
FORALL (u,v: Vector): FORALL (a: real): F(a*u + v) = a*F(u) + F(v)
linear_functional_alt_right: LEMMA linear_functional?(F) IFF
FORALL (u,v: Vector): FORALL (a: real): F(u+a*v) = F(u) + a*F(v)
% Other Theorems
linear_functional_perp_unique: LEMMA u /= zero AND v /= zero AND
linear_functional?(F) AND
linear_functional?(G) AND
orthogonal?(u,v) AND
F(u) = G(u) AND
F(v) = G(v)
IMPLIES
F = G
linear_functional_is_perp_dot: LEMMA
linear_functional?(F) AND
u/=zero AND
F(u) = 0
IMPLIES
(EXISTS (rzk: real): F = (LAMBDA (v: Vector): rzk*det(v,u)))
linear_functional_perp_signs_unique: LEMMA v /= zero AND
linear_functional?(F) AND
linear_functional?(G) AND
F(u)*G(u) > 0 AND
F(v) = 0 AND
G(v) = 0
IMPLIES
FORALL (w: Vector): F(w)*G(w) >= 0
% Auto rewrites for linear functionalations Vect2 -> Vect2
AUTO_REWRITE+ linear_functional_zero % F(zero) = zero
END linear_transformations_2D
¤ Dauer der Verarbeitung: 0.4 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
