| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/Cobol/Test-Suite/SQL M/ Datei vom 4.1.2008 mit Größe 3 kB |
|
Quellcode-Bibliothek vertical_dist_convexity.pvs Sprache: PVS |
|||||||||
|
vertical_dist_convexity[H:posreal] : THEORY
BEGIN IMPORTING analysis@convex_function_props, vectors@vectors_3D s,v,w : VAR Vect3 ttt,tw,tx,ty : VAR real % 1.A Vertical Distance % 1.A.1 Definitions % Vertical Distance vert_dist_scaf(s)(t: real,v): real = abs(s`z+t*v`z)-H % The Squared Version... vert_dist_sq_scaf(s)(t: real, v): real = sq(s`z + t*v`z) - sq(H) % 1.A.2 Convexity vert_dist_convex_scaf: LEMMA convex?((LAMBDA (ttt): vert_dist_scaf(s)(ttt,v))) vert_dist_strictly_convex_scaf: LEMMA v`z /= 0 IMPLIES strictly_convex?((LAMBDA (ttt): v % 1.A.4 Relationship to Squared Version vert_dist_scaf_quad_eq_0: LEMMA vert_dist_scaf(s)(ttt,v) = 0 IFF sq(s`z + ttt*v`z) = sq(H) vert_dist_scaf_quad_ge_0: LEMMA vert_dist_scaf(s)(ttt,v) >= 0 IFF sq(s`z + ttt*v`z) >= sq(H) vert_dist_scaf_quad_gt_0: LEMMA vert_dist_scaf(s)(ttt,v) > 0 IFF sq(s`z + ttt*v`z) > sq(H) vert_dist_scaf_quad_le_0: LEMMA vert_dist_scaf(s)(ttt,v) <= 0 IFF sq(s`z + ttt*v`z) <= sq(H) vert_dist_scaf_quad_lt_0: LEMMA vert_dist_scaf(s)(ttt,v) < 0 IFF sq(s`z + ttt*v`z) < sq(H) END vertical_dist_convexity ¤ 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.0.12Bemerkung: (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28