Outgoing segments and small intersections of equal planar rays

These elementary geometric lemmas relate actual polygonal segments to their outgoing germs. Equal nonzero arguments yield common points at arbitrarily small positive segment parameters; no disk or isotopy provider is assumed.

Main results

• Cslib.Polygonal.exists_small_smul_eq_of_arg_eq: equal rays meet at small positive parameters.
• Cslib.Polygonal.Route.eval_near_end: actual interpolation along an outgoing germ.
• Cslib.Polygonal.Route.position_near_end_mem: these parameters are inside the whole route.

theorem Cslib.Polygonal.exists_small_smul_eq_of_arg_eq {u v : ℂ} (hu : u ≠ 0) (hv : v ≠ 0) (harg : u.arg = v.arg) {δ : ℝ} (hδ : 0 < δ) : ∃ s ∈ Set.Ioo 0 δ, ∃ t ∈ Set.Ioo 0 δ, s • u = t • v

Two nonzero complex vectors with the same argument have equal positive scalar multiples with both scalars smaller than any prescribed positive bound.

def Cslib.Polygonal.Route.endSegment (p : Route) (b : Bool) : Fin p.segments

First segment at the first end; last segment at the last end.

def Cslib.Polygonal.Route.endTime (b : Bool) (t : ℝ) : ℝ

Local outgoing time converted to the orientation of a listed segment.

theorem Cslib.Polygonal.Route.endTime_mem (b : Bool) {t : ℝ} (ht : t ∈ Set.Icc 0 1) : endTime b t ∈ Set.Icc 0 1

Conversion to listed-segment time preserves the unit parameter interval.

theorem Cslib.Polygonal.Route.eval_near_end (p : Route) (b : Bool) (t : ℝ) : p.eval (p.endSegment b) (endTime b t) = p.endpoint b + t • p.germ b

The actual segment at outgoing time t is the endpoint plus t times its germ.

theorem Cslib.Polygonal.Route.position_near_end (p : Route) (b : Bool) (t : ℝ) : p.position (p.endSegment b) (endTime b t) = if b = true then ↑p.segments - t else t

The global parameter of a point on an outgoing segment, including the final segment's reversed local orientation.

theorem Cslib.Polygonal.Route.position_near_end_mem (p : Route) (b : Bool) {t : ℝ} (ht : t ∈ Set.Ioo 0 1) : p.position (p.endSegment b) (endTime b t) ∈ Set.Ioo 0 ↑p.segments

A strictly internal outgoing time is strictly internal to the entire chain.

theorem Cslib.Polygonal.Route.not_atEnd_near_end (p : Route) (b c : Bool) {t : ℝ} (ht : t ∈ Set.Ioo 0 1) : ¬p.AtEnd (p.endSegment b) (endTime b t) c

Strictly internal outgoing parameters are neither end of the entire route.