Exit times of a curve from small balls around a crossed point #
For a curve γ : ℝ → E with γ t₀ = s, the first exit time at radius ε on the right is
the first parameter t ≥ t₀ in a window [t₀, t₀ + δ] with ‖γ t - s‖ = ε; symmetrically on
the left. This file constructs the exit times as sInf/sSup of the closed set of
outside-the-ball times and establishes the API the principal-value excision consumes: the exit
time lies in the window, sits at exact distance ε (for small ε), tends to t₀ one-sidedly
as ε → 0⁺, and eventually has exact radius — the t_eps hypotheses of
Contour.antiderivative_diff_across_crossing_tendsto_zero.
Main definitions #
Contour.firstExitTimeRight γ t₀ δ s ε—sInf {t ∈ [t₀, t₀+δ] | ε ≤ ‖γ t - s‖}.Contour.firstExitTimeLeft γ t₀ δ s ε—sSup {t ∈ [t₀-δ, t₀] | ε ≤ ‖γ t - s‖}(the latest outside-the-ball time beforet₀, i.e. the first exit when moving left fromt₀).
Main results #
Contour.firstExitTimeRight_mem_Icc/Left— the exit time lies in the window.Contour.norm_at_firstExitTimeRight_eq/Left— the exit time is at exact distanceε.Contour.firstExitTimeRight_tendsto/Left— the exit time tends tot₀one-sidedly asε → 0⁺, providedγleavesson the window.Contour.eventually_norm_at_firstExitTimeRight_eq/Left— eventual exact radius along𝓝[>] 0.
The exit times and their properties at a fixed radius hold for a curve into any seminormed group.
The results as ε → 0⁺ are stated in a normed group: their hypothesis that γ leaves s must
give a positive distance from s, which a seminorm does not guarantee.
Provenance #
Migrated from firstExitTimeRight/firstExitTimeLeft and their API in ExitTime.lean of the
AINTLIB LeanModularForms development, restated for a curve into a seminormed group. See
N. Hungerbühler, M. Wasem, Non-integer valued winding numbers and a generalized Residue
Theorem, arXiv:1808.00997, §3.
First exit time at radius ε (right side): the sInf of the times
t ∈ [t₀, t₀ + δ] with ε ≤ ‖γ t - s‖; the junk value is sInf ∅ when the curve never
reaches distance ε in the window.
Equations
Instances For
Radius lower bound at the right exit time: the sInf of the closed set of
outside-the-ball times is itself outside the open ball.
The right exit time is strictly after the crossing when γ t₀ = s and 0 < ε.
Exact radius at the right exit time: for 0 < ε ≤ ‖γ (t₀ + δ) - s‖, the curve is at
distance exactly ε at firstExitTimeRight γ t₀ δ s ε.
First exit time at radius ε (left side): the sSup of the times t ∈ [t₀ - δ, t₀]
with ε ≤ ‖γ t - s‖ — the latest outside-the-ball time before t₀, which is the first exit
when moving left from t₀.
Equations
Instances For
Radius lower bound at the left exit time: the sSup of the closed set of
outside-the-ball times is itself outside the open ball.
The left exit time is strictly before the crossing: the counterpart of
lt_firstExitTimeRight.
Exact radius at the left exit time: the counterpart of
norm_at_firstExitTimeRight_eq.
Upper bound through any witness (right): the right exit time is at most any window
time already at distance ≥ ε.
Lower bound through any witness (left): the left exit time is at least any window
time already at distance ≥ ε.
The right exit time tends to t₀ from above as ε → 0⁺, provided γ leaves s on
(t₀, t₀ + δ].
The left exit time tends to t₀ from below as ε → 0⁺: the counterpart of
firstExitTimeRight_tendsto.
Eventual exact radius (right): for all sufficiently small ε > 0, the right exit time
is at distance exactly ε, provided the window endpoint differs from s. This is the
radius hypothesis of
Contour.antiderivative_diff_across_crossing_tendsto_zero.
Eventual exact radius (left): the counterpart of
eventually_norm_at_firstExitTimeRight_eq, assuming only that the left endpoint
differs from s.