Radial homotopy from polygon to unit circle

Constructs the radial homotopy polygonToCircleRadial that deforms fdPolygon onto the unit circle around an interior point p, and proves all 8 conditions of PiecewiseCurvesHomotopicAvoiding.

• polygonToCircleRadial — radial interpolation H(t,s) = p + ((1-s)‖z-p‖+s)(z-p)/‖z-p‖
• fdPolygonRadialCircle — the endpoint curve at s=1 (on unit circle around p)
• fdPolygon_piecewise_homotopic_to_radialCircle — combined 8-condition proof
• winding_fdPolygon_eq_radialCircle — winding numbers are equal

noncomputable def RectHomotopyProof.polygonToCircleRadial (p : ℂ) : ℝ × ℝ → ℂ

Radial homotopy from polygon to unit circle around p. H(t, s) = p + ((1-s)·‖z-p‖ + s) · (z-p)/‖z-p‖

Equations

• RectHomotopyProof.polygonToCircleRadial p (t, s) = p + ((1 - s) * ‖RectHomotopyProof.fdPolygon t - p‖ + s) • ((RectHomotopyProof.fdPolygon t - p) / ↑‖RectHomotopyProof.fdPolygon t - p‖)

theorem RectHomotopyProof.polygonToCircleRadial_avoids (p : ℂ) (hp_norm : ‖p‖ > 1) (hp_re : |p.re| < 1 / 2) (hp_im : p.im < HHeight) (t : ℝ) (ht : t ∈ Set.Icc 0 5) (s : ℝ) (hs : s ∈ Set.Icc 0 1) : polygonToCircleRadial p (t, s) ≠ p

The radial homotopy avoids p when z ≠ p.

noncomputable def RectHomotopyProof.fdPolygonRadialCircle (p : ℂ) : ℝ → ℂ

The radial circle around p: normalized projection of fdPolygon onto unit circle around p. This is polygonToCircleRadial at s=1.

Equations

• RectHomotopyProof.fdPolygonRadialCircle p t = RectHomotopyProof.polygonToCircleRadial p (t, 1)

theorem RectHomotopyProof.fdPolygonRadialCircle_dist (p : ℂ) (hp_norm : ‖p‖ > 1) (hp_re : |p.re| < 1 / 2) (hp_im : p.im < HHeight) (t : ℝ) (ht : t ∈ Set.Icc 0 5) : ‖fdPolygonRadialCircle p t - p‖ = 1

fdPolygonRadialCircle is on the unit circle around p.

theorem RectHomotopyProof.fdPolygonRadialCircle_avoids (p : ℂ) (hp_norm : ‖p‖ > 1) (hp_re : |p.re| < 1 / 2) (hp_im : p.im < HHeight) (t : ℝ) (ht : t ∈ Set.Icc 0 5) : fdPolygonRadialCircle p t ≠ p

fdPolygonRadialCircle avoids p.

theorem RectHomotopyProof.fdPolygon_ne_p_everywhere (p : ℂ) (hp_norm : ‖p‖ > 1) (hp_re : |p.re| < 1 / 2) (hp_im : p.im < HHeight) (t : ℝ) : fdPolygon t ≠ p

fdPolygon t ≠ p for all t ∈ ℝ under interior hypotheses.

theorem RectHomotopyProof.polygonToCircleRadial_continuous (p : ℂ) (hp_norm : ‖p‖ > 1) (hp_re : |p.re| < 1 / 2) (hp_im : p.im < HHeight) : Continuous (polygonToCircleRadial p)

Radial homotopy is continuous.

theorem RectHomotopyProof.polygonToCircleRadial_at_s_zero (p : ℂ) (hp_norm : ‖p‖ > 1) (hp_re : |p.re| < 1 / 2) (hp_im : p.im < HHeight) (t : ℝ) (ht : t ∈ Set.Icc 0 5) : polygonToCircleRadial p (t, 0) = fdPolygon t

At s=0, radial homotopy equals fdPolygon.

theorem RectHomotopyProof.polygonToCircleRadial_at_s_one (p : ℂ) (t : ℝ) : polygonToCircleRadial p (t, 1) = fdPolygonRadialCircle p t

At s=1, radial homotopy equals fdPolygonRadialCircle.

theorem RectHomotopyProof.polygonToCircleRadial_closed (p : ℂ) (_hp_norm : ‖p‖ > 1) (_hp_re : |p.re| < 1 / 2) (_hp_im : p.im < HHeight) (s : ℝ) (_hs : s ∈ Set.Icc 0 1) : polygonToCircleRadial p (0, s) = polygonToCircleRadial p (5, s)

Radial homotopy is closed at each stage.

theorem RectHomotopyProof.polygonToCircleRadial_differentiable_off_partition (p : ℂ) (hp_norm : ‖p‖ > 1) (hp_re : |p.re| < 1 / 2) (hp_im : p.im < HHeight) (t : ℝ) (ht : t ∈ Set.Ioo 0 5) (ht_not_P : t ∉ {1, 2, 3, 4}) (s : ℝ) (_hs : s ∈ Set.Icc 0 1) : DifferentiableAt ℝ (fun (t' : ℝ) => polygonToCircleRadial p (t', s)) t

Radial homotopy is differentiable in t away from partition points.

theorem RectHomotopyProof.polygonToCircleRadial_deriv_cont_on_piece (p : ℂ) (hp_norm : ‖p‖ > 1) (hp_re : |p.re| < 1 / 2) (hp_im : p.im < HHeight) (p₁ p₂ : ℝ) (_hp₁p₂ : p₁ < p₂) (hpiece : ∀ t ∈ Set.Ioo p₁ p₂, t ∉ {1, 2, 3, 4}) (h_sub : Set.Ioo p₁ p₂ ⊆ Set.Ioo 0 5) : ContinuousOn (fun (q : ℝ × ℝ) => deriv (fun (t' : ℝ) => polygonToCircleRadial p (t', q.2)) q.1) (Set.Ioo p₁ p₂ ×ˢ Set.Icc 0 1)

t-derivative is continuous on each piece.

theorem RectHomotopyProof.norm_normalize_sub_le {w₁ w₂ : ℂ} {δ : ℝ} (hδ : 0 < δ) (hw₁ : δ ≤ ‖w₁‖) (hw₂ : δ ≤ ‖w₂‖) : ‖w₁ / ↑‖w₁‖ - w₂ / ↑‖w₂‖‖ ≤ 2 * ‖w₁ - w₂‖ / δ

Normalization is Lipschitz: ‖w₁/‖w₁‖ - w₂/‖w₂‖‖ ≤ 2·‖w₁ - w₂‖/δ when ‖w₁‖ ≥ δ and ‖w₂‖ ≥ δ.

noncomputable def RectHomotopyProof.fdPolygonRightDeriv (x : ℝ) : ℂ

Right derivative of fdPolygon at each point. At partition points {1,2,3,4}, uses the NEXT segment's derivative.

Equations

• One or more equations did not get rendered due to their size.

theorem RectHomotopyProof.fdPolygon_right_deriv_norm_le (x : ℝ) : ‖fdPolygonRightDeriv x‖ ≤ 3

The right derivative of fdPolygon has norm ≤ 3 everywhere.

theorem RectHomotopyProof.fdPolygon_hasDerivWithinAt_Ici (x : ℝ) : HasDerivWithinAt fdPolygon (fdPolygonRightDeriv x) (Set.Ici x) x

fdPolygon has a right derivative at every point.

theorem RectHomotopyProof.fdPolygon_norm_sub_le (a b : ℝ) : ‖fdPolygon b - fdPolygon a‖ ≤ 3 * |b - a|

fdPolygon is Lipschitz with constant 3.

theorem RectHomotopyProof.polygonToCircleRadial_deriv_bounded (p : ℂ) (hp_norm : ‖p‖ > 1) (hp_re : |p.re| < 1 / 2) (hp_im : p.im < HHeight) : ∃ (M : ℝ), ∀ t ∈ Set.Icc 0 5, ∀ s ∈ Set.Icc 0 1, ‖deriv (fun (t' : ℝ) => polygonToCircleRadial p (t', s)) t‖ ≤ M

t-derivative is bounded.

theorem RectHomotopyProof.fdPolygon_piecewise_homotopic_to_radialCircle (p : ℂ) (hp_norm : ‖p‖ > 1) (hp_re : |p.re| < 1 / 2) (hp_im : p.im < HHeight) : PiecewiseCurvesHomotopicAvoiding fdPolygon (fdPolygonRadialCircle p) 0 5 p {1, 2, 3, 4}

Radial homotopy satisfies PiecewiseCurvesHomotopicAvoiding.

theorem RectHomotopyProof.winding_fdPolygon_eq_radialCircle (p : ℂ) (hp_norm : ‖p‖ > 1) (hp_re : |p.re| < 1 / 2) (hp_im : p.im < HHeight) : generalizedWindingNumber' fdPolygon 0 5 p = generalizedWindingNumber' (fdPolygonRadialCircle p) 0 5 p

winding(fdPolygon) = winding(fdPolygonRadialCircle).