|
omega_2D[D:posreal,B:nnreal,T: {AB: posreal|AB>B}] : THEORY
BEGIN
IMPORTING cd2d[D,B,T],
horizontal_criteria[D],
vect_analysis@vect2_Heine,
analysis@metric_space_real_fun[[real,Vect2],d],
analysis@ms_composition_cont[[real,Vect2],d,Vect2,dist,real,real_dist],
analysis@continuity_of_max_min[[real,Vect2],d],
analysis@convex_function_props
s,v,w : VAR Vect2
t,tlh,t1,t2 : VAR Lookahead
ttt,tw,tx,ty : VAR real
dir,eps : VAR Sign
M : VAR real
sz,vz : VAR real
% 1 Distance Functions
% 1.B Horizontal Distance
% 1.B.2 Continuity
horiz_dist_cont_scaf: LEMMA continuous?(horiz_dist_scaf(s),fullset[[Lookahead,Vect2]])
conflict_2D_on_open_interval: LEMMA conflict_2D?(s,v) IFF
EXISTS (topen: Lookahead): B<topen AND topen <T AND sqv(s+topen*v)<sq(D)
% 1.B.4 Trajectory Information
circle_hit: LEMMA horiz_dist_scaf(s)(t,v) < M IMPLIES
EXISTS (epsilon: posreal): FORALL (t1: Lookahead): abs(t1 - t) < epsilon
IMPLIES horiz_dist_scaf(s)(t1,v) < M
% 1.C Cylindrical Distance
% 1.C.1 Definitions
% 1.C.2 Continuity/Boundedness of omega/omega_2D
horiz_dist_scaf_bounded_below : LEMMA
bounded_below?(LAMBDA(t: Lookahead):horiz_dist_scaf(s)(t,v))
omega_2D(s)(v) : real =
inf(LAMBDA(t: Lookahead):horiz_dist_scaf(s)(t,v))
tau_2D_nonempty : LEMMA
nonempty?({t: Lookahead | horiz_dist_scaf(s)(t,v) = omega_2D(s)(v)})
% 1.C.4 tau_2D Definitions and Basic Properties
tau_2D(s,v) : Lookahead =
choose({t: Lookahead | horiz_dist_scaf(s)(t,v) = omega_2D(s)(v)})
tau_2D_def: LEMMA horiz_dist_scaf(s)(tau_2D(s,v),v) = omega_2D(s)(v)
omega_2D_min_rew: LEMMA omega_2D(s)(v) = min({r: real | EXISTS (t: Lookahead):horiz_dist_scaf(s)(t,v) = r})
tau_2D_min : LEMMA
horiz_dist_scaf(s)(tau_2D(s,v),v) <= horiz_dist_scaf(s)(t,v)
omega_2D_continuous: LEMMA continuous?(omega_2D(s))
tau_2D_unique: LEMMA
v /= zero AND
horiz_dist_scaf(s)(tau_2D(s,v),v) = horiz_dist_scaf(s)(t,v)
IMPLIES tau_2D(s,v) = t
tau_2D_connected: LEMMA horiz_dist_scaf(s)(tau_2D(s,v),v) = 0
AND horiz_dist_scaf(s)(t,v) = 0
IMPLIES
(FORALL (ttt: real): 0<=ttt AND ttt<= 1 IMPLIES
horiz_dist_scaf(s)(ttt*tau_2D(s,v) + (1-ttt)*t,v)=0)
tau_2D_v2: LEMMA v/= zero IMPLIES tau_2D(s,v) = tau_v2(s,v)
omega_2D_horizontal_omega: LEMMA v/= zero IMPLIES omega_2D(s)(v) = horizontal_omega(s,v) - sq(D)
% 1.C.5 Conflicts
omega_2D_conflict : LEMMA
omega_2D(s)(v) < 0 IFF conflict_2D?(s,v)
% 2 Critical Points
% 2.A Case Subdivision
omega_2D_eq_0 : LEMMA
omega_2D(s)(v) = 0 IFF
on_D?(s+tau_2D(s,v)*v)
parts_of_v_nonzero_2D: LEMMA omega_2D(s)(v) = 0 AND NOT horiz_dist_scaf(s)(0,v)=0
IMPLIES
v /= zero
% 2.C Open Tape Solutions
% 2.C.2 Line Solutions or 2-D Circle Solutions
% tape hit solution
lower_circle_hit_solution: LEMMA omega_2D(s)(v) = 0 AND
on_D?(s+B*v) IMPLIES
circle_solution_2D?(s,v,B,Exit)
circle_hit_solution: LEMMA NOT v = zero AND
omega_2D(s)(v) = 0 AND
sqv(s+B*v) /= sq(D)
IMPLIES
horizontal_sep?(s) AND line_solution?(s,v) OR circle_solution_2D?(s,v,T,Entry)
% 2.C.4 |s`z|<H and v`z = 0: 2-D circle solutions
% 2.D Open Disc Solutions
% 2.D.4 omega_2D(s)(v) = 0 and v = 0 implies s is inside circle
% no_horiz_speed_closed_circle
no_horiz_speed_on_D: LEMMA omega_2D(s)(v) = 0 AND v = zero
IMPLIES sqv(s) = sq(D)
% 2.E Corner Solutions
% 2.E.1 Delta >= 0
omega_2D_Delta: LEMMA omega_2D(s)(v) <= 0
IMPLIES Delta(s,v) >= 0
% 2.E.2 Relationship Between Theta_D(Entry) and Theta_D(Exit)
Theta_Ds_equal_line_sol_2D: LEMMA omega_2D(s)(v) = 0
AND strict_horizontal_sep?(s)
AND Theta_D(s,v,Entry) = Theta_D(s,v,Exit)
IMPLIES
line_solution?(s,v)
% 2 The Final Theorem For omega_2D
% 2.B The Critical Points of omega_2D
critical_points_2D : THEOREM
omega_2D(s)(v) = 0 IMPLIES horizontal_sep?(s) AND line_solution?(s,v) OR
circle_solution_2D?(s,v,T,Entry) OR
circle_solution_2D?(s,v,B,Exit)
END omega_2D
¤ Dauer der Verarbeitung: 0.16 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.
|
