Tangent forcing: flatness bounds the deviation against the tangent

Contour.FlatOfOrder γ t₀ n bounds the perpendicular deviation of the curve against some non-zero one-sided witness directions. This file shows the witnesses are forced onto the actual one-sided tangents: if γ has one-sided derivative L ≠ 0 and is flat of order n ≥ 1, the flatness direction is a real multiple of L, so the deviation bound transfers to L itself — the exact hypothesis the higher-order antiderivative asymptotics (Contour.antiderivative_diff_at_tangent_target_tendsto_zero_right / _left) consume.

Main results

• Contour.FlatOfOrder.tangentDeviation_isLittleO_right — from flatness of order n ≥ 1 and a right derivative L ≠ 0, the deviation against L is o(‖γ t - γ t₀‖ ^ n) from the right.
• Contour.FlatOfOrder.tangentDeviation_isLittleO_left — the left counterpart.

Provenance

New to the raw-curve development: the AINTLIB LeanModularForms flatness structure (IsFlatOfOrder) is indexed by the tangent, so no forcing step was needed there; the roadmap's Contour.FlatOfOrder quantifies its witness directions existentially, and this file supplies the bridge. The forcing argument is the standard one: the curve leaves t₀ tangent to L, so a line it hugs to first order can only be ℝ • L. See N. Hungerbühler, M. Wasem, Non-integer valued winding numbers and a generalized Residue Theorem, arXiv:1808.00997, §3.

theorem TauCeti.Contour.FlatOfOrder.tangentDeviation_isLittleO_right {γ : ℝ → ℂ} {t₀ : ℝ} {L : ℂ} {n : ℕ} (hflat : FlatOfOrder γ t₀ n) (hn : 1 ≤ n) (hL : L ≠ 0) (h_deriv : HasDerivWithinAt γ L (Set.Ioi t₀) t₀) : (fun (t : ℝ) => ‖tangentDeviation (γ t - γ t₀) L‖) =o[nhdsWithin t₀ (Set.Ioi t₀)] fun (t : ℝ) => ‖γ t - γ t₀‖ ^ n

Flatness bounds the deviation against the right tangent: from FlatOfOrder γ t₀ n (n ≥ 1) and a right derivative L ≠ 0, the perpendicular deviation against L itself is o(‖γ t - γ t₀‖ ^ n) from the right — the hypothesis the higher-order antiderivative asymptotics consume.

theorem TauCeti.Contour.FlatOfOrder.tangentDeviation_isLittleO_left {γ : ℝ → ℂ} {t₀ : ℝ} {L : ℂ} {n : ℕ} (hflat : FlatOfOrder γ t₀ n) (hn : 1 ≤ n) (hL : L ≠ 0) (h_deriv : HasDerivWithinAt γ L (Set.Iio t₀) t₀) : (fun (t : ℝ) => ‖tangentDeviation (γ t - γ t₀) L‖) =o[nhdsWithin t₀ (Set.Iio t₀)] fun (t : ℝ) => ‖γ t - γ t₀‖ ^ n

Flatness bounds the deviation against the left tangent: the counterpart of FlatOfOrder.tangentDeviation_isLittleO_right from the left.