Derivative norm bounds for the homotopy segments

Proves that the derivative norm of each segment of fdBoundaryToPolygonHomotopy is bounded by 5.

theorem RectHomotopyProof.norm_deriv_H_seg2_le (t s : ℝ) (hs : s ∈ Set.Icc 0 1) : ‖deriv (fun (t' : ℝ) => have arc_point := Complex.exp ((↑Real.pi / 3 + (↑t' - 1) * (↑Real.pi / 2 - ↑Real.pi / 3)) * Complex.I); have chord_point := chordSegment rho' iPoint (t' - 1); (1 - s) • arc_point + s • chord_point) t‖ ≤ 5

Norm bound for segment 2 derivative.

theorem RectHomotopyProof.norm_deriv_H_seg3_le (t s : ℝ) (hs : s ∈ Set.Icc 0 1) : ‖deriv (fun (t' : ℝ) => have arc_point := Complex.exp ((↑Real.pi / 2 + (↑t' - 2) * (2 * ↑Real.pi / 3 - ↑Real.pi / 2)) * Complex.I); have chord_point := chordSegment iPoint rho (t' - 2); (1 - s) • arc_point + s • chord_point) t‖ ≤ 5

Norm bound for segment 3 derivative.

theorem RectHomotopyProof.fdBoundaryToPolygonHomotopy_seg2_deriv_bound (t : ℝ) (_ht : t ∈ Set.Ioo 1 2) (s : ℝ) (hs : s ∈ Set.Icc 0 1) : ‖deriv (fun (t' : ℝ) => have arc_point := Complex.exp ((↑Real.pi / 3 + (↑t' - 1) * (↑Real.pi / 2 - ↑Real.pi / 3)) * Complex.I); have chord_point := chordSegment rho' iPoint (t' - 1); (1 - s) • arc_point + s • chord_point) t‖ ≤ 5

Segment 2 derivative bound for t in (1,2).

theorem RectHomotopyProof.fdBoundaryToPolygonHomotopy_seg3_deriv_bound (t : ℝ) (_ht : t ∈ Set.Ioo 2 3) (s : ℝ) (hs : s ∈ Set.Icc 0 1) : ‖deriv (fun (t' : ℝ) => have arc_point := Complex.exp ((↑Real.pi / 2 + (↑t' - 2) * (2 * ↑Real.pi / 3 - ↑Real.pi / 2)) * Complex.I); have chord_point := chordSegment iPoint rho (t' - 2); (1 - s) • arc_point + s • chord_point) t‖ ≤ 5

Segment 3 derivative bound for t in (2,3).

theorem RectHomotopyProof.norm_deriv_H_seg1_le (t _s : ℝ) : ‖deriv (fun (t' : ℝ) => 1 / 2 + (↑HHeight - ↑t' * (↑HHeight - ↑√3 / 2)) * Complex.I) t‖ ≤ 5

Segment 1 derivative bound.

theorem RectHomotopyProof.norm_deriv_H_seg4_le (t _s : ℝ) : ‖deriv (fun (t' : ℝ) => -1 / 2 + (↑√3 / 2 + (↑t' - 3) * (↑HHeight - ↑√3 / 2)) * Complex.I) t‖ ≤ 5

Segment 4 derivative bound.

theorem RectHomotopyProof.norm_deriv_H_seg5_le (t _s : ℝ) : ‖deriv (fun (t' : ℝ) => ↑t' - 9 / 2 + ↑HHeight * Complex.I) t‖ ≤ 5

Segment 5 derivative bound.