Chord-to-tangent bounds in the plane

The elementary plane geometry behind the Hungerbühler–Wasem connecting-arc analysis: decompose a vector w ∈ ℂ into its projection on a direction L and the orthogonal remainder, and bound the chord from w to the "natural" tangent target (‖w‖/‖L‖) • L — the point of the ray ℝ₊ • L at the same distance — by the orthogonal deviation:

‖w - (‖w‖/‖L‖) • L‖ ≤ ‖tangentDeviation w L‖ + ‖tangentDeviation w L‖² / ‖w‖.

For a curve flat of order n at an on-cycle singularity the deviation is o(‖w‖ⁿ) (Contour.FlatOfOrder), so the chord to the tangent target is too — the radius-based bound the sector analysis of the generalized residue theorem consumes.

Main definitions

• Contour.tangentDeviation w L — the component of w perpendicular to the real line ℝ • L (the remainder after subtracting the private projection on L). Its norm is the distance from w to the line, the quantity Contour.FlatOfOrder bounds (norm_tangentDeviation).

This is a scalar formula on ℂ, deliberately not routed through Mathlib's submodule-valued orthogonalProjection: the contour development needs only the one-line projection onto a known direction, not the inner-product-space machinery.

Main results

• Contour.norm_tangentDeviation — ‖tangentDeviation w L‖ = |(w * conj L).im| / ‖L‖, the bridge to the inline form used by Contour.FlatOfOrder.
• Contour.tangentDeviation_self, Contour.tangentDeviation_real_smul_self — points of the line ℝ • L have zero deviation.
• Contour.norm_tangentDeviation_le_norm_sub_smul — the deviation norm is at most the distance to any point r • L of the line, generalising Contour.norm_tangentDeviation_le.
• Contour.norm_chord_to_tangent_target_le — the chord-to-tangent-target bound (the Pythagoras decomposition and square-root estimates behind it are private implementation steps).

Provenance

Migrated from FlatChordBound.lean (with the orthogonalProjectionComplex and tangentDeviation definitions of FlatnessConditions.lean) of the AINTLIB LeanModularForms development. See N. Hungerbühler, M. Wasem, Non-integer valued winding numbers and a generalized Residue Theorem, arXiv:1808.00997, §3.

noncomputable def TauCeti.Contour.tangentDeviation (w L : ℂ) : ℂ

Orthogonal deviation of w from the direction L: the remainder w - orthogonalProjectionComplex w L, the component of w perpendicular to the line ℝ • L.

Equations

• TauCeti.Contour.tangentDeviation w L = w - TauCeti.Contour.orthogonalProjectionComplex✝ w L

@[simp]

theorem TauCeti.Contour.tangentDeviation_add (a b L : ℂ) : tangentDeviation (a + b) L = tangentDeviation a L + tangentDeviation b L

tangentDeviation is additive in its vector argument.

@[simp]

theorem TauCeti.Contour.tangentDeviation_zero (L : ℂ) : tangentDeviation 0 L = 0

tangentDeviation sends the zero vector to 0.

@[simp]

theorem TauCeti.Contour.tangentDeviation_sub (a b L : ℂ) : tangentDeviation (a - b) L = tangentDeviation a L - tangentDeviation b L

tangentDeviation respects subtraction in its vector argument.

@[simp]

theorem TauCeti.Contour.tangentDeviation_neg (w L : ℂ) : tangentDeviation (-w) L = -tangentDeviation w L

tangentDeviation negates in its vector argument.

theorem TauCeti.Contour.tangentDeviation_real_smul (c : ℝ) (w L : ℂ) : tangentDeviation (c • w) L = c • tangentDeviation w L

tangentDeviation is homogeneous over real scalars in its vector argument. (Not @[simp]: simp normalizes the real smul c • w to ↑c * w, so this left-hand side never fires.)

@[simp]

theorem TauCeti.Contour.tangentDeviation_ofReal_mul (c : ℝ) (w L : ℂ) : tangentDeviation (↑c * w) L = ↑c * tangentDeviation w L

The simp-normal companion of tangentDeviation_real_smul: simp normalizes the real smul c • w to ↑c * w, so this is the form that fires for simp-driven automation.

theorem TauCeti.Contour.norm_tangentDeviation {L : ℂ} (hL : L ≠ 0) (w : ℂ) : ‖tangentDeviation w L‖ = |(w * (starRingEnd ℂ) L).im| / ‖L‖

The norm of the orthogonal deviation is the distance from w to the line ℝ • L: ‖tangentDeviation w L‖ = |Im(w · conj L)| / ‖L‖ — the quantity Contour.FlatOfOrder bounds.

@[simp]

theorem TauCeti.Contour.tangentDeviation_self (L : ℂ) : tangentDeviation L L = 0

A direction has no deviation from its own line.

theorem TauCeti.Contour.tangentDeviation_real_smul_self (r : ℝ) (L : ℂ) : tangentDeviation (r • L) L = 0

Every real multiple of the direction lies on its line, so has no deviation. Not a simp lemma: simp already reaches it through tangentDeviation_ofReal_mul and tangentDeviation_self.

theorem TauCeti.Contour.norm_tangentDeviation_le (w L : ℂ) : ‖tangentDeviation w L‖ ≤ ‖w‖

The deviation norm is bounded by the vector norm: the perpendicular component is no longer than the vector. At L = 0 the deviation is w itself and the bound is an equality.

theorem TauCeti.Contour.norm_tangentDeviation_le_norm_sub_smul (w L : ℂ) (r : ℝ) : ‖tangentDeviation w L‖ ≤ ‖w - r • L‖

The deviation norm is at most the distance to any point of the line. The perpendicular component of w is bounded by ‖w - r • L‖ for every real r. At L = 0 both sides are ‖w‖, and at r = 0 this is norm_tangentDeviation_le.

theorem TauCeti.Contour.norm_tangentDeviation_neg {L : ℂ} (hL : L ≠ 0) (w : ℂ) : ‖tangentDeviation w (-L)‖ = ‖tangentDeviation w L‖

The deviation norm is direction-line invariant: measuring against -L gives the same distance to the line ℝ • L.

theorem TauCeti.Contour.norm_tangentDeviation_smul_real {c : ℝ} (hc : c ≠ 0) {L : ℂ} (hL : L ≠ 0) (w : ℂ) : ‖tangentDeviation w (c • L)‖ = ‖tangentDeviation w L‖

The deviation norm is invariant under real rescaling of the direction: it measures the distance to the line ℝ • L.

theorem TauCeti.Contour.exists_real_smul_of_im_mul_conj_eq_zero {L v : ℂ} (hv : v ≠ 0) (h : (L * (starRingEnd ℂ) v).im = 0) : ∃ (c : ℝ), L = c • v

A complex number with real pairing against a nonzero direction lies on its real line: Im(L · conj v) = 0 forces L = c • v for a real c.

theorem TauCeti.Contour.norm_chord_to_tangent_target_le {w L : ℂ} (hL : L ≠ 0) (hw : 0 < ‖w‖) (h_pos : 0 ≤ (w * (starRingEnd ℂ) L).re) : ‖w - (‖w‖ / ‖L‖) • L‖ ≤ ‖tangentDeviation w L‖ + ‖tangentDeviation w L‖ ^ 2 / ‖w‖

Chord-to-tangent-target bound. For w in the +L hemisphere with ‖w‖ > 0, the chord from w to the natural tangent target (‖w‖/‖L‖) • L is controlled by the orthogonal deviation: ‖w - (‖w‖/‖L‖) • L‖ ≤ ‖tangentDeviation w L‖ + ‖tangentDeviation w L‖² / ‖w‖.