| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/vectors/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 4 kB |
|
SSL linear_transformations_2D.pvs
Interaktion und |
|||||||||
|
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 ¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.14Angebot Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können ¤*Eine klare Vorstellung vom Zielzustand |
|
2026-03-28